awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A)
        (@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]
-- 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
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)
rw₃ :
  Eq.{u_3 + 1} (α := B)
    ((f : (a : A) → B)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A)
          (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
      B)
    (1 : B)
rw₄ : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
⊢ 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) 1 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)
⊢ 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
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.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 :
  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) ((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
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.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 :
  HSMul.hSMul (β := B) r
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
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)
⊢ 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
have rw₂ : Eq.{u_3 + 1} (α := B)
  ((f : (a : A) → B)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A)
        (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
    B)
  (1 : B)
Tactic: rw [← 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 :
  HSMul.hSMul (β := B) r
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
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)
rw₂ :
  Eq.{u_3 + 1} (α := B)
    ((f : (a : A) → B)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A)
          (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
      B)
    (1 : B)
rw₃ : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
⊢ 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
have rw₄ : Eq.{u_3 + 1} (α := B) 1 1
Tactic: rw [← Algebra.smul_def, ← map_smul, Algebra.smul_def, mul_invOf_self, hf]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₃ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E)
  ((b : (a : F) → E) (HSMul.hSMul (β := F) y 1) : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E)
    ((b : (a : F) → E) (HSMul.hSMul (β := F) y 1) : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₄ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = (b : (a : F) → E) (HSMul.hSMul (β := F) y 1)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E)
    ((b : (a : F) → E) (HSMul.hSMul (β := F) y 1) : E)
rw₄ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = (b : (a : F) → E) (HSMul.hSMul (β := F) y 1)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₅ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E)
    ((b : (a : F) → E) (HSMul.hSMul (β := F) y 1) : E)
rw₄ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = (b : (a : F) → E) (HSMul.hSMul (β := F) y 1)
rw₅ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₆ : HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) x : E) ((b : (a : F) → E) 1 : E) =
  HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E)
    ((b : (a : F) → E) (HSMul.hSMul (β := F) y 1) : E)
rw₄ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = (b : (a : F) → E) (HSMul.hSMul (β := F) y 1)
rw₅ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
rw₆ :
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) x : E) ((b : (a : F) → E) 1 : E) =
    HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₇ : HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) x : E) ((b : (a : F) → E) 1 : E) =
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) y : E) ((b : (a : F) → E) 1 : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E)
    ((b : (a : F) → E) (HSMul.hSMul (β := F) y 1) : E)
rw₄ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = (b : (a : F) → E) (HSMul.hSMul (β := F) y 1)
rw₅ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
rw₆ :
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) x : E) ((b : (a : F) → E) 1 : E) =
    HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
rw₇ :
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) x : E) ((b : (a : F) → E) 1 : E) =
    HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) y : E) ((b : (a : F) → E) 1 : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)
have rw₈ : HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) y : E) ((b : (a : F) → E) 1 : E) =
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) y : E) ((b : (a : F) → E) 1 : E)
Tactic: rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
-- 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 : E
⊢ ∃ (a : F), (algebraMap F E : (a : F) → E) a = x
have obtain : ∀ (x : F), ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)
Tactic: obtain ⟨x, rfl⟩ := hb x
Cleared hypotheses: x
-- 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 : F
⊢ ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)
have obtain : ∀ (y : F) (hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
  ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)
Tactic: obtain ⟨y, hy⟩ := hb (b 1 * b 1)
-- 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 : F
hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
⊢ ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)
have refine : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: refine ⟨x * y, ?_⟩
-- 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 : F
hy : (b : (a : F) → E) y = 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)
have obtain : ∀ (z : F) (hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: obtain ⟨z, hz⟩ := hb 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (hypothesis)
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 : F
hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have 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)
Tactic: apply_fun (x • z • ·) 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)
⊢ 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) (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)
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)
⊢ 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) (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)
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