Tactic Cheat Sheet

These notes started as a fork of Bhavik Mehta’s notes. I’ve changed them a bit to better serve as a reference for all the things I’ve seen and confused me.

RW#

The rw or rewrite tactic is a “substitute in” tactic. If h : x = y is a hypothesis then rw [h] changes all of the x’s in the goal to y’s.

rw also works with iff statements: if h : P ↔ Q then rw [h] will replace all the P s in the goal with Q s.

rw [<- h] goes the other way replacing all y’s to x, and all Q’s to P respectively.

The above commands will re-write in the goal, but one can also use the re-write tactic in assumptions or local context.

example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  -- We start with hyp : c = d * a + b
  rw [hyp'] at hyp
  -- will change hyp: c = d*a + a*d
  rw [mul_comm d a] at hyp
  -- will change hyp: c = a*d + a*d 
  rw [← two_mul (a * d)] at hyp
  -- hyp: c = 2*(a*d) 
  rw [← mul_assoc 2 a d] at hyp
  -- hyp: c = (2*a)*d which is the same thing as 2*a*a (left associativity in lean does not show brackets)
  exact hyp

Examples#

Ring#

The ring tactic proves identities in commutative rings such as (x+y)^2=x^2+2*x*y+y^2. It works on concrete rings such as ℝ and abstract rings, and will also prove some results in “semirings” such as ℕ (which isn’t a ring because it doesn’t have additive inverses).

Sometimes you are in a situation where you cannot rw the hypothesis you want to use. For example if the tactic state is

x y : ℝ
h : x ^ 2 = y ^ 2
⊢ x ^ 4 = y ^ 4

then rw h will fail as rw works up to syntactic equality and it cannot see an x^2 in the goal, even though we know from elementary algebra that x^4=(x^2)^2 In this situation we can use ring to prove an intermediate result and then rewrite our way out of trouble. For example this goal can be solved in the following way. It can be solved in a verbose manner as

example (x y : ℝ) (h: x^2 = y^2) : x^4 = y^4 := by {
  have h3: ∀x: ℝ, x ^ 4 = (x ^ 2) ^ 2 := by {
    intro x 
    ring
  }
  rw [h3 x, h3 y]
  rw [h]
}

the have tactic introduces a sub-goal with the same context as the original goal.

or more succintly as

example (x y : ℝ) (h : x ^ 2 = y ^ 2) : x ^ 4 = y ^ 4 := by
  rw [show x ^ 4 = (x ^ 2) ^ 2 by ring] -- prove x^4=(x^2)^2, rewrite with it, forget it
  -- goal now `⊢ (x ^ 2) ^ 2 = y ^ 4`
  rw [h]
  -- goal now `⊢ (y ^ 2) ^ 2 = y ^ 4`
  ring

Here show P by tac is inline term-mode proof syntax — it constructs an anonymous proof of P using tactic tac, right at the point of use. It’s equivalent to: rw [(by ring : x ^ 4 = (x ^ 2) ^ 2)]

ring is a “finishing tactic”; this means that it should only be used to close goals. If ring does not close a goal it will issue a warning that you should use the related tactic ring_nf.

The above case could also be solved using convert to

example (x y : ℝ) (h : x ^ 2 = y ^ 2) : x ^ 4 = y ^ 4 := by
-- i ask for the final goal to be convrted to the following statement
convert_to (x ^ 2) ^ 2 = y ^ 4
-- creates new goal ⊢ x ^ 4 = (x ^ 2) ^ 2 (only then will the convert be possible
· ring -- solves this new goal
-- goal now `⊢ (x ^ 2) ^ 2 = y ^ 4`
rw [h]
-- goal now `⊢ (y ^ 2) ^ 2 = y ^ 4`
ring

Exact#

If we have h: P where P is some proposition type, and h is a term of this type i.e. a proof of this proposition; and the goal is |- P, then exact h will close the goal.

Note that the exact tactic works up to definitional equality. So if h: ¬P and the goal |- P -> False, exact h would still work.

A common mistake amongst beginners is trying exact P to close a goal of type P. The goal is a type, but the exact tactic takes a term of that type, not the type itself. Remember : P is the statement of the problem. To solve the goal you need to supply the proof.

NOTE: I view exact as a very specic example of apply tactic where the goal is exactly matched.

Refine#

The refine tactic is “exact with holes”. You can use an incomplete term containing one or more underscores ?_ and Lean will give you these terms as new goals.

The theorem goal has this shape:

  ∃ (js' : SailJoltState) (v1 v2 : BitVec 64),
    read_rs1 ∧
    read_rs2 ∧
    program_succeeds ∧
    final_sail_state

So

  refine ⟨js', v1, v2, hok1, hok2, h_program_succeeds, ?_⟩

means:

  use js'
  use v1
  use v2
  exact hok1
  exact hok2
  exact h_program_succeeds
  -- now prove the remaining final_sail_state goal

Linarith#

Solves linear equations, and linear inequalities: omega is the tactic to use for integers.

example {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 := by {
  linarith
}

This is quite handy, as without it proving this is kind of annoying. Though I feel like one can make a shorter proof than, I have here.

example {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 := by {
    have h3 : a = 1 + b := sub_eq_iff_eq_add.mp h2
    have h4 : (3 : ℝ) * b = 3 :=
      calc (3 : ℝ) * b = (a + 2 * b) - (a - b) := by ring
                     _ = 4 - 1                  := by rw [h1, h2]
                     _ = 3                      := by ring
    have h5 : b = 1 := by {
      have hne : (3 : ℝ) ≠ 0 := by norm_num
      have h6 : (3 : ℝ) * b = 3 * 1 := by {
        -- the rw is matching the RHS not the LHS!!!!
        rw [ mul_one] -- goal changes from  3 * b = 3 * 1 to 3*b = 3
        exact h4
      }
      exact mul_left_cancel₀ hne h6
    }
    calc a = 1 + b := h3
         _ = 1 + 1 := by rw [h5]
         _ = 2     := by ring
  }

Apply#

Apply does two very specific things – Assume you have h: P-> Q, and you say apply h, then we will match Q against the goal, if this match succeeds then the new goal becomes P.

It is saying because of h it now suffices to prove the simpler thing, as proving it will imply the harder thing Q.

NOTE: apply h will NOT work unless the goal (or sub-goal) is Q.

If apply is ONLY for when we have the implies operation, then why does the following work?

example (X Y : Type) (φ ψ : X → Y) (h : ∀ a, φ a = ψ a) (x : X) :
   φ x = ψ x := by
apply h

The answer is we still have h: P -> Q.

In Lean, when we have something like (h : ∀ a, φ a = ψ a), it is definitionally equal to

h : (a : X) → (φ a = ψ a).

So under the hood we still have an if-then condition. So apply h matches the goal, the new goal becomes showing a: X

Example : Backwards Reasoning#

See a real life example of Chapter 2.2 of Mathematics In Lean Book. We have a theorem that says if (a, b: R) and (a + b)=0 – this is my P in above notation, then Q: a = -b holds true.

-- Given theorem 
-- theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b 

theorem neg_neg (a : R) : - -a = a := by{
  symm  -- makes goal  a = - -a
  have h1 : a + -a = 0 := by rw [ add_comm, neg_add_cancel] 
  -- a will play the role of a, -a will be b so i'll get a = - -a
  apply eq_neg_of_add_eq_zero
  -- backward reasoning, if h1: P -> Q then apply/exact h1 will try to match Q 
  -- which we have a = -b, in the form of a = - -a
  -- Then the goal becomes proving  h: a + -a = 0
  rw [h1] -- exact h1 also works 
}

When apply is used with at, it uses forward reasoning. For example, h: P -> Q and h2: P, then apply h at h2 will change h2 from P to h2: Q. For this to work h MUST be of the form P->Q and we NEED h2: P

The reasoning is we have a proof that P is true (via h2), then by h we actually get a proof of Q. If the goal is an if and only iff statement, apply will NOT work. First use constructor to split into cases.

Example : Forwards Reasoning#

specialize h arg and apply h at arg are interchangeable for forward reasoning. The difference is which hypothesis gets overwritten:

• specialize hq hp — overwrites hq with the result
• apply hq at hp — overwrites hp with the result

example (p q r : Prop) (hq : p → p → q) (hr : q → r) : p → r := by
  intro hp
  specialize hq hp hp  -- hq : p → p → q  becomes  hq : q
  specialize hr hq     -- hr : q → r      becomes  hr : r
  exact hr

For the simpler case hq : p → q the two tactics are equivalent:

specialize hq hp   -- hq becomes q
apply hq at hp     -- hp becomes q  (same result, different name)

To make my life simple – I will always use apply for backwards reasoning, and specialize for forward.

Other Examples#

To actually use le_trans in a proof you’d write:

variable (h : a ≤ b) (h' : b ≤ c)
-- Imagine this is the goal
|- a <= c 

• exact le_trans h h' – closes the goal directly

• apply le_trans h – leaves ⊢ b ≤ c as a new goal

• apply le_trans – leaves ⊢ a ≤ b and ⊢ b ≤ c as two new goals

These are example of using a theorem directly, and using apply.

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans -- creates two sub goals y ?b ≤ z and a ≤ ?b
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans 
  exact h₀
  apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
  le_trans h₀ h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

example (x : ℝ) : x ≤ x :=
  le_refl x

How to use lemmas when they are complicated.

#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)

This is a relatively complicated application of the apply tactic with lemmas of the form P -> (Q -> R).

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by{ 
 apply lt_of_le_of_lt -- this creates ? < e and a <= ? 
 exact h₀ -- this makes ? = b and the new goal becomes b < e
 apply lt_of_lt_of_le -- this creates ? <= e and b < ?
 exact h₁ -- this makes ? = c and the new goal c <= e as b < c
 apply le_trans -- this makes new goal ? <= e and c <= ?
 exact h₂ -- this makes ? = d; and the new goal is d <= e 
 exact le_of_lt h₃ -- d <= e implies d < e
}

-- alternatlively we can do this
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  linarith

Rfl#

The rfl tactic proves goals of the form ⊢ x = y where x and y are definitionally equal. It also proves goals of the form P ↔ Q if P and Q are definitionally equal.

Sym#

symm flips an equality goal from a = b to b = a (or a hypothesis if you write symm at h).

The Congr + Calc Tactic#

The congr tactic is an attempt to prove LHS = RHS, and if this fails, it changes the goal to a sub-goal of proving the bit that does. The way it works is best illustrated with an example: Say the goal is

⊢ f (g (x + y)) = f (g (y + x))

Writing congr, Lean sees that the LHS and RHS both have f( ) = f( ), so it first reduces the goal to proving g(x+y) = g(y+x). Then it trying to prove equality again, and finds that both sides have g( ) = g( ), so the new goal is x+y = y+x. Then it tries to prove equality again, and sees that if we proved x=y and y=x we would be done. The command congr x applies the tactic x times. So when the goal is

⊢ f (g (x + y)) = f (g (y + x))

1. congr 1: would make the goal g(x+y) = g(y+x)
2. congr 2: would make the goal (x + y) = (y+x)
3. congr 3 or highher would result in two cases x=y and y=x.

example (a b : ℝ) (f g : ℝ → ℝ) : f (g (a + b) ) = f (g (b + a)) := by
  congr 2 -- try increasing it to see the issue.
  ring

The calc tactic allows us to string together many congr and ring tactics. As shown below:

example (a b c d : ℝ) (h : c = b*a - d) (h' : d = a*b) : c = 0 := by
  calc
    c = b*a - d   := by congr
    _ = b*a - a*b := by congr
    _ = 0         := by ring

congr is cleve about using the hypotheses to figure out the expansions for c and d. Alternatively we can also use the hypotheses directly:

-- Alternate view
example (a b c d : ℝ) (h : c = b*a - d) (h' : d = a*b) : c = 0 := by
  calc
    c = b*a - d   := by exact h
    _ = b*a - a*b := by rw [h']
    _ = 0         := by ring

exact tells Lean to expand c using the h rule exactly. rw [h] replaces the LHS of h with the RHS. NOTE: rw [<- h'] will replace the RHS with LHS.

The gcongr tactic generalises congr tactic to inequalities

example (a b : ℝ) (h : b ≤ a) : a + b ≤ 2*a := by
  calc
    a + b ≤ a + a := by gcongr
    _  = 2*a := by ring

Using id to specialise#

id is the identity function fun x => x, with type P → P. It is always available and can be used to feed any hypothesis that expects a P → P argument.

-- h4 : (P → P) → Q
-- h5 : P
-- ⊢ P → Q
example (h4 : (P → P) → Q) (h5 : P) : P → Q := by
  specialize h4 id  -- feed id : P → P to h4, giving h4 : Q
  intro _           -- introduce the P in the goal, ignore it
  exact h4

Another example — the same pattern with a different proposition:

-- h : (P → P) → P → Q
-- hp : P
-- ⊢ Q
example (h : (P → P) → P → Q) (hp : P) : Q :=
  h id hp  -- feed id : P → P and hp : P to get Q

Assumption#

Often we have h: P and the goal might be something like |- P. We say exact h to finish the proof. We could also say assumption and if one of the hypotheses in the local context close out the goal, we’ll be done.

Intro#

Note that we can intro multiple times in a proof when applicable. See this example

example : (((P → Q) → Q) → Q) → P → Q := by
  -- Assume we have 
  intro hpqq hp 
  -- hpqq : ((P → Q) → Q) → Q
  --hp : P

  apply hpqq 
  -- New goal is (P->Q) -> Q

  -- Now we can assume that we have P->Q
  intro hpq 

  -- Forward resoning we feed hpq a proof of P to make it now a proof of Q
  specialize hpq hp 
  assumption 

ExFalso#

The exfalso tactic changes your goal to False. Why might you want to do that? Usually because at this point you can deduce a contradiction from your hypotheses (for example because you are in the middle of a proof by contradiction).

Examples#

hP : P
h : P → False
⊢ Q 

then this might initially look problematic, because we don’t have any facts about Q to hand but False -> Q, regardless of whether Q is False or True. So and hP and h between them are enough to prove False

exfalso -- goal now `False`
apply h -- goal now `P`
exact hP -- goal solved

exfalso can always change any goal to False, because False → P holds for any proposition P (the principle of explosion: from a contradiction, anything follows). However, it is only useful when you can actually derive False from your hypotheses. Changing the goal to False when you have no contradiction available just makes your life harder.

False is defined as a proposition with no proof (see Bhavik Mehta’s lean tips – he goes over this). So if you find yourself holding a proof of False, something has gone catastrophically wrong — you have a contradiction. A proof of False → P is a function that takes a proof of False and returns a proof of P, but since False has no proof, this function never gets called — it vacuously satisfies the contract.

Think of it like: “If pigs can fly, I’ll eat my hat.” This is a safe promise because pigs can’t fly, so you’ll never be held to it. Similarly, False → P is safe because False can never be established. In Lean this is False.elim : False → P — sometimes called ex falso quodlibet (“from falsity, anything”).

Change#

Change allows us to either replace the goal with a new expression or change the expersion of a hypothesis. It only works if the expression is definitionally equal to the goal or the hypothesis.

If your goal is ⊢ ¬P then change P → False will change it the goal to ⊢ P → False. change also works on hypotheses: if you have a hypothesis h : ¬P then change P → False at h will change h to h : P → False.

By_contra#

A side note: in Lean, ¬P is defined as P → False. And ¬¬P is ¬(¬P) = ¬(P → False) = (P → False) → False.

The by_contra tactic is strictly stronger than the exfalso tactic in that not only does it change the goal to False but it also throws in an extra hypothesis.

The by_contra tactic is a “proof by contradiction” tactic. If your goal is ⊢ P then by_contra h introduces a hypothesis h : ¬P and changes the goal to False

example (P : Prop) : ¬ ¬ P → P := by
  intro hnnP -- assume ¬ ¬ P
  by_contra hnP -- goal is now `False`
  apply hnnP -- goal is now ¬ P
  exact hnP

Cases#

Obtain#

Sometimes a hypothesis or goal will have many parts. For example, here we see the hypothesis h has two parts a proof of P and a proof of Q. To get each part we use the obtain tactic.

-- You can use `obtain`
example : P ∧ Q → P := by
  intro h
  obtain ⟨left, right⟩ := h
  exact left

R Cases#

One also might use the rcases tactic which does the same thing with different syntax.

-- or `rcases` (which is just `obtain` but with a slightly different syntax)
example : P ∧ Q → P := by
  intro h
  rcases h with ⟨left, right⟩
  exact left

There are other uses of rcases to for getting existential quantifiers out. Let’s say we have are given the following assumption:

ha : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε

Then to extract the B promised to exist, and use it we use rcases.

rcases ha with ⟨B, hB⟩
-- B is the special B that is promised to exist by ha 
-- hB : ∀ (n : ℕ), B ≤ n → |a n - t| < ε

For disjunctions

-- bc : ∀ x ∈ B, x ∈ A ( or x in B ==> x in A)
-- ab : ∀ x ∈ C, x ∈ A ( or x in C ==> x ic C)
-- hb : x ∈ B ∨ x ∈ C
-- x : X 
  rcases hb with h | h 
  . specialize bc x h --  here h: x ∈ B 
    assumption
  . specialize ab x h -- here h: x ∈ C
    assumption

Rintro#

The tactic rintro is like rcases with intro

example : P ∧ Q → P := by
  rintro ⟨left, right⟩
  exact left

Normal Indexing Of Conjunctions#

One could also not use any of these tactics and just use indexing

-- or you can get the relevant part out directly using `.left`
example : P ∧ Q → P := by
  intro h
  exact h.left

-- or by using `.1` (the first part)
example : P ∧ Q → P := by
  intro h
  exact h.1

Constructor#

Constructor does what obtain and rcases does but to the goal.

example : P → Q → P ∧ Q := by
  intro hP hQ
  constructor
  -- After the `constructor` tactic, we have *2 goals* for the first time!
  -- We use centre-dots, typed as `\.` to help Lean (and the reader) figure out when we're done
  · assumption
  · assumption

By Cases#

The by_cases h splits into all possible truth table values of type of h. In the example below, hP is term of a proposition.

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q := by
  constructor
  · intro h -- h: ¬ (P ∧ Q) and |- ¬ P ∨ Q 
    by_cases hP : P -- assume P is true 
    · right
      intro hQ
      apply h
      exact ⟨hP, hQ⟩
    · left -- assume Not ¬ P 
      exact hP
  · rintro (hnP | hnQ) ⟨hP, hQ⟩
    · contradiction
    · apply hnQ; exact hQ

Norm Num#

• norm_num (proves equalities and inequalities involving numerical expressions)

Use#

use (if the goal is ∃ x, x + 37 = 42 then use 8 will change the goal to 8 + 37 = 42, and use 10 will change it to 10 + 37 = 42.

Ite#

ite is just the function behind if-then-else. Writing:

ite h a b

where ite : Prop → α → α → α (with a Decidable instance).

example (x y : Nat) : (if 1 < 2 then x else y) = x := by
  simp only [↓reduceIte]

Lean sees ite (1 < 2) x y, the ↓reduceIte lemma fires top-down, evaluates 1 < 2 to True, and reduces the whole thing to x. Goal closed.

DSimp#

Sometimes you might see something like (fun n => n^2 + 3) 37, which means “take the function sending n to n^2+3 and then evaluate it at 37”. You can use the dsimp (or dsimp only) tactic to simplify this to 37^2+3.

simp: Applies rewrite rules — both definitional reductions and lemmas tagged @[simp] (or ones you pass explicitly). It can close goals or transform them using propositional equalities.

dsimp: Definitional simp. Only applies reductions that hold by definition — things the kernel considers definitionally equal without any proof. No lemmas, no propositional rewrites.

Specialize#

We have already seen how specialize allows us to forward reason with logical implications. For example if h:P and h1: P->Q, then specialize h1 h makes h1: Q by feeding it a proof that P is true, which implies that we get a proof that Q is true.

When dealing with a hypothesis that includes universal quantifiers as h shown below does, specialize allows us to feed h a specific instance that satisfies the for all condition.

/-- If `a(n)` tends to `t` then `a(n) + c` tends to `t + c` -/
theorem tendsTo_add_const {a : ℕ → ℝ} {t : ℝ} (c : ℝ) (h : TendsTo a t) :
    TendsTo (fun n => a n + c) (t + c) := by
  intro ε hε -- here hε: ε > 0 
  rw [tendsTo_def] at h -- this will just epand h to the for all definition
  -- h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
  
  -- this is saying use this epsilon as the forall epsilon, 
  -- and it's valid because he: ε > 0
  specialize h ε hε

The ext tactic#

If the goal is ⊢ A = B where A and B are subsets of X, then the tactic ext x, will create a hypothesis x : X and change the goal to x ∈ A ↔ x ∈ B.

Function Pulling And Pushing#

This horrible notation is because f takes terms of type X and S is of type Set X.

f '' S <-> {y : Y | ∃ x : X, x ∈ S ∧ f x = y}

Similarly, f⁻¹(T) doesn’t make sense in Lean either, because ⁻¹ is notation for Inv.inv, whose type in Lean is α → α. In other words, if x has a certain type, then x⁻¹ must have the same type: the notation was basically designed for group theory. So we write

f ⁻¹' T <-> {x : X | f x ∈ T}

TODO: Draw picture

conv#

conv lets you navigate into a specific subexpression of your goal and rewrite only there.

Why not just use rw with explicit arguments? Usually you can. For a * (b * c) = a * (c * b), just do rw [Nat.mul_comm b c].

When conv is actually needed: rewriting under binders rw cannot see inside fun, ∑, ∫, ∀, ∃, etc. The bound variable doesn’t exist at the tactic level, so you can’t pass it as an explicit argument.

-- rw [add_zero] fails here: it can't find `? + 0` under the binder
example (s : Finset ℕ) (f : ℕ → ℕ) : ∑ i in s, (f i + 0) = ∑ i in s, f i := by
  conv => lhs; intro i; rw [add_zero]

What’s happening step by step:

conv => — enter conversion mode, focus on entire goal lhs — focus on ∑ i in s, (f i + 0) intro i — enter the binder, focus on f i + 0 rw [add_zero] — rewrite to f i, done

congrArg#

This not necessarily a tactic but a helpful theorem to use. In simple words, if you wish to show f(x) = f(y), and then you have x=y, then you can just invoke congrArg by explicitly passing it f and a proof that x=y

theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α}
    (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂

As a minimal working example

example (a b : Nat) (h : a = b) : a + 1 = b + 1 :=
   congrArg (· + 1) h

What congrArg really lets us do is explicitly specify which argument of the function is equal. Normally with congr and congr 2 etc. we need to guess the number of unfoldings.

TODO: Move this to a newly created syntax section later, which accumulates all the Lean4 syntax updates.

(· + 1) is Lean 4’s anonymous function shorthand using \cdot. Each · inside parentheses becomes a parameter of an anonymous function. It’s equivalent to writing a fun lambda.

(· + 1)         -- fun x => x + 1
(· * 2)         -- fun x => x * 2
(· + ·)         -- fun x y => x + y     -- two dots = two params
(f · 3)         -- fun x => f x 3
(· :: [])       -- fun x => [x]

If you had two arguments, then we would just use congrArg twice.

example (f : Nat → Nat → Nat) (a b c d : Nat)
    (h1 : a = c) (h2 : b = d) : f a b = f c d := by
  -- f · b is syntax for fun x b => f x b 
  have step1 : f a b = f c b := congrArg (f · b) h1
  have step2 : f c b = f c d := congrArg (f c) h2
  -- Using the fact that equality is transitive
  exact step1.trans step2

What congrArg lets us do is explicitly specify the function through which equality is being pushed. For multi-argument functions, we control which argument varies by partially applying or using ·-syntax:

congrArg (f a) h pushes equality through the second argument, congrArg (f · b) h through the first.

simpa#

simpa using h simplifies both the goal and h, then tries to close the goal with the simplified h. It does not treat h as a simp lemma

simp at the goal
simp at h        -- a fresh copy of h, h itself is not modified in the context
exact h          -- (up to defeq / closing)

This can be reduced to

simpa [lemmas] using h

subst#

subst x looks in the local context for an equality involving the variable x i.e it looks for some hypthesis h : x = t or h : t = x.

It then:

1. Replaces every occurrence of x with t in the target and hypotheses.
2. Removes x from the context when possible.
3. Removes the equality h, because it is no longer needed.

For example:

x y : Nat
h : x = y
p : x > 3
⊢ x + 1 = y + 1

After: subst x the state becomes essentially:

y : Nat
p : y > 3
⊢ y + 1 = y + 1

If there is no suitable equality involving x, the tactic fails.