Theorem: Algebra.baseChange_bot (DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean)

State before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
⊢ Subalgebra.toSubmodule ⊥ = LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
Tactic:
ext x
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ x ∈ Subalgebra.toSubmodule ⊥ ↔ x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ x ∈ Subalgebra.toSubmodule ⊥ ↔ x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
Tactic:
simp only [Subalgebra.mem_toSubmodule, Algebra.mem_bot]
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ x ∈ Set.range ⇑(algebraMap R (R ⊗[A] S)) ↔
    x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ x ∈ Set.range ⇑(algebraMap R (R ⊗[A] S)) ↔
    x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
Tactic:
simp only [Set.mem_range, LinearMap.mem_range]
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ (∃ y, (algebraMap R (R ⊗[A] S)) y = x) ↔ ∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ (∃ y, (algebraMap R (R ⊗[A] S)) y = x) ↔ ∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x
Tactic:
constructor
State after:
case h.mp
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ (∃ y, (algebraMap R (R ⊗[A] S)) y = x) → ∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x

case h.mpr
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ (∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x) → ∃ y, (algebraMap R (R ⊗[A] S)) y = x

State before:
case h.mp
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ (∃ y, (algebraMap R (R ⊗[A] S)) y = x) → ∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x
Tactic:
rintro ⟨y, rfl⟩
State after:
case h.mp.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
y : R
⊢ ∃ y_1, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y_1 = (algebraMap R (R ⊗[A] S)) y

State before:
case h.mp.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
y : R
⊢ ∃ y_1, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y_1 = (algebraMap R (R ⊗[A] S)) y
Tactic:
exact ⟨y ⊗ₜ[A] ⟨1, (Subalgebra.mem_toSubmodule ⊥).mpr (one_mem ⊥)⟩, rfl⟩
State after:
no goals

State before:
case h.mpr
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ (∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x) → ∃ y, (algebraMap R (R ⊗[A] S)) y = x
Tactic:
rintro ⟨y, rfl⟩
State after:
case h.mpr.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
⊢ ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y

State before:
case h.mpr.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
⊢ ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
Tactic:
induction y using TensorProduct.induction_on with
| zero =>
  use 0
  simp only [zero_tmul, LinearMap.map_zero]
  simp
| tmul r s =>
  rcases s with ⟨s, hs⟩
  simp only [Subalgebra.mem_toSubmodule] at hs
  obtain ⟨a, rfl⟩ := hs
  use a • r
  simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.id.map_eq_id, RingHom.id_apply,
    toRingHom_eq_coe, coe_coe, baseChange_tmul, coeSubtype]
  simp only [smul_tmul]
  rw [Algebra.ofId_apply, Algebra.algebraMap_eq_smul_one]
| add x y hx hy =>
  obtain ⟨x', hx⟩ := hx
  obtain ⟨y', hy⟩ := hy
  use x' + y'
  simp only [add_tmul, hx, hy, map_add]
State after:
no goals

State before:
case h.mpr.intro.zero
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
⊢ ∃ y, (algebraMap R (R ⊗[A] S)) y = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) 0
Tactic:
use 0
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
⊢ (algebraMap R (R ⊗[A] S)) 0 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) 0

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
⊢ (algebraMap R (R ⊗[A] S)) 0 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) 0
Tactic:
simp only [zero_tmul, LinearMap.map_zero]
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
⊢ (algebraMap R (R ⊗[A] S)) 0 = 0

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
⊢ (algebraMap R (R ⊗[A] S)) 0 = 0
Tactic:
simp
State after:
no goals

State before:
case h.mpr.intro.tmul
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
s : ↥(Subalgebra.toSubmodule ⊥)
⊢ ∃ y, (algebraMap R (R ⊗[A] S)) y = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] s)
Tactic:
rcases s with ⟨s, hs⟩
State after:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
s : S
hs : s ∈ Subalgebra.toSubmodule ⊥
⊢ ∃ y, (algebraMap R (R ⊗[A] S)) y = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨s, hs⟩)

State before:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
s : S
hs : s ∈ Subalgebra.toSubmodule ⊥
⊢ ∃ y, (algebraMap R (R ⊗[A] S)) y = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨s, hs⟩)
Tactic:
simp only [Subalgebra.mem_toSubmodule] at hs
State after:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
s : S
hs✝ : s ∈ Subalgebra.toSubmodule ⊥
hs : s ∈ ⊥
⊢ ∃ y, (algebraMap R (R ⊗[A] S)) y = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨s, hs✝⟩)

State before:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
s : S
hs✝ : s ∈ Subalgebra.toSubmodule ⊥
hs : s ∈ ⊥
⊢ ∃ y, (algebraMap R (R ⊗[A] S)) y = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨s, hs✝⟩)
Tactic:
obtain ⟨a, rfl⟩ := hs
State after:
case h.mpr.intro.tmul.mk.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ ∃ y,
    (algebraMap R (R ⊗[A] S)) y =
      (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨(ofId A S).toRingHom a, hs⟩)

State before:
case h.mpr.intro.tmul.mk.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ ∃ y,
    (algebraMap R (R ⊗[A] S)) y =
      (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨(ofId A S).toRingHom a, hs⟩)
Tactic:
use a • r
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ (algebraMap R (R ⊗[A] S)) (a • r) =
    (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨(ofId A S).toRingHom a, hs⟩)

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ (algebraMap R (R ⊗[A] S)) (a • r) =
    (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (r ⊗ₜ[A] ⟨(ofId A S).toRingHom a, hs⟩)
Tactic:
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.id.map_eq_id, RingHom.id_apply,
  toRingHom_eq_coe, coe_coe, baseChange_tmul, coeSubtype]
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ (a • r) ⊗ₜ[A] 1 = r ⊗ₜ[A] (ofId A S) a

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ (a • r) ⊗ₜ[A] 1 = r ⊗ₜ[A] (ofId A S) a
Tactic:
simp only [smul_tmul]
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ r ⊗ₜ[A] (a • 1) = r ⊗ₜ[A] (ofId A S) a

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
r : R
a : A
hs : (ofId A S).toRingHom a ∈ Subalgebra.toSubmodule ⊥
⊢ r ⊗ₜ[A] (a • 1) = r ⊗ₜ[A] (ofId A S) a
Tactic:
rw [Algebra.ofId_apply, Algebra.algebraMap_eq_smul_one]
State after:
no goals

State before:
case h.mpr.intro.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
hx : ∃ y, (algebraMap R (R ⊗[A] S)) y = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) x
hy : ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
⊢ ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (x + y)
Tactic:
obtain ⟨x', hx⟩ := hx
State after:
case h.mpr.intro.add.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
hy : ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
x' : R
hx : (algebraMap R (R ⊗[A] S)) x' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) x
⊢ ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (x + y)

State before:
case h.mpr.intro.add.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
hy : ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
x' : R
hx : (algebraMap R (R ⊗[A] S)) x' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) x
⊢ ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (x + y)
Tactic:
obtain ⟨y', hy⟩ := hy
State after:
case h.mpr.intro.add.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
x' : R
hx : (algebraMap R (R ⊗[A] S)) x' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) x
y' : R
hy : (algebraMap R (R ⊗[A] S)) y' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
⊢ ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (x + y)

State before:
case h.mpr.intro.add.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
x' : R
hx : (algebraMap R (R ⊗[A] S)) x' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) x
y' : R
hy : (algebraMap R (R ⊗[A] S)) y' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
⊢ ∃ y_1, (algebraMap R (R ⊗[A] S)) y_1 = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (x + y)
Tactic:
use x' + y'
State after:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
x' : R
hx : (algebraMap R (R ⊗[A] S)) x' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) x
y' : R
hy : (algebraMap R (R ⊗[A] S)) y' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
⊢ (algebraMap R (R ⊗[A] S)) (x' + y') = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (x + y)

State before:
case h
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x y : R ⊗[A] ↥(Subalgebra.toSubmodule ⊥)
x' : R
hx : (algebraMap R (R ⊗[A] S)) x' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) x
y' : R
hy : (algebraMap R (R ⊗[A] S)) y' = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y
⊢ (algebraMap R (R ⊗[A] S)) (x' + y') = (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) (x + y)
Tactic:
simp only [add_tmul, hx, hy, map_add]
State after:
no goals