awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hac : c ≤ a
hbc : c ≤ b
h : a \ c = b \ c
rw : a \ c ⊔ c = b
rw₁ : b \ c ⊔ c = b
⊢ a = b
have rw₂ : b = b
Tactic: rw [← sdiff_sup_cancel hac, h, sdiff_sup_cancel hbc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b = ⊥ ↔ a ≤ b
have rw : a \ b ≤ ⊥ ↔ a ≤ b
Tactic: rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ b ≤ ⊥ ↔ a ≤ b
⊢ a \ b = ⊥ ↔ a ≤ b
have rw₁ : a ≤ b ⊔ ⊥ ↔ a ≤ b
Tactic: rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ b ≤ ⊥ ↔ a ≤ b
rw₁ : a ≤ b ⊔ ⊥ ↔ a ≤ b
⊢ a \ b = ⊥ ↔ a ≤ b
have rw₂ : a ≤ b ↔ a ≤ b
Tactic: rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ ⊥ ≤ b ↔ a ≤ b
have rw : a ≤ ⊥ ⊔ b ↔ a ≤ b
Tactic: rw [sdiff_le_iff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ≤ ⊥ ⊔ b ↔ a ≤ b
⊢ a \ ⊥ ≤ b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [sdiff_le_iff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ (a \ b) \ (a \ c) ≤ c \ b
have rw : a ≤ a ⊔ (b ⊔ c)
Tactic: rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self,
    sup_left_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d
have simp_rw : a ≤ b ⊔ (c ⊔ d) ↔ a ≤ b ⊔ c ⊔ d
Tactic: simp_rw [sdiff_le_iff, sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ (a \ b) \ c = (a \ c) \ b
have simp_rw : a \ (b ⊔ c) = a \ (c ⊔ b)
Tactic: simp_rw [sdiff_sdiff, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) \ b = a \ b
have rw : a \ (b ⊔ b) = a \ b
Tactic: rw [sdiff_sdiff_left, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ (b ⊔ b) = a \ b
⊢ (a \ b) \ b = a \ b
have rw₁ : a \ b = a \ b
Tactic: rw [sdiff_sdiff_left, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) \ a = ⊥
have rw : (a \ a) \ b = ⊥
Tactic: rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (a \ a) \ b = ⊥
⊢ (a \ b) \ a = ⊥
have rw₁ : ⊥ \ b = ⊥
Tactic: rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (a \ a) \ b = ⊥
rw₁ : ⊥ \ b = ⊥
⊢ (a \ b) \ a = ⊥
have rw₂ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
Tactic: rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a ⊔ b) \ c ≤ d ↔ a \ c ⊔ b \ c ≤ d
have simp_rw : a ⊔ b ≤ c ⊔ d ↔ a \ c ⊔ b \ c ≤ d
Tactic: simp_rw [sdiff_le_iff, sup_le_iff, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
simp_rw : a ⊔ b ≤ c ⊔ d ↔ a \ c ⊔ b \ c ≤ d
⊢ (a ⊔ b) \ c ≤ d ↔ a \ c ⊔ b \ c ≤ d
have simp_rw₁ : a ≤ c ⊔ d ∧ b ≤ c ⊔ d ↔ a \ c ≤ d ∧ b \ c ≤ d
Tactic: simp_rw [sdiff_le_iff, sup_le_iff, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b ⊓ c) ≤ d ↔ a \ b ⊔ a \ c ≤ d
have rw : a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d
Tactic: rw [sup_le_iff, sdiff_le_comm, le_inf_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊔ b) \ b = a \ b
have rw : a \ b ⊔ b \ b = a \ b
Tactic: rw [sup_sdiff, sdiff_self, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ b ⊔ b \ b = a \ b
⊢ (a ⊔ b) \ b = a \ b
have rw₁ : a \ b ⊔ ⊥ = a \ b
Tactic: rw [sup_sdiff, sdiff_self, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ b ⊔ b \ b = a \ b
rw₁ : a \ b ⊔ ⊥ = a \ b
⊢ (a ⊔ b) \ b = a \ b
have rw₂ : a \ b = a \ b
Tactic: rw [sup_sdiff, sdiff_self, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊔ b) \ a = b \ a
have rw : (b ⊔ a) \ a = b \ a
Tactic: rw [sup_comm, sup_sdiff_right_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (b ⊔ a) \ a = b \ a
⊢ (a ⊔ b) \ a = b \ a
have rw₁ : b \ a = b \ a
Tactic: rw [sup_comm, sup_sdiff_right_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (a ⊓ b) = a \ b
have rw : a \ a ⊔ a \ b = a \ b
Tactic: rw [sdiff_inf, sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ a ⊔ a \ b = a \ b
⊢ a \ (a ⊓ b) = a \ b
have rw₁ : ⊥ ⊔ a \ b = a \ b
Tactic: rw [sdiff_inf, sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ a ⊔ a \ b = a \ b
rw₁ : ⊥ ⊔ a \ b = a \ b
⊢ a \ (a ⊓ b) = a \ b
have rw₂ : a \ b = a \ b
Tactic: rw [sdiff_inf, sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ b \ (a ⊓ b) = b \ a
have rw : b \ a ⊔ b \ b = b \ a
Tactic: rw [sdiff_inf, sdiff_self, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : b \ a ⊔ b \ b = b \ a
⊢ b \ (a ⊓ b) = b \ a
have rw₁ : b \ a ⊔ ⊥ = b \ a
Tactic: rw [sdiff_inf, sdiff_self, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : b \ a ⊔ b \ b = b \ a
rw₁ : b \ a ⊔ ⊥ = b \ a
⊢ b \ (a ⊓ b) = b \ a
have rw₂ : b \ a = b \ a
Tactic: rw [sdiff_inf, sdiff_self, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
| a
have rw : a \ ⊥
Tactic: rw [← @sdiff_bot _ _ a]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a \ b = a
have conv_rhs : a \ b = a \ ⊥
Tactic: conv_rhs => rw [← @sdiff_bot _ _ a]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a \ b = a \ ⊥
have rw : a \ b = a \ (a ⊓ b)
Tactic: rw [← h.eq_bot, sdiff_inf_self_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b = a \ (a ⊓ b)
⊢ a \ b = a \ ⊥
have rw₁ : a \ b = a \ b
Tactic: rw [← h.eq_bot, sdiff_inf_self_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ (a ⊔ b) \ a = b
have rw : a \ a ⊔ b \ a = b
Tactic: rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ a ⊔ b \ a = b
⊢ (a ⊔ b) \ a = b
have rw₁ : ⊥ ⊔ b \ a = b
Tactic: rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ a ⊔ b \ a = b
rw₁ : ⊥ ⊔ b \ a = b
⊢ (a ⊔ b) \ a = b
have rw₂ : b \ a = b
Tactic: rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ a ⊔ b \ a = b
rw₁ : ⊥ ⊔ b \ a = b
rw₂ : b \ a = b
⊢ (a ⊔ b) \ a = b
have rw₃ : b = b
Tactic: rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ (a ⊔ b) \ b = a
have rw : a \ b ⊔ b \ b = a
Tactic: rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b ⊔ b \ b = a
⊢ (a ⊔ b) \ b = a
have rw₁ : a \ b ⊔ ⊥ = a
Tactic: rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b ⊔ b \ b = a
rw₁ : a \ b ⊔ ⊥ = a
⊢ (a ⊔ b) \ b = a
have rw₂ : a \ b = a
Tactic: rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b ⊔ b \ b = a
rw₁ : a \ b ⊔ ⊥ = a
rw₂ : a \ b = a
⊢ (a ⊔ b) \ b = a
have rw₃ : a = a
Tactic: rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ c ≤ a \ b ⊔ b \ c
have rw : a \ (a \ b) ≤ c ⊔ b \ c
Tactic: rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ a \ b ⊔ b \ c = a \ c
have refine : a \ b ≤ a \ c
Tactic: refine (sdiff_triangle ..).antisymm' <| sup_le ?_ <| by simpa [sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ a \ b ≤ a \ c
have rw : a \ b ≤ a \ (a ⊓ c)
Tactic: rw [← sdiff_inf_self_left (b := c)]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ a \ c ≤ b \ c
have rw : (c ⊔ a) \ c ≤ (c ⊔ b) \ c
Tactic: rw [← sup_sdiff_left_self, ← @sup_sdiff_left_self _ _ _ b]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ a \ c ≤ b \ c
have rw : (a ⊔ c) \ c ≤ (b ⊔ c) \ c
Tactic: rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α
a_1 b_1 c_1 d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have simp_rw : (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
Tactic: simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α
a_1 b_1 c_1 d : α
a b c : αᵒᵈ
⊢ a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ a ⊓ b ≤ c
have rw : a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ b ⊓ a ≤ c
Tactic: rw [inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
have simp_rw : a ⊔ b ⇨ ⊥ = (a ⇨ ⊥) ⊓ (b ⇨ ⊥)
Tactic: simp_rw [← himp_bot, sup_himp_distrib]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ⇨ aᶜ = aᶜ
have rw : a ⇨ a ⇨ ⊥ = a ⇨ ⊥
Tactic: rw [← himp_bot, himp_himp, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : a ⇨ a ⇨ ⊥ = a ⇨ ⊥
⊢ a ⇨ aᶜ = aᶜ
have rw₁ : a ⊓ a ⇨ ⊥ = a ⇨ ⊥
Tactic: rw [← himp_bot, himp_himp, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : a ⇨ a ⇨ ⊥ = a ⇨ ⊥
rw₁ : a ⊓ a ⇨ ⊥ = a ⇨ ⊥
⊢ a ⇨ aᶜ = aᶜ
have rw₂ : a ⇨ ⊥ = a ⇨ ⊥
Tactic: rw [← himp_bot, himp_himp, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ
have simp_rw : a ⇨ b ⇨ ⊥ = b ⇨ a ⇨ ⊥
Tactic: simp_rw [← himp_bot, himp_left_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ Disjoint a b
have rw : a ≤ b ⇨ ⊥ ↔ Disjoint a b
Tactic: rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
rw : a ≤ b ⇨ ⊥ ↔ Disjoint a b
⊢ a ≤ bᶜ ↔ Disjoint a b
have rw₁ : a ⊓ b ≤ ⊥ ↔ Disjoint a b
Tactic: rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
rw : a ≤ b ⇨ ⊥ ↔ Disjoint a b
rw₁ : a ⊓ b ≤ ⊥ ↔ Disjoint a b
⊢ a ≤ bᶜ ↔ Disjoint a b
have rw₂ : a ⊓ b ≤ ⊥ ↔ a ⊓ b ≤ ⊥
Tactic: rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ b ≤ aᶜ
have rw : Disjoint a b ↔ b ≤ aᶜ
Tactic: rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
rw : Disjoint a b ↔ b ≤ aᶜ
⊢ a ≤ bᶜ ↔ b ≤ aᶜ
have rw₁ : Disjoint a b ↔ Disjoint a b
Tactic: rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥
have rw : Disjoint a ⊤ ↔ a ≤ ⊥
Tactic: rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : Disjoint a ⊤ ↔ a ≤ ⊥
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥
have rw₁ : a = ⊥ ↔ a ≤ ⊥
Tactic: rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : Disjoint a ⊤ ↔ a ≤ ⊥
rw₁ : a = ⊥ ↔ a ≤ ⊥
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥
have rw₂ : a = ⊥ ↔ a = ⊥
Tactic: rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
⊢ Eq.{u_2 + 1} (α := α) ⊥ᶜ ⊤
have rw : Eq.{u_2 + 1} (α := α) (⊥ ⇨ ⊥) ⊤
Tactic: rw [← himp_bot, himp_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
rw : Eq.{u_2 + 1} (α := α) (⊥ ⇨ ⊥) ⊤
⊢ Eq.{u_2 + 1} (α := α) ⊥ᶜ ⊤
have rw₁ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
Tactic: rw [← himp_bot, himp_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ≤ aᶜ ↔ a = ⊥
have rw : Disjoint a a ↔ a = ⊥
Tactic: rw [le_compl_iff_disjoint_left, disjoint_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : Disjoint a a ↔ a = ⊥
⊢ a ≤ aᶜ ↔ a = ⊥
have rw₁ : a = ⊥ ↔ a = ⊥
Tactic: rw [le_compl_iff_disjoint_left, disjoint_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (hypothesis)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
inst_1 : Nontrivial α
h : a = aᶜ
⊢ False
have h₁ : Eq.{u_2 + 1} (α := α) ⊥ ⊥ᶜ
Tactic: cases le_compl_self.1 (le_of_eq h)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
inst_1 : Nontrivial α
⊢ a < aᶜ ↔ a = ⊥
have rw : a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥
Tactic: rw [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ Disjoint aᶜᶜ b ↔ Disjoint a b
have simp_rw : b ≤ aᶜᶜᶜ ↔ b ≤ aᶜ
Tactic: simp_rw [← le_compl_iff_disjoint_left, compl_compl_compl]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ Disjoint a bᶜᶜ ↔ Disjoint a b
have simp_rw : a ≤ bᶜᶜᶜ ↔ a ≤ bᶜ
Tactic: simp_rw [← le_compl_iff_disjoint_right, compl_compl_compl]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ
have refine : aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ
Tactic: refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ
have rw : Disjoint (a ⊓ b) (a ⊓ b)ᶜ
Tactic: 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]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
have a₁ : (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
a₁ : (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ
⊢ (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
have a₂ : aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ
have a₁ : ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ
Tactic: rw [le_himp_iff, ← compl_compl_inf_distrib]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ
have a₁ : (aᶜ ⊔ b)ᶜ ≤ (aᶜᶜ ⇨ bᶜᶜ)ᶜ
Tactic: refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ (aᶜ ⊔ b)ᶜ ≤ (aᶜᶜ ⇨ bᶜᶜ)ᶜ
have a₁ : aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ
Tactic: rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ←
      le_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ b ⊔ c
have rw : (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢(a ⊓ b) = ￢a ⊔ ￢b
have simp_rw : ⊤ \ (a ⊓ b) = ⊤ \ a ⊔ ⊤ \ b
Tactic: simp_rw [← top_sdiff', sdiff_inf_distrib]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
a_1 b_1 a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have simp_rw : (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
Tactic: simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ￢a \ a = ￢a
have rw : (⊤ \ a) \ a = ⊤ \ a
Tactic: rw [← top_sdiff', sdiff_sdiff, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : (⊤ \ a) \ a = ⊤ \ a
⊢ ￢a \ a = ￢a
have rw₁ : ⊤ \ (a ⊔ a) = ⊤ \ a
Tactic: rw [← top_sdiff', sdiff_sdiff, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : (⊤ \ a) \ a = ⊤ \ a
rw₁ : ⊤ \ (a ⊔ a) = ⊤ \ a
⊢ ￢a \ a = ￢a
have rw₂ : ⊤ \ a = ⊤ \ a
Tactic: rw [← top_sdiff', sdiff_sdiff, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢a \ b = ￢b \ a
have simp_rw : (⊤ \ a) \ b = (⊤ \ b) \ a
Tactic: simp_rw [← top_sdiff', sdiff_right_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ b ↔ Codisjoint a b
have rw : ⊤ \ a ≤ b ↔ Codisjoint a b
Tactic: rw [← top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
rw : ⊤ \ a ≤ b ↔ Codisjoint a b
⊢ ￢a ≤ b ↔ Codisjoint a b
have rw₁ : ⊤ ≤ a ⊔ b ↔ Codisjoint a b
Tactic: rw [← top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
rw : ⊤ \ a ≤ b ↔ Codisjoint a b
rw₁ : ⊤ ≤ a ⊔ b ↔ Codisjoint a b
⊢ ￢a ≤ b ↔ Codisjoint a b
have rw₂ : ⊤ ≤ a ⊔ b ↔ ⊤ ≤ a ⊔ b
Tactic: rw [← top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ b ↔ ￢b ≤ a
have rw : Codisjoint a b ↔ ￢b ≤ a
Tactic: rw [hnot_le_iff_codisjoint_right, hnot_le_iff_codisjoint_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
rw : Codisjoint a b ↔ ￢b ≤ a
⊢ ￢a ≤ b ↔ ￢b ≤ a
have rw₁ : Codisjoint a b ↔ Codisjoint a b
Tactic: rw [hnot_le_iff_codisjoint_right, hnot_le_iff_codisjoint_left]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ￢⊥ ≤ a ↔ ⊤ ≤ a
have rw : Codisjoint a ⊥ ↔ ⊤ ≤ a
Tactic: rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : Codisjoint a ⊥ ↔ ⊤ ≤ a
⊢ ￢⊥ ≤ a ↔ ⊤ ≤ a
have rw₁ : a = ⊤ ↔ ⊤ ≤ a
Tactic: rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : Codisjoint a ⊥ ↔ ⊤ ≤ a
rw₁ : a = ⊤ ↔ ⊤ ≤ a
⊢ ￢⊥ ≤ a ↔ ⊤ ≤ a
have rw₂ : a = ⊤ ↔ a = ⊤
Tactic: rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
⊢ Eq.{u_2 + 1} (α := α) (￢⊤) ⊥
have rw : Eq.{u_2 + 1} (α := α) (⊤ \ ⊤) ⊥
Tactic: rw [← top_sdiff', sdiff_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
rw : Eq.{u_2 + 1} (α := α) (⊤ \ ⊤) ⊥
⊢ Eq.{u_2 + 1} (α := α) (￢⊤) ⊥
have rw₁ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
Tactic: rw [← top_sdiff', sdiff_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢￢a) b ↔ Codisjoint a b
have simp_rw : ￢￢￢a ≤ b ↔ ￢a ≤ b
Tactic: simp_rw [← hnot_le_iff_codisjoint_right, hnot_hnot_hnot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢￢b) ↔ Codisjoint a b
have simp_rw : ￢￢￢b ≤ a ↔ ￢b ≤ a
Tactic: simp_rw [← hnot_le_iff_codisjoint_left, hnot_hnot_hnot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b
have refine : ￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b
Tactic: refine ((hnot_inf_distrib _ _).ge.trans <| hnot_anti le_hnot_inf_hnot).antisymm' ?_