awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
hy :
  x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
rwa :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z • y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₁ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z * y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have rwa₂ : ∀
  (hy :
    HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
      x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
hy :
  x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
rwa :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z • y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₁ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z * y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₂ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have rwa₃ : ∀
  (hy :
    HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
      x • HMul.hMul (β := E) (HSMul.hSMul (β := E) z ((b : (a : F) → E) 1 : E)) ((b : (a : F) → E) 1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
hy :
  x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
rwa :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z • y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₁ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z * y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₂ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₃ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (β := E) (HSMul.hSMul (β := E) z ((b : (a : F) → E) 1 : E)) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have rwa₄ : ∀
  (hy :
    HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
      x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) z 1) : E) ((b : (a : F) → E) 1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
hy :
  x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
rwa :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z • y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₁ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z * y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₂ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₃ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (β := E) (HSMul.hSMul (β := E) z ((b : (a : F) → E) 1 : E)) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₄ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) z 1) : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have rwa₅ : ∀
  (hy :
    HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
      x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (z * 1) : E) ((b : (a : F) → E) 1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
hy :
  x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
rwa :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z • y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₁ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z * y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₂ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₃ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (β := E) (HSMul.hSMul (β := E) z ((b : (a : F) → E) 1 : E)) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₄ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) z 1) : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₅ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (z * 1) : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have rwa₆ : ∀
  (hy :
    HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
      x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) z : E) ((b : (a : F) → E) 1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
hy :
  x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
rwa :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z • y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₁ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z * y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₂ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₃ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (β := E) (HSMul.hSMul (β := E) z ((b : (a : F) → E) 1 : E)) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₄ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) z 1) : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₅ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (z * 1) : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₆ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) z : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have rwa₇ : ∀
  (hy :
    HSMul.hSMul (β := E) x ((b : (a : F) → E) (y • z) : E) =
      x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) z : E) ((b : (a : F) → E) 1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M →ₗ[R] N
r : S
x : M
⊢ f.toFun (r • x) = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) (f.toFun x)
have obtain : ∀ (r : R),
  f.toFun (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) r : S) : S) (f.toFun x)
Tactic: obtain ⟨r, rfl⟩ := h r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M ≃ₗ[R] N
r : S
x : M
⊢ (↑f : M →ₗ[R] N).toFun (r • x) = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) ((↑f : M →ₗ[R] N).toFun x)
have obtain : ∀ (r : R),
  (↑f : M →ₗ[R] N).toFun (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) r : S) : S)
      ((↑f : M →ₗ[R] N).toFun x)
Tactic: obtain ⟨r, rfl⟩ := h r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ HSMul.hSMul (β := A) r 1 * x = r • x
have rw : r • (1 * x) = r • x
Tactic: rw [h₁, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
rw : r • (1 * x) = r • x
⊢ HSMul.hSMul (β := A) r 1 * x = r • x
have rw₁ : r • x = r • x
Tactic: rw [h₁, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ x * HSMul.hSMul (β := A) r 1 = r • x
have rw : r • (x * 1) = r • x
Tactic: rw [h₂, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
rw : r • (x * 1) = r • x
⊢ x * HSMul.hSMul (β := A) r 1 = r • x
have rw₁ : r • x = r • x
Tactic: rw [h₂, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : ∀ (r : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) r : A)
⊢ P = Q
have h₁ : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
Tactic: replace h : P.algebraMap = Q.algebraMap := DFunLike.ext _ _ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
⊢ Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2
have h₁ : ∀ (r : R) (a : A), r • a = r • a
Tactic: funext r a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
r : R
a : A
⊢ r • a = r • a
have h₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a = r • a
Tactic: rw [P.smul_def', Q.smul_def', h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
r : R
a : A
h₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a = r • a
⊢ r • a = r • a
have h₂ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a
Tactic: rw [P.smul_def', Q.smul_def', h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
r : R
a : A
h₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a = r • a
h₂ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a
⊢ r • a = r • a
have h₃ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a
Tactic: rw [P.smul_def', Q.smul_def', h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
⊢ P = Q
have h' : Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2
Tactic: have h' : (haveI := P; (· • ·) : R → A → A) = (haveI := Q; (· • ·) : R → A → A) := by
    funext r a
    rw [P.smul_def', Q.smul_def', h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
h' : Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2
⊢ P = Q
have rcases : ∀ (algebraMap : R →+* A)
  (commutes' :
    ∀ (r : R) (x : A),
      HMul.hMul (α := A) ((algebraMap : (a : R) → A) r : A) x = HMul.hMul (β := A) x ((algebraMap : (a : R) → A) r : A))
  (P : R → A → A) (smul_def' : ∀ (r : R) (x : A), r • x = HMul.hMul (α := A) ((algebraMap : (a : R) → A) r : A) x)
  (h : Eq (α := R →+* A) (Algebra.algebraMap R A) (Algebra.algebraMap R A))
  (h' : Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2),
  { smul := P, algebraMap := algebraMap, commutes' := commutes', smul_def' := smul_def' : Algebra R A } = Q
Tactic: rcases P with @⟨⟨P⟩⟩
Cleared hypotheses: P, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
y : A
⊢ x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
have rw : HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) * y =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
Tactic: rw [← mul_assoc, ← commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
y : A
rw :
  HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) * y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
⊢ x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
have rw₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x * y =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
Tactic: rw [← mul_assoc, ← commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
y : A
rw :
  HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) * y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
rw₁ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x * y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
⊢ x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
have rw₂ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y) =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
Tactic: rw [← mul_assoc, ← commutes, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
y : A
⊢ HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) * y =
    HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
have rw : x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
  HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
Tactic: rw [mul_assoc, commutes, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Defs (goal)
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
y : A
rw :
  x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
⊢ HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) * y =
    HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
have rw₁ : x * HMul.hMul (β := A) y ((algebraMap R A : (a : R) → A) r : A) =
  HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
Tactic: rw [mul_assoc, commutes, ← mul_assoc]