[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
⊢ Injective toFun
[PROOFSTEP]
rintro ⟨f₁, f₂, hf⟩ ⟨g₁, g₂, hg⟩ (rfl : f₁ = g₁)
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
δ : Type x
f₁ : α → Option β
f₂ : β → Option α
hf : ∀ (a : α) (b : β), a ∈ f₂ b ↔ b ∈ f₁ a
g₂ : β → Option α
hg : ∀ (a : α) (b : β), a ∈ g₂ b ↔ b ∈ f₁ a
⊢ { toFun := f₁, invFun := f₂, inv := hf } = { toFun := f₁, invFun := g₂, inv := hg }
[PROOFSTEP]
congr with y x
[GOAL]
case mk.mk.e_invFun.h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f₁ : α → Option β
f₂ : β → Option α
hf : ∀ (a : α) (b : β), a ∈ f₂ b ↔ b ∈ f₁ a
g₂ : β → Option α
hg : ∀ (a : α) (b : β), a ∈ g₂ b ↔ b ∈ f₁ a
y : β
x : α
⊢ x ∈ f₂ y ↔ x ∈ g₂ y
[PROOFSTEP]
simp only [hf, hg]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
b : γ
⊢ a ∈ (fun a => Option.bind (↑(PEquiv.symm g) a) ↑(PEquiv.symm f)) b ↔ b ∈ (fun a => Option.bind (↑f a) ↑g) a
[PROOFSTEP]
simp_all [and_comm, eq_some_iff f, eq_some_iff g]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.symm (PEquiv.symm f) = f
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u
β : Type v
γ : Type w
δ : Type x
toFun✝ : α → Option β
invFun✝ : β → Option α
inv✝ : ∀ (a : α) (b : β), a ∈ invFun✝ b ↔ b ∈ toFun✝ a
⊢ PEquiv.symm (PEquiv.symm { toFun := toFun✝, invFun := invFun✝, inv := inv✝ }) =
    { toFun := toFun✝, invFun := invFun✝, inv := inv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ ↑(PEquiv.trans f g) a = none ↔ ∀ (b : β) (c : γ), ¬b ∈ ↑f a ∨ ¬c ∈ ↑g b
[PROOFSTEP]
simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ¬∃ b, b ∈ ↑f a ∧ a_1 ∈ ↑g b) ↔ ∀ (b : β) (c : γ), b ∈ ↑f a → ¬c ∈ ↑g b
[PROOFSTEP]
push_neg
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ) (b : β), b ∈ ↑f a → ¬a_1 ∈ ↑g b) ↔ ∀ (b : β) (c : γ), b ∈ ↑f a → ¬c ∈ ↑g b
[PROOFSTEP]
exact forall_swap
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans (PEquiv.refl α) f = f
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ ↑(PEquiv.trans (PEquiv.refl α) f) x✝ ↔ a✝ ∈ ↑f x✝
[PROOFSTEP]
dsimp [PEquiv.trans]
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ ↑f x✝ ↔ a✝ ∈ ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans f (PEquiv.refl β) = f
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ ↑(PEquiv.trans f (PEquiv.refl β)) x✝ ↔ a✝ ∈ ↑f x✝
[PROOFSTEP]
dsimp [PEquiv.trans]
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ Option.bind (↑f x✝) ↑(PEquiv.refl β) ↔ a✝ ∈ ↑f x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : b ∈ ↑f a₁
h₂ : b ∈ ↑f a₂
⊢ a₁ = a₂
[PROOFSTEP]
rw [← mem_iff_mem] at *
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ ↑(PEquiv.symm f) b
h₂ : a₂ ∈ ↑(PEquiv.symm f) b
⊢ a₁ = a₂
[PROOFSTEP]
cases h : f.symm b
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ ↑(PEquiv.symm f) b
h₂ : a₂ ∈ ↑(PEquiv.symm f) b
h : ↑(PEquiv.symm f) b = none
⊢ a₁ = a₂
[PROOFSTEP]
simp_all
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ ↑(PEquiv.symm f) b
h₂ : a₂ ∈ ↑(PEquiv.symm f) b
val✝ : α
h : ↑(PEquiv.symm f) b = some val✝
⊢ a₁ = a₂
[PROOFSTEP]
simp_all
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) (↑f x) = x
[PROOFSTEP]
classical
cases hfx : f x
· have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
  simp [this]
· dsimp only
  rw [(eq_some_iff f).2 hfx]
  rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) (↑f x) = x
[PROOFSTEP]
cases hfx : f x
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) none = x
[PROOFSTEP]
have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
⊢ ¬isSome none = true
[PROOFSTEP]
simp
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
this : x = a₂
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) none = x
[PROOFSTEP]
simp [this]
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) (some val✝) = x
[PROOFSTEP]
dsimp only
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ Option.rec a₂ id (↑(PEquiv.symm f) val✝) = x
[PROOFSTEP]
rw [(eq_some_iff f).2 hfx]
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ Option.rec a₂ id (some x) = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ a ∈ (fun a => if a ∈ s then some a else none) b ↔ b ∈ (fun a => if a ∈ s then some a else none) a
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ b ∈ if a ∈ s then some a else none
[PROOFSTEP]
split_ifs with hb ha ha
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
hb : b ∈ s
ha : a ∈ s
⊢ a ∈ some b ↔ b ∈ some a
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
hb : b ∈ s
ha : ¬a ∈ s
⊢ a ∈ some b ↔ b ∈ none
[PROOFSTEP]
simp [ne_of_mem_of_not_mem hb ha]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
hb : ¬b ∈ s
ha : a ∈ s
⊢ a ∈ none ↔ b ∈ some a
[PROOFSTEP]
simp [ne_of_mem_of_not_mem ha hb]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
hb : ¬b ∈ s
ha : ¬a ∈ s
⊢ a ∈ none ↔ b ∈ none
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ a ∈ ↑(ofSet s) a ↔ a ∈ s
[PROOFSTEP]
dsimp [ofSet]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h✝ : a ∈ s
⊢ a ∈ some a ↔ a ∈ s
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h✝ : ¬a ∈ s
⊢ a ∈ none ↔ a ∈ s
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ a ∈ ↑(ofSet s) b ↔ a = b ∧ a ∈ s
[PROOFSTEP]
dsimp [ofSet]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a ∈ some b ↔ a = b ∧ a ∈ s
[PROOFSTEP]
simp only [mem_def, eq_comm, some.injEq, iff_self_and]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a = b → a ∈ s
[PROOFSTEP]
rintro rfl
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : a ∈ s
⊢ a ∈ s
[PROOFSTEP]
exact h
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : ¬b ∈ s
⊢ a ∈ none ↔ a = b ∧ a ∈ s
[PROOFSTEP]
simp only [mem_def, false_iff, not_and]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : ¬b ∈ s
⊢ a = b → ¬a ∈ s
[PROOFSTEP]
rintro rfl
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : ¬a ∈ s
⊢ ¬a ∈ s
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
⊢ s = Set.univ
[PROOFSTEP]
rw [Set.eq_univ_iff_forall]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
⊢ ∀ (x : α), x ∈ s
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ s
[PROOFSTEP]
rw [← mem_ofSet_self_iff, h]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ ↑(PEquiv.refl α) x✝
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
h : s = Set.univ
⊢ ofSet s = PEquiv.refl α
[PROOFSTEP]
simp only [← ofSet_univ, h]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans f (PEquiv.symm f) = ofSet {a | isSome (↑f a) = true}
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ ↑(PEquiv.trans f (PEquiv.symm f)) x✝ ↔ a✝ ∈ ↑(ofSet {a | isSome (↑f a) = true}) x✝
[PROOFSTEP]
dsimp [PEquiv.trans]
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ Option.bind (↑f x✝) ↑(PEquiv.symm f) ↔ a✝ ∈ ↑(ofSet {a | isSome (↑f a) = true}) x✝
[PROOFSTEP]
simp only [eq_some_iff f, Option.isSome_iff_exists, Option.mem_def, bind_eq_some', ofSet_eq_some_iff]
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a) ↔ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
[PROOFSTEP]
constructor
[GOAL]
case h.a.mp
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a) → a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
[PROOFSTEP]
rintro ⟨b, hb₁, hb₂⟩
[GOAL]
case h.a.mp.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
b : β
hb₁ : ↑f x✝ = some b
hb₂ : ↑f a✝ = some b
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1}
[PROOFSTEP]
exact ⟨PEquiv.inj _ hb₂ hb₁, b, hb₂⟩
[GOAL]
case h.a.mpr
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ a✝ : α
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, ↑f a = some a_1} → ∃ a, ↑f x✝ = some a ∧ ↑f a✝ = some a
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.symm (PEquiv.trans (PEquiv.symm f) f) = PEquiv.symm (ofSet {b | isSome (↑(PEquiv.symm f) b) = true})
[PROOFSTEP]
simp [symm_trans_rev, self_trans_symm, -symm_symm]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans f (PEquiv.symm f) = PEquiv.refl α ↔ ∀ (a : α), isSome (↑f a) = true
[PROOFSTEP]
rw [self_trans_symm, ofSet_eq_refl, Set.eq_univ_iff_forall]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | isSome (↑f a) = true}) ↔ ∀ (a : α), isSome (↑f a) = true
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
⊢ ∀ (a : α) (b : β), a ∈ (fun x => none) b ↔ b ∈ (fun x => none) a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans f ⊥ = ⊥
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : γ
⊢ a✝ ∈ ↑(PEquiv.trans f ⊥) x✝ ↔ a✝ ∈ ↑⊥ x✝
[PROOFSTEP]
dsimp [PEquiv.trans]
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
x✝ : α
a✝ : γ
⊢ a✝ ∈ Option.bind (↑f x✝) ↑⊥ ↔ a✝ ∈ none
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : β ≃. γ
⊢ PEquiv.trans ⊥ f = ⊥
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ a✝ ∈ ↑(PEquiv.trans ⊥ f) x✝ ↔ a✝ ∈ ↑⊥ x✝
[PROOFSTEP]
dsimp [PEquiv.trans]
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ a✝ ∈ none ↔ a✝ ∈ none
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a : α
h : isSome (↑f a) = true
⊢ ↑(PEquiv.symm f) (Option.get (↑f a) h) = some a
[PROOFSTEP]
rw [f.eq_some_iff, some_get]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
⊢ x ∈ (fun x => if x = b then some a else none) y ↔ y ∈ (fun x => if x = a then some b else none) x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
⊢ (x ∈ if y = b then some a else none) ↔ y ∈ if x = a then some b else none
[PROOFSTEP]
split_ifs with h1 h2
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : x = a
⊢ x ∈ some a ↔ y ∈ some b
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
⊢ x ∈ some a ↔ y ∈ none
[PROOFSTEP]
simp only [mem_def, some.injEq, iff_false] at *
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
⊢ ¬a = x
[PROOFSTEP]
exact Ne.symm h2
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : x = a
⊢ x ∈ none ↔ y ∈ some b
[PROOFSTEP]
simp only [mem_def, some.injEq, false_iff] at *
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : x = a
⊢ ¬b = y
[PROOFSTEP]
exact Ne.symm h1
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : ¬x = a
⊢ x ∈ none ↔ y ∈ none
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a₁ a₂ : α
b₁ b₂ : β
⊢ b₁ ∈ ↑(single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
dsimp [single]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a₁ a₂ : α
b₁ b₂ : β
h✝ : a₁ = a₂
⊢ b₁ ∈ some b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp [*, eq_comm]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a₁ a₂ : α
b₁ b₂ : β
h✝ : ¬a₁ = a₂
⊢ b₁ ∈ none ↔ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp [*, eq_comm]
[GOAL]
α : 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
[PROOFSTEP]
ext
[GOAL]
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✝
[PROOFSTEP]
dsimp [single, PEquiv.trans]
[GOAL]
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ ↑f b
x✝ : α
a✝ : γ
h✝ : x✝ = a
⊢ a✝ ∈ Option.bind (some b) ↑f ↔ a✝ ∈ some c
[PROOFSTEP]
simp_all
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ ↑f b
x✝ : α
a✝ : γ
h✝ : ¬x✝ = a
⊢ a✝ ∈ Option.bind none ↑f ↔ a✝ ∈ none
[PROOFSTEP]
simp_all
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b : α
⊢ single a b = PEquiv.refl α
[PROOFSTEP]
ext i j
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b i j : α
⊢ j ∈ ↑(single a b) i ↔ j ∈ ↑(PEquiv.refl α) i
[PROOFSTEP]
dsimp [single]
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b i j : α
⊢ (j ∈ if i = a then some b else none) ↔ j ∈ some i
[PROOFSTEP]
rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]
[GOAL]
α : 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) = ⊥
[PROOFSTEP]
ext
[GOAL]
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✝
[PROOFSTEP]
simp only [eq_none_iff_forall_not_mem, Option.mem_def, f.eq_some_iff] at h 
[GOAL]
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✝
[PROOFSTEP]
dsimp [PEquiv.trans, single]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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✝
[PROOFSTEP]
intros
[GOAL]
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✝¹
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : 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✝
h✝ : x✝ = b
⊢ ¬some c = some a✝¹
[PROOFSTEP]
simp_all
[GOAL]
case neg
α : 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✝
h✝ : ¬x✝ = b
⊢ ¬False
[PROOFSTEP]
simp_all
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : f ≤ g
gf : g ≤ f
⊢ ∀ (x : α), ↑f x = ↑g x
[PROOFSTEP]
intro a
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : f ≤ g
gf : g ≤ f
a : α
⊢ ↑f a = ↑g a
[PROOFSTEP]
cases' h : g a with b
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : f ≤ g
gf : g ≤ f
a : α
h : ↑g a = none
⊢ ↑f a = none
[PROOFSTEP]
exact eq_none_iff_forall_not_mem.2 fun b hb => Option.not_mem_none b <| h ▸ fg a b hb
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : f ≤ g
gf : g ≤ f
a : α
b : β
h : ↑g a = some b
⊢ ↑f a = some b
[PROOFSTEP]
exact gf _ _ h
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
⊢ a ∈ (fun b => if ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b then ↑(PEquiv.symm f) b else none) b ↔
    b ∈ (fun a => if ↑f a = ↑g a then ↑f a else none) a
[PROOFSTEP]
have hf := @mem_iff_mem _ _ f a b
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : a ∈ ↑(PEquiv.symm f) b ↔ b ∈ ↑f a
⊢ a ∈ (fun b => if ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b then ↑(PEquiv.symm f) b else none) b ↔
    b ∈ (fun a => if ↑f a = ↑g a then ↑f a else none) a
[PROOFSTEP]
have hg := @mem_iff_mem _ _ g a b
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : a ∈ ↑(PEquiv.symm f) b ↔ b ∈ ↑f a
hg : a ∈ ↑(PEquiv.symm g) b ↔ b ∈ ↑g a
⊢ a ∈ (fun b => if ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b then ↑(PEquiv.symm f) b else none) b ↔
    b ∈ (fun a => if ↑f a = ↑g a then ↑f a else none) a
[PROOFSTEP]
simp only [Option.mem_def] at *
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
⊢ (if ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b then ↑(PEquiv.symm f) b else none) = some a ↔
    (if ↑f a = ↑g a then ↑f a else none) = some b
[PROOFSTEP]
split_ifs with h1 h2 h2
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = ↑g a
⊢ ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
[PROOFSTEP]
try simp [hf]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = ↑g a
⊢ ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
[PROOFSTEP]
simp [hf]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ¬↑f a = ↑g a
⊢ ↑(PEquiv.symm f) b = some a ↔ False
[PROOFSTEP]
try simp [hf]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ¬↑f a = ↑g a
⊢ ↑(PEquiv.symm f) b = some a ↔ False
[PROOFSTEP]
simp [hf]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ¬↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = ↑g a
⊢ False ↔ ↑f a = some b
[PROOFSTEP]
try simp [hf]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ¬↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = ↑g a
⊢ False ↔ ↑f a = some b
[PROOFSTEP]
simp [hf]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ¬↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ¬↑f a = ↑g a
⊢ False ↔ False
[PROOFSTEP]
try simp [hf]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ¬↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ¬↑f a = ↑g a
⊢ False ↔ False
[PROOFSTEP]
simp [hf]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ¬↑f a = ↑g a
⊢ ¬↑f a = some b
[PROOFSTEP]
contrapose! h2
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = some b
⊢ ↑f a = ↑g a
[PROOFSTEP]
rw [h2]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = some b
⊢ some b = ↑g a
[PROOFSTEP]
rw [← h1, hf, h2] at hg 
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : some b = some b ↔ ↑g a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = some b
⊢ some b = ↑g a
[PROOFSTEP]
simp only [mem_def, true_iff_iff, eq_self_iff_true] at hg 
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
h1 : ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = some b
hg : ↑g a = some b
⊢ some b = ↑g a
[PROOFSTEP]
rw [hg]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h1 : ¬↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
h2 : ↑f a = ↑g a
⊢ ¬↑f a = some b
[PROOFSTEP]
contrapose! h1
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ ↑f a = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h2 : ↑f a = ↑g a
h1 : ↑f a = some b
⊢ ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
[PROOFSTEP]
rw [h1] at hf h2 
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ some b = some b
hg : ↑(PEquiv.symm g) b = some a ↔ ↑g a = some b
h2 : some b = ↑g a
h1 : ↑f a = some b
⊢ ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
[PROOFSTEP]
rw [← h2] at hg 
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
hf : ↑(PEquiv.symm f) b = some a ↔ some b = some b
hg : ↑(PEquiv.symm g) b = some a ↔ some b = some b
h2 : some b = ↑g a
h1 : ↑f a = some b
⊢ ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
[PROOFSTEP]
simp only [iff_true] at hf hg 
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g : α ≃. β
a : α
b : β
h2 : some b = ↑g a
h1 : ↑f a = some b
hf : ↑(PEquiv.symm f) b = some a
hg : ↑(PEquiv.symm g) b = some a
⊢ ↑(PEquiv.symm f) b = ↑(PEquiv.symm g) b
[PROOFSTEP]
rw [hf, hg]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ ↑(x✝³ ⊓ x✝²) x✝¹ → x✝ ∈ ↑x✝³ x✝¹
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if ↑x✝³ x✝¹ = ↑x✝² x✝¹ then ↑x✝³ x✝¹ else none) = some x✝ → ↑x✝³ x✝¹ = some x✝
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : ↑x✝³ x✝¹ = ↑x✝² x✝¹
⊢ ↑x✝³ x✝¹ = some x✝ → ↑x✝³ x✝¹ = some x✝
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : ¬↑x✝³ x✝¹ = ↑x✝² x✝¹
⊢ False → ↑x✝³ x✝¹ = some x✝
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ ↑(x✝³ ⊓ x✝²) x✝¹ → x✝ ∈ ↑x✝² x✝¹
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if ↑x✝³ x✝¹ = ↑x✝² x✝¹ then ↑x✝³ x✝¹ else none) = some x✝ → ↑x✝² x✝¹ = some x✝
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : ↑x✝³ x✝¹ = ↑x✝² x✝¹
⊢ ↑x✝³ x✝¹ = some x✝ → ↑x✝² x✝¹ = some x✝
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : ¬↑x✝³ x✝¹ = ↑x✝² x✝¹
⊢ False → ↑x✝² x✝¹ = some x✝
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
⊢ b ∈ ↑f a → b ∈ ↑(g ⊓ h) a
[PROOFSTEP]
intro H
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : b ∈ ↑f a
⊢ b ∈ ↑(g ⊓ h) a
[PROOFSTEP]
have hf := fg a b H
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : b ∈ ↑f a
hf : b ∈ ↑g a
⊢ b ∈ ↑(g ⊓ h) a
[PROOFSTEP]
have hg := gh a b H
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : b ∈ ↑f a
hf : b ∈ ↑g a
hg : b ∈ ↑h a
⊢ b ∈ ↑(g ⊓ h) a
[PROOFSTEP]
simp only [Option.mem_def, PEquiv.coe_mk_apply] at *
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
src✝ : PartialOrder (α ≃. β) := instPartialOrderPEquiv
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : ↑f a = some b
hf : ↑g a = some b
hg : ↑h a = some b
⊢ (if ↑g a = ↑h a then ↑g a else none) = some b
[PROOFSTEP]
rw [hf, hg, if_pos rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ≃ β
⊢ ∀ (a : α) (b : β), a ∈ (some ∘ ↑f.symm) b ↔ b ∈ (some ∘ ↑f) a
[PROOFSTEP]
simp [Equiv.eq_symm_apply, eq_comm]
