awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ insert j t, f i)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ x ∈ t, f x)), Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)

Tactic:
rwa [iSup_insert] at ih

Premises used: iSup_insert
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
⊢ Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)

Tactic:
replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
rw : Disjoint (f j) (⨆ x ∈ t ∪ (↑s₀ : Set ι), f x)
⊢ Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)

Tactic:
rw [← iSup_union]

Premises used: iSup_union
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ j ∉ t ∪ (↑s₀ : Set ι)

Tactic:
aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ Disjoint (f j) (⨆ x ∈ t ∪ (↑s₀ : Set ι), f x)

Tactic:
exact disjoint_biSup hf <| by aesop

Premises used: iSupIndep.disjoint_biSup
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)

Tactic:
have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (Insert.insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)
insert : Disjoint (⨆ i ∈ t, f i) ((⨆ x ∈ s₀, f x) ⊔ f j)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ Insert.insert j s₀, f i) (⨆ i ∈ t, f i)

Tactic:
rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]

Premises used: disjoint_comm, Finset.iSup_insert, sup_comm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)
⊢ Disjoint (⨆ i ∈ t, f i) ((⨆ x ∈ s₀, f x) ⊔ f j)

Tactic:
disjoint_sup_right_of_disjoint_sup_right ih this

Premises used: disjoint_sup_right_of_disjoint_sup_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ (↑s₀ : Set ι), f i)
⊢ Disjoint (⨆ i ∈ t, f i) ((⨆ x ∈ s₀, f x) ⊔ f j)

Tactic:
exact disjoint_sup_right_of_disjoint_sup_right ih this

Premises used: disjoint_sup_right_of_disjoint_sup_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s : Set ι) t
empty :
  ∀ {t : Set ι} (hst : Disjoint (↑∅ : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) (⨆ i ∈ t, f i)
insert :
  ∀ (j : ι) (s₀ : Finset ι) (hj : j ∉ s₀)
    (ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i))
    {t : Set ι} (hst : Disjoint (↑(Insert.insert j s₀) : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ i ∈ Insert.insert j s₀, f i) (⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this

Premises used: disjoint_comm, Insert.insert, sup_comm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s : Set ι) t
empty :
  ∀ {t : Set ι} (hst : Disjoint (↑∅ : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) (⨆ i ∈ t, f i)
insert :
  ∀ (j : ι) (s₀ : Finset ι) (hj : j ∉ s₀)
    (ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i))
    {t : Set ι} (hst : Disjoint (↑(Insert.insert j s₀) : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ i ∈ Insert.insert j s₀, f i) (⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
classical
  induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this

Premises used: disjoint_comm, Insert.insert, sup_comm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : f i ≠ ⊥
by_contra : ∀ (contra : i ∉ s), False
⊢ i ∈ s

Tactic:
by_contra contra
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
⊢ ∀ i_1 ∈ s, i_1 ≠ i

Tactic:
aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
⊢ Disjoint (f i) (⨆ i ∈ s, f i)

Tactic:
replace h₁ : Disjoint (f i) (⨆ i ∈ s, f i) := (h₁ i).mono_right <| biSup_mono <| by aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set ι
h₂ : Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
h₁ : Disjoint (f i) (⨆ i ∈ s, f i)
⊢ False

Tactic:
aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : Order.Frame α
s : Set α
⊢ sSupIndep s ↔ s.PairwiseDisjoint id

Tactic:
⟨sSupIndep.pairwiseDisjoint, fun hs _ hi =>
    disjoint_sSup_iff.2 fun _ hj => hs hi hj.1 <| Ne.symm hj.2⟩

Premises used: Iff.mpr, sSupIndep.pairwiseDisjoint, Ne.symm, And.right, disjoint_sSup_iff, And.left, Iff.intro
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Order.Frame α
f : ι → α
⊢ iSupIndep f ↔ Pairwise (Disjoint on f)

Tactic:
⟨iSupIndep.pairwiseDisjoint, fun hs _ =>
    disjoint_iSup_iff.2 fun _ => disjoint_iSup_iff.2 fun hij => hs hij.symm⟩

Premises used: Iff.mpr, iSupIndep.pairwiseDisjoint, disjoint_iSup_iff, Ne.symm, Iff.intro
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : Max α
inst_1 : SDiff α
a b : α
⊢ a ∆ b = a \ b ⊔ b \ a

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : Min α
inst_1 : HImp α
a b : α
⊢ a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)

Tactic:
rfl

Premises used: bihimp, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
p q : Prop
⊢ p ∆ q = Xor p q

Tactic:
rfl

Premises used: Xor, symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
p q : Prop
⊢ p ⇔ q ↔ (p ↔ q)

Tactic:
iff_iff_implies_and_implies.symm.trans Iff.comm

Premises used: iff_iff_implies_and_implies, bihimp, Iff.trans, Iff.comm, Iff.symm
-- Module: Mathlib.Order.SymmDiff
Goal:
⊢ ∀ (p q : Bool), p ∆ q = (p ^^ q)

Tactic:
decide
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (a ∆ b) : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a ⇔ (toDual : (a : α) → αᵒᵈ) b : αᵒᵈ)

Tactic:
rfl

Premises used: bihimp, symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (a ⇔ b) : α) ((ofDual : (a : αᵒᵈ) → α) a ∆ (ofDual : (a : αᵒᵈ) → α) b : α)

Tactic:
rfl

Premises used: bihimp, symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = b ∆ a

Tactic:
simp only [symmDiff, sup_comm]

Premises used: sup_comm, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ Std.Commutative fun (x1 x2 : α) ↦ x1 ∆ x2

Tactic:
⟨symmDiff_comm⟩

Premises used: symmDiff_comm, Std.Commutative.mk
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a \ a ⊔ a \ a = ⊥
rw₁ : a \ a = ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
⊢ a ∆ a = ⊥

Tactic:
rw [symmDiff, sup_idem, sdiff_self]

Premises used: sdiff_self, sup_idem, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a \ ⊥ ⊔ ⊥ \ a = a
rw₁ : a ⊔ ⊥ \ a = a
rw₂ : a ⊔ ⊥ = a
rw₃ rw₄ : a = a
⊢ a ∆ ⊥ = a

Tactic:
rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]

Premises used: bot_sdiff, sup_bot_eq, sdiff_bot, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
rw : a ∆ ⊥ = a
rw₁ rw₂ : a = a
⊢ ⊥ ∆ a = a

Tactic:
rw [symmDiff_comm, symmDiff_bot]

Premises used: symmDiff_comm, symmDiff_bot
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
simp_rw : a \ b ⊔ b \ a = ⊥ ↔ a = b
simp_rw₁ : a \ b = ⊥ ∧ b \ a = ⊥ ↔ a = b
simp_rw₂ : a ≤ b ∧ b ≤ a ↔ a = b
⊢ a ∆ b = ⊥ ↔ a = b

Tactic:
simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]

Premises used: sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
rw : a \ b ⊔ b \ a = b \ a
rw₁ : ⊥ ⊔ b \ a = b \ a
rw₂ rw₃ : b \ a = b \ a
⊢ a ∆ b = b \ a

Tactic:
rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]

Premises used: Iff.mpr, bot_sup_eq, sdiff_eq_bot_iff, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
rw : a \ b ⊔ b \ a = a \ b
rw₁ : a \ b ⊔ ⊥ = a \ b
rw₂ rw₃ : a \ b = a \ b
⊢ a ∆ b = a \ b

Tactic:
rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]

Premises used: Iff.mpr, sup_bot_eq, sdiff_eq_bot_iff, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
ha : a ≤ b ⊔ c
hb : b ≤ a ⊔ c
⊢ a ∆ b ≤ c

Tactic:
sup_le (sdiff_le_iff.2 ha) <| sdiff_le_iff.2 hb

Premises used: Iff.mpr, sup_le, sdiff_le_iff, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
simp_rw : a \ b ⊔ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
simp_rw₁ : a \ b ≤ c ∧ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Tactic:
simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]

Premises used: sup_le_iff, sdiff_le_iff, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ≤ a ⊔ b

Tactic:
sup_le_sup sdiff_le sdiff_le

Premises used: sup_le_sup, sdiff_le, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = (a ⊔ b) \ (a ⊓ b)

Tactic:
simp [sup_sdiff, symmDiff]

Premises used: sup_sdiff, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b ⊔ b \ a = a ⊔ b
rw₁ : a ⊔ b \ a = a ⊔ b
rw₂ rw₃ : a ⊔ b = a ⊔ b
⊢ a ∆ b = a ⊔ b

Tactic:
rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]

Premises used: Disjoint.sdiff_eq_right, Disjoint.sdiff_eq_left, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : (a \ b ⊔ b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
rw₁ : (a \ b) \ c ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
rw₂ : a \ (b ⊔ c) ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
rw₃ rw₄ : a \ (b ⊔ c) ⊔ b \ (a ⊔ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

Tactic:
rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]

Premises used: sdiff_sdiff_left, sup_sdiff_distrib, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
⊢ a ∆ b \ (a ⊓ b) = a ∆ b

Tactic:
rw [symmDiff_sdiff]

Premises used: symmDiff_sdiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b

Tactic:
simp [symmDiff]

Premises used: symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ (b \ a) ⊔ b \ a = a ⊔ b
⊢ a ∆ (b \ a) = a ⊔ b

Tactic:
rw [symmDiff, sdiff_idem]

Premises used: sdiff_idem, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b

Tactic:
le_antisymm (sup_le_sup sdiff_le sdiff_le)
      (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)

Premises used: sup_le_sup, le_sup_right, sdiff_le, le_antisymm, sup_le, LE.le.trans, le_sdiff_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b

Tactic:
exact
    le_antisymm (sup_le_sup sdiff_le sdiff_le)
      (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)

Premises used: sup_le_sup, le_sup_right, sdiff_le, le_antisymm, sup_le, LE.le.trans, le_sdiff_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : b ∆ (a \ b) = a ⊔ b
rw₁ : b ⊔ a = a ⊔ b
rw₂ rw₃ : a ⊔ b = a ⊔ b
⊢ (a \ b) ∆ b = a ⊔ b

Tactic:
rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]

Premises used: symmDiff_comm, sup_comm, symmDiff_sdiff_eq_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b

Tactic:
le_antisymm (sup_le symmDiff_le_sup inf_le_sup) ?_

Premises used: inf_le_sup, le_antisymm, symmDiff_le_sup, sup_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
refine : a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b

Tactic:
refine le_antisymm (sup_le symmDiff_le_sup inf_le_sup) ?_

Premises used: inf_le_sup, le_antisymm, symmDiff_le_sup, sup_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b

Tactic:
rw [sup_inf_left, symmDiff]

Premises used: sup_inf_left, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)

Tactic:
sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)

Premises used: le_sup_right, le_inf, sup_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
refine_1 : a ≤ a \ b ⊔ b \ a ⊔ b
refine_2 : b ≤ a \ b ⊔ b \ a ⊔ a
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)

Tactic:
refine sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)

Premises used: sup_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
refine_1 : a ≤ a \ b ⊔ b ⊔ b \ a
⊢ a ≤ a \ b ⊔ b \ a ⊔ b

Tactic:
rw [sup_right_comm]

Premises used: sup_right_comm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a

Tactic:
le_sup_of_le_left le_sdiff_sup

Premises used: le_sup_of_le_left, le_sdiff_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a

Tactic:
exact le_sup_of_le_left le_sdiff_sup

Premises used: le_sup_of_le_left, le_sdiff_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
refine_2 : b ≤ a \ b ⊔ (b \ a ⊔ a)
⊢ b ≤ a \ b ⊔ b \ a ⊔ a

Tactic:
rw [sup_assoc]

Premises used: sup_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)

Tactic:
le_sup_of_le_right le_sdiff_sup

Premises used: le_sup_of_le_right, le_sdiff_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)

Tactic:
exact le_sup_of_le_right le_sdiff_sup

Premises used: le_sup_of_le_right, le_sdiff_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ∆ b ⊔ a ⊓ b = a ⊔ b
rw₁ rw₂ : a ⊔ b = a ⊔ b
⊢ a ⊓ b ⊔ a ∆ b = a ⊔ b

Tactic:
rw [sup_comm, symmDiff_sup_inf]

Premises used: symmDiff_sup_inf, sup_comm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b
rw₁ : a ∆ b ⊔ a ⊓ b = a ⊔ b
rw₂ rw₃ : a ⊔ b = a ⊔ b
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b

Tactic:
rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]

Premises used: symmDiff_sup_inf, symmDiff_sdiff_inf, sdiff_symmDiff_eq_sup
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ∆ b ∆ (a ⊓ b) = a ⊔ b
rw₁ rw₂ : a ⊔ b = a ⊔ b
⊢ (a ⊓ b) ∆ (a ∆ b) = a ⊔ b

Tactic:
rw [symmDiff_comm, symmDiff_symmDiff_inf]

Premises used: symmDiff_comm, symmDiff_symmDiff_inf
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ c ≤ a ∆ b ⊔ b ∆ c

Tactic:
(sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq ?_

Premises used: sup_le_sup, LE.le.trans_eq, symmDiff, sdiff_triangle
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
refine : a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
⊢ a ∆ c ≤ a ∆ b ⊔ b ∆ c

Tactic:
refine (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq ?_

Premises used: sup_le_sup, LE.le.trans_eq, sdiff_triangle
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a \ b ⊔ b \ c ⊔ (b \ a ⊔ c \ b) = a ∆ b ⊔ b ∆ c
rw₁ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a ∆ b ⊔ b ∆ c
rw₂ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ b ∆ c
rw₃ rw₄ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b)
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c

Tactic:
rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]

Premises used: sup_sup_sup_comm, SDiff.sdiff, sup_comm, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ ⊥ ≤ a ∆ b ⊔ b ∆ ⊥

Tactic:
symmDiff_triangle a b ⊥

Premises used: Bot.bot, symmDiff_triangle
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : a = a ∆ ⊥
h₁ : b = b ∆ ⊥
⊢ a ≤ a ∆ b ⊔ b

Tactic:
convert! symmDiff_triangle a b ⊥

Premises used: Bot.bot, symmDiff_triangle
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h h₁ : a = a
⊢ a = a ∆ ⊥

Tactic:
rw [symmDiff_bot]

Premises used: symmDiff_bot
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h h₁ : b = b
⊢ b = b ∆ ⊥

Tactic:
rw [symmDiff_bot]

Premises used: symmDiff_bot
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a ∆ b ⊔ a

Tactic:
symmDiff_comm a b ▸ le_symmDiff_sup_right ..

Premises used: symmDiff_comm, Eq.rec, le_symmDiff_sup_right, Eq.symm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (a ⇔ b) : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a ∆ (toDual : (a : α) → αᵒᵈ) b : αᵒᵈ)

Tactic:
rfl

Premises used: bihimp, symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (a ∆ b) : α) ((ofDual : (a : αᵒᵈ) → α) a ⇔ (ofDual : (a : αᵒᵈ) → α) b : α)

Tactic:
rfl

Premises used: bihimp, symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇔ b = b ⇔ a

Tactic:
simp only [(· ⇔ ·), inf_comm]

Premises used: inf_comm, bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ Std.Commutative fun (x1 x2 : α) ↦ x1 ⇔ x2

Tactic:
⟨bihimp_comm⟩

Premises used: bihimp_comm, Std.Commutative.mk
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : (a ⇨ a) ⊓ (a ⇨ a) = ⊤
rw₁ : a ⇨ a = ⊤
rw₂ rw₃ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
⊢ a ⇔ a = ⊤

Tactic:
rw [bihimp, inf_idem, himp_self]

Premises used: bihimp, himp_self, inf_idem
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : (⊤ ⇨ a) ⊓ (a ⇨ ⊤) = a
rw₁ : (⊤ ⇨ a) ⊓ ⊤ = a
rw₂ : a ⊓ ⊤ = a
rw₃ rw₄ : a = a
⊢ a ⇔ ⊤ = a

Tactic:
rw [bihimp, himp_top, top_himp, inf_top_eq]

Premises used: himp_top, inf_top_eq, bihimp, top_himp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : a ⇔ ⊤ = a
rw₁ rw₂ : a = a
⊢ ⊤ ⇔ a = a

Tactic:
rw [bihimp_comm, bihimp_top]

Premises used: bihimp_comm, bihimp_top
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇔ b = ⊤ ↔ a = b

Tactic:
@symmDiff_eq_bot αᵒᵈ _ _ _

Premises used: bihimp, symmDiff_eq_bot, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : a ≤ b
rw : (b ⇨ a) ⊓ (a ⇨ b) = b ⇨ a
rw₁ : (b ⇨ a) ⊓ ⊤ = b ⇨ a
rw₂ rw₃ : b ⇨ a = b ⇨ a
⊢ a ⇔ b = b ⇨ a

Tactic:
rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]

Premises used: Iff.mpr, inf_top_eq, himp_eq_top_iff, bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : b ≤ a
rw : (b ⇨ a) ⊓ (a ⇨ b) = a ⇨ b
rw₁ : ⊤ ⊓ (a ⇨ b) = a ⇨ b
rw₂ rw₃ : a ⇨ b = a ⇨ b
⊢ a ⇔ b = a ⇨ b

Tactic:
rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]

Premises used: Iff.mpr, himp_eq_top_iff, top_inf_eq, bihimp