case intro.intro
ι : Type u_1
ι' : Type ?u.464205
R : Type u_2
R₂ : Type ?u.464211
K : Type ?u.464214
M : Type u_3
M' : Type ?u.464220
M'' : Type ?u.464223
V : Type u
V' : Type ?u.464228
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
⊢ Nonempty ι
ι : Type u_1
ι' : Type ?u.464205
R : Type u_2
R₂ : Type ?u.464211
K : Type ?u.464214
M : Type u_3
M' : Type ?u.464220
M'' : Type ?u.464223
V : Type u
V' : Type ?u.464228
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x : M
b : Basis ι R M
inst✝ : Nontrivial M
⊢ Nonempty ι
obtain ⟨x, y, ne⟩ : ∃ x y : M, x ≠ y := Nontrivial.exists_pair_ne
case intro.intro.intro
ι : Type u_1
ι' : Type ?u.464205
R : Type u_2
R₂ : Type ?u.464211
K : Type ?u.464214
M : Type u_3
M' : Type ?u.464220
M'' : Type ?u.464223
V : Type u
V' : Type ?u.464228
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i✝ : ι
c : R
x✝ : M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
i : ι
h✝ : ¬↑(↑b.repr x) i = ↑(↑b.repr y) i
⊢ Nonempty ι
case intro.intro
ι : Type u_1
ι' : Type ?u.464205
R : Type u_2
R₂ : Type ?u.464211
K : Type ?u.464214
M : Type u_3
M' : Type ?u.464220
M'' : Type ?u.464223
V : Type u
V' : Type ?u.464228
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
⊢ Nonempty ι
obtain ⟨i, _⟩ := not_forall.mp (mt b.ext_elem_iff.2 ne)
no goals
case intro.intro.intro
ι : Type u_1
ι' : Type ?u.464205
R : Type u_2
R₂ : Type ?u.464211
K : Type ?u.464214
M : Type u_3
M' : Type ?u.464220
M'' : Type ?u.464223
V : Type u
V' : Type ?u.464228
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i✝ : ι
c : R
x✝ : M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
i : ι
h✝ : ¬↑(↑b.repr x) i = ↑(↑b.repr y) i
⊢ Nonempty ι
exact ⟨i⟩