internlm/Lean-Github huggingface dataset:
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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⟩
Proof 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
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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)
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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'
Proof 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)
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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]
Proof state after:
no goals