case refine'_1
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ Disjoint s (sᶜ)

case refine'_2
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ Disjoint t (tᶜ)

case refine'_3
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ Disjoint (⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) (⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a))
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ Disjoint (⨆ (a : α) (_ : a ∈ s), LinearMap.range (lsingle a)) (⨆ (a : α) (_ : a ∈ t), LinearMap.range (lsingle a))
refine'
  (Disjoint.mono
    (lsingle_range_le_ker_lapply s (sᶜ) _)
    (lsingle_range_le_ker_lapply t (tᶜ) _))
    _
case refine'_3
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ⊥
case refine'_3
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ Disjoint (⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) (⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a))
rw [disjoint_iff_inf_le]
case refine'_3
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
case refine'_3
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ⊥
refine' le_trans (le_iInf fun i => _) iInf_ker_lapply_le_bot
no goals
case refine'_1
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ Disjoint s (sᶜ)
apply disjoint_compl_right
no goals
case refine'_2
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
⊢ Disjoint t (tᶜ)
apply disjoint_compl_right
case pos
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)

case neg
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : ¬i ∈ s
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
case refine'_3
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
by_cases his : i ∈ s
no goals
case neg
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : ¬i ∈ s
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)
case pos
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∈ t
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)

case neg
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : ¬i ∈ t
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
case pos
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
by_cases hit : i ∈ t
no goals
case neg
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : ¬i ∈ t
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
no goals
case pos
α : Type u_1
M : Type u_2
N : Type ?u.38530
P : Type ?u.38533
R : Type u_3
S : Type ?u.38539
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∈ t
⊢ ((⨅ (a : α) (_ : a ∈ sᶜ), ker (lapply a)) ⊓ ⨅ (a : α) (_ : a ∈ tᶜ), ker (lapply a)) ≤ ker (lapply i)
exact (hs.le_bot ⟨his, hit⟩).elim