awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (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))
⊢ 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))
  (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
Tactic: rw [← smul_tmul, 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)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
      A ⊗[R] A)
have rw : Eq (α := A ⊗[R] A) ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) b : A)
        (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
      HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
    A ⊗[R] A)
Tactic: rw [smul_def, mul_div_cancel₀ _ 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)
rw :
  Eq (α := A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) b : A)
          (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
      A ⊗[R] A)
⊢ Eq (α := A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
      A ⊗[R] A)
have rw₁ : Eq (α := A ⊗[R] A) ((f : (a : R) → A) a ⊗ₜ[R] 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)
Tactic: rw [smul_def, mul_div_cancel₀ _ 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)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
      HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
have rw : Eq (α := A ⊗[R] A)
  (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
    (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
  (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
    (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
Tactic: rw [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
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)
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      (b • HDiv.hDiv (α := A) (β := A) (1 : 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 rw : Eq (α := A ⊗[R] A)
  (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) b : A)
      (HDiv.hDiv (α := A) (β := A) (1 : 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: rw [smul_def, mul_div_cancel₀ _ 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)
rw :
  Eq (α := A ⊗[R] A)
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) b : A)
        (HDiv.hDiv (α := A) (β := A) (1 : 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)
⊢ Eq (α := A ⊗[R] A)
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      (b • HDiv.hDiv (α := A) (β := A) (1 : 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 rw₁ : Eq (α := A ⊗[R] A) (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R] 1)
  (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R] 1)
Tactic: rw [smul_def, mul_div_cancel₀ _ 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))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R] 1)
have calc : 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)))
Tactic: calc 1 ⊗ₜ[R] (f a / f b)
       = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a]
     _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a]
     _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb]
     _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul]
     _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ 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)
calc :
  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)))
⊢ 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 calc₁ : 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)
Tactic: calc 1 ⊗ₜ[R] (f a / f b)
       = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a]
     _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a]
     _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb]
     _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul]
     _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ 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)
calc :
  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)))
calc₁ :
  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)
⊢ 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 calc₂ : Eq (α := A ⊗[R] A) ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
  ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
      HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
    A ⊗[R] A)
Tactic: calc 1 ⊗ₜ[R] (f a / f b)
       = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a]
     _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a]
     _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb]
     _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul]
     _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ 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)
calc :
  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)))
calc₁ :
  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)
calc₂ :
  Eq (α := A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
      A ⊗[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 calc₃ : Eq (α := A ⊗[R] A)
  ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
    HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
  (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
    (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
Tactic: calc 1 ⊗ₜ[R] (f a / f b)
       = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a]
     _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a]
     _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb]
     _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul]
     _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ 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)
calc :
  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)))
calc₁ :
  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)
calc₂ :
  Eq (α := A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
      A ⊗[R] A)
calc₃ :
  Eq (α := A ⊗[R] A)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
      HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((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))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R] 1)
have calc₄ : Eq (α := A ⊗[R] A)
  (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
    (b • HDiv.hDiv (α := A) (β := A) (1 : 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: calc 1 ⊗ₜ[R] (f a / f b)
       = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a]
     _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a]
     _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb]
     _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul]
     _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ 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 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
⊢ Algebra.IsEpi R A ↔ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have refine : ∀ (h : Algebra.IsEpi R A), Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: refine ⟨fun h ↦ ?_, isEpi_of_surjective_algebraMap R 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 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have inl : ∀ (h : Subsingleton.{u_2 + 1} (A ⧸ R')),
  Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rcases subsingleton_or_nontrivial (A ⧸ R') with h | _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
inl :
  ∀ (h : Subsingleton.{u_2 + 1} (A ⧸ R')),
    Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have inr : Nontrivial.{u_2} (A ⧸ R') → Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rcases subsingleton_or_nontrivial (A ⧸ R') with h | _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h_1 : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h : Subsingleton.{u_2 + 1} (A ⧸ R')
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have inl : ∀ (h : R' = ⊤), Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rwa [Submodule.Quotient.subsingleton_iff, LinearMap.range_eq_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h_1 : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h : Subsingleton.{u_2 + 1} (A ⧸ R')
inl : ∀ (h : R' = ⊤), Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have inl₁ : ∀ (h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(Algebra.linearMap R A) : (a : R) → A)),
  Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rwa [Submodule.Quotient.subsingleton_iff, LinearMap.range_eq_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
⊢ Subsingleton.{u_2 + 1} ((A ⧸ R') ⊗[R] (A ⧸ R'))
have refine : ∀ (y : (A ⧸ R') ⊗[R] (A ⧸ R')), y = 0
Tactic: refine subsingleton_of_forall_eq 0 fun y ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
a b : (A ⧸ R') ⊗[R] (A ⧸ R')
e₁ : a = 0
e₂ : b = 0
⊢ a + b = 0
have add : 0 + b = 0
Tactic: rwa [e₁, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y : A ⧸ R'
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) (x ⊗ₜ[R] y) 0
have tmul : ∀ (x : A),
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: obtain ⟨x, rfl⟩ := R'.mkQ_surjective 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 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
y : A ⧸ R'
x : A
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have tmul : ∀ (y : A),
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y : A
⊢ ∃ (s : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)
have h₁ : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] (x * y)) (x ⊗ₜ[R] y)
Tactic: use x * y
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y : A
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] (x * y)) (x ⊗ₜ[R] y)
have trans : 1 ⊗ₜ[R] (x * y) = HMul.hMul (α := A ⊗[R] A) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y)
Tactic: trans x ⊗ₜ 1 * 1 ⊗ₜ y
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y : A
trans : 1 ⊗ₜ[R] (x * y) = HMul.hMul (α := A ⊗[R] A) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y)
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] (x * y)) (x ⊗ₜ[R] y)
have trans₁ : HMul.hMul (α := A ⊗[R] A) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y) = x ⊗ₜ[R] y
Tactic: trans x ⊗ₜ 1 * 1 ⊗ₜ y
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y : A
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have tmul : ∀ (s : A) (hs : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)),
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by
        use x * y
        trans x ⊗ₜ 1 * 1 ⊗ₜ y
        · simp [(isEpi_iff_forall_one_tmul_eq R A).mp]
        · simp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y s : A
hs : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have this : Eq.{u_2 + 1} (α := A ⧸ R') ((R'.mkQ : (a : A) → A ⧸ R') 1) 0
Tactic: have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R 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 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y s : A
hs : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)
this : Eq.{u_2 + 1} (α := A ⧸ R') ((R'.mkQ : (a : A) → A ⧸ R') 1) 0
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have tmul : Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
  (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R') (N₂ :=
            A ⧸ R') R'.mkQ R'.mkQ :
          A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
        (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
      (x ⊗ₜ[R] y) :
    (A ⧸ R') ⊗[R] (A ⧸ R'))
  (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]