Theorem: LinearMap.isCompl_lTensor (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
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
⊢ IsCompl (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Tactic:
have hq :
  M₁.subtype.comp (linearProjOfIsCompl _ _ hM)
    + M₂.subtype.comp (linearProjOfIsCompl _ _ hM.symm) = id := by
  ext x
  simp only [add_apply, coe_comp, coeSubtype, Function.comp_apply,
    id_coe, id_eq]
  rw [linear_proj_add_linearProjOfIsCompl_eq_self]
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₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ IsCompl (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))

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₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
hq : M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
⊢ IsCompl (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))
Tactic:
apply IsCompl.mk
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
⊢ Disjoint (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype))

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))

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₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯ = id
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
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
x : M
⊢ (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯) x = id 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
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
x : M
⊢ (M₁.subtype ∘ₗ M₁.linearProjOfIsCompl M₂ hM + M₂.subtype ∘ₗ M₂.linearProjOfIsCompl M₁ ⋯) x = id x
Tactic:
simp only [add_apply, coe_comp, coeSubtype, Function.comp_apply,
  id_coe, id_eq]
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
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
x : M
⊢ ↑((M₁.linearProjOfIsCompl M₂ hM) x) + ↑((M₂.linearProjOfIsCompl M₁ ⋯) x) = 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
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
x : M
⊢ ↑((M₁.linearProjOfIsCompl M₂ hM) x) + ↑((M₂.linearProjOfIsCompl M₁ ⋯) x) = x
Tactic:
rw [linear_proj_add_linearProjOfIsCompl_eq_self]
State after:
no goals

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]
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

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'
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

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]
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

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]
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

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'
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

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
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

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'
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

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]
State after:
no goals

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]
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) = ⊤

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]
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)

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 _
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)

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]
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)

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]
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)

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 _ _))
State after:
no goals