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

State before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : ∀ (x : α), e₁.fwd x = e₂.fwd x
⊢ e₁ = e₂
Tactic:
ext
State after:
case h.h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : ∀ (x : α), e₁.fwd x = e₂.fwd x
x✝ : α
⊢ e₁.fwd x✝ = e₂.fwd x✝

State before:
case h.h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : ∀ (x : α), e₁.fwd x = e₂.fwd x
x✝ : α
⊢ e₁.fwd x✝ = e₂.fwd x✝
Tactic:
exact h ..
State after:
no goals