[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e₁ e₂ : α ≃ β
h₁ : e₁.toFun = e₂.toFun
h₂ : e₁.invFun = e₂.invFun
⊢ e₁ = e₂
[PROOFSTEP]
cases e₁
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
e₂ : α ≃ β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
h₁ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun = e₂.toFun
h₂ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂
[PROOFSTEP]
cases e₂
[GOAL]
case mk.mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
congr
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.16583
h : α = β
x✝ : α
⊢ cast (_ : β = α) (cast h x✝) = x✝
[PROOFSTEP]
cases h
[GOAL]
case refl
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort ?u.16583
x✝ : α
⊢ cast (_ : α = α) (cast (_ : α = α) x✝) = x✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.16583
h : α = β
x✝ : β
⊢ cast h (cast (_ : β = α) x✝) = x✝
[PROOFSTEP]
cases h
[GOAL]
case refl
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort ?u.16583
x✝ : α
⊢ cast (_ : α = α) (cast (_ : α = α) x✝) = x✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ ↑e = id
[PROOFSTEP]
rw [Perm.subsingleton_eq_refl e, coe_refl]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
⊢ ↑f x = y ↔ x = ↑f.symm y
[PROOFSTEP]
conv_lhs => rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
| ↑f x = y
[PROOFSTEP]
rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
| ↑f x = y
[PROOFSTEP]
rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
| ↑f x = y
[PROOFSTEP]
rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
⊢ ↑f x = ↑f (↑f.symm y) ↔ x = ↑f.symm y
[PROOFSTEP]
rw [apply_eq_iff_eq]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ ↑((Equiv.cast h).trans (Equiv.cast h2)) x = ↑(Equiv.cast (_ : α = γ)) x
[PROOFSTEP]
substs h h2
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
x : α
⊢ ↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort u_1
h : α = β
a : α
b : β
⊢ ↑(Equiv.cast h) a = b ↔ HEq a b
[PROOFSTEP]
subst h
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
a b : α
⊢ ↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b
[PROOFSTEP]
simp [coe_refl]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : (fun x => α) x
H : ↑e.symm x = y
⊢ x = ↑e y
[PROOFSTEP]
simp [H.symm]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : (fun x => α) x
H : x = ↑e y
⊢ ↑e.symm x = y
[PROOFSTEP]
simp [H]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ e.symm.symm = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.symm.symm =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ (Equiv.refl α).trans e = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ (Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ ∀ (x : β), ↑(e.symm.trans e) x = ↑(Equiv.refl β) x
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ ∀ (x : α), ↑(e.trans e.symm) x = ↑(Equiv.refl α) x
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
⊢ (fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac) = ac
[PROOFSTEP]
ext x
[GOAL]
case H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
x : α
⊢ ↑((fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac)) x = ↑ac x
[PROOFSTEP]
simp only [trans_apply, comp_apply, symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : β ≃ δ
⊢ (fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac) = ac
[PROOFSTEP]
ext x
[GOAL]
case H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : β ≃ δ
x : β
⊢ ↑((fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac)) x = ↑ac x
[PROOFSTEP]
simp only [trans_apply, comp_apply, apply_symm_apply]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
⊢ equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)
[PROOFSTEP]
ext
[GOAL]
case H.H
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
x✝¹ : α ≃ β
x✝ : α
⊢ ↑(↑(equivCongr (Equiv.refl α) (Equiv.refl β)) x✝¹) x✝ = ↑(↑(Equiv.refl (α ≃ β)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (equivCongr ab cd).symm = equivCongr ab.symm cd.symm
[PROOFSTEP]
ext
[GOAL]
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ↑(↑(equivCongr ab cd).symm x✝¹) x✝ = ↑(↑(equivCongr ab.symm cd.symm) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)
[PROOFSTEP]
ext
[GOAL]
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
x✝¹ : α ≃ δ
x✝ : γ
⊢ ↑(↑((equivCongr ab de).trans (equivCongr bc ef)) x✝¹) x✝ = ↑(↑(equivCongr (ab.trans bc) (de.trans ef)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
⊢ ↑(permCongr e) (Equiv.refl α') = Equiv.refl β'
[PROOFSTEP]
simp [permCongr_def]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
⊢ (↑(permCongr e) p).trans (↑(permCongr e) p') = ↑(permCongr e) (p.trans p')
[PROOFSTEP]
ext
[GOAL]
case H
α : Sort u
β : Sort v
γ : Sort w
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
x✝ : β'
⊢ ↑((↑(permCongr e) p).trans (↑(permCongr e) p')) x✝ = ↑(↑(permCongr e) (p.trans p')) x✝
[PROOFSTEP]
simp only [trans_apply, comp_apply, permCongr_apply, symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₁ → β₁
x : α₁
⊢ (fun f => ↑e₂.symm ∘ f ∘ ↑e₁) ((fun f => ↑e₂ ∘ f ∘ ↑e₁.symm) f) x = f x
[PROOFSTEP]
simp only [comp_apply, symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₂ → β₂
x : α₂
⊢ (fun f => ↑e₂ ∘ f ∘ ↑e₁.symm) ((fun f => ↑e₂.symm ∘ f ∘ ↑e₁) f) x = f x
[PROOFSTEP]
simp only [comp_apply, apply_symm_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
⊢ ↑(arrowCongr ea ec) (g ∘ f) = ↑(arrowCongr eb ec) g ∘ ↑(arrowCongr ea eb) f
[PROOFSTEP]
ext
[GOAL]
case h
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
x✝ : α₂
⊢ ↑(arrowCongr ea ec) (g ∘ f) x✝ = (↑(arrowCongr eb ec) g ∘ ↑(arrowCongr ea eb) f) x✝
[PROOFSTEP]
simp only [comp, arrowCongr_apply, eb.symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f₁ f₂ : α → α
⊢ ↑(conj e) (f₁ ∘ f₂) = ↑(conj e) f₁ ∘ ↑(conj e) f₂
[PROOFSTEP]
apply arrowCongr_comp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : Prop
⊢ (fun b => b = true) ((fun p => decide p) p) = p
[PROOFSTEP]
simp [@Bool.decide_iff p (Classical.propDecidable _)]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun p => decide p) ((fun b => b = true) b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
α : Sort u
β : Sort v
γ : Sort w
⊢ (fun p => decide p) ((fun b => b = true) false) = false
[PROOFSTEP]
simp
[GOAL]
case true
α : Sort u
β : Sort v
γ : Sort w
⊢ (fun p => decide p) ((fun b => b = true) true) = true
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β✝ : Sort v
γ : Sort w
β : α → Sort u_1
inst✝ : Subsingleton α
a : α
x✝ : (a' : α) → β a'
b : α
⊢ (fun x b => cast (_ : β a = β b) x) (eval a x✝) b = x✝ b
[PROOFSTEP]
rw [Subsingleton.elim b a]
[GOAL]
α : Sort u
β✝ : Sort v
γ : Sort w
β : α → Sort u_1
inst✝ : Subsingleton α
a : α
x✝ : (a' : α) → β a'
b : α
⊢ (fun x b => cast (_ : β a = β b) x) (eval a x✝) a = x✝ a
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∃! x, p x) ↔ ∃! y, q y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∃! x, p x) → ∃! y, q y
[PROOFSTEP]
rintro ⟨a, ha₁, ha₂⟩
[GOAL]
case mp.intro.intro
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
a : α
ha₁ : p a
ha₂ : ∀ (y : α), (fun x => p x) y → y = a
⊢ ∃! y, q y
[PROOFSTEP]
exact ⟨f a, h.1 ha₁, fun b hb => f.symm_apply_eq.1 (ha₂ (f.symm b) (h.2 (by simpa using hb)))⟩
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
a : α
ha₁ : p a
ha₂ : ∀ (y : α), (fun x => p x) y → y = a
b : β
hb : (fun y => q y) b
⊢ q (↑f (↑f.symm b))
[PROOFSTEP]
simpa using hb
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∃! y, q y) → ∃! x, p x
[PROOFSTEP]
rintro ⟨b, hb₁, hb₂⟩
[GOAL]
case mpr.intro.intro
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
b : β
hb₁ : q b
hb₂ : ∀ (y : β), (fun y => q y) y → y = b
⊢ ∃! x, p x
[PROOFSTEP]
exact ⟨f.symm b, h.2 (by simpa using hb₁), fun y hy => (eq_symm_apply f).2 (hb₂ _ (h.1 hy))⟩
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
b : β
hb₁ : q b
hb₂ : ∀ (y : β), (fun y => q y) y → y = b
⊢ q (↑f (↑f.symm b))
[PROOFSTEP]
simpa using hb₁
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
f : α ≃ β
x✝ : α
⊢ p x✝ ↔ p (↑f.symm (↑f x✝))
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∀ (x : α), p x) ↔ ∀ (y : β), q y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∀ (x : α), p x) → ∀ (y : β), q y
[PROOFSTEP]
intro h₂ x
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∀ (y : β), q y) → ∀ (x : α), p x
[PROOFSTEP]
intro h₂ x
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q x
[PROOFSTEP]
rw [← f.right_inv x]
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q (toFun f (invFun f x))
[PROOFSTEP]
apply h.mp
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ p (invFun f x)
[PROOFSTEP]
apply h₂
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ p x
[PROOFSTEP]
apply h.mpr
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ q (↑f x)
[PROOFSTEP]
apply h₂
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
f : α ≃ β
⊢ ∀ {x : α}, p x ↔ p (↑f.symm (↑f x))
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
f : α ≃ β
p : α → Prop
x✝ : ∃ a, p a
a : α
h : p a
⊢ p (↑f.symm (↑f a))
[PROOFSTEP]
simpa using h
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
⊢ LeftInverse (Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂)))
    (Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂)))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
x✝ : Quot ra
a : α
⊢ Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂))
      (Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂)) (mk ra a)) =
    mk ra a
[PROOFSTEP]
simp only [Quot.map, Equiv.symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
⊢ Function.RightInverse (Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂)))
    (Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂)))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
x✝ : Quot rb
a : β
⊢ Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂))
      (Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂)) (mk rb a)) =
    mk rb a
[PROOFSTEP]
simp only [Quot.map, Equiv.apply_symm_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
r : α → α → Prop
e : α ≃ β
x✝¹ x✝ : α
⊢ r x✝¹ x✝ ↔ r (↑e.symm (↑e x✝¹)) (↑e.symm (↑e x✝))
[PROOFSTEP]
simp only [e.symm_apply_apply]
