no goals
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∏ x : Kˣ, x = -1
classical
  have : (∏ x in (@univ Kˣ _).erase (-1), x) = 1 :=
    prod_involution (fun x _ => x⁻¹) (by simp)
      (fun a => by simp (config := { contextual := true }) [Units.inv_eq_self_iff])
      (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
  rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _), this, mul_one]
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
this : ∏ x in erase univ (-1), x = 1
⊢ ∏ x : Kˣ, x = -1
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∏ x : Kˣ, x = -1
have : (∏ x in (@univ Kˣ _).erase (-1), x) = 1 :=
  prod_involution (fun x _ => x⁻¹) (by simp)
    (fun a => by simp (config := { contextual := true }) [Units.inv_eq_self_iff])
    (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
no goals
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
this : ∏ x in erase univ (-1), x = 1
⊢ ∏ x : Kˣ, x = -1
rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _), this, mul_one]
no goals
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : a ∈ erase univ (-1)), a * (fun x x_1 => x⁻¹) a ha = 1
simp
no goals
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : a ∈ erase univ (-1)), a ≠ 1 → (fun x x_1 => x⁻¹) a ha ≠ a
simp (config := { contextual := true }) [Units.inv_eq_self_iff]
no goals
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : a ∈ erase univ (-1)), (fun x x_1 => x⁻¹) a ha ∈ erase univ (-1)
simp [@inv_eq_iff_eq_inv _ _ a]
no goals
K : Type u_1
R : Type ?u.99451
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : a ∈ erase univ (-1)), (fun x x_1 => x⁻¹) ((fun x x_1 => x⁻¹) a ha) (_ : a⁻¹ ∈ erase univ (-1)) = a
simp