Apply the constant iff_of_eq to the goal.

The main part of the body for the loop in congr'. This will try to replace a goal f x = f y with x = y. Also has support for == and ↔.

The main function in convert_to. Changes the goal to r and a proof obligation that the goal is equal to r.

Attempts to prove the goal by proof irrelevance, but avoids unifying universe metavariables to do so.

Same as the congr tactic, but takes an optional argument which gives the depth of recursive applications.

• This is useful when congr is too aggressive in breaking down the goal.
• For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr' produces the goals ⊢ x = y and ⊢ y = x, while congr' 2 produces the intended ⊢ x + y = y + x.
• If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.

Same as the congr tactic, but takes an optional argument which gives the depth of recursive applications.

• This is useful when congr is too aggressive in breaking down the goal.
• For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr' produces the goals ⊢ x = y and ⊢ y = x, while congr' 2 produces the intended ⊢ x + y = y + x.
• If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
• You can use congr' with p (: n)? to call ext p (: n)? to all subgoals generated by congr'. For example, if the goal is ⊢ f '' s = g '' s then congr' with x generates the goal x : α ⊢ f x = g x.

Repeatedly and apply congr' and ext, using the given patterns as arguments for ext.

There are two ways this tactic stops:

• congr' fails (makes no progress), after having already applied ext.
• congr' canceled out the last usage of ext. In this case, the state is reverted to before the congr' was applied.

For example, when the goal is

⊢ (λ x, f x + 3) '' s = (λ x, g x + 3) '' s

then rcongr x produces the goal

x : α ⊢ f x = g x

This gives the same result as congr', ext x, congr'.

In contrast, congr' would produce

⊢ (λ x, f x + 3) = (λ x, g x + 3)

and congr' with x (or congr', ext x) would produce

x : α ⊢ f x + 3 = g x + 3

The exact e and refine e tactics require a term e whose type is definitionally equal to the goal. convert e is similar to refine e, but the type of e is not required to exactly match the goal. Instead, new goals are created for differences between the type of e and the goal. For example, in the proof state

n : ℕ,
e : prime (2 * n + 1)
⊢ prime (n + n + 1)

the tactic convert e will change the goal to

⊢ n + n = 2 * n

In this example, the new goal can be solved using ring.

The convert tactic applies congruence lemmas eagerly before reducing, therefore it can fail in cases where exact succeeds:

def p (n : ℕ) := true
example (h : p 0) : p 1 := by exact h -- succeeds
example (h : p 0) : p 1 := by convert h -- fails, with leftover goal `1 = 0`

If x y : t, and an instance subsingleton t is in scope, then any goals of the form x = y are solved automatically.

The syntax convert ← e will reverse the direction of the new goals (producing ⊢ 2 * n = n + n in this example).

Internally, convert e works by creating a new goal asserting that the goal equals the type of e, then simplifying it using congr'. The syntax convert e using n can be used to control the depth of matching (like congr' n). In the example, convert e using 1 would produce a new goal ⊢ n + n + 1 = 2 * n + 1.

convert_to g using n attempts to change the current goal to g, but unlike change, it will generate equality proof obligations using congr' n to resolve discrepancies. convert_to g defaults to using congr' 1.

convert_to is similar to convert, but convert_to takes a type (the desired subgoal) while convert takes a proof term. That is, convert_to g using n is equivalent to convert (_ : g) using n.

ac_change g using n is convert_to g using n followed by ac_refl. It is useful for rearranging/reassociating e.g. sums:

example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N :=
begin
  ac_change a + d + e + f + c + g + b ≤ _,
-- ⊢ a + d + e + f + c + g + b ≤ N
end