internlm/Lean-Github huggingface dataset:
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ Disjoint (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Tactic:
rw [disjoint_def]
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ ∀ x ∈ range (lTensor Q M₁.subtype), x ∈ range (lTensor Q M₂.subtype) → x = 0
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ ∀ x ∈ range (lTensor Q M₁.subtype), x ∈ range (lTensor Q M₂.subtype) → x = 0
Tactic:
intro x h h'
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ range (lTensor Q M₂.subtype)
⊢ x = 0
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ range (lTensor Q M₂.subtype)
⊢ x = 0
Tactic:
rw [← id_apply x (R := A), ← lTensor_id, ← hq]
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ range (lTensor Q M₂.subtype)
⊢ (lTensor Q (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯)) x = 0
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ range (lTensor Q M₂.subtype)
⊢ (lTensor Q (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯)) x = 0
Tactic:
simp only [lTensor_add, lTensor_comp,
  LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply]
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ range (lTensor Q M₂.subtype)
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ range (lTensor Q M₂.subtype)
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Tactic:
rw [← ker_lTensor_of_linearProjOfIsCompl hM Q] at h'
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ ker (lTensor Q (M₁.linearProjOfIsCompl M₂ hM))
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ range (lTensor Q M₁.subtype)
h' : x ∈ ker (lTensor Q (M₁.linearProjOfIsCompl M₂ hM))
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Tactic:
rw [← ker_lTensor_of_linearProjOfIsCompl hM.symm Q] at h
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ ker (lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯))
h' : x ∈ ker (lTensor Q (M₁.linearProjOfIsCompl M₂ hM))
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : x ∈ ker (lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯))
h' : x ∈ ker (lTensor Q (M₁.linearProjOfIsCompl M₂ hM))
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Tactic:
rw [mem_ker] at h h'
Proof state after:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : (lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x = 0
h' : (lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x = 0
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case disjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
h : (lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x = 0
h' : (lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x = 0
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) =
    0
Tactic:
simp only [h', _root_.map_zero, h, add_zero]
Proof state after:
no goals
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ Codisjoint (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Tactic:
rw [codisjoint_iff]
Proof state after:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype) = ⊤
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype) = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ ⊤ ≤ range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ ⊤ ≤ range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Tactic:
intro x _
Proof state after:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
a✝ : x ∈ ⊤
⊢ x ∈ range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
a✝ : x ∈ ⊤
⊢ x ∈ range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Tactic:
rw [← lTensor_id_apply Q _ x, ← hq]
Proof state after:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
a✝ : x ∈ ⊤
⊢ (lTensor Q (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯)) x ∈
    range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
a✝ : x ∈ ⊤
⊢ (lTensor Q (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯)) x ∈
    range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Tactic:
simp only [lTensor_add, lTensor_comp, add_apply, coe_comp, Function.comp_apply]
Proof state after:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
a✝ : x ∈ ⊤
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) ∈
    range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Theorem: LinearMap.isCompl_lTensor
Proof state before:
case codisjoint
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
x : Q ⊗[A] M
a✝ : x ∈ ⊤
⊢ (lTensor Q M₁.subtype) ((lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) x) +
      (lTensor Q M₂.subtype) ((lTensor Q (M₂.linearProjOfIsCompl M₁ ⋯)) x) ∈
    range (lTensor Q M₁.subtype) ⊔ range (lTensor Q M₂.subtype)
Tactic:
exact Submodule.add_mem _
  (mem_sup_left (LinearMap.mem_range_self _ _))
  (mem_sup_right (LinearMap.mem_range_self _ _))
Proof state after:
no goals
Theorem: LinearMap.isCompl_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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (range (baseChange R M₁.subtype)) (range (baseChange R M₂.subtype))
Tactic:
rw [← isCompl_restrictScalars_iff A]
Proof state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Submodule.restrictScalars A (range (baseChange R M₁.subtype)))
    (Submodule.restrictScalars A (range (baseChange R M₂.subtype)))
Theorem: LinearMap.isCompl_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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Submodule.restrictScalars A (range (baseChange R M₁.subtype)))
    (Submodule.restrictScalars A (range (baseChange R M₂.subtype)))
Tactic:
exact isCompl_lTensor hM R
Proof state after:
no goals
Theorem: Algebra.baseChange_bot
Proof state before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
⊢ Subalgebra.toSubmodule ⊥ = LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
Tactic:
ext x
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 : R ⊗[A] S
⊢ x ∈ Subalgebra.toSubmodule ⊥ ↔ x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
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 : R ⊗[A] S
⊢ x ∈ Subalgebra.toSubmodule ⊥ ↔ x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
Tactic:
simp only [Subalgebra.mem_toSubmodule, Algebra.mem_bot]
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 : R ⊗[A] S
⊢ x ∈ Set.range ⇑(algebraMap R (R ⊗[A] S)) ↔
    x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
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 : R ⊗[A] S
⊢ x ∈ Set.range ⇑(algebraMap R (R ⊗[A] S)) ↔
    x ∈ LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype)
Tactic:
simp only [Set.mem_range, LinearMap.mem_range]
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 : R ⊗[A] S
⊢ (∃ y, (algebraMap R (R ⊗[A] S)) y = x) ↔ ∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x
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 : R ⊗[A] S
⊢ (∃ y, (algebraMap R (R ⊗[A] S)) y = x) ↔ ∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).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
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
x : R ⊗[A] S
⊢ (∃ y, (algebraMap R (R ⊗[A] S)) y = x) → ∃ y, (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype) y = x

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