K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
h : ¬(⋃ (k : κ), ↑(↑b.repr (v k)).support) = Set.univ
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
⊢ (⋃ (k : κ), ↑(↑b.repr (v k)).support) = Set.univ
by_contra h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
h : ∃ a, ∀ (x : κ), ↑(↑b.repr (v x)) a = 0
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
h : ¬(⋃ (k : κ), ↑(↑b.repr (v k)).support) = Set.univ
⊢ False
simp only [← Ne.def, ne_univ_iff_exists_not_mem, mem_iUnion, not_exists_not,
  Finsupp.mem_support_iff, Finset.mem_coe] at h
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
h : ∃ a, ∀ (x : κ), ↑(↑b.repr (v x)) a = 0
⊢ False
obtain ⟨b', w⟩ := h
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
⊢ False
let v' : Option κ → M := fun o => o.elim (b b') v
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
⊢ False
have r : range v ⊆ range v' := by
  rintro - ⟨k, rfl⟩
  use some k
  rfl
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
⊢ False
have r' : b b' ∉ range v := by
  rintro ⟨k, p⟩
  simpa [w] using congr_arg (fun m => (b.repr m) b') p
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
⊢ False
have r'' : range v ≠ range v' := by
  intro e
  have p : b b' ∈ range v' := by
    use none
    rfl
  rw [← e] at p
  exact r' p
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : ∀ (s : Set M), LinearIndependent R Subtype.val → range v ⊆ s → range v = s
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
i' : LinearIndependent R Subtype.val
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
i' : LinearIndependent R Subtype.val
⊢ False
dsimp [LinearIndependent.Maximal] at m
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
i' : LinearIndependent R Subtype.val
m : range v = range v'
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : ∀ (s : Set M), LinearIndependent R Subtype.val → range v ⊆ s → range v = s
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
i' : LinearIndependent R Subtype.val
⊢ False
specialize m (range v') i' r
no goals
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
i' : LinearIndependent R Subtype.val
m : range v = range v'
⊢ False
exact r'' m
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
k : κ
⊢ v k ∈ range v'
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
⊢ range v ⊆ range v'
rintro - ⟨k, rfl⟩
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
k : κ
⊢ v' (some k) = v k
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
k : κ
⊢ v k ∈ range v'
use some k
no goals
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
k : κ
⊢ v' (some k) = v k
rfl
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
k : κ
p : v k = ↑b b'
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
⊢ ¬↑b b' ∈ range v
rintro ⟨k, p⟩
no goals
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
k : κ
p : v k = ↑b b'
⊢ False
simpa [w] using congr_arg (fun m => (b.repr m) b') p
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
⊢ range v ≠ range v'
intro e
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
p : ↑b b' ∈ range v'
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
⊢ False
have p : b b' ∈ range v' := by
  use none
  rfl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
p : ↑b b' ∈ range v
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
p : ↑b b' ∈ range v'
⊢ False
rw [← e] at p
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
p : ↑b b' ∈ range v
⊢ False
exact r' p
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
⊢ v' none = ↑b b'
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
⊢ ↑b b' ∈ range v'
use none
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
e : range v = range v'
⊢ v' none = ↑b b'
rfl
case none.none
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
z : v' none = v' none
⊢ none = none

case none.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' none = v' (some k)
⊢ none = some k

case some.none
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' (some k) = v' none
⊢ some k = none

case some.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k✝ k : κ
z : v' (some k✝) = v' (some k)
⊢ some k✝ = some k
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
⊢ Injective v'
rintro (_ | k) (_ | k) z
no goals
case none.none
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
z : v' none = v' none
⊢ none = none
rfl
case none.some.h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' none = v' (some k)
⊢ False
case none.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' none = v' (some k)
⊢ none = some k
exfalso
no goals
case none.some.h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' none = v' (some k)
⊢ False
exact r' ⟨k, z.symm⟩
case some.none.h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' (some k) = v' none
⊢ False
case some.none
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' (some k) = v' none
⊢ some k = none
exfalso
no goals
case some.none.h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k : κ
z : v' (some k) = v' none
⊢ False
exact r' ⟨k, z⟩
case some.some.e_val
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k✝ k : κ
z : v' (some k✝) = v' (some k)
⊢ k✝ = k
case some.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k✝ k : κ
z : v' (some k✝) = v' (some k)
⊢ some k✝ = some k
congr
no goals
case some.some.e_val
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
k✝ k : κ
z : v' (some k✝) = v' (some k)
⊢ k✝ = k
exact i.injective z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
⊢ ∀ (l : Option κ →₀ R), ↑(Finsupp.total (Option κ) M R v') l = 0 → l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
⊢ LinearIndependent R Subtype.val
rw [linearIndependent_subtype_range inj', linearIndependent_iff]
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑(Finsupp.total (Option κ) M R v') l = 0
⊢ l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
⊢ ∀ (l : Option κ →₀ R), ↑(Finsupp.total (Option κ) M R v') l = 0 → l = 0
intro l z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • v' none + ↑(Finsupp.total κ M R (v' ∘ some)) (Finsupp.some l) = 0
⊢ l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑(Finsupp.total (Option κ) M R v') l = 0
⊢ l = 0
rw [Finsupp.total_option] at z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z :
  ↑l none • Option.elim none (↑b b') v +
      ↑(Finsupp.total κ M R ((fun o => Option.elim o (↑b b') v) ∘ some)) (Finsupp.some l) =
    0
⊢ l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • v' none + ↑(Finsupp.total κ M R (v' ∘ some)) (Finsupp.some l) = 0
⊢ l = 0
simp only [Option.elim'] at z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
⊢ l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z :
  ↑l none • Option.elim none (↑b b') v +
      ↑(Finsupp.total κ M R ((fun o => Option.elim o (↑b b') v) ∘ some)) (Finsupp.some l) =
    0
⊢ l = 0
change _ + Finsupp.total κ M R v l.some = 0 at z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
⊢ l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
⊢ l = 0
have l₀ : l none = 0 := by
  rw [← eq_neg_iff_add_eq_zero] at z
  replace z := neg_eq_iff_eq_neg.mpr z
  apply_fun fun x => b.repr x b'  at z
  simp only [repr_self, LinearEquiv.map_smul, mul_one, Finsupp.single_eq_same, Pi.neg_apply,
    Finsupp.smul_single', LinearEquiv.map_neg, Finsupp.coe_neg] at z
  erw [FunLike.congr_fun (Finsupp.apply_total R (b.repr : M →ₗ[R] ι →₀ R) v l.some) b'] at z
  simpa [Finsupp.total_apply, w] using z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
⊢ l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
⊢ l = 0
have l₁ : l.some = 0 := by
  rw [l₀, zero_smul, zero_add] at z
  exact linearIndependent_iff.mp i _ z
case h.none
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
⊢ ↑l none = ↑0 none

case h.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
a : κ
⊢ ↑l (some a) = ↑0 (some a)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
⊢ l = 0
ext (_ | a)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v = -↑(Finsupp.total κ M R v) (Finsupp.some l)
⊢ ↑l none = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
⊢ ↑l none = 0
rw [← eq_neg_iff_add_eq_zero] at z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : -(↑l none • Option.elim none (↑b b') v) = ↑(Finsupp.total κ M R v) (Finsupp.some l)
⊢ ↑l none = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v = -↑(Finsupp.total κ M R v) (Finsupp.some l)
⊢ ↑l none = 0
replace z := neg_eq_iff_eq_neg.mpr z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑(↑b.repr (-(↑l none • Option.elim none (↑b b') v))) b' = ↑(↑b.repr (↑(Finsupp.total κ M R v) (Finsupp.some l))) b'
⊢ ↑l none = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : -(↑l none • Option.elim none (↑b b') v) = ↑(Finsupp.total κ M R v) (Finsupp.some l)
⊢ ↑l none = 0
apply_fun fun x => b.repr x b'  at z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : -↑(↑l none • ↑b.repr (Option.elim none (↑b b') v)) b' = ↑(↑b.repr (↑(Finsupp.total κ M R v) (Finsupp.some l))) b'
⊢ ↑l none = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑(↑b.repr (-(↑l none • Option.elim none (↑b b') v))) b' = ↑(↑b.repr (↑(Finsupp.total κ M R v) (Finsupp.some l))) b'
⊢ ↑l none = 0
simp only [repr_self, LinearEquiv.map_smul, mul_one, Finsupp.single_eq_same, Pi.neg_apply,
  Finsupp.smul_single', LinearEquiv.map_neg, Finsupp.coe_neg] at z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z :
  -↑(↑l none • ↑b.repr (Option.elim none (↑b b') v)) b' =
    ↑(↑(Finsupp.total κ (ι →₀ R) R (↑↑b.repr ∘ v)) (Finsupp.some l)) b'
⊢ ↑l none = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : -↑(↑l none • ↑b.repr (Option.elim none (↑b b') v)) b' = ↑(↑b.repr (↑(Finsupp.total κ M R v) (Finsupp.some l))) b'
⊢ ↑l none = 0
erw [FunLike.congr_fun (Finsupp.apply_total R (b.repr : M →ₗ[R] ι →₀ R) v l.some) b'] at z
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z :
  -↑(↑l none • ↑b.repr (Option.elim none (↑b b') v)) b' =
    ↑(↑(Finsupp.total κ (ι →₀ R) R (↑↑b.repr ∘ v)) (Finsupp.some l)) b'
⊢ ↑l none = 0
simpa [Finsupp.total_apply, w] using z
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
⊢ Finsupp.some l = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
⊢ Finsupp.some l = 0
rw [l₀, zero_smul, zero_add] at z
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
⊢ Finsupp.some l = 0
exact linearIndependent_iff.mp i _ z
no goals
case h.none
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
⊢ ↑l none = ↑0 none
simp only [l₀, Finsupp.coe_zero, Pi.zero_apply]
case h.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
a : κ
⊢ ↑0 a = ↑0 (some a)
case h.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
a : κ
⊢ ↑l (some a) = ↑0 (some a)
erw [FunLike.congr_fun l₁ a]
no goals
case h.some
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.160592
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
b' : ι
w : ∀ (x : κ), ↑(↑b.repr (v x)) b' = 0
v' : Option κ → M := fun o => Option.elim o (↑b b') v
r : range v ⊆ range v'
r' : ¬↑b b' ∈ range v
r'' : range v ≠ range v'
inj' : Injective v'
l : Option κ →₀ R
z : ↑l none • Option.elim none (↑b b') v + ↑(Finsupp.total κ M R v) (Finsupp.some l) = 0
l₀ : ↑l none = 0
l₁ : Finsupp.some l = 0
a : κ
⊢ ↑0 a = ↑0 (some a)
simp only [Finsupp.coe_zero, Pi.zero_apply]