dumb proof

FltRegular/NumberTheory/Hilbert92.lean

@@ -84,7 +84,15 @@ lemma LinearIndependent.update {ι} [DecidableEq ι] {R} [CommRing R] [Module R
 @[to_additive]
 lemma Subgroup.index_mono {G : Type*} [Group G] {H₁ H₂ : Subgroup G} (h : H₁ < H₂)
   [h₁ : Fintype (G ⧸ H₁)] :
-  H₂.index < H₁.index := sorry
+  H₂.index < H₁.index := by
+  rcases eq_or_ne H₂.index 0 with hn | hn
+  · rw [hn, index_eq_card]
+    exact Fintype.card_pos
+  apply lt_of_le_of_ne
+  · refine Nat.le_of_dvd (by rw [index_eq_card]; apply Fintype.card_pos) <| Subgroup.index_dvd_of_le h.le
+  · have := fintypeOfIndexNeZero hn
+    rw [←mul_one H₂.index, ←relindex_mul_index h.le, mul_comm, Ne, eq_comm]
+    simp [-one_mul, -Nat.one_mul, hn, h.not_le]
 
 namespace systemOfUnits