-- Mathlib/LinearAlgebra/Finsupp/Span.lean
theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) :
    Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M))
      (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M))

Proof state:
case refine_3
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint (⨅ a ∈ sᶜ, ker (lapply a)) (⨅ a ∈ tᶜ, ker (lapply a))

Tactic:
rw [disjoint_iff_inf_le]

Result:
case refine_3
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ⊥

Proof state:
case refine_3
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

Tactic:
by_cases his : i ∈ s

Result:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∉ s
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

Proof state:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∈ t
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

Tactic:
exact (hs.le_bot ⟨his, hit⟩).elim

Result:
no goals

Proof state:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

Tactic:
by_cases hit : i ∈ t

Result:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∈ t
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∉ t
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

Proof state:
case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∉ s
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

Tactic:
exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint t tᶜ

Tactic:
apply disjoint_compl_right

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint s sᶜ

Tactic:
apply disjoint_compl_right

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∉ t
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)

Tactic:
exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨆ a ∈ t, LinearMap.range (lsingle a))

Tactic:
refine
  (Disjoint.mono
    (lsingle_range_le_ker_lapply s sᶜ ?_)
    (lsingle_range_le_ker_lapply t tᶜ ?_))
    ?_

Result:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint s sᶜ

case refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint t tᶜ

case refine_3
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint (⨅ a ∈ sᶜ, ker (lapply a)) (⨅ a ∈ tᶜ, ker (lapply a))

Proof state:
case refine_3
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ⊥

Tactic:
refine le_trans (le_iInf fun i => ?_) iInf_ker_lapply_le_bot

Result:
case refine_3
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
⊢ (⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)