K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this : Subsingleton M
⊢ Module.rank R M = 1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ Module.rank R M = 1
haveI := Module.subsingleton R M
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
⊢ Module.rank R M = 1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this : Subsingleton M
⊢ Module.rank R M = 1
have : Nonempty { s : Set M // LinearIndependent R ((↑) : s → M) } :=
  ⟨⟨∅, linearIndependent_empty _ _⟩⟩
case 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.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
⊢ ∀ (i : { s // LinearIndependent R Subtype.val }), (#↑↑i) ≤ 1

case 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.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
⊢ ∀ (w : Cardinal), w < 1 → ∃ i, w < (#↑↑i)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
⊢ Module.rank R M = 1
rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
case 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.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ ∃ i, w < (#↑↑i)
case 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.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
⊢ ∀ (w : Cardinal), w < 1 → ∃ i, w < (#↑↑i)
intro w hw
case h₂.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ LinearIndependent R Subtype.val

case h₂.refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ w < (#↑↑{ val := {0}, property := ?h₂.refine'_1 })
case 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.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ ∃ i, w < (#↑↑i)
refine' ⟨⟨{0}, _⟩, _⟩
case h₁.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
s : Set M
hs : LinearIndependent R Subtype.val
⊢ (#↑↑{ val := s, property := hs }) ≤ 1
case 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.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
⊢ ∀ (i : { s // LinearIndependent R Subtype.val }), (#↑↑i) ≤ 1
rintro ⟨s, hs⟩
case h₁.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
s : Set M
hs : LinearIndependent R Subtype.val
⊢ Set.Subsingleton ↑{ val := s, property := hs }
case h₁.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
s : Set M
hs : LinearIndependent R Subtype.val
⊢ (#↑↑{ val := s, property := hs }) ≤ 1
rw [Cardinal.mk_le_one_iff_set_subsingleton]
no goals
case h₁.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
s : Set M
hs : LinearIndependent R Subtype.val
⊢ Set.Subsingleton ↑{ val := s, property := hs }
apply subsingleton_of_subsingleton
case h₂.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ ∀ (s : Finset { x // x ∈ {0} }) (g : { x // x ∈ {0} } → R),
    ∑ i in s, g i • ↑i = 0 → ∀ (i : { x // x ∈ {0} }), i ∈ s → g i = 0
case h₂.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ LinearIndependent R Subtype.val
rw [linearIndependent_iff']
case h₂.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
s✝ : Finset { x // x ∈ {0} }
g✝ : { x // x ∈ {0} } → R
a✝¹ : ∑ i in s✝, g✝ i • ↑i = 0
i✝ : { x // x ∈ {0} }
a✝ : i✝ ∈ s✝
⊢ g✝ i✝ = 0
case h₂.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ ∀ (s : Finset { x // x ∈ {0} }) (g : { x // x ∈ {0} } → R),
    ∑ i in s, g i • ↑i = 0 → ∀ (i : { x // x ∈ {0} }), i ∈ s → g i = 0
intros
no goals
case h₂.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
s✝ : Finset { x // x ∈ {0} }
g✝ : { x // x ∈ {0} } → R
a✝¹ : ∑ i in s✝, g✝ i • ↑i = 0
i✝ : { x // x ∈ {0} }
a✝ : i✝ ∈ s✝
⊢ g✝ i✝ = 0
exact Subsingleton.elim _ _
no goals
case h₂.refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.228981
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndependent R Subtype.val }
w : Cardinal
hw : w < 1
⊢ w < (#↑↑{ val := {0}, property := (_ : LinearIndependent R Subtype.val) })
exact hw.trans_eq (Cardinal.mk_singleton _).symm