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