internlm/Lean-Github huggingface dataset:
Theorem: Algebra.baseChange_bot
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
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]
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
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
Theorem: Algebra.baseChange_bot
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
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
Proof state after:
no goals
Theorem: Algebra.baseChange_bot
Proof 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⟩
Proof 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⟩)
Theorem: Algebra.baseChange_bot
Proof 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
Proof 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✝⟩)
Theorem: Algebra.baseChange_bot
Proof 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
Proof 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⟩)
Theorem: Algebra.baseChange_bot
Proof 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
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
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⟩)
Theorem: Algebra.baseChange_bot
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
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]
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
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
Theorem: Algebra.baseChange_bot
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
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]
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
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
Theorem: Algebra.baseChange_bot
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
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]
Proof state after:
no goals
Theorem: Algebra.baseChange_bot
Proof 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
Proof 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)
Theorem: Algebra.baseChange_bot
Proof 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
Proof 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)
Theorem: Algebra.baseChange_bot
Proof 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'
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
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)
Theorem: Algebra.baseChange_bot
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
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]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
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
⊢ x ∈ Submodule.restrictScalars R (Ideal.map includeRight I) ↔
    x ∈ LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype)
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
⊢ 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]
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
⊢ x ∈ Ideal.map includeRight I ↔ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x
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
⊢ x ∈ Ideal.map includeRight I ↔ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x
Tactic:
constructor
Proof 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
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
Proof 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
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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 )
Proof 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
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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⟩
Proof 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
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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⟩
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
s : S
hs : s ∈ ↑I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (1 ⊗ₜ[A] ⟨s, hs⟩) = includeRight 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
s : S
hs : s ∈ ↑I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (1 ⊗ₜ[A] ⟨s, hs⟩) = includeRight s
Tactic:
rfl
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
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
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 = 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
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 = 0
Tactic:
simp only [_root_.map_zero]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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⟩
Proof 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
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof 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
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
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