awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Epi
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)
rw₁ 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)
⊢ 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:
rw [smul_def, mul_div_cancel₀ _ hb]

Premises used: mul_div_cancel₀, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Epi
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)))
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)
⊢ 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:
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]

Premises used: HDiv.hDiv, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Epi
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)

Tactic:
⟨fun h ↦ ?_, isEpi_of_surjective_algebraMap R A⟩

Premises used: Algebra.isEpi_of_surjective_algebraMap, Iff.intro
-- Module: Mathlib.Algebra.Algebra.Epi
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
refine : ∀ (h : Algebra.IsEpi R A), Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ 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⟩
-- Module: Mathlib.Algebra.Algebra.Epi
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)
inr : Nontrivial.{u_2} (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)

Tactic:
rcases subsingleton_or_nontrivial (A ⧸ R') with h | _

Premises used: subsingleton_or_nontrivial, HasQuotient.Quotient
-- Module: Mathlib.Algebra.Algebra.Epi
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)
inl₁ inl₂ inl₃ 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)
⊢ 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

Premises used: LinearMap.range_eq_top, Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.Algebra.Algebra.Epi
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'))

Tactic:
subsingleton_of_forall_eq 0 fun y ↦ ?_

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Epi
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')
refine : ∀ (y : (A ⧸ R') ⊗[R] (A ⧸ R')), y = 0
⊢ Subsingleton.{u_2 + 1} ((A ⧸ R') ⊗[R] (A ⧸ R'))

Tactic:
refine subsingleton_of_forall_eq 0 fun y ↦ ?_

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Epi
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')
⊢ Eq.{u_2 + 1} (α := (A ⧸ R') ⊗[R] (A ⧸ R')) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Epi
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
add : 0 + b = 0
add₁ add₂ add₃ add₄ : b = 0
⊢ a + b = 0

Tactic:
rwa [e₁, zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Algebra.Epi
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'
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'))
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) (x ⊗ₜ[R] y) 0

Tactic:
obtain ⟨x, rfl⟩ := R'.mkQ_surjective x

Premises used: Submodule.mkQ_surjective, rfl
-- Module: Mathlib.Algebra.Algebra.Epi
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
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'))
⊢ 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 ⟨y, rfl⟩ := R'.mkQ_surjective y

Premises used: Submodule.mkQ_surjective, rfl
-- Module: Mathlib.Algebra.Algebra.Epi
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
h₁ : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] (x * y)) (x ⊗ₜ[R] y)
⊢ ∃ (s : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)

Tactic:
use x * y
-- Module: Mathlib.Algebra.Algebra.Epi
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)
trans₁ : HMul.hMul (α := A ⊗[R] A) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y) = x ⊗ₜ[R] y
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] (x * y)) (x ⊗ₜ[R] y)

Tactic:
trans x ⊗ₜ 1 * 1 ⊗ₜ y
-- Module: Mathlib.Algebra.Algebra.Epi
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
⊢ 1 ⊗ₜ[R] (x * y) = HMul.hMul (α := A ⊗[R] A) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y)

Tactic:
simp [(isEpi_iff_forall_one_tmul_eq R A).mp]

Premises used: Iff.mp, Algebra.isEpi_iff_forall_one_tmul_eq
-- Module: Mathlib.Algebra.Algebra.Epi
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
⊢ HMul.hMul (α := A ⊗[R] A) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y) = x ⊗ₜ[R] y

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Epi
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
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'))
⊢ 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
-- Module: Mathlib.Algebra.Algebra.Epi
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.{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)⟩
-- Module: Mathlib.Algebra.Algebra.Epi
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
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'))
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'))
        (1 ⊗ₜ[R] s) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₂ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') 1 ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') s : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₃ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) (0 ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') s : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₄ tmul₅ : Eq.{u_2 + 1} (α := (A ⧸ R') ⊗[R] (A ⧸ R')) 0 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'))

Tactic:
rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]

Premises used: TensorProduct.zero_tmul, TensorProduct.map_tmul, Submodule.mkQ
-- Module: Mathlib.Algebra.Algebra.Epi
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') ⊗[R] (A ⧸ R')
zero : Eq.{u_2 + 1} (α := (A ⧸ R') ⊗[R] (A ⧸ R')) 0 0
add : ∀ (a b : (A ⧸ R') ⊗[R] (A ⧸ R')) (e₁ : a = 0) (e₂ : b = 0), a + b = 0
tmul : ∀ (x y : A ⧸ R'), Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) (x ⊗ₜ[R] y) 0
⊢ y = 0

Tactic:
induction y with
    | zero => rfl
    | add a b e₁ e₂ => rwa [e₁, zero_add]
    | tmul x y =>
      obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
      obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
      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
      have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩
      rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]

Premises used: zero_add, TensorProduct.zero_tmul, TensorProduct.map_tmul, Submodule.mkQ, TensorProduct.tmul, rfl
-- Module: Mathlib.Algebra.Algebra.Epi
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'))

Tactic:
have : Subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R')) := by
    refine subsingleton_of_forall_eq 0 fun y ↦ ?_
    induction y with
    | zero => rfl
    | add a b e₁ e₂ => rwa [e₁, zero_add]
    | tmul x y =>
      obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
      obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
      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
      have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩
      rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
-- Module: Mathlib.Algebra.Algebra.Epi
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')
this : Subsingleton.{u_2 + 1} ((A ⧸ R') ⊗[R] (A ⧸ R'))
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
cases false_of_nontrivial_of_subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R'))

Premises used: false_of_nontrivial_of_subsingleton, HasQuotient.Quotient, TensorProduct
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a_1 b_1 a b : A
rw rw₁ : HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b)
⊢ a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b)

Tactic:
rw [tmul_eq_smul_one_tmul]

Premises used: TensorProduct.tmul_eq_smul_one_tmul
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a_1 b_1 a b : A
rw rw₁ : HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1) = HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1)
⊢ HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1)

Tactic:
rw [(isEpi_iff_forall_one_tmul_eq R A).mp inferInstance b]

Premises used: inferInstance, Iff.mp, Algebra.isEpi_iff_forall_one_tmul_eq
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a_1 b_1 a b : A
rw rw₁ : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
⊢ HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1) = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)

Tactic:
rw [tmul_eq_smul_one_tmul]

Premises used: TensorProduct.tmul_eq_smul_one_tmul
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a b : A
⊢ ∀ (a b : A), a ⊗ₜ[R] b = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)

Tactic:
have (a b : A) := calc a ⊗ₜ[R] b
      = a • (1 ⊗ₜ[R] b) := by rw [tmul_eq_smul_one_tmul]
    _ = a • (b ⊗ₜ[R] 1) := by rw [(isEpi_iff_forall_one_tmul_eq R A).mp inferInstance b]
    _ = a • (b • (1 ⊗ₜ[R] 1)) := by rw [tmul_eq_smul_one_tmul]
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
rw : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = b ⊗ₜ[R] a
rw₁ : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = b • HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] 1)
rw₂ rw₃ : b • HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] 1) = b • HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] 1)
⊢ Eq (α := A ⊗[R] A) (a ⊗ₜ[R] b) (b ⊗ₜ[R] a)

Tactic:
rw [this a b, this b a, smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
this : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
f : M →ₗ[R] A ⊗[R] M := { toFun := fun (m : M) ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
a :
  ∀ (a : A) (m : M),
    Eq (α := A ⊗[R] M)
      (((((AlgebraTensorModule.curry (f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) :
                    A →ₗ[R] M →ₗ[R] A ⊗[R] M) :
                  (a : A) → M →ₗ[R] A ⊗[R] M)
                a :
              M →ₗ[R] A ⊗[R] M) :
            (a : M) → A ⊗[R] M)
          m :
        A ⊗[R] M)
      (((((AlgebraTensorModule.curry LinearMap.id : A →ₗ[R] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) a :
              M →ₗ[R] A ⊗[R] M) :
            (a : M) → A ⊗[R] M)
          m :
        A ⊗[R] M)
⊢ f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = LinearMap.id

Tactic:
ext a m
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
this : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
f : M →ₗ[R] A ⊗[R] M := { toFun := fun (m : M) ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
a : A
m : M
⊢ Eq (α := A ⊗[R] M)
    (((((AlgebraTensorModule.curry (f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) :
                  A →ₗ[R] M →ₗ[R] A ⊗[R] M) :
                (a : A) → M →ₗ[R] A ⊗[R] M)
              a :
            M →ₗ[R] A ⊗[R] M) :
          (a : M) → A ⊗[R] M)
        m :
      A ⊗[R] M)
    (((((AlgebraTensorModule.curry LinearMap.id : A →ₗ[R] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) a :
            M →ₗ[R] A ⊗[R] M) :
          (a : M) → A ⊗[R] M)
        m :
      A ⊗[R] M)

Tactic:
simpa using this a m
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
this : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
f : M →ₗ[R] A ⊗[R] M := { toFun := fun (m : M) ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = LinearMap.id

Tactic:
have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by
      ext a m; simpa using this a m
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
this : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
f : M →ₗ[R] A ⊗[R] M := { toFun := fun (m : M) ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
aux : f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = LinearMap.id
⊢ Injective (α := A ⊗[R] M) (β := M)
    (⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) : (a : A ⊗[R] M) → M)

Tactic:
HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩

Premises used: Function.HasLeftInverse.injective, congrArg, id, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
this : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
f : M →ₗ[R] A ⊗[R] M := { toFun := fun (m : M) ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
aux : f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = LinearMap.id
⊢ Injective (α := A ⊗[R] M) (β := M)
    (⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) : (a : A ⊗[R] M) → M)

Tactic:
exact HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩

Premises used: Function.HasLeftInverse.injective, congrArg, id, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
suffices : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
⊢ Injective (α := A ⊗[R] M) (β := M)
    (⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) : (a : A ⊗[R] M) → M)

Tactic:
suffices ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m by
    let f : M →ₗ[R] A ⊗[R] M :=
      { toFun m := 1 ⊗ₜ m
        map_add' m n := tmul_add _ _ _
        map_smul' r m := tmul_smul _ _ _ }
    have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by
      ext a m; simpa using this a m
    exact HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩