Theorem: Equiv.ext (Extra/Equiv/Basic.lean)

State before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
⊢ e₁ = e₂
Tactic:
have h' : e₁.rev = e₂.rev := by funext; rw [← fwd_eq_iff_rev_eq, h, fwd_rev]
State after:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
h' : e₁.rev = e₂.rev
⊢ e₁ = e₂

State before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
h' : e₁.rev = e₂.rev
⊢ e₁ = e₂
Tactic:
match e₁, e₂ with | ⟨_,_,_⟩, ⟨_,_,_⟩ => cases h; cases h'; rfl
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
⊢ e₁.rev = e₂.rev
Tactic:
funext
State after:
case h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
x✝ : β
⊢ e₁.rev x✝ = e₂.rev x✝

State before:
case h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
x✝ : β
⊢ e₁.rev x✝ = e₂.rev x✝
Tactic:
rw [← fwd_eq_iff_rev_eq, h, fwd_rev]
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝¹ : α → β
rev✝¹ : β → α
fwd_eq_iff_rev_eq✝¹ : ∀ {x : α} {y : β}, fwd✝¹ x = y ↔ rev✝¹ y = x
fwd✝ : α → β
rev✝ : β → α
fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
h :
  { fwd := fwd✝¹, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.fwd =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.fwd
h' :
  { fwd := fwd✝¹, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.rev =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.rev
⊢ { fwd := fwd✝¹, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Tactic:
cases h
State after:
case refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝¹ : β → α
fwd_eq_iff_rev_eq✝¹ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝¹ y = x
rev✝ : β → α
fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
h' :
  { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.rev =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.rev
⊢ { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }

State before:
case refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝¹ : β → α
fwd_eq_iff_rev_eq✝¹ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝¹ y = x
rev✝ : β → α
fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
h' :
  { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.rev =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.rev
⊢ { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Tactic:
cases h'
State after:
case refl.refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝ : β → α
fwd_eq_iff_rev_eq✝¹ fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
⊢ { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }

State before:
case refl.refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝ : β → α
fwd_eq_iff_rev_eq✝¹ fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
⊢ { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Tactic:
rfl
State after:
no goals