case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ ↑f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ ↑(PEquiv.trans (single a b) f) x✝ ↔ a✝ ∈ ↑(single a c) x✝
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ ↑f b
⊢ PEquiv.trans (single a b) f = single a c
ext
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ ↑f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ Option.bind (if x✝ = a then some b else none) ↑f ↔ a✝ ∈ if x✝ = a then some c else none
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ ↑f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ ↑(PEquiv.trans (single a b) f) x✝ ↔ a✝ ∈ ↑(single a c) x✝
dsimp [single, PEquiv.trans]
no goals
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ ↑f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ Option.bind (if x✝ = a then some b else none) ↑f ↔ a✝ ∈ if x✝ = a then some c else none
split_ifs <;> simp_all