awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b c : α
rw : a ≤ c ⊔ bᶜ ↔ a ⊓ b ≤ c
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
have rw₁ : a ⊓ b ≤ c ↔ a ⊓ b ≤ c
Tactic: rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a : α
⊢ ⊤ \ a = aᶜ
have rw : ⊤ ⊓ aᶜ = aᶜ
Tactic: rw [sdiff_eq, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a : α
rw : ⊤ ⊓ aᶜ = aᶜ
⊢ ⊤ \ a = aᶜ
have rw₁ : aᶜ = aᶜ
Tactic: rw [sdiff_eq, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl x y
have rw : IsCompl yᶜ y
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x y
have rw : IsCompl x xᶜ
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ xᶜ = y ↔ yᶜ = x
have rw : y = xᶜ ↔ yᶜ = x
Tactic: rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : y = xᶜ ↔ yᶜ = x
⊢ xᶜ = y ↔ yᶜ = x
have rw₁ : y = xᶜ ↔ IsCompl y x
Tactic: rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : y = xᶜ ↔ yᶜ = x
rw₁ : y = xᶜ ↔ IsCompl y x
⊢ xᶜ = y ↔ yᶜ = x
have rw₂ : IsCompl y x ↔ IsCompl y x
Tactic: rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x = yᶜ ↔ y = xᶜ
have rw : yᶜ = x ↔ y = xᶜ
Tactic: rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : yᶜ = x ↔ y = xᶜ
⊢ x = yᶜ ↔ y = xᶜ
have rw₁ : IsCompl y x ↔ y = xᶜ
Tactic: rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : yᶜ = x ↔ y = xᶜ
rw₁ : IsCompl y x ↔ y = xᶜ
⊢ x = yᶜ ↔ y = xᶜ
have rw₂ : IsCompl y x ↔ IsCompl y x
Tactic: rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : yᶜ ≤ xᶜ
⊢ x ≤ y
have h₁ : xᶜᶜ ≤ yᶜᶜ
Tactic: have h := compl_le_compl h
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x \ yᶜ = x ⊓ y
have rw : x ⊓ yᶜᶜ = x ⊓ y
Tactic: rw [sdiff_eq, compl_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : x ⊓ yᶜᶜ = x ⊓ y
⊢ x \ yᶜ = x ⊓ y
have rw₁ : x ⊓ y = x ⊓ y
Tactic: rw [sdiff_eq, compl_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x ⊓ y ⊔ x ⊓ yᶜ = x
have rw : x ⊓ y ⊔ x \ y = x
Tactic: rw [← sdiff_eq, sup_inf_sdiff _ _]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : x ⊓ y ⊔ x \ y = x
⊢ x ⊓ y ⊔ x ⊓ yᶜ = x
have rw₁ : x = x
Tactic: rw [← sdiff_eq, sup_inf_sdiff _ _]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ (x \ y)ᶜ = x ⇨ y
have rw : (x ⊓ yᶜ)ᶜ = x ⇨ y
Tactic: rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : (x ⊓ yᶜ)ᶜ = x ⇨ y
⊢ (x \ y)ᶜ = x ⇨ y
have rw₁ : (x ⊓ yᶜ)ᶜ = y ⊔ xᶜ
Tactic: rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : (x ⊓ yᶜ)ᶜ = x ⇨ y
rw₁ : (x ⊓ yᶜ)ᶜ = y ⊔ xᶜ
⊢ (x \ y)ᶜ = x ⇨ y
have rw₂ : xᶜ ⊔ yᶜᶜ = y ⊔ xᶜ
Tactic: rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : (x ⊓ yᶜ)ᶜ = x ⇨ y
rw₁ : (x ⊓ yᶜ)ᶜ = y ⊔ xᶜ
rw₂ : xᶜ ⊔ yᶜᶜ = y ⊔ xᶜ
⊢ (x \ y)ᶜ = x ⇨ y
have rw₃ : xᶜ ⊔ y = y ⊔ xᶜ
Tactic: rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : (x ⊓ yᶜ)ᶜ = x ⇨ y
rw₁ : (x ⊓ yᶜ)ᶜ = y ⊔ xᶜ
rw₂ : xᶜ ⊔ yᶜᶜ = y ⊔ xᶜ
rw₃ : xᶜ ⊔ y = y ⊔ xᶜ
⊢ (x \ y)ᶜ = x ⇨ y
have rw₄ : y ⊔ xᶜ = y ⊔ xᶜ
Tactic: rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ xᶜ \ yᶜ = y \ x
have rw : xᶜ ⊓ y = y \ x
Tactic: rw [sdiff_compl, sdiff_eq, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : xᶜ ⊓ y = y \ x
⊢ xᶜ \ yᶜ = y \ x
have rw₁ : xᶜ ⊓ y = y ⊓ xᶜ
Tactic: rw [sdiff_compl, sdiff_eq, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : xᶜ ⊓ y = y \ x
rw₁ : xᶜ ⊓ y = y ⊓ xᶜ
⊢ xᶜ \ yᶜ = y \ x
have rw₂ : y ⊓ xᶜ = y ⊓ xᶜ
Tactic: rw [sdiff_compl, sdiff_eq, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ Disjoint xᶜ y ↔ y ≤ x
have rw : y ≤ xᶜᶜ ↔ y ≤ x
Tactic: rw [← le_compl_iff_disjoint_left, compl_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : y ≤ xᶜᶜ ↔ y ≤ x
⊢ Disjoint xᶜ y ↔ y ≤ x
have rw₁ : y ≤ x ↔ y ≤ x
Tactic: rw [← le_compl_iff_disjoint_left, compl_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ Disjoint x yᶜ ↔ x ≤ y
have rw : x ≤ yᶜᶜ ↔ x ≤ y
Tactic: rw [← le_compl_iff_disjoint_right, compl_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : x ≤ yᶜᶜ ↔ x ≤ y
⊢ Disjoint x yᶜ ↔ x ≤ y
have rw₁ : x ≤ y ↔ x ≤ y
Tactic: rw [← le_compl_iff_disjoint_right, compl_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : BooleanAlgebra α
⊢ x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z
have rw : y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)
Tactic: rw [himp_eq, sup_le_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤
have rw : x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤
Tactic: rw [codisjoint_himp_self_left.eq_iff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
⊢ x ⊓ xᶜ ≤ ⊥
have left : (x ⊓ xᶜ).fst ≤ fst.{u, u_1} (β := β) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
left : (x ⊓ xᶜ).fst ≤ fst.{u, u_1} (β := β) ⊥
⊢ x ⊓ xᶜ ≤ ⊥
have right : (x ⊓ xᶜ).snd ≤ snd.{u, u_1} (α := α) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
⊢ ⊤ ≤ x ⊔ xᶜ
have left : fst.{u, u_1} (β := β) ⊤ ≤ (x ⊔ xᶜ).fst
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
left : fst.{u, u_1} (β := β) ⊤ ≤ (x ⊔ xᶜ).fst
⊢ ⊤ ≤ x ⊔ xᶜ
have right : snd.{u, u_1} (α := α) ⊤ ≤ (x ⊔ xᶜ).snd
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
⊢ x \ y = x ⊓ yᶜ
have fst : (x \ y).fst = (x ⊓ yᶜ).fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
fst : (x \ y).fst = (x ⊓ yᶜ).fst
⊢ x \ y = x ⊓ yᶜ
have snd : (x \ y).snd = (x ⊓ yᶜ).snd
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
⊢ x ⇨ y = y ⊔ xᶜ
have fst : (x ⇨ y).fst = (y ⊔ xᶜ).fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
fst : (x ⇨ y).fst = (y ⊔ xᶜ).fst
⊢ x ⇨ y = y ⊔ xᶜ
have snd : (x ⇨ y).snd = (y ⊔ xᶜ).snd
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
⊢ f (a ⊓ b ⊔ a \ b) = f a
have rw : f (a ⊓ b) ⊔ f (a \ b) = f a
Tactic: rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
rw : f (a ⊓ b) ⊔ f (a \ b) = f a
⊢ f (a ⊓ b ⊔ a \ b) = f a
have rw₁ : f (a ⊓ b) ⊔ f a \ f b = f a
Tactic: rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
rw : f (a ⊓ b) ⊔ f (a \ b) = f a
rw₁ : f (a ⊓ b) ⊔ f a \ f b = f a
⊢ f (a ⊓ b ⊔ a \ b) = f a
have rw₂ : f a ⊓ f b ⊔ f a \ f b = f a
Tactic: rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
rw : f (a ⊓ b) ⊔ f (a \ b) = f a
rw₁ : f (a ⊓ b) ⊔ f a \ f b = f a
rw₂ : f a ⊓ f b ⊔ f a \ f b = f a
⊢ f (a ⊓ b ⊔ a \ b) = f a
have rw₃ : f a = f a
Tactic: rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥
have rw : f (a ⊓ b) ⊓ f (a \ b) = f ⊥
Tactic: rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
rw : f (a ⊓ b) ⊓ f (a \ b) = f ⊥
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥
have rw₁ : f (a ⊓ b) ⊓ f a \ f b = f ⊥
Tactic: rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
rw : f (a ⊓ b) ⊓ f (a \ b) = f ⊥
rw₁ : f (a ⊓ b) ⊓ f a \ f b = f ⊥
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥
have rw₂ : f a ⊓ f b ⊓ f a \ f b = f ⊥
Tactic: rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
rw : f (a ⊓ b) ⊓ f (a \ b) = f ⊥
rw₁ : f (a ⊓ b) ⊓ f a \ f b = f ⊥
rw₂ : f a ⊓ f b ⊓ f a \ f b = f ⊥
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥
have rw₃ : ⊥ = f ⊥
Tactic: rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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
a b : α
rw : f (a ⊓ b) ⊓ f (a \ b) = f ⊥
rw₁ : f (a ⊓ b) ⊓ f a \ f b = f ⊥
rw₂ : f a ⊓ f b ⊓ f a \ f b = f ⊥
rw₃ : ⊥ = f ⊥
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥
have rw₄ : Eq.{u_1 + 1} (α := β) ⊥ ⊥
Tactic: rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ⊓ f aᶜ = f ⊥
have rw : f a ⊓ (f a)ᶜ = f ⊥
Tactic: rw [map_compl, inf_compl_eq_bot, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⊓ (f a)ᶜ = f ⊥
⊢ f a ⊓ f aᶜ = f ⊥
have rw₁ : ⊥ = f ⊥
Tactic: rw [map_compl, inf_compl_eq_bot, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⊓ (f a)ᶜ = f ⊥
rw₁ : ⊥ = f ⊥
⊢ f a ⊓ f aᶜ = f ⊥
have rw₂ : Eq.{u_1 + 1} (α := β) ⊥ ⊥
Tactic: rw [map_compl, inf_compl_eq_bot, map_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ⊔ f aᶜ = f ⊤
have rw : f a ⊔ (f a)ᶜ = f ⊤
Tactic: rw [map_compl, sup_compl_eq_top, map_top]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⊔ (f a)ᶜ = f ⊤
⊢ f a ⊔ f aᶜ = f ⊤
have rw₁ : ⊤ = f ⊤
Tactic: rw [map_compl, sup_compl_eq_top, map_top]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⊔ (f a)ᶜ = f ⊤
rw₁ : ⊤ = f ⊤
⊢ f a ⊔ f aᶜ = f ⊤
have rw₂ : Eq.{u_1 + 1} (α := β) ⊤ ⊤
Tactic: rw [map_compl, sup_compl_eq_top, map_top]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f a ⊓ (f b)ᶜ = f (a ⊓ bᶜ)
have rw : f a ⊓ (f b)ᶜ = f a ⊓ f bᶜ
Tactic: rw [map_inf, map_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
rw : f a ⊓ (f b)ᶜ = f a ⊓ f bᶜ
⊢ f a ⊓ (f b)ᶜ = f (a ⊓ bᶜ)
have rw₁ : f a ⊓ (f b)ᶜ = f a ⊓ (f b)ᶜ
Tactic: rw [map_inf, map_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f b ⊔ (f a)ᶜ = f (b ⊔ aᶜ)
have rw : f b ⊔ (f a)ᶜ = f b ⊔ f aᶜ
Tactic: rw [map_sup, map_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
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_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
rw : f b ⊔ (f a)ᶜ = f b ⊔ f aᶜ
⊢ f b ⊔ (f a)ᶜ = f (b ⊔ aᶜ)
have rw₁ : f b ⊔ (f a)ᶜ = f b ⊔ (f a)ᶜ
Tactic: rw [map_sup, map_compl]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
⊢ GeneralizedBooleanAlgebra α
have le : ∀ {x y : α}, LE.le.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.generalizedBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
le : ∀ {x y : α}, LE.le.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ GeneralizedBooleanAlgebra α
have lt : ∀ {x y : α}, LT.lt.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.generalizedBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
le : ∀ {x y : α}, LE.le.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ GeneralizedBooleanAlgebra α
have map_sup : ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.generalizedBooleanAlgebra