-- Mathlib/RingTheory/RingHom/Surjective.lean
theorem surjective_isStableUnderBaseChange : IsStableUnderBaseChange surjective

Proof state:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, includeLeftRingHom a = x

Tactic:
induction x with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩

Result:
no goals

Proof state:
case add.intro.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x y : S
⊢ ∃ a, includeLeftRingHom a = includeLeftRingHom x + includeLeftRingHom y

Tactic:
exact ⟨x + y, map_add _ x y⟩

Result:
no goals

Proof state:
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Function.Surjective ⇑(algebraMap R T) → Function.Surjective ⇑includeLeftRingHom

Tactic:
classical
introv h x
induction x with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩

Result:
no goals

Proof state:
case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : T
⊢ ∃ a, includeLeftRingHom a = x ⊗ₜ[R] y

Tactic:
obtain ⟨y, rfl⟩ := h y

Result:
case tmul.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ ∃ a, includeLeftRingHom a = x ⊗ₜ[R] (algebraMap R T) y

Proof state:
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Function.Surjective ⇑(algebraMap R T) → Function.Surjective ⇑includeLeftRingHom

Tactic:
introv h x

Result:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, includeLeftRingHom a = x

Proof state:
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ (y • x) ⊗ₜ[R] 1 = x ⊗ₜ[R] (algebraMap R T) y

Tactic:
rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]

Result:
no goals

Proof state:
case add
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x y : S ⊗[R] T
ex : ∃ a, includeLeftRingHom a = x
ey : ∃ a, includeLeftRingHom a = y
⊢ ∃ a, includeLeftRingHom a = x + y

Tactic:
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey

Result:
case add.intro.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x y : S
⊢ ∃ a, includeLeftRingHom a = includeLeftRingHom x + includeLeftRingHom y

Proof state:
⊢ IsStableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f

Tactic:
refine IsStableUnderBaseChange.mk _ surjective_respectsIso ?_

Result:
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Function.Surjective ⇑(algebraMap R T) → Function.Surjective ⇑includeLeftRingHom

Proof state:
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ includeLeftRingHom (y • x) = x ⊗ₜ[R] (algebraMap R T) y

Tactic:
dsimp

Result:
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ (y • x) ⊗ₜ[R] 1 = x ⊗ₜ[R] (algebraMap R T) y

Proof state:
case zero
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ ∃ a, includeLeftRingHom a = 0

Tactic:
exact ⟨0, map_zero _⟩

Result:
no goals

Proof state:
case tmul.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ ∃ a, includeLeftRingHom a = x ⊗ₜ[R] (algebraMap R T) y

Tactic:
use y • x

Result:
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ includeLeftRingHom (y • x) = x ⊗ₜ[R] (algebraMap R T) y