ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ LinearIndependent R fun ji => f ji.fst ji.snd
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
⊢ LinearIndependent R fun ji => f ji.fst ji.snd
nontriviality R
case hf
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ Injective fun ji => f ji.fst ji.snd

case a
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ LinearIndependent R Subtype.val
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ LinearIndependent R fun ji => f ji.fst ji.snd
apply LinearIndependent.of_subtype_range
case a
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ LinearIndependent R Subtype.val
case a
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ LinearIndependent R Subtype.val
rw [range_sigma_eq_iUnion_range]
no goals
case a
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ LinearIndependent R Subtype.val
apply linearIndependent_iUnion_finite_subtype (fun j => (hindep j).to_subtype_range) hd
case hf.mk.mk
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
case hf
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
⊢ Injective fun ji => f ji.fst ji.snd
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy
case pos
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : x₁ = y₁
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }

case neg
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
case hf.mk.mk
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
by_cases h_cases : x₁ = y₁
case pos
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ } = { fst := x₁, snd := y₂ }

case neg
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
case pos
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : x₁ = y₁
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }

case neg
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
subst h_cases
case pos.a
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ Eq.recOn ?pos.h₁✝ { fst := x₁, snd := x₂ }.snd = { fst := x₁, snd := y₂ }.snd

case pos.h₁
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ }.fst = { fst := x₁, snd := y₂ }.fst
case pos
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ } = { fst := x₁, snd := y₂ }
apply Sigma.eq
case pos.h₁
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ }.fst = { fst := x₁, snd := y₂ }.fst

case pos.h₁
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ }.fst = { fst := x₁, snd := y₂ }.fst
case pos.a
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ Eq.recOn ?pos.h₁✝ { fst := x₁, snd := x₂ }.snd = { fst := x₁, snd := y₂ }.snd

case pos.h₁
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ }.fst = { fst := x₁, snd := y₂ }.fst
rw [LinearIndependent.injective (hindep _) hxy]
no goals
case pos.h₁
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ }.fst = { fst := x₁, snd := y₂ }.fst

case pos.h₁
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := x₁, snd := y₂ }
⊢ { fst := x₁, snd := x₂ }.fst = { fst := x₁, snd := y₂ }.fst
rfl
case neg
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
h0 : f x₁ x₂ = 0
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
case neg
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
have h0 : f x₁ x₂ = 0 := by
  apply
    disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
      (f x₁ x₂) (subset_span (mem_range_self _))
  rw [iSup_singleton]
  simp only at hxy
  rw [hxy]
  exact subset_span (mem_range_self y₂)
no goals
case neg
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
h0 : f x₁ x₂ = 0
⊢ { fst := x₁, snd := x₂ } = { fst := y₁, snd := y₂ }
exact False.elim ((hindep x₁).ne_zero _ h0)
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ ⨆ (i : η) (_ : i ∈ {y₁}), span R (range (f i))
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ = 0
apply
  disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
    (f x₁ x₂) (subset_span (mem_range_self _))
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ ⨆ (i : η) (_ : i ∈ {y₁}), span R (range (f i))
rw [iSup_singleton]
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) { fst := x₁, snd := x₂ } = (fun ji => f ji.fst ji.snd) { fst := y₁, snd := y₂ }
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))
simp only at hxy
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f y₁ y₂ ∈ span R (range (f y₁))
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))
rw [hxy]
no goals
ι : Type u'
ι' : Type ?u.387224
R : Type u_3
K : Type ?u.387230
M : Type u_4
M' : Type ?u.387236
M'' : Type ?u.387239
V : Type u
V' : Type ?u.387244
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
η : Type u_1
ιs : η → Type u_2
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    Set.Finite t → ¬i ∈ t → Disjoint (span R (range (f i))) (⨆ (i : η) (_ : i ∈ t), span R (range (f i)))
✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f y₁ y₂ ∈ span R (range (f y₁))
exact subset_span (mem_range_self y₂)