awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : -a + (-a + a) = -a + -a + a
rw₁ : α
rw₂ : -a + (-a + a) = -a + (-a + a)
rw₃ : α
rw₄ : -a + (-a + a) = -a + (-a + a)
rw₅ : α
⊢ -a + 0 = -a + -a + a

Tactic:
rw [← neg_add_cancel, add_assoc]

Premises used: add_assoc, neg_add_cancel
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : 0 + a = a
rw₁ rw₂ : a = a
⊢ -a + -a + a = a

Tactic:
rw [add_self, zero_add]

Premises used: zero_add, BooleanRing.add_self
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw rw₁ : a = b ↔ a = b
⊢ a = -b ↔ a = b

Tactic:
rw [neg_eq]

Premises used: BooleanRing.neg_eq
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw rw₁ : a + b = a + b
⊢ a + b = (a + b) * (a + b)

Tactic:
rw [mul_self]

Premises used: BooleanRing.mul_self
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + b * (a + b) = a * a + a * b + (b * a + b * b)
rw₁ : a * a + a * b + b * (a + b) = a * a + a * b + (b * a + b * b)
rw₂ rw₃ : a * a + a * b + (b * a + b * b) = a * a + a * b + (b * a + b * b)
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)

Tactic:
rw [add_mul, mul_add, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a * a + a * b + (b * a + b * b) = a + a * b + (b * a + b)

Tactic:
simp only [mul_self]

Premises used: BooleanRing.mul_self
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)

Tactic:
abel
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a + b = a + b + (a * b + b * a)

Tactic:
have : a + b = a + b + (a * b + b * a) :=
    calc
      a + b = (a + b) * (a + b) := by rw [mul_self]
      _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
      _ = a + a * b + (b * a + b) := by simp only [mul_self]
      _ = a + b + (a * b + b * a) := by abel
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : a * b + b * a = 0), a * b + b * a = 0
⊢ a * b + b * a = 0

Tactic:
rwa [left_eq_add] at this

Premises used: left_eq_add
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + -b = a + b
rw₁ : -b = b
rw₂ rw₃ : b = b
⊢ a - b = a + b

Tactic:
rw [sub_eq_add_neg, add_right_inj, neg_eq]

Premises used: sub_eq_add_neg, BooleanRing.neg_eq, add_right_inj
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : a * 1 + a * a = 0
rw₁ : a + a * a = 0
rw₂ : a + a = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) 0 0
⊢ a * (1 + a) = 0

Tactic:
rw [mul_add, mul_one, mul_self, add_self]

Premises used: BooleanRing.mul_self, BooleanRing.add_self, mul_add, mul_one
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
a_1 b_1 a b : α
rw : a * b + b * a = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) 0 0
⊢ a * b = b * a

Tactic:
rw [← add_eq_zero', mul_add_mul]

Premises used: BooleanRing.add_eq_zero', BooleanRing.mul_add_mul
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := AsBoolAlg α ≃ α) (Equiv.symm toBoolAlg) ofBoolAlg

Tactic:
rfl

Premises used: AsBoolAlg, ofBoolAlg, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ AsBoolAlg α) (Equiv.symm ofBoolAlg) toBoolAlg

Tactic:
rfl

Premises used: AsBoolAlg, toBoolAlg, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a : AsBoolAlg α
⊢ (toBoolAlg : (a : α) → AsBoolAlg α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a : α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) ((toBoolAlg : (a : α) → AsBoolAlg α) a : AsBoolAlg α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a b : α
⊢ Eq (α := AsBoolAlg α) ((toBoolAlg : (a : α) → AsBoolAlg α) a : AsBoolAlg α)
      ((toBoolAlg : (a : α) → AsBoolAlg α) b : AsBoolAlg α) ↔
    a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, AsBoolAlg
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a b : AsBoolAlg α
⊢ Eq (α := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) ↔ a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, AsBoolAlg
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
dsimp : a + b + a * b = b + a + b * a
⊢ a ⊔ b = b ⊔ a

Tactic:
dsimp only [(· ⊔ ·)]

Premises used: Max.max
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a + b + a * b = b + a + b * a

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
dsimp : a * b = b * a
⊢ a ⊓ b = b ⊓ a

Tactic:
dsimp only [(· ⊓ ·)]

Premises used: Min.min
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a * b = b * a

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
dsimp : a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)
⊢ a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

Tactic:
dsimp only [(· ⊔ ·)]

Premises used: Max.max
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
dsimp : a * b * c = a * (b * c)
⊢ a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

Tactic:
dsimp only [(· ⊓ ·)]

Premises used: Min.min
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ a * b * c = a * (b * c)

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
dsimp : a + a * b + a * (a * b) = a
⊢ a ⊔ a ⊓ b = a

Tactic:
dsimp only [(· ⊔ ·), (· ⊓ ·)]

Premises used: Max.max, Min.min
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + a * b + a * a * b = a
rw₁ : a + a * b + a * b = a
rw₂ : a + (a * b + a * b) = a
rw₃ : a + 0 = a
rw₄ rw₅ : a = a
⊢ a + a * b + a * (a * b) = a

Tactic:
rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]

Premises used: BooleanRing.mul_self, add_assoc, mul_assoc, BooleanRing.add_self, add_zero
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
dsimp : a * (a + b + a * b) = a
⊢ a ⊓ (a ⊔ b) = a

Tactic:
dsimp only [(· ⊔ ·), (· ⊓ ·)]

Premises used: Max.max, Min.min
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
rw₁ : a * a + a * b + a * (a * b) = a
rw₂ : a + a * b + a * (a * b) = a
rw₃ : a + a * b + a * a * b = a
rw₄ : a + a * b + a * b = a
rw₅ : a + (a * b + a * b) = a
rw₆ : a + 0 = a
rw₇ rw₈ : a = a
⊢ a * (a + b + a * b) = a

Tactic:
rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]

Premises used: BooleanRing.mul_self, add_assoc, mul_assoc, BooleanRing.add_self, mul_add, add_zero
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) =
    a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c)

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c) =
    a + b * c + a * (b * c)

Tactic:
simp only [mul_self, add_self, add_zero]

Premises used: BooleanRing.mul_self, BooleanRing.add_self, add_zero
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
dsimp :
  (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c

Tactic:
dsimp only [(· ⊔ ·), (· ⊓ ·)]

Premises used: Max.max, Min.min
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
rw :
  a + b * c + a * (b * c) + (a + b * c + a * (b * c)) + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
rw₁ : 0 + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
rw₂ : 0 + (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
rw₃ rw₄ : a + b * c + a * (b * c) = a + b * c + a * (b * c)
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)

Tactic:
rw [le_sup_inf_aux, add_self, mul_self, zero_add]

Premises used: BooleanRing.mul_self, zero_add, BooleanRing.add_self, BooleanRing.le_sup_inf_aux
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
⊢ a * (1 + a) + 0 + a * (1 + a) * 0 = 0

Tactic:
simp [mul_add, mul_self, add_self]

Premises used: BooleanRing.mul_self, BooleanRing.add_self, mul_add
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
a₁ : 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)
⊢ 1 ≤ a ⊔ (1 + a)

Tactic:
change
        1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) =
          a + (1 + a) + a * (1 + a)

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
simp : 1 + (a + (1 + a)) = 0
⊢ 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)

Tactic:
simp [mul_add, mul_self, add_self]

Premises used: BooleanRing.mul_self, BooleanRing.add_self, mul_add
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : 1 + a + (1 + a) = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) 0 0
⊢ 1 + (a + (1 + a)) = 0

Tactic:
rw [← add_assoc, add_self]

Premises used: add_assoc, BooleanRing.add_self
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : a + 1 + a = 1
rw₁ : 1 + a + a = 1
rw₂ : 1 + (a + a) = 1
rw₃ : HAdd.hAdd (α := α) 1 0 = 1
rw₄ rw₅ : Eq.{u_1 + 1} (α := α) 1 1
⊢ a + 1 + a * 1 = 1

Tactic:
rw [mul_one, add_comm a 1,
                                                     add_assoc, add_self, add_zero]

Premises used: add_assoc, add_comm, BooleanRing.add_self, mul_one, add_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : 0 + a + 0 = a
rw₁ : a + 0 = a
rw₂ rw₃ : a = a
⊢ 0 + a + 0 * a = a

Tactic:
rw [zero_mul, zero_add, add_zero]

Premises used: MulZeroClass.zero_mul, zero_add, add_zero
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
⊢ Eq.{u_1 + 1} (α := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) ⊤ : α) (1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
⊢ Eq.{u_1 + 1} (α := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) ⊥ : α) (0 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) (a ⊔ b) =
    HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
        ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) +
      HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
        ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) (a ⊓ b) =
    HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : AsBoolAlg α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) aᶜ =
    HAdd.hAdd (α := α) (β := α) (1 : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) (a \ b) =
    HMul.hMul (α := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
      (HAdd.hAdd (α := α) (β := α) (1 : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ (a + b + a * b) * (1 + a * b) = a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b)

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b

Tactic:
simp only [mul_self, add_self, add_zero]

Premises used: BooleanRing.mul_self, BooleanRing.add_self, add_zero
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
rw :
  (ofBoolAlg : (a : AsBoolAlg α) → α) ((a ⊔ b) \ (a ⊓ b)) =
    HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) (a ∆ b) =
    HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Premises used: symmDiff_eq_sup_sdiff_inf
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) ((a ⊔ b) \ (a ⊓ b)) =
    HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)

Tactic:
of_boolalg_symmDiff_aux _ _

Premises used: _private.0.of_boolalg_symmDiff_aux
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) ((a ⊔ b) \ (a ⊓ b)) =
    HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)

Tactic:
exact of_boolalg_symmDiff_aux _ _

Premises used: _private.0.of_boolalg_symmDiff_aux
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
⊢ HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) =
      (ofBoolAlg : (a : AsBoolAlg α) → α) a ↔
    a ≤ b

Tactic:
@inf_eq_left (AsBoolAlg α) _ _ _

Premises used: AsBoolAlg, inf_eq_left
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
⊢ Eq.{u_1 + 1} (α := AsBoolAlg α) ((toBoolAlg : (a : α) → AsBoolAlg α) 0 : AsBoolAlg α) (⊥ : AsBoolAlg α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
⊢ Eq.{u_1 + 1} (α := AsBoolAlg α) ((toBoolAlg : (a : α) → AsBoolAlg α) 1 : AsBoolAlg α) (⊤ : AsBoolAlg α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ Eq (α := AsBoolAlg α) ((toBoolAlg : (a : α) → AsBoolAlg α) (a * b) : AsBoolAlg α)
    ((toBoolAlg : (a : α) → AsBoolAlg α) a ⊓ (toBoolAlg : (a : α) → AsBoolAlg α) b : AsBoolAlg α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ Eq (α := AsBoolAlg α) ((toBoolAlg : (a : α) → AsBoolAlg α) (a + b + a * b) : AsBoolAlg α)
    ((toBoolAlg : (a : α) → AsBoolAlg α) a ⊔ (toBoolAlg : (a : α) → AsBoolAlg α) b : AsBoolAlg α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ Eq (α := AsBoolAlg α) ((toBoolAlg : (a : α) → AsBoolAlg α) (a + b) : AsBoolAlg α)
    ((toBoolAlg : (a : α) → AsBoolAlg α) a ∆ (toBoolAlg : (a : α) → AsBoolAlg α) b : AsBoolAlg α)

Tactic:
(ofBoolAlg_symmDiff a b).symm

Premises used: AsBoolAlg, ofBoolAlg_symmDiff, Eq.symm, symmDiff
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
dsimp :
  Eq.{u_2 + 1} (α := AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β)
        ((f : (a : α) → β)
            (HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) +
              HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
          β) :
      AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
        (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
      AsBoolAlg β)
⊢ Eq.{u_2 + 1} (α := AsBoolAlg β)
    (Function.comp (β := β) (⇑toBoolAlg : (a : β) → AsBoolAlg β)
      (Function.comp (β := α) (⇑f : (a : α) → β) (⇑ofBoolAlg : (a : AsBoolAlg α) → α)) (a ⊔ b))
    (Function.comp (β := β) (⇑toBoolAlg : (a : β) → AsBoolAlg β)
        (Function.comp (β := α) (⇑f : (a : α) → β) (⇑ofBoolAlg : (a : AsBoolAlg α) → α)) a ⊔
      Function.comp (β := β) (⇑toBoolAlg : (a : β) → AsBoolAlg β)
        (Function.comp (β := α) (⇑f : (a : α) → β) (⇑ofBoolAlg : (a : AsBoolAlg α) → α)) b)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
simp_rw :
  Eq (α := AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β)
        (HAdd.hAdd (β := β)
          (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β)
            ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β))
          ((f : (a : α) → β)
              (HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
            β)) :
      AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
        (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
      AsBoolAlg β)
simp_rw₁ :
  Eq (α := AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β)
        (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β)
            ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) +
          HMul.hMul (α := β) (β := β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β)
            ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β)) :
      AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
        (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
      AsBoolAlg β)
⊢ Eq.{u_2 + 1} (α := AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β)
        ((f : (a : α) → β)
            (HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) +
              HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
          β) :
      AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
        (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
      AsBoolAlg β)

Tactic:
simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]

Premises used: map_add, toBoolAlg_add_add_mul, map_mul
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
⊢ Eq (α := BoundedLatticeHom (AsBoolAlg α) (AsBoolAlg α)) (RingHom.asBoolAlg (id α))
    (BoundedLatticeHom.id (AsBoolAlg α))

Tactic:
rfl

Premises used: BoundedLatticeHom.id, LatticeHom.id, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
g : β →+* γ
f : α →+* β
⊢ (g.comp f).asBoolAlg = g.asBoolAlg.comp f.asBoolAlg

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, BoundedLatticeHom.comp, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := AsBoolRing α ≃ α) (Equiv.symm toBoolRing) ofBoolRing

Tactic:
rfl

Premises used: AsBoolRing, ofBoolRing, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ AsBoolRing α) (Equiv.symm ofBoolRing) toBoolRing

Tactic:
rfl

Premises used: toBoolRing, AsBoolRing, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a : AsBoolRing α
⊢ (toBoolRing : (a : α) → AsBoolRing α) ((ofBoolRing : (a : AsBoolRing α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a : α
⊢ (ofBoolRing : (a : AsBoolRing α) → α) ((toBoolRing : (a : α) → AsBoolRing α) a : AsBoolRing α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a b : α
⊢ Eq (α := AsBoolRing α) ((toBoolRing : (a : α) → AsBoolRing α) a : AsBoolRing α)
      ((toBoolRing : (a : α) → AsBoolRing α) b : AsBoolRing α) ↔
    a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, AsBoolRing
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
a b : AsBoolRing α
⊢ Eq (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) a : α) ((ofBoolRing : (a : AsBoolRing α) → α) b : α) ↔ a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, AsBoolRing
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ Eq.{u_1 + 1} (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) 0 : α) (⊥ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ Eq.{u_1 + 1} (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) 1 : α) (⊤ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
a : AsBoolRing α
⊢ Eq (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) (-a) : α) ((ofBoolRing : (a : AsBoolRing α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
a b : AsBoolRing α
⊢ Eq (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) (a + b) : α)
    ((ofBoolRing : (a : AsBoolRing α) → α) a ∆ (ofBoolRing : (a : AsBoolRing α) → α) b : α)

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
a b : AsBoolRing α
⊢ Eq (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) (a - b) : α)
    ((ofBoolRing : (a : AsBoolRing α) → α) a ∆ (ofBoolRing : (a : AsBoolRing α) → α) b : α)

Tactic:
rfl

Premises used: SubNegMonoid.sub', symmDiff, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
a b : AsBoolRing α
⊢ Eq (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) (a * b) : α)
    ((ofBoolRing : (a : AsBoolRing α) → α) a ⊓ (ofBoolRing : (a : AsBoolRing α) → α) b : α)

Tactic:
rfl

Premises used: rfl