-- Mathlib/LinearAlgebra/FreeModule/PID.lean
theorem Ideal.exists_smith_normal_form (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) :
    ∃ (b' : Basis ι R S) (a : ι → R) (ab' : Basis ι R I), ∀ i, (ab' i : S) = a i • b' i

Proof state:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
val✝ : Fintype ι
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Tactic:
let ⟨bS, bI, f, a, snf⟩ := I.smithNormalForm b hI

Result:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
val✝ : Fintype ι
bS : Basis ι R S
bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Proof state:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
val✝ : Fintype ι
bS : Basis ι R S
bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Tactic:
let e : Fin (Fintype.card ι) ≃ ι :=
  Equiv.ofBijective f
    ((Fintype.bijective_iff_injective_and_card f).mpr ⟨f.injective, Fintype.card_fin _⟩)

Result:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
val✝ : Fintype ι
bS : Basis ι R S
bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective ⇑f ⋯
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
val✝ : Fintype ι
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Proof state:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
val✝ : Fintype ι
bS : Basis ι R S
bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective ⇑f ⋯
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Tactic:
have fe : ∀ i, f (e.symm i) = i := e.apply_symm_apply

Result:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
val✝ : Fintype ι
bS : Basis ι R S
bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective ⇑f ⋯
fe : ∀ (i : ι), f (e.symm i) = i
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i