awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Regular.ULift
Goal:
R : Type v
inst : Mul R
a : ULift.{u, v} R
⊢ IsRegular a.down ↔ IsRegular a

Tactic:
isRegular_up.symm

Premises used: ULift.isRegular_up, Iff.symm
-- Module: Mathlib.Algebra.Regular.ULift
Goal:
α : Type u_1
R : Type v
inst : SMul α R
r : α
⊢ IsSMulRegular (ULift.{u_2, v} R) r ↔ IsSMulRegular R r

Tactic:
Equiv.ulift.symm.comp_injective _ |>.trans <| Equiv.ulift.symm.injective_comp _ |>.symm

Premises used: Equiv.ulift, Equiv.injective_comp, IsSMulRegular, Iff.trans, Equiv.comp_injective, Equiv.symm, Iff.symm
-- Module: Mathlib.Algebra.Ring.Action.Basic
Goal:
M : Type u_1
inst : Monoid M
R : Type v
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
inst_3 : FaithfulSMul M R
⊢ Function.Injective (β := R →+* R) (MulSemiringAction.toRingHom M R)

Tactic:
fun _ _ h =>
  eq_of_smul_eq_smul fun r => RingHom.ext_iff.1 h r

Premises used: FaithfulSMul.eq_of_smul_eq_smul, RingHom.ext_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Ring.Action.Basic
Goal:
R : Type v
inst : Semiring R
f : R →+* R
a : R
⊢ f • a = (f : (a : R) → R) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Action.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
R : Type v
inst_2 : Semiring R
⊢ FaithfulSMul (R →+* R) R

Tactic:
⟨fun {_ _} h => RingHom.ext h⟩

Premises used: RingHom.ext, FaithfulSMul.mk
-- Module: Mathlib.Algebra.Ring.Action.ConjAct
Goal:
R : Type u_1
inst : Semiring R
⊢ ∀ (a : ConjAct Rˣ), HSMul.hSMul (β := R) a 0 = 0

Tactic:
simp [units_smul_def]

Premises used: ConjAct.units_smul_def
-- Module: Mathlib.Algebra.Ring.Action.ConjAct
Goal:
R : Type u_1
inst : Semiring R
⊢ ∀ (a : ConjAct Rˣ) (x y : R), a • (x + y) = a • x + a • y

Tactic:
simp [units_smul_def, mul_add, add_mul]

Premises used: add_mul, ConjAct.units_smul_def, mul_add
-- Module: Mathlib.Algebra.Ring.Action.End
Goal:
R : Type u_2
inst : Semiring R
f : RingAut R
r : R
⊢ f • r = (f : (a : R) → R) r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Action.End
Goal:
G : Type u_1
R : Type u_2
inst : Group G
inst_1 : Semiring R
⊢ FaithfulSMul (RingAut R) R

Tactic:
⟨RingEquiv.ext⟩

Premises used: RingEquiv.ext, FaithfulSMul.mk
-- Module: Mathlib.Algebra.Ring.Action.Field
Goal:
M : Type u_1
inst : Monoid M
F : Type u_2
inst_1 : DivisionRing F
inst_2 : MulSemiringAction M F
x : M
m : F
⊢ x • m⁻¹ = (x • m)⁻¹

Tactic:
map_inv₀ (MulSemiringAction.toRingHom M F x) _

Premises used: map_inv₀, MulSemiringAction.toRingHom
-- Module: Mathlib.Algebra.Ring.Action.Invariant
Goal:
M : Type u_1
inst : Monoid M
R' : Type u_2
inst_1 : Ring R'
inst_2 : MulSemiringAction M R'
U : Subring R'
inst_3 : IsInvariantSubring M U
⊢ Eq (α := (a : ↥U) → R') (⇑(subtypeHom M U) : (a : ↥U) → R') (Subtype.val (p := fun (x : R') ↦ x ∈ U))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Action.Invariant
Goal:
M : Type u_1
inst : Monoid M
R' : Type u_2
inst_1 : Ring R'
inst_2 : MulSemiringAction M R'
U : Subring R'
inst_3 : IsInvariantSubring M U
⊢ (↑(subtypeHom M U) : ↥U →+* R') = U.subtype

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, Subring.subtype, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
a : α
t : Set β
simp_rw : Eq (α := Set β) ((fun (x : β) ↦ a • x) '' (-t)) (-(fun (x : β) ↦ a • x) '' t)
simp_rw₁ :
  Eq (α := Set β) ((fun (x : β) ↦ a • x) '' (fun (x : β) ↦ -x) '' t) ((fun (x : β) ↦ -x) '' (fun (x : β) ↦ a • x) '' t)
simp_rw₂ : Eq (α := Set β) ((fun (x : β) ↦ a • -x) '' t) ((fun (x : β) ↦ -(a • x)) '' t)
⊢ a • -t = -(a • t)

Tactic:
simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]

Premises used: Set.image_image, Set.image_smul, Set.image_neg_eq_neg, smul_neg
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
s : Set α
t : Set β
simp_rw : HSMul.hSMul (β := Set β) s ((fun (x : β) ↦ -x) '' t) = (fun (x : β) ↦ -x) '' (s • t)
⊢ s • -t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]

Premises used: Set.image_neg_eq_neg
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
s : Set α
t : Set β
⊢ HSMul.hSMul (β := Set β) s ((fun (x : β) ↦ -x) '' t) = (fun (x : β) ↦ -x) '' (s • t)

Tactic:
image_image2_right_comm smul_neg

Premises used: smul_neg, Set.image_image2_right_comm
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
s : Set α
t : Set β
⊢ HSMul.hSMul (β := Set β) s ((fun (x : β) ↦ -x) '' t) = (fun (x : β) ↦ -x) '' (s • t)

Tactic:
exact image_image2_right_comm smul_neg

Premises used: smul_neg, Set.image_image2_right_comm
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun (x : β) ↦ (a + b) • x) x ∈ a • s + b • s

Tactic:
simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)

Premises used: Set.add_mem_add, add_smul, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t

Tactic:
⟨?_, zero_mem_smul_set⟩

Premises used: Iff.intro, Set.zero_mem_smul_set
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
refine : 0 ∈ a • t → 0 ∈ t
⊢ 0 ∈ a • t ↔ 0 ∈ t

Tactic:
refine ⟨?_, zero_mem_smul_set⟩
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
b : β
hb : b ∈ t
h : Eq.{u_2 + 1} (α := β) ((fun (x : β) ↦ a • x) b) 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (hb : 0 ∈ t) (h : Eq.{u_2 + 1} (α := β) ((fun (x : β) ↦ a • x) b) 0), 0 ∈ t
⊢ 0 ∈ t

Tactic:
rwa [(smul_eq_zero.1 h).resolve_left ha] at hb

Premises used: Or.resolve_left, Iff.mp, smul_eq_zero
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) a b) 0
inl :
  ∀ (ha : 0 ∈ s) (h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) 0 b) 0),
    0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
inr :
  ∀ (hb : 0 ∈ t) (h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) a 0) 0),
    0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
obtain rfl | rfl := smul_eq_zero.1 h

Premises used: Iff.mp, rfl, smul_eq_zero
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
s : Set α
t : Set β
b : β
hb : b ∈ t
ha : 0 ∈ s
h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) 0 b) 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
.inl ⟨ha, b, hb⟩

Premises used: And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
s : Set α
t : Set β
a : α
ha : a ∈ s
hb : 0 ∈ t
h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) a 0) 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
.inr ⟨hb, a, ha⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
s : Set α
t : Set β
b : β
hb : b ∈ t
ha : 0 ∈ s
h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) 0 b) 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
exacts [.inl ⟨ha, b, hb⟩, .inr ⟨hb, a, ha⟩]
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
a : α
t : Set β
simp_rw : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) (-(fun (x : β) ↦ a • x) '' t)
simp_rw₁ : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) ((fun (x : β) ↦ -x) '' (fun (x : β) ↦ a • x) '' t)
simp_rw₂ : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) ((fun (x : β) ↦ -(a • x)) '' t)
⊢ -a • t = -(a • t)

Tactic:
simp_rw [← image_smul, ← image_neg_eq_neg, image_image, neg_smul]

Premises used: Set.image_image, Set.image_smul, neg_smul, Set.image_neg_eq_neg
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
s : Set α
t : Set β
simp_rw : HSMul.hSMul (α := Set α) ((fun (x : α) ↦ -x) '' s) t = (fun (x : β) ↦ -x) '' (s • t)
⊢ -s • t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]

Premises used: Set.image_neg_eq_neg
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
s : Set α
t : Set β
⊢ HSMul.hSMul (α := Set α) ((fun (x : α) ↦ -x) '' s) t = (fun (x : β) ↦ -x) '' (s • t)

Tactic:
image2_image_left_comm neg_smul

Premises used: neg_smul, Set.image2_image_left_comm
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
s : Set α
t : Set β
⊢ HSMul.hSMul (α := Set α) ((fun (x : α) ↦ -x) '' s) t = (fun (x : β) ↦ -x) '' (s • t)

Tactic:
exact image2_image_left_comm neg_smul

Premises used: neg_smul, Set.image2_image_left_comm
-- Module: Mathlib.Algebra.Ring.Action.Rat
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
rw : HMul.hMul (α := R) (↑a : R) 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HSMul.hSMul (β := R) a 0 = 0

Tactic:
rw [smul_def, mul_zero]

Premises used: MulZeroClass.mul_zero, NNRat.smul_def
-- Module: Mathlib.Algebra.Ring.Action.Rat
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
rw₂ : (↑a : R) * (x + y) = (↑a : R) * x + (↑a : R) * y
rw₃ rw₄ : (↑a : R) * x + (↑a : R) * y = (↑a : R) * x + (↑a : R) * y
⊢ a • (x + y) = a • x + a • y

Tactic:
rw [smul_def, smul_def, smul_def, mul_add]

Premises used: mul_add, NNRat.smul_def
-- Module: Mathlib.Algebra.Ring.Action.Rat
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ (a • x) • y = a • x • y

Tactic:
simp only [smul_def, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, smul_eq_mul, NNRat.smul_def
-- Module: Mathlib.Algebra.Ring.Action.Rat
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
rw : HMul.hMul (α := R) (↑a : R) 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HSMul.hSMul (β := R) a 0 = 0

Tactic:
rw [smul_def, mul_zero]

Premises used: MulZeroClass.mul_zero, Rat.smul_def
-- Module: Mathlib.Algebra.Ring.Action.Rat
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
rw₂ : (↑a : R) * (x + y) = (↑a : R) * x + (↑a : R) * y
rw₃ rw₄ : (↑a : R) * x + (↑a : R) * y = (↑a : R) * x + (↑a : R) * y
⊢ a • (x + y) = a • x + a • y

Tactic:
rw [smul_def, smul_def, smul_def, mul_add]

Premises used: mul_add, Rat.smul_def
-- Module: Mathlib.Algebra.Ring.Action.Rat
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
x y : R
⊢ (a • x) • y = a • x • y

Tactic:
simp only [smul_def, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, smul_eq_mul, Rat.smul_def
-- Module: Mathlib.Algebra.Ring.Action.Submonoid
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddMonoid α
inst_2 : DistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
rw : x • a + x • b = a + b
rw₁ : a + x • b = a + b
rw₂ rw₃ : a + b = a + b
⊢ x • (a + b) = a + b

Tactic:
rw [smul_add, ha, hb]

Premises used: smul_add
-- Module: Mathlib.Algebra.Ring.Action.Submonoid
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddMonoid α
inst_2 : DistribMulAction M α
a : α
⊢ Membership.mem (γ := AddSubmonoid α) (addSubmonoid M α) a ↔ ∀ (m : M), m • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedPoints
-- Module: Mathlib.Algebra.Ring.Action.Submonoid
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddGroup α
inst_2 : DistribMulAction M α
x : α
ha : x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (addSubmonoid M α))
x_1 : M
rw : -(x_1 • x) = -x
rw₁ rw₂ : -x = -x
⊢ x_1 • -x = -x

Tactic:
rw [smul_neg, ha]

Premises used: smul_neg
-- Module: Mathlib.Algebra.Ring.Action.Submonoid
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddGroup α
inst_2 : DistribMulAction M α
a : α
⊢ Membership.mem (γ := AddSubgroup α) (α^+M) a ↔ ∀ (m : M), m • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedPoints
-- Module: Mathlib.Algebra.Ring.Action.Submonoid
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddGroup α
inst_2 : DistribMulAction M α
⊢ Eq (α := AddSubmonoid α) (AddSubgroup.toAddSubmonoid (α^+M)) (addSubmonoid M α)

Tactic:
rfl

Premises used: FixedPoints.addSubmonoid, rfl
-- Module: Mathlib.Algebra.Ring.AddAut
Goal:
R : Type u_1
inst : Semiring R
u : Rˣ
x : R
⊢ (mulRight u : (a : R) → R) x = x * (↑u : R)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Ring.AddAut
Goal:
R : Type u_1
inst : Semiring R
u : Rˣ
x : R
⊢ (AddEquiv.symm (mulRight u) : (a : R) → R) x = x * (↑u⁻¹ : R)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Ring.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : HasDistribNeg M
a b : M
h : Associated a b
u : Mˣ
hu : a * (↑u : M) = b
⊢ -a * (↑(-u) : M) = b

Tactic:
simp [hu]
-- Module: Mathlib.Algebra.Ring.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : HasDistribNeg M
a b : M
h : Associated a b
⊢ Associated a (-b)

Tactic:
h.symm.neg_left.symm

Premises used: Associated.symm, Associated.neg_left
-- Module: Mathlib.Algebra.Ring.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : HasDistribNeg M
a b : M
h : Associated a b
⊢ Associated (-a) (-b)

Tactic:
h.neg_left.neg_right

Premises used: Associated.neg_right, Associated.neg_left
-- Module: Mathlib.Algebra.Ring.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : HasDistribNeg M
a b : M
⊢ Associated (-a) b ↔ Associated a b

Tactic:
⟨fun h ↦ _root_.neg_neg a ▸ h.neg_left, fun h ↦ h.neg_left⟩

Premises used: Eq.rec, neg_neg, Iff.intro, Associated.neg_left
-- Module: Mathlib.Algebra.Ring.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : HasDistribNeg M
a b : M
⊢ Associated a (-b) ↔ Associated a b

Tactic:
⟨fun h ↦ _root_.neg_neg b ▸ h.neg_right, fun h ↦ h.neg_right⟩

Premises used: Associated.neg_right, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x y z : R
⊢ associator x y z = x * y * z - x * (y * z)

Tactic:
rfl

Premises used: associator, rfl
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
h : Std.Associative fun (x y : R) ↦ x * y
h₁ : ∀ (x y z : R), associator x y z = 0 x y z
⊢ Eq.{u_1 + 1} (α := (x y z : R) → R) associator 0

Tactic:
ext x y z
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
h : Std.Associative fun (x y : R) ↦ x * y
x y z : R
⊢ associator x y z = 0 x y z

Tactic:
simp [associator, Std.Associative.assoc]

Premises used: Std.Associative.assoc, associator
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b c d : R
simp :
  a * (b * c * d) - a * (b * (c * d)) - (a * b * c * d - a * b * (c * d)) + (a * (b * c) * d - a * (b * c * d)) -
        (a * b * (c * d) - a * (b * (c * d))) +
      (a * b * c * d - a * (b * c) * d) =
    0
⊢ a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) +
      associator a b c * d =
    0

Tactic:
simp only [associator, mul_sub, sub_mul]

Premises used: mul_sub, sub_mul, associator
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b c d : R
⊢ a * (b * c * d) - a * (b * (c * d)) - (a * b * c * d - a * b * (c * d)) + (a * (b * c) * d - a * (b * c * d)) -
        (a * b * (c * d) - a * (b * (c * d))) +
      (a * b * c * d - a * (b * c) * d) =
    0

Tactic:
abel1
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x y z : Rᵐᵒᵖ
⊢ associator x y z = -op (associator (unop z) (unop y) (unop x))

Tactic:
simp only [associator_apply, ← unop_mul, ← unop_sub, op_unop, neg_sub]

Premises used: neg_sub, MulOpposite.unop_sub, associator_apply, MulOpposite.op_unop, MulOpposite.unop_mul
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalRing R
⊢ Eq.{u_1 + 1} (α := (x y z : R) → R) associator 0

Tactic:
associator_eq_zero_iff_associative.mpr inferInstance

Premises used: Iff.mpr, inferInstance, associator_eq_zero_iff_associative
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h :
  ∀ (x x_1 : R),
    Eq (α := R) ((((comp mul (mulLeft 0) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
      ((((0 : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R) (comp mul (mulLeft 0)) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x x_1 : R
⊢ Eq (α := R) ((((comp mul (mulLeft 0) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
    ((((0 : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
h :
  ∀ (x_1 x_2 : R),
    Eq (α := R) ((((comp mul (mulLeft (x + y)) : (a : R) → R →+ R) x_1 : R →+ R) : (a : R) → R) x_2 : R)
      ((((HAdd.hAdd (α := R →+ R →+ R) (comp mul (mulLeft x)) (comp mul (mulLeft y)) : (a : R) → R →+ R) x_1 : R →+ R) :
            (a : R) → R)
          x_2 :
        R)
⊢ comp mul (mulLeft (x + y)) = HAdd.hAdd (α := R →+ R →+ R) (comp mul (mulLeft x)) (comp mul (mulLeft y))

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y x_1 x_2 : R
⊢ Eq (α := R) ((((comp mul (mulLeft (x + y)) : (a : R) → R →+ R) x_1 : R →+ R) : (a : R) → R) x_2 : R)
    ((((HAdd.hAdd (α := R →+ R →+ R) (comp mul (mulLeft x)) (comp mul (mulLeft y)) : (a : R) → R →+ R) x_1 : R →+ R) :
          (a : R) → R)
        x_2 :
      R)

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y z : R
⊢ (((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z = x * y * z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h :
  ∀ (x x_1 : R),
    Eq (α := R) ((((compr₂ mul (mulLeft 0) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
      ((((0 : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R) (compr₂ mul (mulLeft 0)) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x x_1 : R
⊢ Eq (α := R) ((((compr₂ mul (mulLeft 0) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
    ((((0 : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
h :
  ∀ (x_1 x_2 : R),
    Eq (α := R) ((((compr₂ mul (mulLeft (x + y)) : (a : R) → R →+ R) x_1 : R →+ R) : (a : R) → R) x_2 : R)
      ((((HAdd.hAdd (α := R →+ R →+ R) (compr₂ mul (mulLeft x)) (compr₂ mul (mulLeft y)) : (a : R) → R →+ R) x_1 :
              R →+ R) :
            (a : R) → R)
          x_2 :
        R)
⊢ compr₂ mul (mulLeft (x + y)) = HAdd.hAdd (α := R →+ R →+ R) (compr₂ mul (mulLeft x)) (compr₂ mul (mulLeft y))

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y x_1 x_2 : R
⊢ Eq (α := R) ((((compr₂ mul (mulLeft (x + y)) : (a : R) → R →+ R) x_1 : R →+ R) : (a : R) → R) x_2 : R)
    ((((HAdd.hAdd (α := R →+ R →+ R) (compr₂ mul (mulLeft x)) (compr₂ mul (mulLeft y)) : (a : R) → R →+ R) x_1 :
            R →+ R) :
          (a : R) → R)
        x_2 :
      R)

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y z : R
⊢ (((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z =
    x * (y * z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) mulLeft₃ mulRight₃
x y z : R
rw :
  (((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z = x * (y * z)
rw₁ :
  Eq (α := R)
    ((((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
    ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
rw₂ rw₃ :
  Eq (α := R)
    ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
    ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
⊢ x * y * z = x * (y * z)

Tactic:
rw [← mulLeft₃_apply, ← mulRight₃_apply, h]

Premises used: AddMonoidHom.mulLeft₃_apply, AddMonoidHom.mulRight₃_apply
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : Std.Associative fun (x y : R) ↦ x * y
h₁ :
  ∀ (x y z : R),
    Eq (α := R)
      ((((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
      ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) mulLeft₃ mulRight₃

Tactic:
ext x y z
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : Std.Associative fun (x y : R) ↦ x * y
x y z : R
⊢ Eq (α := R)
    ((((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
    ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)

Tactic:
simp [Std.Associative.assoc]

Premises used: Std.Associative.assoc
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalSemiring R
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) mulLeft₃ mulRight₃

Tactic:
mulLeft₃_eq_mulRight₃_iff_associative.2 inferInstance

Premises used: Iff.mpr, inferInstance, AddMonoidHom.mulLeft₃_eq_mulRight₃_iff_associative
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b c : R
⊢ (((((associator : (a : R) → R →+ R →+ R) a : R →+ R →+ R) : (a : R) → R →+ R) b : R →+ R) : (a : R) → R) c =
    _root_.associator a b c

Tactic:
rfl

Premises used: associator, rfl
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) associator 0 ↔ Std.Associative fun (x y : R) ↦ x * y

Tactic:
simp [mulLeft₃_eq_mulRight₃_iff_associative, associator, sub_eq_zero]

Premises used: sub_eq_zero, AddMonoidHom.mulLeft₃_eq_mulRight₃_iff_associative, AddMonoidHom.associator
-- Module: Mathlib.Algebra.Ring.Associator
Goal:
R : Type u_1
inst : NonUnitalRing R
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) associator 0

Tactic:
associator_eq_zero_iff_associative.mpr inferInstance

Premises used: Iff.mpr, inferInstance, AddMonoidHom.associator_eq_zero_iff_associative