awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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₂ : HMul.hMul (β := A) (x * 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]
-- 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 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x : R
y z : A
⊢ (x • y) • z = x • y • z
have rw : x • y * z = x • y • z
Tactic: rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]
-- 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 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x : R
y z : A
rw : x • y * z = x • y • z
⊢ (x • y) • z = x • y • z
have rw₁ : x • y * z = x • (y * z)
Tactic: rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]
-- 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 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x : R
y z : A
rw : x • y * z = x • y • z
rw₁ : x • y * z = x • (y * z)
⊢ (x • y) • z = x • y • z
have rw₂ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) y * z = x • (y * z)
Tactic: rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]
-- 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 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x : R
y z : A
rw : x • y * z = x • y • z
rw₁ : x • y * z = x • (y * z)
rw₂ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) y * z = x • (y * z)
⊢ (x • y) • z = x • y • z
have rw₃ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) y * z =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) (y * z)
Tactic: rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]
-- 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 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x : R
y z : A
rw : x • y * z = x • y • z
rw₁ : x • y * z = x • (y * z)
rw₂ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) y * z = x • (y * z)
rw₃ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) y * z =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) (y * z)
⊢ (x • y) • z = x • y • z
have rw₄ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) (y * z) =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) (y * z)
Tactic: rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, 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
s : R
x y : A
⊢ x * s • y = s • (x * y)
have rw : x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) y = s • (x * y)
Tactic: rw [smul_def, smul_def, left_comm]
-- 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
s : R
x y : A
rw : x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) y = s • (x * y)
⊢ x * s • y = s • (x * y)
have rw₁ : x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) y =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) (x * y)
Tactic: rw [smul_def, smul_def, left_comm]
-- 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
s : R
x y : A
rw : x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) y = s • (x * y)
rw₁ :
  x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) (x * y)
⊢ x * s • y = s • (x * y)
have rw₂ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) (x * y) =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) (x * y)
Tactic: rw [smul_def, smul_def, left_comm]
-- 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
α : Type u_2
inst_3 : Monoid α
inst_4 : MulDistribMulAction α A
inst_5 : SMulCommClass α R A
a : α
r : R
⊢ HSMul.hSMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) r
have rw : a • HSMul.hSMul (β := A) r 1 = HSMul.hSMul (β := A) r 1
Tactic: rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]
-- 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
α : Type u_2
inst_3 : Monoid α
inst_4 : MulDistribMulAction α A
inst_5 : SMulCommClass α R A
a : α
r : R
rw : a • HSMul.hSMul (β := A) r 1 = HSMul.hSMul (β := A) r 1
⊢ HSMul.hSMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) r
have rw₁ : r • HSMul.hSMul (β := A) a 1 = HSMul.hSMul (β := A) r 1
Tactic: rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]
-- 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
α : Type u_2
inst_3 : Monoid α
inst_4 : MulDistribMulAction α A
inst_5 : SMulCommClass α R A
a : α
r : R
rw : a • HSMul.hSMul (β := A) r 1 = HSMul.hSMul (β := A) r 1
rw₁ : r • HSMul.hSMul (β := A) a 1 = HSMul.hSMul (β := A) r 1
⊢ HSMul.hSMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) r
have rw₂ : HSMul.hSMul (β := A) r 1 = HSMul.hSMul (β := A) r 1
Tactic: rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Algebra.IsEpi R A ↔ ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
have refine : ∀ (h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) (x y : A ⊗[R] A)
  (hxy :
    Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
      ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)),
  x = y
Tactic: refine ⟨fun h a ↦ IsEpi.injective_lift_mul <| by simp, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
⊢ ∃ (a : A), Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) (a ⊗ₜ[R] 1)
have h₁ : Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) ((u * v) ⊗ₜ[R] 1)
Tactic: use u * v
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
⊢ HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v) = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1)
have rw : HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1) = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
⊢ Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) ((u * v) ⊗ₜ[R] 1)
have calc : u ⊗ₜ[R] v = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v)
Tactic: calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
calc : u ⊗ₜ[R] v = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v)
⊢ Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) ((u * v) ⊗ₜ[R] 1)
have calc₁ : HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v) = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1)
Tactic: calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
calc : u ⊗ₜ[R] v = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v)
calc₁ : HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v) = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1)
⊢ Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) ((u * v) ⊗ₜ[R] 1)
have calc₂ : HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1) = (u * v) ⊗ₜ[R] 1
Tactic: calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A ⊗[R] A
hu : ∃ (a : A), u = a ⊗ₜ[R] 1
hv : ∃ (a : A), v = a ⊗ₜ[R] 1
⊢ ∃ (a : A), u + v = a ⊗ₜ[R] 1
have add : ∀ (u : A), ∃ (a : A), u ⊗ₜ[R] 1 + v = a ⊗ₜ[R] 1
Tactic: obtain ⟨u, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x_1 y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x_1 : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
x : A ⊗[R] A
⊢ ∃ (a : A), x = a ⊗ₜ[R] 1
have zero : ∃ (a : A), Eq (α := A ⊗[R] A) 0 (a ⊗ₜ[R] 1)
Tactic: induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x_1 y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x_1 : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
x : A ⊗[R] A
zero : ∃ (a : A), Eq (α := A ⊗[R] A) 0 (a ⊗ₜ[R] 1)
⊢ ∃ (a : A), x = a ⊗ₜ[R] 1
have tmul : ∀ (u v : A), ∃ (a : A), Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) (a ⊗ₜ[R] 1)
Tactic: induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x_1 y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x_1 : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
x : A ⊗[R] A
zero : ∃ (a : A), Eq (α := A ⊗[R] A) 0 (a ⊗ₜ[R] 1)
tmul : ∀ (u v : A), ∃ (a : A), Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) (a ⊗ₜ[R] 1)
⊢ ∃ (a : A), x = a ⊗ₜ[R] 1
have add : ∀ (u v : A ⊗[R] A) (hu : ∃ (a : A), u = a ⊗ₜ[R] 1) (hv : ∃ (a : A), v = a ⊗ₜ[R] 1), ∃ (a : A), u + v = a ⊗ₜ[R] 1
Tactic: induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
⊢ x = y
have h' : ∀ (x : A ⊗[R] A), ∃ (a : A), x = a ⊗ₜ[R] 1
Tactic: have h' (x : A ⊗[R] A) : ∃ a : A, x = a ⊗ₜ 1 := by
    induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
h' : ∀ (x : A ⊗[R] A), ∃ (a : A), x = a ⊗ₜ[R] 1
⊢ x = y
have obtain : ∀ (a : A)
  (hxy :
    Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)
      ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)),
  a ⊗ₜ[R] 1 = y
Tactic: obtain ⟨a, rfl⟩ := h' x
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
y : A ⊗[R] A
h' : ∀ (x : A ⊗[R] A), ∃ (a : A), x = a ⊗ₜ[R] 1
a : A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
⊢ a ⊗ₜ[R] 1 = y
have obtain : ∀ (b : A)
  (hxy :
    Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)
      ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (b ⊗ₜ[R] 1) : A)),
  Eq (α := A ⊗[R] A) (a ⊗ₜ[R] 1) (b ⊗ₜ[R] 1)
Tactic: obtain ⟨b, rfl⟩ := h' y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Algebra.IsEpi R A
have refine : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
Tactic: refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
have obtain : ∀ (r : R),
  Eq.{u_2 + 1} (α := A ⊗[R] A) (1 ⊗ₜ[R] (algebraMap R A : (a : R) → A) r : A ⊗[R] A)
    ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] A)
Tactic: obtain ⟨r, rfl⟩ := h a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : R
⊢ Eq.{u_2 + 1} (α := A ⊗[R] A) (1 ⊗ₜ[R] (algebraMap R A : (a : R) → A) r : A ⊗[R] A)
    ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] A)
have rw : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HSMul.hSMul (β := A) r 1) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1)
Tactic: rw [algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : R
rw : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HSMul.hSMul (β := A) r 1) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1)
⊢ Eq.{u_2 + 1} (α := A ⊗[R] A) (1 ⊗ₜ[R] (algebraMap R A : (a : R) → A) r : A ⊗[R] A)
    ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] A)
have rw₁ : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HSMul.hSMul (β := A) r 1) (1 ⊗ₜ[R] HSMul.hSMul (β := A) r 1)
Tactic: rw [algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
⊢ Algebra.IsEpi R A
have refine : ∀ (x : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1)
Tactic: refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
x : A
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1)
have obtain : ∀ (a b : R) (hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b),
  Eq (α := A ⊗[R] A)
    (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A) ⊗ₜ[R] 1)
Tactic: obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective R x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
⊢ Eq (α := A ⊗[R] A)
    (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A) ⊗ₜ[R] 1)
have set : let f : R →+* A := algebraMap R A;
∀ (hf : f = algebraMap R A),
  Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R] 1)
Tactic: set f := algebraMap R A with hf
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R] 1)
have hb₁ : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
Tactic: replace hb : f b ≠ 0 := by aesop
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
    (1 ⊗ₜ[R] (a • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
have rw : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
  (1 ⊗ₜ[R] HDiv.hDiv (β := A) (HSMul.hSMul (β := A) a 1) ((f : (a : R) → A) b : A))
Tactic: rw [← smul_div_assoc, algebraMap_eq_smul_one a]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
rw :
  Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
    (1 ⊗ₜ[R] HDiv.hDiv (β := A) (HSMul.hSMul (β := A) a 1) ((f : (a : R) → A) b : A))
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
    (1 ⊗ₜ[R] (a • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
have rw₁ : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (β := A) (HSMul.hSMul (β := A) a 1) ((f : (a : R) → A) b : A))
  (1 ⊗ₜ[R] HDiv.hDiv (β := A) (HSMul.hSMul (β := A) a 1) ((f : (a : R) → A) b : A))
Tactic: rw [← smul_div_assoc, algebraMap_eq_smul_one a]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] (a • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)) : A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
have rw : Eq (α := A ⊗[R] A) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
  ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
Tactic: rw [← smul_tmul, algebraMap_eq_smul_one a]