tidy up

FltRegular/NumberTheory/Hilbert92.lean

@@ -718,6 +718,19 @@ lemma h_exists' : ∃ (h : ℕ) (ζ : (𝓞 k)ˣ),
 --     obtain ⟨ζ, hζ⟩ := this
 --     refine ⟨n, hζ.unit', hζ, by simpa only [h] using Nat.find_spec H⟩
 
+local notation "r" => NumberField.Units.rank k
+
+lemma Units.coe_val_inv {M S} [DivisionMonoid M]
+    [SetLike S M] [SubmonoidClass S M] {s : S} (v : sˣ) :
+    (v : M)⁻¹ = ((v⁻¹ : _) : M) := by
+  apply inv_eq_of_mul_eq_one_right
+  show ((v * v⁻¹ : _) : M) = 1
+  rw [mul_inv_self]
+  rfl
+
+-- lemma Units.coe_val_inv' {M} [Field M] {s : Subalgebra ℤ M} (v : (↥s)ˣ) :
+--     ((v⁻¹ : _) : M) = (v : M)⁻¹ := Units.coe_val_inv v
+set_option maxHeartbeats 10000000 in
 lemma Hilbert92ish (hp : Nat.Prime p)
     [Algebra k K] [IsGalois k K] [FiniteDimensional k K] [InfinitePlace.IsUnramified k K]
     [IsCyclic (K ≃ₐ[k] K)]
@@ -727,40 +740,35 @@ lemma Hilbert92ish (hp : Nat.Prime p)
     by_cases H : ∀ ε : (𝓞 K)ˣ, (algebraMap k K ζ) ≠ ε / (σ ε : K)
     sorry
     simp only [ne_eq, not_forall, not_not] at H
-    obtain ⟨ E, hE⟩:= H
-    let NE := Units.map (RingOfIntegers.norm k ) E
+    obtain ⟨E, hE⟩ := H
+    let NE := Units.map (RingOfIntegers.norm k) E
     obtain ⟨S, hS⟩ := Hilbert91ish p (K := K) (k := k) hp hKL σ hσ
-    have NE_p_pow : ((Units.map (algebraMap (𝓞 k) (𝓞 K) ).toMonoidHom  ) NE) = E^(p : ℕ) := by sorry
+    have NE_p_pow : (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom NE) = E ^ (p : ℕ) := by sorry
     let H := unitlifts p hp hKL σ hσ S
-    let N : Fin (NumberField.Units.rank k + 1) →  Additive (𝓞 k)ˣ :=
-      fun e => Additive.ofMul (Units.map (RingOfIntegers.norm k )) (Additive.toMul (H e))
-    let η : Fin (NumberField.Units.rank k + 1).succ →  Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
-    obtain ⟨a, ι,i, ha⟩ := lh_pow_free p hp ζ (k := k) (K:= K) hζ.2 η
-    let Ζ :=  ((Units.map (algebraMap (𝓞 k) (𝓞 K) ).toMonoidHom  ) ζ)^(-a)
-    let H2 : Fin (NumberField.Units.rank k + 1).succ →  Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul (E))
-    let J := (Additive.toMul (∑ i : Fin (NumberField.Units.rank k + 1).succ, ι i • H2 i)) *
-                 ((Units.map (algebraMap (𝓞 k) (𝓞 K) ).toMonoidHom  ) ζ)^(-a)
+    let N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
+      fun e => Additive.ofMul (Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e))
+    let η : Fin (r + 1).succ → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
+    obtain ⟨a, ι, i, ha, ha'⟩ := lh_pow_free p hp ζ (k := k) (K := K) hζ.2 η
+    let Ζ := (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom ζ) ^ (-a)
+    let H2 : Fin (r + 1).succ → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
+    let J := (Additive.toMul (∑ i : Fin (r + 1).succ, ι i • H2 i)) *
+                 (Units.map (algebraMap (𝓞 k) (𝓞 K) ).toMonoidHom ζ)^(-a)
     refine ⟨J, ?_⟩
     constructor
 
-    have JM : J = E^(ι (Fin.last (NumberField.Units.rank k + 1)))* Ζ *
-          ∏ i : (Fin (NumberField.Units.rank k + 1)), (Additive.toMul (H2 i))^(ι i) := by
-      simp only  [toMul_sum]
+    have JM : J = E ^ (ι (Fin.last (r + 1))) * Ζ *
+          ∏ i : (Fin (r + 1)), (Additive.toMul (H2 i)) ^ (ι i) := by
+      simp only [toMul_sum]
       rw [Fin.prod_univ_castSucc]
       simp only [Fin.snoc_castSucc, toMul_zsmul, Fin.snoc_last, toMul_ofMul,
         RingHom.toMonoidHom_eq_coe, zpow_neg, Fin.coe_eq_castSucc]
-      sorry
-
-
-
+      conv_rhs => rw [mul_comm, ← mul_assoc]
     rw [JM]
     simp only [zpow_neg, RingHom.toMonoidHom_eq_coe, Fin.coe_eq_castSucc, Fin.snoc_castSucc,
       Units.val_mul, Units.coe_prod, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid,
       Subalgebra.coe_toSubsemiring, coe_zpow', Submonoid.coe_finset_prod, map_mul, map_prod]
-
-
-
-
+    rw [← Units.coe_val_inv, norm_map_inv]
+    simp only [coe_zpow', Units.coe_map, MonoidHom.coe_coe]
     sorry
     sorry
 /-