-- Mathlib/RingTheory/TensorProduct/Finite.lean
lemma RingHom.surjective_of_tmul_eq_tmul_of_finite {R S}
    [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
    (h₁ : ∀ s : S, s ⊗ₜ[R] 1 = 1 ⊗ₜ s) : Function.Surjective (algebraMap R S)

Proof state:
case tmul.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y s : S
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
⊢ R'.mkQ x ⊗ₜ[R] R'.mkQ y = 0

Tactic:
have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R S)⟩

Result:
case tmul.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y s : S
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
this : R'.mkQ 1 = 0
⊢ R'.mkQ x ⊗ₜ[R] R'.mkQ y = 0

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ 1 ⊗ₜ[R] (x * y) = x ⊗ₜ[R] y

Tactic:
trans x ⊗ₜ 1 * 1 ⊗ₜ y

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ 1 ⊗ₜ[R] (x * y) = x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y

R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y = x ⊗ₜ[R] y

Proof state:
case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
⊢ Subsingleton ((S ⧸ R') ⊗[R] (S ⧸ R'))

Tactic:
refine subsingleton_of_forall_eq 0 fun y ↦ ?_

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
y : (S ⧸ R') ⊗[R] (S ⧸ R')
⊢ y = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y

Tactic:
use x * y

Result:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ 1 ⊗ₜ[R] (x * y) = x ⊗ₜ[R] y

Proof state:
case tmul
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S ⧸ R'
⊢ x ⊗ₜ[R] y = 0

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

Result:
case tmul.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
y : S ⧸ R'
x : S
⊢ R'.mkQ x ⊗ₜ[R] y = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
⊢ Function.Surjective ⇑(algebraMap R S)

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

Result:
case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h : Subsingleton (S ⧸ R')
⊢ Function.Surjective ⇑(algebraMap R S)

case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
⊢ Function.Surjective ⇑(algebraMap R S)

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h : Subsingleton (S ⧸ R')
⊢ Function.Surjective ⇑(algebraMap R S)

Tactic:
rwa [Submodule.subsingleton_quotient_iff_eq_top, LinearMap.range_eq_top] at h

Result:
no goals

Proof state:
case tmul.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y s : S
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
this : R'.mkQ 1 = 0
⊢ R'.mkQ x ⊗ₜ[R] R'.mkQ y = 0

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

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y = x ⊗ₜ[R] y

Tactic:
simp

Result:
no goals

Proof state:
case tmul.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
y : S ⧸ R'
x : S
⊢ R'.mkQ x ⊗ₜ[R] y = 0

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

Result:
case tmul.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ R'.mkQ x ⊗ₜ[R] R'.mkQ y = 0

Proof state:
case add
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
a b : (S ⧸ R') ⊗[R] (S ⧸ R')
e₁ : a = 0
e₂ : b = 0
⊢ a + b = 0

Tactic:
rwa [e₁, zero_add]

Result:
no goals

Proof state:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
this : Subsingleton ((S ⧸ R') ⊗[R] (S ⧸ R'))
⊢ Function.Surjective ⇑(algebraMap R S)

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

Result:
no goals