case mk
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R { x // x ∈ ⊥ }
⊢ { fst := n, snd := b' } = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
⊢ basisOfPid b ⊥ = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }
obtain ⟨n, b'⟩ := Submodule.basisOfPid b ⊥
case mk
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R { x // x ∈ ⊥ }
e : Fin n ≃ Fin 0 := Basis.indexEquiv b' (Basis.empty { x // x ∈ ⊥ })
⊢ { fst := n, snd := b' } = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }
case mk
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R { x // x ∈ ⊥ }
⊢ { fst := n, snd := b' } = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }
let e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty _ : Basis (Fin 0) R (⊥ : Submodule R M))
case mk
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
b' : Basis (Fin 0) R { x // x ∈ ⊥ }
e : Fin 0 ≃ Fin 0 := Basis.indexEquiv b' (Basis.empty { x // x ∈ ⊥ })
⊢ { fst := 0, snd := b' } = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }
case mk
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R { x // x ∈ ⊥ }
e : Fin n ≃ Fin 0 := Basis.indexEquiv b' (Basis.empty { x // x ∈ ⊥ })
⊢ { fst := n, snd := b' } = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }
obtain rfl : n = 0 := by simpa using Fintype.card_eq.mpr ⟨e⟩
no goals
case mk
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
b' : Basis (Fin 0) R { x // x ∈ ⊥ }
e : Fin 0 ≃ Fin 0 := Basis.indexEquiv b' (Basis.empty { x // x ∈ ⊥ })
⊢ { fst := 0, snd := b' } = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }
exact Sigma.eq rfl (Basis.eq_of_apply_eq <| finZeroElim)
no goals
ι✝ : Type ?u.139339
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b✝ : ι✝ → M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R { x // x ∈ ⊥ }
e : Fin n ≃ Fin 0 := Basis.indexEquiv b' (Basis.empty { x // x ∈ ⊥ })
⊢ n = 0
simpa using Fintype.card_eq.mpr ⟨e⟩