awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
⊢ Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)
    (((↑h.unit : End S M) : (a : M) → M) m' : M)
have rw : Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) (x • m') : M) : M)
  (((↑h.unit : End S M) : (a : M) → M) m' : M)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
⊢ m' = ((↑h.unit⁻¹ : End S M) : (a : M) → M) m
have apply_fun : Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) m' : M)
  (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)
Tactic: apply_fun (↑h.unit : M → M) using ((isUnit_iff _).mp h).injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
⊢ Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) m' : M)
    (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)
have rw : Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) m' : M)
  (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) (x • m') : M) : M)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
have rw : (f : (a : A) → B) (r • a) = HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
Tactic: rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
rw :
  (f : (a : A) → B) (r • a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
⊢ (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
have rw₁ : (f : (a : A) → B) (r • a) = HSMul.hSMul (β := B) r ((f : (a : A) → B) a : B)
Tactic: rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
rw :
  (f : (a : A) → B) (r • a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
rw₁ : (f : (a : A) → B) (r • a) = HSMul.hSMul (β := B) r ((f : (a : A) → B) a : B)
⊢ (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
have rw₂ : HSMul.hSMul (β := B) r ((f : (a : A) → B) a : B) = HSMul.hSMul (β := B) r ((f : (a : A) → B) a : B)
Tactic: rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ (f : (a : A) → B) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)
have rw : (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)
Tactic: rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
rw :
  (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)
⊢ (f : (a : A) → B) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)
have rw₁ : (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
Tactic: rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
a : A
r : R
rw :
  (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)
rw₁ :
  (f : (a : A) → B) (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) =
    HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
⊢ (f : (a : A) → B) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((algebraMap R B : (a : R) → B) r : B)
have rw₂ : HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B) =
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B) ((f : (a : A) → B) a : B)
Tactic: rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
P Q : Algebra ℕ R
⊢ P = Q
have h : ∀ (r : ℕ), Eq (α := R) ((algebraMap ℕ R : (a : ℕ) → R) r : R) ((algebraMap ℕ R : (a : ℕ) → R) r : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_3 + 1} (α := ℕ → A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Nat.cast) Nat.cast
have h : ∀ (x : ℕ),
  Eq.{u_3 + 1} (α := A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Nat.cast x) (↑x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Eq.{u_3 + 1} (α := ℤ → A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Int.cast) Int.cast
have h : ∀ (x : ℤ),
  Eq.{u_3 + 1} (α := A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Int.cast x) (↑x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ FaithfulSMul R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have rw : (Injective.{u_1 + 1, u_2 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1) ↔
  Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
rw :
  (Injective.{u_1 + 1, u_2 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1) ↔
    Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ FaithfulSMul R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have rw₁ : (Injective.{u_1 + 1, u_2 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1) ↔
  Injective.{u_1 + 1, u_2 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1
Tactic: rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
m : M
⊢ r • m = HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m
have rw : r • HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m =
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
Tactic: rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
m : M
rw :
  r • HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
⊢ r • m = HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m
have rw₁ : HSMul.hSMul (β := A) r 1 • m =
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
Tactic: rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
m : M
rw :
  r • HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₁ :
  HSMul.hSMul (β := A) r 1 • m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
⊢ r • m = HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m
have rw₂ : HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A) • m =
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
Tactic: rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
m : M
rw :
  r • HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₁ :
  HSMul.hSMul (β := A) r 1 • m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₂ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A) • m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
⊢ r • m = HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m
have rw₃ : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m =
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
Tactic: rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
m : M
rw :
  r • HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₁ :
  HSMul.hSMul (β := A) r 1 • m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₂ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A) • m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₃ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
⊢ r • m = HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m
have rw₄ : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m =
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m
Tactic: rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
a : A
m : M
⊢ r • a • m = a • r • m
have rw : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • m) = a • r • m
Tactic: rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
a : A
m : M
rw : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • m) = a • r • m
⊢ r • a • m = a • r • m
have rw₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • m = a • r • m
Tactic: rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
a : A
m : M
rw : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • m) = a • r • m
rw₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • m = a • r • m
⊢ r • a • m = a • r • m
have rw₂ : HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) • m = a • r • m
Tactic: rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
a : A
m : M
rw : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • m) = a • r • m
rw₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • m = a • r • m
rw₂ : HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) • m = a • r • m
⊢ r • a • m = a • r • m
have rw₃ : a • HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m = a • r • m
Tactic: rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
a : A
m : M
rw : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • m) = a • r • m
rw₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • m = a • r • m
rw₂ : HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) • m = a • r • m
rw₃ : a • HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m = a • r • m
⊢ r • a • m = a • r • m
have rw₄ : a • r • m = a • r • m
Tactic: rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
A_1 : Type u_2
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A_1 M
inst_5 : Module R_1 M
inst_6 : IsScalarTower R_1 A_1 M
R : Type u_4
S : Type u_5
A : Type u_6
inst_7 : CommSemiring R
inst_8 : CommSemiring S
inst_9 : Semiring A
inst_10 : Algebra R A
inst_11 : Algebra S A
r : R
s : S
a : A
⊢ r • s • a = s • r • a
have rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (s • a) = s • r • a
Tactic: rw [Algebra.smul_def, mul_smul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
A_1 : Type u_2
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A_1 M
inst_5 : Module R_1 M
inst_6 : IsScalarTower R_1 A_1 M
R : Type u_4
S : Type u_5
A : Type u_6
inst_7 : CommSemiring R
inst_8 : CommSemiring S
inst_9 : Semiring A
inst_10 : Algebra R A
inst_11 : Algebra S A
r : R
s : S
a : A
rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (s • a) = s • r • a
⊢ r • s • a = s • r • a
have rw₁ : s • HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a = s • r • a
Tactic: rw [Algebra.smul_def, mul_smul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
A_1 : Type u_2
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A_1 M
inst_5 : Module R_1 M
inst_6 : IsScalarTower R_1 A_1 M
R : Type u_4
S : Type u_5
A : Type u_6
inst_7 : CommSemiring R
inst_8 : CommSemiring S
inst_9 : Semiring A
inst_10 : Algebra R A
inst_11 : Algebra S A
r : R
s : S
a : A
rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (s • a) = s • r • a
rw₁ : s • HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a = s • r • a
⊢ r • s • a = s • r • a
have rw₂ : s • r • a = s • r • a
Tactic: rw [Algebra.smul_def, mul_smul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
inst_4 : IsDomain A
⊢ IsTorsionFree R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have rw : FaithfulSMul R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
inst_4 : IsDomain A
rw : FaithfulSMul R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ IsTorsionFree R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have rw₁ : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ↔
  Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
hf : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
r : R
h : Invertible (α := A) ((algebraMap R A : (a : R) → A) r : A)
⊢ HMul.hMul (α := B) (β := B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B)
      ((algebraMap R B : (a : R) → B) r : B) =
    1
have rw : HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B)
    ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
  1
Tactic: rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def,
    mul_invOf_self, hf]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
hf : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
r : R
h : Invertible (α := A) ((algebraMap R A : (a : R) → A) r : A)
rw :
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
⊢ HMul.hMul (α := B) (β := B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B)
      ((algebraMap R B : (a : R) → B) r : B) =
    1
have rw₁ : HSMul.hSMul (β := B) r
    ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
  1
Tactic: rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def,
    mul_invOf_self, hf]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
hf : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
r : R
h : Invertible (α := A) ((algebraMap R A : (a : R) → A) r : A)
rw :
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
rw₁ :
  HSMul.hSMul (β := B) r
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
⊢ HMul.hMul (α := B) (β := B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B)
      ((algebraMap R B : (a : R) → B) r : B) =
    1
have rw₂ : Eq.{u_3 + 1} (α := B)
  ((f : (a : A) → B)
      (HSMul.hSMul (β := A) r
        (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
    B)
  (1 : B)
Tactic: rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def,
    mul_invOf_self, hf]