Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange (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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ Submodule.restrictScalars R (Ideal.map includeRight I) =
    LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ x ∈ Submodule.restrictScalars R (Ideal.map includeRight I) ↔
    x ∈ LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ x ∈ Submodule.restrictScalars R (Ideal.map includeRight I) ↔
    x ∈ LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype)
Tactic:
simp only [restrictScalars_mem, 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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ x ∈ Ideal.map includeRight I ↔ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ x ∈ Ideal.map includeRight I ↔ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ x ∈ Ideal.map includeRight I → ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ (∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x) → x ∈ Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ x ∈ Ideal.map includeRight I → ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x
Tactic:
intro hx
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x
Tactic:
apply Submodule.span_induction hx
  (p := fun x ↦ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x )
State after:
case h.mp.mem
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∀ x ∈ ⇑includeRight '' ↑I, ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x

case h.mp.zero
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = 0

case h.mp.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∀ (x y : R ⊗[A] S),
    (∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x) →
      (∃ y_1, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 = y) →
        ∃ y_1, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 = x + y

case h.mp.smul
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∀ (a x : R ⊗[A] S),
    (∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x) →
      ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = a • x

State before:
case h.mp.mem
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∀ x ∈ ⇑includeRight '' ↑I, ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x
Tactic:
rintro x ⟨s, hs, rfl⟩
State after:
case h.mp.mem.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
s : S
hs : s ∈ ↑I
⊢ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = includeRight s

State before:
case h.mp.mem.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
s : S
hs : s ∈ ↑I
⊢ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = includeRight s
Tactic:
use 1 ⊗ₜ[A] ⟨s, hs⟩
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
s : S
hs : s ∈ ↑I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (1 ⊗ₜ[A] ⟨s, hs⟩) = includeRight s

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
s : S
hs : s ∈ ↑I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (1 ⊗ₜ[A] ⟨s, hs⟩) = includeRight s
Tactic:
rfl
State after:
no goals

State before:
case h.mp.zero
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = 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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 = 0
Tactic:
simp only [_root_.map_zero]
State after:
no goals

State before:
case h.mp.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∀ (x y : R ⊗[A] S),
    (∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x) →
      (∃ y_1, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 = y) →
        ∃ y_1, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 = x + y
Tactic:
rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
State after:
case h.mp.add.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx : x✝ ∈ Ideal.map includeRight I
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
        (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y

State before:
case h.mp.add.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx : x✝ ∈ Ideal.map includeRight I
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
        (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx : x✝ ∈ Ideal.map includeRight I
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y) =
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx : x✝ ∈ Ideal.map includeRight I
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y) =
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
Tactic:
simp only [map_add]
State after:
no goals

State before:
case h.mp.smul
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
⊢ ∀ (a x : R ⊗[A] S),
    (∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x) →
      ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = a • x
Tactic:
rintro a _ ⟨x, rfl⟩
State after:
case h.mp.smul.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x

State before:
case h.mp.smul.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
Tactic:
induction x using TensorProduct.induction_on with
| zero => use 0; simp only [_root_.map_zero, smul_eq_mul, mul_zero]
| tmul r s =>
  induction a using TensorProduct.induction_on with
  | zero =>
    use 0
    simp only [_root_.map_zero, baseChange_tmul, coeSubtype, smul_eq_mul, zero_mul]
  | tmul u v =>
    use (u * r) ⊗ₜ[A] (v • s)
    simp only [baseChange_tmul, coeSubtype, smul_eq_mul,
      Algebra.TensorProduct.tmul_mul_tmul]
    rw [Submodule.coe_smul, smul_eq_mul]
  | add u v hu hv =>
    obtain ⟨x, hx⟩ := hu
    obtain ⟨y, hy⟩ := hv
    use x + y
    rw [LinearMap.map_add, add_smul, hx, hy]
| add x y hx hy =>
  obtain ⟨x', hx⟩ := hx
  obtain ⟨y', hy⟩ := hy
  use x' + y'
  simp only [map_add, hx, smul_eq_mul, hy, mul_add]
State after:
no goals

State before:
case h.mp.smul.intro.zero
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
a : R ⊗[A] S
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
a : R ⊗[A] S
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
a : R ⊗[A] S
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0
Tactic:
simp only [_root_.map_zero, smul_eq_mul, mul_zero]
State after:
no goals

State before:
case h.mp.smul.intro.tmul
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
a : R ⊗[A] S
r : R
s : ↥(Submodule.restrictScalars A I)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
Tactic:
induction a using TensorProduct.induction_on with
| zero =>
  use 0
  simp only [_root_.map_zero, baseChange_tmul, coeSubtype, smul_eq_mul, zero_mul]
| tmul u v =>
  use (u * r) ⊗ₜ[A] (v • s)
  simp only [baseChange_tmul, coeSubtype, smul_eq_mul,
    Algebra.TensorProduct.tmul_mul_tmul]
  rw [Submodule.coe_smul, smul_eq_mul]
| add u v hu hv =>
  obtain ⟨x, hx⟩ := hu
  obtain ⟨y, hy⟩ := hv
  use x + y
  rw [LinearMap.map_add, add_smul, hx, hy]
State after:
no goals

State before:
case h.mp.smul.intro.tmul.zero
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      0 • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 =
    0 • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 =
    0 • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
Tactic:
simp only [_root_.map_zero, baseChange_tmul, coeSubtype, smul_eq_mul, zero_mul]
State after:
no goals

State before:
case h.mp.smul.intro.tmul.tmul
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u : R
v : S
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      u ⊗ₜ[A] v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
Tactic:
use (u * r) ⊗ₜ[A] (v • s)
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u : R
v : S
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) ((u * r) ⊗ₜ[A] (v • s)) =
    u ⊗ₜ[A] v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u : R
v : S
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) ((u * r) ⊗ₜ[A] (v • s)) =
    u ⊗ₜ[A] v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
Tactic:
simp only [baseChange_tmul, coeSubtype, smul_eq_mul,
  Algebra.TensorProduct.tmul_mul_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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u : R
v : S
⊢ (u * r) ⊗ₜ[A] ↑(v • s) = (u * r) ⊗ₜ[A] (v * ↑s)

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u : R
v : S
⊢ (u * r) ⊗ₜ[A] ↑(v • s) = (u * r) ⊗ₜ[A] (v * ↑s)
Tactic:
rw [Submodule.coe_smul, smul_eq_mul]
State after:
no goals

State before:
case h.mp.smul.intro.tmul.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
hx : x ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u v : R ⊗[A] S
hu :
  ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      u • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
hv :
  ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      (u + v) • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
Tactic:
obtain ⟨x, hx⟩ := hu
State after:
case h.mp.smul.intro.tmul.add.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u v : R ⊗[A] S
hv :
  ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x =
    u • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      (u + v) • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)

State before:
case h.mp.smul.intro.tmul.add.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u v : R ⊗[A] S
hv :
  ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x =
    u • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      (u + v) • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
Tactic:
obtain ⟨y, hy⟩ := hv
State after:
case h.mp.smul.intro.tmul.add.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u v : R ⊗[A] S
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x =
    u • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
    v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      (u + v) • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)

State before:
case h.mp.smul.intro.tmul.add.intro.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u v : R ⊗[A] S
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x =
    u • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
    v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
⊢ ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      (u + v) • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u v : R ⊗[A] S
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x =
    u • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
    v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y) =
    (u + v) • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
r : R
s : ↥(Submodule.restrictScalars A I)
u v : R ⊗[A] S
x : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x =
    u • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
    v • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y) =
    (u + v) • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s)
Tactic:
rw [LinearMap.map_add, add_smul, hx, hy]
State after:
no goals

State before:
case h.mp.smul.intro.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  ∃ y,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
hy :
  ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
⊢ ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y)
Tactic:
obtain ⟨x', hx⟩ := hx
State after:
case h.mp.smul.intro.add.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
x' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
⊢ ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y)

State before:
case h.mp.smul.intro.add.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
x' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
⊢ ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y)
Tactic:
obtain ⟨y', hy⟩ := hy
State after:
case h.mp.smul.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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x y x' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
y' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
⊢ ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y)

State before:
case h.mp.smul.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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x y x' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
y' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
⊢ ∃ y_1,
    (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y_1 =
      a • (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x y x' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
y' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x' + y') =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x✝ : R ⊗[A] S
hx✝ : x✝ ∈ Ideal.map includeRight I
a : R ⊗[A] S
x y x' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x
y' : R ⊗[A] ↥(Submodule.restrictScalars A I)
hy :
  (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y' =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x' + y') =
    a • (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y)
Tactic:
simp only [map_add, hx, smul_eq_mul, hy, mul_add]
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ (∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x) → x ∈ Ideal.map includeRight I
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
Tactic:
induction y using TensorProduct.induction_on with
| zero => simp only [_root_.map_zero, Submodule.zero_mem]
| tmul r s =>
  rcases s with ⟨s, hs⟩
  simp only [restrictScalars_mem] at hs
  simp only [baseChange_tmul, coeSubtype]
  rw [← mul_one r, ← smul_eq_mul, ← TensorProduct.smul_tmul']
  rw [← IsScalarTower.algebraMap_smul (R ⊗[A] S) r, smul_eq_mul]
  apply Ideal.mul_mem_left
  exact Ideal.mem_map_of_mem Algebra.TensorProduct.includeRight hs
| add x y hx hy =>
  simp only [map_add]
  exact Ideal.add_mem _ hx hy
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 ∈ Ideal.map includeRight I
Tactic:
simp only [_root_.map_zero, Submodule.zero_mem]
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s) ∈ Ideal.map includeRight I
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs : s ∈ Submodule.restrictScalars A I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs⟩) ∈ Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs : s ∈ Submodule.restrictScalars A I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs⟩) ∈ Ideal.map includeRight I
Tactic:
simp only [restrictScalars_mem] 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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs✝⟩) ∈ Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs✝⟩) ∈ Ideal.map includeRight I
Tactic:
simp only [baseChange_tmul, coeSubtype]
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r ⊗ₜ[A] s ∈ Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
rw [← mul_one r, ← smul_eq_mul, ← TensorProduct.smul_tmul']
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r • 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r • 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
rw [← IsScalarTower.algebraMap_smul (R ⊗[A] S) r, smul_eq_mul]
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (algebraMap R (R ⊗[A] S)) r * 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (algebraMap R (R ⊗[A] S)) r * 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
apply Ideal.mul_mem_left
State after:
case h.mpr.intro.tmul.mk.a
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I

State before:
case h.mpr.intro.tmul.mk.a
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
exact Ideal.mem_map_of_mem Algebra.TensorProduct.includeRight hs
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x ∈ Ideal.map includeRight I
hy : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y) ∈ Ideal.map includeRight I
Tactic:
simp only [map_add]
State after:
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x ∈ Ideal.map includeRight I
hy : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈
    Ideal.map includeRight I

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x ∈ Ideal.map includeRight I
hy : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈
    Ideal.map includeRight I
Tactic:
exact Ideal.add_mem _ hx hy
State after:
no goals