awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ OneHom.toFun (↑(↑(↑f : A →+* B) : A →* B) : OneHom A B) ((algebraMap R A : (a : R) → A) r) =
    (algebraMap R B : (a : R) → B) r
have rw : OneHom.toFun (↑(↑(↑f : A →+* B) : A →* B) : OneHom A B)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
  (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [algebraMap_apply R S A, algebraMap_apply R S B]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap R A : (a : R) → A) r) = (algebraMap R B : (a : R) → B) r
have rw : f.toRingEquiv.toFun ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
  (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [algebraMap_apply R S A, algebraMap_apply R S B]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
⊢ Eq (α := Submodule R M) (restrictScalars R (span A X)) (span R X)
have refine : ∀ (m : M) (hm : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m),
  Membership.mem (γ := Submodule R M) (span R X) m
Tactic: refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
m : M
hm : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m
⊢ Membership.mem (γ := Submodule R M) (span R X) m
have refine : ∀ (a : A) (m : M),
  Membership.mem (γ := Submodule A M) (span A X) m →
    ∀ (hm : Membership.mem (γ := Submodule R M) (span R X) m), Membership.mem (γ := Submodule R M) (span R X) (a • m)
Tactic: refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m_1
a : A
m : M
h : Membership.mem (γ := Submodule A M) (span A X) m
hm : Membership.mem (γ := Submodule R M) (span R X) m
⊢ Membership.mem (γ := Submodule R M) (span R X) (a • m)
have obtain : ∀ (r : R),
  Membership.mem (γ := Submodule R M) (span R X)
    (HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) m)
Tactic: obtain ⟨r, rfl⟩ := hsur a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 x)
have rw : Membership.mem (γ := Submodule R A) (span R (s • t)) 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
c₁ c₂ : S
h : Membership.mem (γ := Submodule R S) (span R s) c₁
h_1 : Membership.mem (γ := Submodule R S) (span R s) c₂
ih₁ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x)
ih₂ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₂ • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) ((c₁ + c₂) • x)
have rw : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x + c₂ • x)
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
b : R
c : S
h : Membership.mem (γ := Submodule R S) (span R s) c
hc : Membership.mem (γ := Submodule R A) (span R (s • t)) (c • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) ((b • c) • x)
have rw : Membership.mem (γ := Submodule R A) (span R (s • t)) (b • c • x)
Tactic: rw [IsScalarTower.smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)
have refine_1 : Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 y)
Tactic: refine span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
        (hs ▸ mem_top : s0 ∈ span R s)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
refine_1 : Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)
have refine_2 : ∀ (x y_1 : S) (hx : Membership.mem (γ := Submodule R S) (span R s) x)
  (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
  Membership.mem (γ := Submodule R A) (span R (s • t)) (x • y) →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) ((x + y_1) • y)
Tactic: refine span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
        (hs ▸ mem_top : s0 ∈ span R s)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
refine_1 : Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 y)
refine_2 :
  ∀ (x y_1 : S) (hx : Membership.mem (γ := Submodule R S) (span R s) x)
    (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) ((x + y_1) • y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)
have refine_3 : ∀ (a : R) (x : S) (hx : Membership.mem (γ := Submodule R S) (span R s) x),
  Membership.mem (γ := Submodule R A) (span R (s • t)) (x • y) →
    Membership.mem (γ := Submodule R A) (span R (s • t)) ((a • x) • y)
Tactic: refine span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
        (hs ▸ mem_top : s0 ∈ span R s)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 y)
have refine_1 : Membership.mem (γ := Submodule R A) (span R (s • t)) 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
x_1 y_1 : S
hx : Membership.mem (γ := Submodule R S) (span R s) x_1
hy_1 : Membership.mem (γ := Submodule R S) (span R s) y_1
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)
have refine_2 : Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
  Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y + y_1 • y)
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0_1 : S
y : A
hy_1 : y ∈ t
r : R
s0 : S
hx : Membership.mem (γ := Submodule R S) (span R s) s0
hy : Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) ((r • s0) • y)
have refine_3 : Membership.mem (γ := Submodule R A) (span R (s • t)) (r • s0 • y)
Tactic: rw [IsScalarTower.smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (span R (s • t)) x
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (k • x)
have rw : ∀ (hx : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x),
  Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)
Tactic: rw [span_smul_of_span_eq_top hs] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (span R t) x
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (k • x)
have rw : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)
Tactic: rw [span_smul_of_span_eq_top hs]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
T : Type u_2
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
x : S
a : Set S
hx : Membership.mem (γ := Submodule R S) (span R a) x
⊢ Membership.mem.{u_2, u_2} (α := T) (γ := Submodule R T) (span R ((⇑(algebraMap S T) : (a : S) → T) '' a))
    ((algebraMap S T : (a : S) → T) x : T)
have rw : ∃ (y : S),
  Membership.mem (γ := Submodule R S) (span R a) y ∧
    Eq.{u_2 + 1} (α := T)
      (((↑R :
                {S M : Type u_1} →
                  {M₂ : Type u_2} →
                    [inst : Semiring R] →
                      [inst_7 : Semiring S] →
                        [inst_8 : AddCommMonoid M] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module R M] →
                              [inst_11 : Module R M₂] →
                                [inst_12 : Module S M] →
                                  [inst_13 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (Algebra.linearMap S T) :
            (a : S) → T)
          y :
        T)
      ((algebraMap S T : (a : S) → T) x : T)
Tactic: rw [span_algebraMap_image_of_tower, mem_map]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : CommSemiring R
e_1 e : α ≃ β
inst_1 : Semiring β
inst_2 : Algebra R β
semiring : Semiring α := e.semiring
algebra : Algebra R α := Equiv.algebra R e
r : R
⊢ (RingEquiv.toEquiv e.ringEquiv).toFun ((algebraMap R α : (a : R) → α) r) = (algebraMap R β : (a : R) → β) r
have a : Eq.{u_2 + 1} (α := α)
  ((e.symm : (a : β) → α) ((RingEquiv.toEquiv e.ringEquiv).toFun ((algebraMap R α : (a : R) → α) r)) : α)
  ((e.symm : (a : β) → α) ((algebraMap R β : (a : R) → β) r : β) : α)
Tactic: apply e.symm.injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x x_1 x_2 : Unitization R A
⊢ (x * (x_1 + x_2)).toProd.2 = (x * x_1 + x * x_2).toProd.2
have simp : x.toProd.1 • x_1.toProd.2 + x.toProd.1 • x_2.toProd.2 + (x_1.toProd.1 • x.toProd.2 + x_2.toProd.1 • x.toProd.2) +
    (x.toProd.2 * x_1.toProd.2 + x.toProd.2 * x_2.toProd.2) =
  x.toProd.1 • x_1.toProd.2 + x_1.toProd.1 • x.toProd.2 + x.toProd.2 * x_1.toProd.2 +
    (x.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x.toProd.2 + x.toProd.2 * x_2.toProd.2)
Tactic: simp [smul_add, add_smul, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x x_1 x_2 : Unitization R A
⊢ ((x + x_1) * x_2).toProd.2 = (x * x_2 + x_1 * x_2).toProd.2
have simp : x.toProd.1 • x_2.toProd.2 + x_1.toProd.1 • x_2.toProd.2 + (x_2.toProd.1 • x.toProd.2 + x_2.toProd.1 • x_1.toProd.2) +
    (x.toProd.2 * x_2.toProd.2 + x_1.toProd.2 * x_2.toProd.2) =
  x.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x.toProd.2 + x.toProd.2 * x_2.toProd.2 +
    (x_1.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x_1.toProd.2 + x_1.toProd.2 * x_2.toProd.2)
Tactic: simp [smul_add, add_smul, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommMonoid R
inst_1 : NonUnitalSemiring A
inst_2 : DistribMulAction R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x y z : Unitization R A
⊢ (x * y * z).toProd.2 = (x * (y * z)).toProd.2
have simp : (x.toProd.1 * y.toProd.1) • z.toProd.2 +
      ((x.toProd.1 * z.toProd.1) • y.toProd.2 + (y.toProd.1 * z.toProd.1) • x.toProd.2 +
        z.toProd.1 • (x.toProd.2 * y.toProd.2)) +
    (x.toProd.1 • (y.toProd.2 * z.toProd.2) + y.toProd.1 • (x.toProd.2 * z.toProd.2) +
      x.toProd.2 * (y.toProd.2 * z.toProd.2)) =
  (x.toProd.1 * y.toProd.1) • z.toProd.2 + (x.toProd.1 * z.toProd.1) • y.toProd.2 +
        x.toProd.1 • (y.toProd.2 * z.toProd.2) +
      (y.toProd.1 * z.toProd.1) • x.toProd.2 +
    (y.toProd.1 • (x.toProd.2 * z.toProd.2) + z.toProd.1 • (x.toProd.2 * y.toProd.2) +
      x.toProd.2 * (y.toProd.2 * z.toProd.2))
Tactic: simp only [snd_mul, fst_mul, smul_add, smul_smul, add_mul, smul_mul_assoc, mul_assoc, mul_add,
        mul_smul_comm, mul_comm z.fst x.fst, mul_comm z.fst y.fst]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
⊢ HMul.hMul (α := Unitization R A)
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A)
      (inl r + (↑a : Unitization R A)) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A)
have inl_add_inr : HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
    (inl r + (↑a : Unitization R A)) =
  HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
    (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
Tactic: change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
⊢ HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A)) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
have inl_add_inr : HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      ((↑a : Unitization R A) : Unitization R A) =
  HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
    (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
Tactic: rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
⊢ HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A)) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
have inl_add_inr₁ : HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      ((↑a : Unitization R A) : Unitization R A) =
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl r)
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
Tactic: rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
inl_add_inr₁ :
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl r)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
⊢ HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A)) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
have inl_add_inr₂ : inl (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) s : R) r) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      ((↑a : Unitization R A) : Unitization R A) =
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl r)
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
Tactic: rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]