[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c
[PROOFSTEP]
rw [le_himp_iff, inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ b ⇨ c ↔ b ≤ a ⇨ c
[PROOFSTEP]
rw [le_himp_iff, le_himp_iff']
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ a ⇨ b ↔ a ≤ b
[PROOFSTEP]
rw [le_himp_iff, inf_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⊓ (a ⇨ b) ≤ b
[PROOFSTEP]
rw [inf_comm, ← le_himp_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
⊢ a ⊓ (a ⇨ b) ≤ b
[PROOFSTEP]
rw [inf_comm, ← le_himp_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
⊢ (a ⇨ b) ⊓ a = b ⊓ a
[PROOFSTEP]
rw [inf_comm, inf_himp, inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇨ b = ⊤ ↔ a ≤ b
[PROOFSTEP]
rw [← top_le_iff, le_himp_iff, top_inf_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b✝ c d b : α
⊢ b ≤ ⊤ ⇨ a ↔ b ≤ a
[PROOFSTEP]
rw [le_himp_iff, inf_top_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c
[PROOFSTEP]
simp_rw [le_himp_iff, inf_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
[PROOFSTEP]
rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ c ⊓ (b ⊓ a) ≤ c
[PROOFSTEP]
exact inf_le_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c
[PROOFSTEP]
simpa using @himp_le_himp_himp_himp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ⇨ b ⇨ c = b ⇨ a ⇨ c
[PROOFSTEP]
simp_rw [himp_himp, inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ b ⇨ b ⇨ a = b ⇨ a
[PROOFSTEP]
rw [himp_himp, inf_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
[PROOFSTEP]
simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ d ≤ a ⊔ b ⇨ c ↔ d ≤ (a ⇨ c) ⊓ (b ⇨ c)
[PROOFSTEP]
rw [le_inf_iff, le_himp_comm, sup_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
[PROOFSTEP]
simp_rw [le_himp_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
⊢ a ⊔ b ⇨ a = b ⇨ a
[PROOFSTEP]
rw [sup_himp_distrib, himp_self, top_inf_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
⊢ a ⊔ b ⇨ b = a ⇨ b
[PROOFSTEP]
rw [sup_himp_distrib, himp_self, inf_top_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ b ⇨ a = a
[PROOFSTEP]
conv_rhs => rw [← @top_himp _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
| a
[PROOFSTEP]
rw [← @top_himp _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
| a
[PROOFSTEP]
rw [← @top_himp _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
| a
[PROOFSTEP]
rw [← @top_himp _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a
[PROOFSTEP]
rw [← h.eq_top, sup_himp_self_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ a ⇨ a ⊓ b = b
[PROOFSTEP]
rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ b ⇨ a ⊓ b = a
[PROOFSTEP]
rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c
[PROOFSTEP]
rw [le_himp_iff, inf_right_comm, ← le_himp_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
[PROOFSTEP]
exact himp_inf_le.trans le_himp_himp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
[PROOFSTEP]
simp_rw [@inf_comm _ _ a, ← le_himp_iff, sup_le_iff, le_himp_iff, ← sup_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ⊓ a ⊔ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : OrderBot αᵒᵈ := orderBot α
a b c : αᵒᵈ
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
[PROOFSTEP]
rw [sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : OrderBot αᵒᵈ := orderBot α
a b c : αᵒᵈ
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b
[PROOFSTEP]
exact le_himp_iff
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : GeneralizedHeytingAlgebra α✝
a b c d : α✝
α : ι → Type u_4
inst✝ : (i : ι) → GeneralizedHeytingAlgebra (α i)
src✝¹ : Lattice ((i : ι) → α i) := lattice
src✝ : OrderTop ((i : ι) → α i) := orderTop
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i ≤ b ⇨ c ↔ i ⊓ b ≤ c
[PROOFSTEP]
simp [le_def]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b
[PROOFSTEP]
rw [sdiff_le_iff, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b ≤ c ↔ a \ c ≤ b
[PROOFSTEP]
rw [sdiff_le_iff, sdiff_le_iff']
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b ≤ b ↔ a ≤ b
[PROOFSTEP]
rw [sdiff_le_iff, sup_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b
[PROOFSTEP]
rw [sup_comm, ← sdiff_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
⊢ b \ a ⊔ a = b ⊔ a
[PROOFSTEP]
rw [sup_comm, sup_sdiff_self, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ⊔ c \ a = c
[PROOFSTEP]
rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : b ≤ a
⊢ a \ b ⊔ b = a
[PROOFSTEP]
rw [sup_comm, sup_sdiff_cancel_right h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b = ⊥ ↔ a ≤ b
[PROOFSTEP]
rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b✝ c d b : α
⊢ a \ ⊥ ≤ b ↔ a ≤ b
[PROOFSTEP]
rw [sdiff_le_iff, bot_sup_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ (a \ c) ≤ c \ b
[PROOFSTEP]
rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self, sup_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a ⊔ (b ⊔ c)
[PROOFSTEP]
exact le_sup_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ b ⊔ (a \ c ⊔ c \ b)
[PROOFSTEP]
simpa using @sdiff_sdiff_sdiff_le_sdiff
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d
[PROOFSTEP]
simp_rw [sdiff_le_iff, sup_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a \ b) \ c = (a \ c) \ b
[PROOFSTEP]
simp_rw [sdiff_sdiff, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ b = a \ b
[PROOFSTEP]
rw [sdiff_sdiff_left, sup_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ a = ⊥
[PROOFSTEP]
rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ (a ⊔ b) \ c ≤ d ↔ a \ c ⊔ b \ c ≤ d
[PROOFSTEP]
simp_rw [sdiff_le_iff, sup_le_iff, sdiff_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a \ (b ⊓ c) ≤ d ↔ a \ b ⊔ a \ c ≤ d
[PROOFSTEP]
rw [sup_le_iff, sdiff_le_comm, le_inf_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d
[PROOFSTEP]
simp_rw [sdiff_le_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a ⊔ b) \ b = a \ b
[PROOFSTEP]
rw [sup_sdiff, sdiff_self, sup_bot_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a ⊔ b) \ a = b \ a
[PROOFSTEP]
rw [sup_comm, sup_sdiff_right_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
⊢ a \ (a ⊓ b) = a \ b
[PROOFSTEP]
rw [sdiff_inf, sdiff_self, bot_sup_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
⊢ b \ (a ⊓ b) = b \ a
[PROOFSTEP]
rw [sdiff_inf, sdiff_self, sup_bot_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
⊢ a \ b = a
[PROOFSTEP]
conv_rhs => rw [← @sdiff_bot _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
| a
[PROOFSTEP]
rw [← @sdiff_bot _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
| a
[PROOFSTEP]
rw [← @sdiff_bot _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
| a
[PROOFSTEP]
rw [← @sdiff_bot _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
⊢ a \ b = a \ ⊥
[PROOFSTEP]
rw [← h.eq_bot, sdiff_inf_self_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
⊢ (a ⊔ b) \ a = b
[PROOFSTEP]
rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
⊢ (a ⊔ b) \ b = a
[PROOFSTEP]
rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a \ c ≤ a \ b ⊔ b \ c
[PROOFSTEP]
rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c
[PROOFSTEP]
exact sdiff_sdiff_le.trans le_sup_sdiff
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : c ⊔ a ≤ c ⊔ b
⊢ a \ c ≤ b \ c
[PROOFSTEP]
rw [← sup_sdiff_left_self, ← @sup_sdiff_left_self _ _ _ b]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : c ⊔ a ≤ c ⊔ b
⊢ (c ⊔ a) \ c ≤ (c ⊔ b) \ c
[PROOFSTEP]
exact sdiff_le_sdiff_right h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : a ⊔ c ≤ b ⊔ c
⊢ a \ c ≤ b \ c
[PROOFSTEP]
rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c
[PROOFSTEP]
exact sdiff_le_sdiff_right h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
src✝ : GeneralizedCoheytingAlgebra α := inst✝
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
[PROOFSTEP]
simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
src✝ : GeneralizedCoheytingAlgebra α := inst✝
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : OrderTop αᵒᵈ := orderTop α
a b c : αᵒᵈ
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
[PROOFSTEP]
rw [inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : OrderTop αᵒᵈ := orderTop α
a b c : αᵒᵈ
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c
[PROOFSTEP]
exact sdiff_le_iff
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : GeneralizedCoheytingAlgebra α✝
a b c d : α✝
α : ι → Type u_4
inst✝ : (i : ι) → GeneralizedCoheytingAlgebra (α i)
src✝¹ : Lattice ((i : ι) → α i) := lattice
src✝ : OrderBot ((i : ι) → α i) := orderBot
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i \ b ≤ c ↔ i ≤ b ⊔ c
[PROOFSTEP]
simp [le_def]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
[PROOFSTEP]
simp_rw [← himp_bot, sup_himp_distrib]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b c a : α
⊢ a ⇨ aᶜ = aᶜ
[PROOFSTEP]
rw [← himp_bot, himp_himp, inf_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ
[PROOFSTEP]
simp_rw [← himp_bot, himp_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a b c : α
⊢ a ≤ bᶜ ↔ Disjoint a b
[PROOFSTEP]
rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a b c : α
⊢ a ≤ bᶜ ↔ b ≤ aᶜ
[PROOFSTEP]
rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b c a : α
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥
[PROOFSTEP]
rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a b c : α
⊢ ⊥ᶜ = ⊤
[PROOFSTEP]
rw [← himp_bot, himp_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a b c : α
⊢ a ≤ aᶜ ↔ a = ⊥
[PROOFSTEP]
rw [le_compl_iff_disjoint_left, disjoint_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α
a b c : α
inst✝ : Nontrivial α
⊢ a ≠ aᶜ
[PROOFSTEP]
intro h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α
a b c : α
inst✝ : Nontrivial α
h : a = aᶜ
⊢ False
[PROOFSTEP]
cases le_compl_self.1 (le_of_eq h)
[GOAL]
case refl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α
b c : α
inst✝ : Nontrivial α
h : ⊥ = ⊥ᶜ
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α
a b c : α
inst✝ : Nontrivial α
⊢ a < aᶜ ↔ a = ⊥
[PROOFSTEP]
rw [lt_iff_le_and_ne]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α
a b c : α
inst✝ : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a b c : α
⊢ Disjoint aᶜᶜ b ↔ Disjoint a b
[PROOFSTEP]
simp_rw [← le_compl_iff_disjoint_left, compl_compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a b c : α
⊢ Disjoint a bᶜᶜ ↔ Disjoint a b
[PROOFSTEP]
simp_rw [← le_compl_iff_disjoint_right, compl_compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ
[PROOFSTEP]
refine' ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ
[PROOFSTEP]
rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff, disjoint_left_comm,
  disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ Disjoint (a ⊓ b) (a ⊓ b)ᶜ
[PROOFSTEP]
exact disjoint_compl_right
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ
[PROOFSTEP]
rw [le_himp_iff, ← compl_compl_inf_distrib]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ
[PROOFSTEP]
exact compl_anti (compl_anti himp_inf_le)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ
[PROOFSTEP]
refine' le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans _)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ (aᶜ ⊔ b)ᶜ ≤ (aᶜᶜ ⇨ bᶜᶜ)ᶜ
[PROOFSTEP]
rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ← le_compl_iff_disjoint_right]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ
[PROOFSTEP]
exact inf_himp_le
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c✝ : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : BoundedOrder αᵒᵈ := boundedOrder α
a b c : αᵒᵈ
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
[PROOFSTEP]
rw [sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ c✝ : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : BoundedOrder αᵒᵈ := boundedOrder α
a b c : αᵒᵈ
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b
[PROOFSTEP]
exact le_himp_iff
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢(a ⊓ b) = ￢a ⊔ ￢b
[PROOFSTEP]
simp_rw [← top_sdiff', sdiff_inf_distrib]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c✝ : α
src✝ : CoheytingAlgebra α := inst✝
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
[PROOFSTEP]
simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c✝ : α
src✝ : CoheytingAlgebra α := inst✝
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b c a : α
⊢ ￢a \ a = ￢a
[PROOFSTEP]
rw [← top_sdiff', sdiff_sdiff, sup_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢a \ b = ￢b \ a
[PROOFSTEP]
simp_rw [← top_sdiff', sdiff_right_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a b c : α
⊢ ￢a ≤ b ↔ Codisjoint a b
[PROOFSTEP]
rw [← top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a b c : α
⊢ ￢a ≤ b ↔ ￢b ≤ a
[PROOFSTEP]
rw [hnot_le_iff_codisjoint_right, hnot_le_iff_codisjoint_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b c a : α
⊢ ￢⊥ ≤ a ↔ ⊤ ≤ a
[PROOFSTEP]
rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a b c : α
⊢ ￢⊤ = ⊥
[PROOFSTEP]
rw [← top_sdiff', sdiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a b c : α
⊢ Codisjoint (￢￢a) b ↔ Codisjoint a b
[PROOFSTEP]
simp_rw [← hnot_le_iff_codisjoint_right, hnot_hnot_hnot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a b c : α
⊢ Codisjoint a (￢￢b) ↔ Codisjoint a b
[PROOFSTEP]
simp_rw [← hnot_le_iff_codisjoint_left, hnot_hnot_hnot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b
[PROOFSTEP]
refine' ((hnot_inf_distrib _ _).ge.trans <| hnot_anti le_hnot_inf_hnot).antisymm' _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b
[PROOFSTEP]
rw [hnot_le_iff_codisjoint_left, codisjoint_assoc, codisjoint_hnot_hnot_left_iff, codisjoint_left_comm,
  codisjoint_hnot_hnot_left_iff, ← codisjoint_assoc, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ Codisjoint (a ⊔ b) (￢(a ⊔ b))
[PROOFSTEP]
exact codisjoint_hnot_right
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢(a \ b) = ￢￢a \ ￢￢b
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b
[PROOFSTEP]
refine' hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' _)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)
[PROOFSTEP]
rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm, ← hnot_le_iff_codisjoint_right]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b
[PROOFSTEP]
exact le_sdiff_sup
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a \ ￢￢b ≤ ￢￢(a \ b)
[PROOFSTEP]
rw [sdiff_le_iff, ← hnot_hnot_sup_distrib]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a ≤ ￢￢(b ⊔ a \ b)
[PROOFSTEP]
exact hnot_anti (hnot_anti le_sup_sdiff)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c✝ : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : BoundedOrder αᵒᵈ := boundedOrder α
a b c : αᵒᵈ
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
[PROOFSTEP]
rw [inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : CoheytingAlgebra α
a✝ b✝ c✝ : α
src✝¹ : Lattice αᵒᵈ := lattice α
src✝ : BoundedOrder αᵒᵈ := boundedOrder α
a b c : αᵒᵈ
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c
[PROOFSTEP]
exact sdiff_le_iff
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
[PROOFSTEP]
change _ ≤ ite _ _ _ ↔ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
⊢ (a ≤ if b ≤ c then ⊤ else c) ↔ a ⊓ b ≤ c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
h : b ≤ c
⊢ a ≤ ⊤ ↔ a ⊓ b ≤ c
[PROOFSTEP]
exact iff_of_true le_top (inf_le_of_right_le h)
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ a ⊓ b ≤ c
[PROOFSTEP]
rw [inf_le_iff, or_iff_left h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
[PROOFSTEP]
change ite _ _ _ ≤ _ ↔ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
⊢ (if a ≤ b then ⊥ else a) ≤ c ↔ a ≤ b ⊔ c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
h : a ≤ b
⊢ ⊥ ≤ c ↔ a ≤ b ⊔ c
[PROOFSTEP]
exact iff_of_true bot_le (le_sup_of_le_left h)
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
src✝¹ : Lattice α := toLattice
src✝ : BoundedOrder α := inst✝
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ b ⊔ c
[PROOFSTEP]
rw [le_sup_iff, or_iff_right h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Top α := inst✝²
src✝ : HImp α := inst✝¹
a : α
⊢ a ≤ ⊤
[PROOFSTEP]
change f _ ≤ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Top α := inst✝²
src✝ : HImp α := inst✝¹
a : α
⊢ f a ≤ f ⊤
[PROOFSTEP]
rw [map_top]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Top α := inst✝²
src✝ : HImp α := inst✝¹
a : α
⊢ f a ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Top α := inst✝²
src✝ : HImp α := inst✝¹
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
[PROOFSTEP]
change f _ ≤ _ ↔ f _ ≤ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Top α := inst✝²
src✝ : HImp α := inst✝¹
a b c : α
⊢ f a ≤ f (b ⇨ c) ↔ f (a ⊓ b) ≤ f c
[PROOFSTEP]
erw [map_himp, map_inf, le_himp_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Bot α := inst✝²
src✝ : SDiff α := inst✝¹
a : α
⊢ ⊥ ≤ a
[PROOFSTEP]
change f _ ≤ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Bot α := inst✝²
src✝ : SDiff α := inst✝¹
a : α
⊢ f ⊥ ≤ f a
[PROOFSTEP]
rw [map_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Bot α := inst✝²
src✝ : SDiff α := inst✝¹
a : α
⊢ ⊥ ≤ f a
[PROOFSTEP]
exact bot_le
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Bot α := inst✝²
src✝ : SDiff α := inst✝¹
a b c : α
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
[PROOFSTEP]
change f _ ≤ _ ↔ f _ ≤ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : Lattice α := Injective.lattice f hf map_sup map_inf
src✝¹ : Bot α := inst✝²
src✝ : SDiff α := inst✝¹
a b c : α
⊢ f (a \ b) ≤ f c ↔ f a ≤ f (b ⊔ c)
[PROOFSTEP]
erw [map_sdiff, map_sup, sdiff_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : GeneralizedHeytingAlgebra α := Injective.generalizedHeytingAlgebra f hf map_sup map_inf map_top map_himp
src✝¹ : Bot α := inst✝³
src✝ : HasCompl α := inst✝²
a : α
⊢ ⊥ ≤ a
[PROOFSTEP]
change f _ ≤ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : GeneralizedHeytingAlgebra α := Injective.generalizedHeytingAlgebra f hf map_sup map_inf map_top map_himp
src✝¹ : Bot α := inst✝³
src✝ : HasCompl α := inst✝²
a : α
⊢ f ⊥ ≤ f a
[PROOFSTEP]
rw [map_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : GeneralizedHeytingAlgebra α := Injective.generalizedHeytingAlgebra f hf map_sup map_inf map_top map_himp
src✝¹ : Bot α := inst✝³
src✝ : HasCompl α := inst✝²
a : α
⊢ ⊥ ≤ f a
[PROOFSTEP]
exact bot_le
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
src✝² : GeneralizedHeytingAlgebra α := Injective.generalizedHeytingAlgebra f hf map_sup map_inf map_top map_himp
src✝¹ : Bot α := inst✝³
src✝ : HasCompl α := inst✝²
a : α
⊢ f (a ⇨ ⊥) = f aᶜ
[PROOFSTEP]
erw [map_himp, map_compl, map_bot, himp_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : GeneralizedCoheytingAlgebra α := Injective.generalizedCoheytingAlgebra f hf map_sup map_inf map_bot map_sdiff
src✝¹ : Top α := inst✝⁴
src✝ : HNot α := inst✝²
a : α
⊢ a ≤ ⊤
[PROOFSTEP]
change f _ ≤ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : GeneralizedCoheytingAlgebra α := Injective.generalizedCoheytingAlgebra f hf map_sup map_inf map_bot map_sdiff
src✝¹ : Top α := inst✝⁴
src✝ : HNot α := inst✝²
a : α
⊢ f a ≤ f ⊤
[PROOFSTEP]
rw [map_top]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : GeneralizedCoheytingAlgebra α := Injective.generalizedCoheytingAlgebra f hf map_sup map_inf map_bot map_sdiff
src✝¹ : Top α := inst✝⁴
src✝ : HNot α := inst✝²
a : α
⊢ f a ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CoheytingAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝² : GeneralizedCoheytingAlgebra α := Injective.generalizedCoheytingAlgebra f hf map_sup map_inf map_bot map_sdiff
src✝¹ : Top α := inst✝⁴
src✝ : HNot α := inst✝²
a : α
⊢ f (⊤ \ a) = f (￢a)
[PROOFSTEP]
erw [map_sdiff, map_hnot, map_top, top_sdiff']