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 : α
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ GeneralizedBooleanAlgebra α
have map_inf : ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ GeneralizedBooleanAlgebra α
have map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ GeneralizedBooleanAlgebra α
have map_sdiff : ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
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 : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ BooleanAlgebra α
have le : ∀ {x y : α}, LE.le.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
le : ∀ {x y : α}, LE.le.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ BooleanAlgebra α
have lt : ∀ {x y : α}, LT.lt.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
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
⊢ BooleanAlgebra α
have map_sup : ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ BooleanAlgebra α
have map_inf : ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ BooleanAlgebra α
have map_top : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ BooleanAlgebra α
have map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ BooleanAlgebra α
have map_compl : ∀ (a : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
⊢ BooleanAlgebra α
have map_sdiff : ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
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
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_sdiff :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
⊢ BooleanAlgebra α
have map_himp : ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
Tactic: apply e.injective.booleanAlgebra
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s : Set α
⊢ sᶜ ∪ s = univ
have rw : s ∪ sᶜ = univ
Tactic: rw [union_comm, union_compl_self]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s : Set α
rw : s ∪ sᶜ = univ
⊢ sᶜ ∪ s = univ
have rw₁ : Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [union_comm, union_compl_self]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
⊢ s \ t = tᶜ ∩ s
have rw : s ∩ tᶜ = tᶜ ∩ s
Tactic: rw [diff_eq, inter_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
rw : s ∩ tᶜ = tᶜ ∩ s
⊢ s \ t = tᶜ ∩ s
have rw₁ : tᶜ ∩ s = tᶜ ∩ s
Tactic: rw [diff_eq, inter_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
⊢ s \ t ∪ s ∩ t = s
have rw : s ∩ t ∪ s \ t = s
Tactic: rw [union_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t u : Set α
⊢ (s ∩ t) \ u = s \ u ∩ t
have rw : s ∩ t ∩ uᶜ = s \ u ∩ t
Tactic: rw [diff_eq, diff_eq, inter_right_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t u : Set α
rw : s ∩ t ∩ uᶜ = s \ u ∩ t
⊢ (s ∩ t) \ u = s \ u ∩ t
have rw₁ : s ∩ t ∩ uᶜ = s ∩ uᶜ ∩ t
Tactic: rw [diff_eq, diff_eq, inter_right_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t u : Set α
rw : s ∩ t ∩ uᶜ = s \ u ∩ t
rw₁ : s ∩ t ∩ uᶜ = s ∩ uᶜ ∩ t
⊢ (s ∩ t) \ u = s \ u ∩ t
have rw₂ : s ∩ uᶜ ∩ t = s ∩ uᶜ ∩ t
Tactic: rw [diff_eq, diff_eq, inter_right_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t u : Set α
⊢ s \ u ∩ t = (s ∩ t) \ u
have rw : s ∩ uᶜ ∩ t = (s ∩ t) \ u
Tactic: rw [diff_eq, diff_eq, inter_right_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t u : Set α
rw : s ∩ uᶜ ∩ t = (s ∩ t) \ u
⊢ s \ u ∩ t = (s ∩ t) \ u
have rw₁ : s ∩ uᶜ ∩ t = s ∩ t ∩ uᶜ
Tactic: rw [diff_eq, diff_eq, inter_right_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t u : Set α
rw : s ∩ uᶜ ∩ t = (s ∩ t) \ u
rw₁ : s ∩ uᶜ ∩ t = s ∩ t ∩ uᶜ
⊢ s \ u ∩ t = (s ∩ t) \ u
have rw₂ : s ∩ t ∩ uᶜ = s ∩ t ∩ uᶜ
Tactic: rw [diff_eq, diff_eq, inter_right_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
⊢ ¬Disjoint t s ↔ (s ∩ t).Nonempty
have rw : (t ∩ s).Nonempty ↔ (s ∩ t).Nonempty
Tactic: rw [not_disjoint_iff_nonempty_inter, inter_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
rw : (t ∩ s).Nonempty ↔ (s ∩ t).Nonempty
⊢ ¬Disjoint t s ↔ (s ∩ t).Nonempty
have rw₁ : (s ∩ t).Nonempty ↔ (s ∩ t).Nonempty
Tactic: rw [not_disjoint_iff_nonempty_inter, inter_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
x : α
s : Set α
⊢ s ⊆ insert x (s \ {x})
have rw : s \ {x} ⊆ s \ {x}
Tactic: rw [← diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ insert a s \ {a} = s
have h₁ : ∀ (x : α), x ∈ insert a s \ {a} ↔ x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s
have h : ∀ (x : α), x ∈ insert a (s \ {a}) ↔ x ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
a b : α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}
have simp_rw : s \ {b} ∪ {a} = (s ∪ {a}) \ {b}
Tactic: simp_rw [← union_singleton, union_diff_distrib,
    diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
a b : α
hab : a ≠ b
s : Set α
simp_rw : s \ {b} ∪ {a} = (s ∪ {a}) \ {b}
⊢ insert a (s \ {b}) = insert a s \ {b}
have simp_rw₁ : s \ {b} ∪ {a} = s \ {b} ∪ {a} \ {b}
Tactic: simp_rw [← union_singleton, union_diff_distrib,
    diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
a : α
⊢ insert a (s \ insert a t) = insert a (s \ t)
have rw : insert a (s \ (t ∪ {a})) = insert a (s \ t)
Tactic: rw [← union_singleton (s := t), ← diff_diff, insert_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
a : α
rw : insert a (s \ (t ∪ {a})) = insert a (s \ t)
⊢ insert a (s \ insert a t) = insert a (s \ t)
have rw₁ : insert a ((s \ t) \ {a}) = insert a (s \ t)
Tactic: rw [← union_singleton (s := t), ← diff_diff, insert_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
s t : Set α
a : α
rw : insert a (s \ (t ∪ {a})) = insert a (s \ t)
rw₁ : insert a ((s \ t) \ {a}) = insert a (s \ t)
⊢ insert a (s \ insert a t) = insert a (s \ t)
have rw₂ : insert a (s \ t) = insert a (s \ t)
Tactic: rw [← union_singleton (s := t), ← diff_diff, insert_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
a b : α
hab : a ≠ b
⊢ Eq (α := Set α) ({a, b} \ {a}) {b}
have rw : Eq (α := Set α) ({b} \ {a}) {b}
Tactic: rw [insert_diff_of_mem _ (mem_singleton a), diff_singleton_eq_self (by simpa)]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
a b : α
hab : a ≠ b
rw : Eq (α := Set α) ({b} \ {a}) {b}
⊢ Eq (α := Set α) ({a, b} \ {a}) {b}
have rw₁ : Eq (α := Set α) {b} {b}
Tactic: rw [insert_diff_of_mem _ (mem_singleton a), diff_singleton_eq_self (by simpa)]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
a b : α
hab : a ≠ b
⊢ Eq (α := Set α) ({a, b} \ {b}) {a}
have rw : Eq (α := Set α) ({b, a} \ {b}) {a}
Tactic: rw [pair_comm, pair_diff_left hab.symm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
a b : α
hab : a ≠ b
rw : Eq (α := Set α) ({b, a} \ {b}) {a}
⊢ Eq (α := Set α) ({a, b} \ {b}) {a}
have rw₁ : Eq (α := Set α) {a} {a}
Tactic: rw [pair_comm, pair_diff_left hab.symm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
⊢ t.ite s s' ∩ t = s ∩ t
have rw : (s ∩ t ∪ s' \ t) ∩ t = s ∩ t
Tactic: rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : (s ∩ t ∪ s' \ t) ∩ t = s ∩ t
⊢ t.ite s s' ∩ t = s ∩ t
have rw₁ : s ∩ t ∩ t ∪ s' \ t ∩ t = s ∩ t
Tactic: rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : (s ∩ t ∪ s' \ t) ∩ t = s ∩ t
rw₁ : s ∩ t ∩ t ∪ s' \ t ∩ t = s ∩ t
⊢ t.ite s s' ∩ t = s ∩ t
have rw₂ : s ∩ t ∩ t ∪ ∅ = s ∩ t
Tactic: rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : (s ∩ t ∪ s' \ t) ∩ t = s ∩ t
rw₁ : s ∩ t ∩ t ∪ s' \ t ∩ t = s ∩ t
rw₂ : s ∩ t ∩ t ∪ ∅ = s ∩ t
⊢ t.ite s s' ∩ t = s ∩ t
have rw₃ : s ∩ (t ∩ t) ∪ ∅ = s ∩ t
Tactic: rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : (s ∩ t ∪ s' \ t) ∩ t = s ∩ t
rw₁ : s ∩ t ∩ t ∪ s' \ t ∩ t = s ∩ t
rw₂ : s ∩ t ∩ t ∪ ∅ = s ∩ t
rw₃ : s ∩ (t ∩ t) ∪ ∅ = s ∩ t
⊢ t.ite s s' ∩ t = s ∩ t
have rw₄ : s ∩ t ∪ ∅ = s ∩ t
Tactic: rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : (s ∩ t ∪ s' \ t) ∩ t = s ∩ t
rw₁ : s ∩ t ∩ t ∪ s' \ t ∩ t = s ∩ t
rw₂ : s ∩ t ∩ t ∪ ∅ = s ∩ t
rw₃ : s ∩ (t ∩ t) ∪ ∅ = s ∩ t
rw₄ : s ∩ t ∪ ∅ = s ∩ t
⊢ t.ite s s' ∩ t = s ∩ t
have rw₅ : s ∩ t = s ∩ t
Tactic: rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
⊢ tᶜ.ite s s' = t.ite s' s
have rw : s ∩ tᶜ ∪ s' \ tᶜ = t.ite s' s
Tactic: rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : s ∩ tᶜ ∪ s' \ tᶜ = t.ite s' s
⊢ tᶜ.ite s s' = t.ite s' s
have rw₁ : s ∩ tᶜ ∪ s' \ tᶜ = s' ∩ t ∪ s \ t
Tactic: rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : s ∩ tᶜ ∪ s' \ tᶜ = t.ite s' s
rw₁ : s ∩ tᶜ ∪ s' \ tᶜ = s' ∩ t ∪ s \ t
⊢ tᶜ.ite s s' = t.ite s' s
have rw₂ : s ∩ tᶜ ∪ s' ∩ t = s' ∩ t ∪ s \ t
Tactic: rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : s ∩ tᶜ ∪ s' \ tᶜ = t.ite s' s
rw₁ : s ∩ tᶜ ∪ s' \ tᶜ = s' ∩ t ∪ s \ t
rw₂ : s ∩ tᶜ ∪ s' ∩ t = s' ∩ t ∪ s \ t
⊢ tᶜ.ite s s' = t.ite s' s
have rw₃ : s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s \ t
Tactic: rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : s ∩ tᶜ ∪ s' \ tᶜ = t.ite s' s
rw₁ : s ∩ tᶜ ∪ s' \ tᶜ = s' ∩ t ∪ s \ t
rw₂ : s ∩ tᶜ ∪ s' ∩ t = s' ∩ t ∪ s \ t
rw₃ : s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s \ t
⊢ tᶜ.ite s s' = t.ite s' s
have rw₄ : s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s ∩ tᶜ
Tactic: rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
⊢ t.ite s s' ∩ tᶜ = s' ∩ tᶜ
have rw : tᶜ.ite s' s ∩ tᶜ = s' ∩ tᶜ
Tactic: rw [← ite_compl, ite_inter_self]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' : Set α
rw : tᶜ.ite s' s ∩ tᶜ = s' ∩ tᶜ
⊢ t.ite s s' ∩ tᶜ = s' ∩ tᶜ
have rw₁ : s' ∩ tᶜ = s' ∩ tᶜ
Tactic: rw [← ite_compl, ite_inter_self]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
⊢ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'
have h : ∀ (x : α), x ∈ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') ↔ x ∈ t.ite s₁ s₁' ∩ t.ite s₂ s₂'
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
have h : (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t →
  (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
h :
  (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t →
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
have h₁ : (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t) →
  (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
h :
  (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t →
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₁ :
  (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t) →
    (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
have h₂ : x ∈ t → x ∈ s₁ → x ∈ s₂ → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
h :
  (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t →
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₁ :
  (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t) →
    (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₂ : x ∈ t → x ∈ s₁ → x ∈ s₂ → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
have h₃ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
Tactic: tauto