awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
⊢ StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S ↔
    NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
have refine_1 : ∀ (h : StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S),
  NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
refine_1 :
  ∀ (h : StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S),
    NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
⊢ StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S ↔
    NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
have refine_2 : ∀ (h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra),
  StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
x : Unitization R A
⊢ Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R)
            (↑((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) : Unitization R A →ₐ[R] C) :
          (a : Unitization R A) → C)
        x :
      C)
have refine_2 : ∀ (r : R) (a : A),
  Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R)
            (↑((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) : Unitization R A →ₐ[R] C) :
          (a : Unitization R A) → C)
        (inl r + (↑a : Unitization R A)) :
      C)
Tactic: induction x with
    | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
c : StarSubalgebra R C
⊢ StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ c ↔
    StarAlgebra.adjoin R (↑(NonUnitalStarAlgHom.range f) : Set C) ≤ c
have rw : NonUnitalStarAlgHom.range f ≤ c.toNonUnitalStarSubalgebra ↔ (↑(NonUnitalStarAlgHom.range f) : Set C) ⊆ (↑c : Set C)
Tactic: rw [starLift_range_le, StarAlgebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
⊢ Eq (α := StarSubalgebra R A) (StarAlgHom.range (A := Unitization.{u_1, u_3} R ↥s) (unitization s))
    (StarAlgebra.adjoin R (↑s : Set A))
have rw : Eq (α := StarSubalgebra R A)
  (StarAlgebra.adjoin R
    (↑(NonUnitalStarAlgHom.range (F := ↥s →⋆ₙₐ[R] A) (NonUnitalStarSubalgebraClass.subtype s)) : Set A))
  (StarAlgebra.adjoin R (↑s : Set A))
Tactic: rw [unitization, Unitization.starLift_range]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
⊢ Eq (α := StarSubalgebra R A)
    (StarAlgebra.adjoin R
      (↑(NonUnitalStarAlgHom.range (F := ↥s →⋆ₙₐ[R] A) (NonUnitalStarSubalgebraClass.subtype s)) : Set A))
    (StarAlgebra.adjoin R (↑s : Set A))
have simp : Eq (α := StarSubalgebra R A) (StarAlgebra.adjoin R {x : A | x ∈ s}) (StarAlgebra.adjoin R (↑s : Set A))
Tactic: simp only [NonUnitalStarAlgHom.coe_range, NonUnitalStarSubalgebraClass.coe_subtype,
    Subtype.range_coe_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
⊢ Function.Bijective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))
have refine_1 : Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
  (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))
Tactic: refine ⟨?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
refine_1 :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))
⊢ Function.Bijective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))
have refine_2 : ∀ (x : ↥(StarAlgebra.adjoin R (↑s : Set A))),
  ∃ (a : Unitization.{u_1, u_3} R ↥s),
    (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x
Tactic: refine ⟨?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))
have this : Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
  (⇑(StarAlgHom.comp (StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) starAlgHom) :
    (a : Unitization R ↥s) → A)
Tactic: have := AlgHomClass.unitization_injective s h1 ((StarSubalgebra.subtype _).comp starAlgHom)
        fun _ ↦ by simp [starAlgHom]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
this :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) starAlgHom) :
      (a : Unitization R ↥s) → A)
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))
have this₁ : Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
  (Function.comp (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑(StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) : (a : ↥(StarAlgebra.adjoin R (↑s : Set A))) → A)
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))))
Tactic: rw [StarAlgHom.coe_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
x : ↥(StarAlgebra.adjoin R (↑s : Set A))
⊢ ∃ (a : Unitization.{u_1, u_3} R ↥s),
    (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x
have refine_2 : ∀ (a : Unitization.{u_1, u_3} R ↥s)
  (ha : (AlgHom.toRingHom (↑(unitization s) : Unitization R ↥s →ₐ[R] A) : (a : Unitization R ↥s) → A) a = (↑x : A)),
  ∃ (a : Unitization.{u_1, u_3} R ↥s),
    (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x
Tactic: obtain (⟨a, ha⟩ : (x : A) ∈ (unitization s).range) :=
        (unitization_range s).ge x.property
-- 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 : MulAction A M
inst_4 : SMul R M
inst_5 : IsScalarTower R A M
r : R
x : M
⊢ HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
have rw : HSMul.hSMul (β := A) r 1 • x = r • x
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- 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 : MulAction A M
inst_4 : SMul R M
inst_5 : IsScalarTower R A M
r : R
x : M
rw : HSMul.hSMul (β := A) r 1 • x = r • x
⊢ HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
have rw₁ : r • HSMul.hSMul.{w, v₁, v₁} (α := A) 1 x = r • x
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- 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 : MulAction A M
inst_4 : SMul R M
inst_5 : IsScalarTower R A M
r : R
x : M
rw : HSMul.hSMul (β := A) r 1 • x = r • x
rw₁ : r • HSMul.hSMul.{w, v₁, v₁} (α := A) 1 x = r • x
⊢ HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
have rw₂ : r • x = r • x
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- 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 : MulAction A M
inst_4 : SMul R M
h : ∀ (r : R) (x : M), HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
r : R
a : A
x : M
⊢ (r • a) • x = r • a • x
have rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • x = r • a • x
Tactic: rw [Algebra.smul_def, mul_smul, h]
-- 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 : MulAction A M
inst_4 : SMul R M
h : ∀ (r : R) (x : M), HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
r : R
a : A
x : M
rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • x = r • a • x
⊢ (r • a) • x = r • a • x
have rw₁ : HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • x) = r • a • x
Tactic: rw [Algebra.smul_def, mul_smul, h]
-- 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 : MulAction A M
inst_4 : SMul R M
h : ∀ (r : R) (x : M), HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
r : R
a : A
x : M
rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • x = r • a • x
rw₁ : HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • x) = r • a • x
⊢ (r • a) • x = r • a • x
have rw₂ : r • a • x = r • a • x
Tactic: rw [Algebra.smul_def, mul_smul, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
h :
  ∀ (x : R),
    Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
      ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
x : R
y : S
z : A
⊢ (x • y) • z = x • y • z
have simp_rw : HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) y) : A)
    z =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
    (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
Tactic: simp_rw [Algebra.smul_def, map_mul, mul_assoc, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
h :
  ∀ (x : R),
    Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
      ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
x : R
y : S
z : A
simp_rw :
  HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) y) : A)
      z =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
      (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
⊢ (x • y) • z = x • y • z
have simp_rw₁ : HMul.hMul (α := A) (β := A) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
      ((algebraMap S A : (a : S) → A) y : A) *
    z =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
    (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
Tactic: simp_rw [Algebra.smul_def, map_mul, mul_assoc, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
h :
  ∀ (x : R),
    Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
      ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
x : R
y : S
z : A
simp_rw :
  HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) y) : A)
      z =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
      (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
simp_rw₁ :
  HMul.hMul (α := A) (β := A) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
        ((algebraMap S A : (a : S) → A) y : A) *
      z =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
      (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
⊢ (x • y) • z = x • y • z
have simp_rw₂ : HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
    (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z) =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
    (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
Tactic: simp_rw [Algebra.smul_def, map_mul, mul_assoc, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
x : R
⊢ Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S) : (a : R) → A) x : A)
have simp_rw : Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
  ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
Tactic: simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
x : R
simp_rw :
  Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
⊢ Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S) : (a : R) → A) x : A)
have simp_rw₁ : HSMul.hSMul (β := A) x 1 = HSMul.hSMul (β := A) (HSMul.hSMul (β := S) x 1) 1
Tactic: simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
x : R
simp_rw :
  Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
simp_rw₁ : HSMul.hSMul (β := A) x 1 = HSMul.hSMul (β := A) (HSMul.hSMul (β := S) x 1) 1
⊢ Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S) : (a : R) → A) x : A)
have simp_rw₂ : HSMul.hSMul (β := A) x 1 = x • HSMul.hSMul.{v, w, w} (α := S) (β := A) 1 1
Tactic: simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
x : R
⊢ Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
have rw : Eq.{w + 1} (α := A)
  ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S) : (a : R) → A) x : A)
  ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
Tactic: rw [algebraMap_eq R S A, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
x : R
rw :
  Eq.{w + 1} (α := A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S) : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
⊢ Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
have rw₁ : Eq.{w + 1} (α := A) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
  ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
Tactic: rw [algebraMap_eq R S A, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S_1 : Type v
A_1 : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Semiring A_1
inst_3 : Semiring B
inst_4 : Algebra R S_1
inst_5 : Algebra S_1 A_1
inst_6 : Algebra S_1 B
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : IsScalarTower R S_1 A_1
inst_10 : IsScalarTower R S_1 B
S : Type u
A : Type v
inst_11 : CommSemiring S
inst_12 : Semiring A
h1 h2 : Algebra S A
r : S
x : A
⊢ A
have have : (I : Algebra S A) → A
Tactic: have I := h1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
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
⊢ Eq.{u₁ + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
have rw : Eq.{u₁ + 1} (α := B) ((f : (a : A) → B) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S) : A) : B)
  ((algebraMap R B : (a : R) → B) r : B)
Tactic: rw [algebraMap_apply R S A r, f.commutes, ← 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₁
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
rw :
  Eq.{u₁ + 1} (α := B)
    ((f : (a : A) → B) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S) : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
⊢ Eq.{u₁ + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
have rw₁ : Eq.{u₁ + 1} (α := B) ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S) : B)
  ((algebraMap R B : (a : R) → B) r : B)
Tactic: rw [algebraMap_apply R S A r, f.commutes, ← 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₁
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
rw :
  Eq.{u₁ + 1} (α := B)
    ((f : (a : A) → B) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S) : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
rw₁ :
  Eq.{u₁ + 1} (α := B) ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S) : B)
    ((algebraMap R B : (a : R) → B) r : B)
⊢ Eq.{u₁ + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
have rw₂ : Eq.{u₁ + 1} (α := B) ((algebraMap R B : (a : R) → B) r : B) ((algebraMap R B : (a : R) → B) r : B)
Tactic: rw [algebraMap_apply R S A r, f.commutes, ← algebraMap_apply R S B]