-- Mathlib/LinearAlgebra/StdBasis.lean
theorem linearIndependent_single [Ring R] [∀ i, AddCommGroup (Ms i)] [∀ i, Module R (Ms i)]
    [DecidableEq η] (v : ∀ j, ιs j → Ms j) (hs : ∀ i, LinearIndependent R (v i)) :
    LinearIndependent R fun ji : Σj, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2)

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
⊢ ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)

Tactic:
intro j

Result:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : J.Finite
hiJ : j✝ ∉ J
j : η
⊢ span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
h₀ :
  ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)
h₁ :
  span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (LinearMap.single R Ms i)
h₂ :
  ⨆ j ∈ J, span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤
    ⨆ j ∈ J, LinearMap.range (LinearMap.single R (fun j => Ms j) j)
⊢ Disjoint (fun i => i ∈ {j}) J

Tactic:
convert Set.disjoint_singleton_left.2 hiJ using 0

Result:
no goals

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
h₀ :
  ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)
h₁ :
  span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (LinearMap.single R Ms i)
h₂ :
  ⨆ j ∈ J, span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤
    ⨆ j ∈ J, LinearMap.range (LinearMap.single R (fun j => Ms j) j)
⊢ Disjoint (span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)))
    (⨆ i ∈ J, span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))

Tactic:
have h₃ : Disjoint (fun i : η => i ∈ ({j} : Set _)) J := by
  convert Set.disjoint_singleton_left.2 hiJ using 0

Result:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
h₀ :
  ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)
h₁ :
  span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (LinearMap.single R Ms i)
h₂ :
  ⨆ j ∈ J, span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤
    ⨆ j ∈ J, LinearMap.range (LinearMap.single R (fun j => Ms j) j)
h₃ : Disjoint (fun i => i ∈ {j}) J
⊢ Disjoint (span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)))
    (⨆ i ∈ J, span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
h₀ :
  ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)
⊢ Disjoint (span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)))
    (⨆ i ∈ J, span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))

Tactic:
have h₁ :
  span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
    ⨆ i ∈ ({j} : Set _), LinearMap.range (LinearMap.single R Ms i) := by
  rw [@iSup_singleton _ _ _ fun i => LinearMap.range (LinearMap.single R (Ms) i)]
  apply h₀

Result:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
h₀ :
  ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)
h₁ :
  span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (LinearMap.single R Ms i)
⊢ Disjoint (span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)))
    (⨆ i ∈ J, span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
h₀ :
  ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)
h₁ :
  span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (LinearMap.single R Ms i)
⊢ Disjoint (span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)))
    (⨆ i ∈ J, span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))

Tactic:
have h₂ :
  ⨆ j ∈ J, span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
    ⨆ j ∈ J, LinearMap.range (LinearMap.single R (fun j : η => Ms j) j) :=
  iSup₂_mono fun i _ => h₀ i

Result:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j : η
J : Set η
a✝ : J.Finite
hiJ : j ∉ J
h₀ :
  ∀ (j : η), span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)
h₁ :
  span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (LinearMap.single R Ms i)
h₂ :
  ⨆ j ∈ J, span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤
    ⨆ j ∈ J, LinearMap.range (LinearMap.single R (fun j => Ms j) j)
⊢ Disjoint (span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)))
    (⨆ i ∈ J, span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))