awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
h :
  Membership.mem (γ := Set K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ)) a
u : (𝓞 K)ˣ
h_tors : u ∈ (↑(torsion K) : Set (𝓞 K)ˣ)
h_ua : (fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u = a
φ : K →+* ℂ
⊢ norm (E := ℂ) ((φ : (a : K) → ℂ) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u) : ℂ) ≤
    1

Tactic:
le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)

Premises used: NumberField.Units.mem_torsion, Iff.mp, NumberField.InfinitePlace.eq_iff_eq, le_of_eq, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
h :
  Membership.mem (γ := Set K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ)) a
u : (𝓞 K)ˣ
h_tors : u ∈ (↑(torsion K) : Set (𝓞 K)ˣ)
h_ua : (fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u = a
φ : K →+* ℂ
⊢ norm (E := ℂ) ((φ : (a : K) → ℂ) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u) : ℂ) ≤
    1

Tactic:
exact le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)

Premises used: NumberField.Units.mem_torsion, Iff.mp, NumberField.InfinitePlace.eq_iff_eq, le_of_eq, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsCyclic.{u_1} ↥(torsion K)

Tactic:
isCyclic_subgroup_units _

Premises used: isCyclic_subgroup_units
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ NeZero (torsionOrder K)

Tactic:
inferInstanceAs (NeZero (Fintype.card (torsion K)))

Premises used: _private.0.NumberField.Units.instNeZeroNatTorsionOrder._proof_1
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ torsionOrder K ≠ 0

Tactic:
NeZero.ne (torsionOrder K)

Premises used: NumberField.Units.torsionOrder, NeZero.ne
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < torsionOrder K

Tactic:
Nat.pos_of_neZero (torsionOrder K)

Premises used: NumberField.Units.torsionOrder, Nat.pos_of_neZero
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ = 1
rw : HPow.hPow (α := (𝓞 K)ˣ) 1 (↑k : ℕ) = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 1
⊢ ζ ^ (↑k : ℕ) = 1

Tactic:
rw [h, one_pow]

Premises used: one_pow
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
refine : ∀ (h : ζ ^ (↑k : ℕ) = 1), ζ = 1
⊢ ζ ^ (↑k : ℕ) = 1 ↔ ζ = 1

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ ζ = 1

Tactic:
orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)

Premises used: Nat.eq_one_of_dvd_coprimes, Iff.mp, orderOf_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
refine_1 : orderOf ζ ∣ (↑k : ℕ)
refine_2 : orderOf ζ ∣ torsionOrder K
⊢ ζ = 1

Tactic:
refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)

Premises used: Nat.eq_one_of_dvd_coprimes, Iff.mp, orderOf_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ orderOf ζ ∣ (↑k : ℕ)

Tactic:
orderOf_dvd_of_pow_eq_one h

Premises used: orderOf_dvd_of_pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ orderOf ζ ∣ (↑k : ℕ)

Tactic:
exact orderOf_dvd_of_pow_eq_one h

Premises used: orderOf_dvd_of_pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
rw : ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ

Tactic:
rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]

Premises used: NumberField.Units.torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1

Tactic:
⟨k, k.prop, h⟩

Premises used: PNat.val, Subtype.prop, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1

Tactic:
exact ⟨k, k.prop, h⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ

Tactic:
have hζ : ζ ∈ torsion K := by
      rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
      exact ⟨k, k.prop, h⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
refine_2 :
  orderOf (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ hζ) ∣
    torsionOrder K
⊢ orderOf ζ ∣ torsionOrder K

Tactic:
rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]

Premises used: orderOf_submonoid, Subtype.mk
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ orderOf (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ hζ) ∣
    torsionOrder K

Tactic:
orderOf_dvd_card

Premises used: Set.Mem, CommMonoid.torsion, CommGroup.torsion, NumberField.Units.torsionOrder, orderOf_dvd_card, NumberField.Units.torsion
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ orderOf (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ hζ) ∣
    torsionOrder K

Tactic:
exact orderOf_dvd_card

Premises used: orderOf_dvd_card
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (ζ : (𝓞 K)ˣ),
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) ζ ↔
      Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) (torsion K)

Tactic:
ext ζ
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ^ torsionOrder K = 1 ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : ∀ (h : ζ ^ torsionOrder K = 1), Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
h₁ : ∀ (h : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ), ζ ^ torsionOrder K = 1
⊢ ζ ^ torsionOrder K = 1 ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
h₁ : ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ

Tactic:
rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]

Premises used: CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1

Tactic:
⟨torsionOrder K, torsionOrder_pos K, h⟩

Premises used: NumberField.Units.torsionOrder_pos, NumberField.Units.torsionOrder, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1

Tactic:
exact ⟨torsionOrder K, torsionOrder_pos K, h⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
⊢ ζ ^ torsionOrder K = 1

Tactic:
Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ _ ⟨ζ, h⟩)

Premises used: pow_card_eq_one, NumberField.Units.torsionOrder, Subtype.ext_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
⊢ ζ ^ torsionOrder K = 1

Tactic:
exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ _ ⟨ζ, h⟩)

Premises used: pow_card_eq_one, Subtype.ext_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hle : Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ
hcard : Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) = rootsOfUnity (torsionOrder K) ℂ

Tactic:
apply Subgroup.eq_of_le_of_card_ge

Premises used: Subgroup.eq_of_le_of_card_ge
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hle : Subgroup.map (Units.complexEmbedding φ) (rootsOfUnity (torsionOrder K) (𝓞 K)) ≤ rootsOfUnity (torsionOrder K) ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ

Tactic:
rw [← rootsOfUnity_eq_torsion]

Premises used: NumberField.Units.rootsOfUnity_eq_torsion
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (rootsOfUnity (torsionOrder K) (𝓞 K)) ≤ rootsOfUnity (torsionOrder K) ℂ

Tactic:
map_rootsOfUnity _ (torsionOrder K)

Premises used: Set.Mem, NumberField.Units.torsionOrder, map_rootsOfUnity
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (rootsOfUnity (torsionOrder K) (𝓞 K)) ≤ rootsOfUnity (torsionOrder K) ℂ

Tactic:
exact map_rootsOfUnity _ (torsionOrder K)

Premises used: NumberField.Units.torsionOrder, map_rootsOfUnity
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  MulEquiv.toEquiv (MulEquiv.symm (Subgroup.equivMapOfInjective (torsion K) (Units.complexEmbedding φ) ⋯))
hcard :
  Fintype.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
hcard₁ : torsionOrder K ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
hcard₂ : torsionOrder K ≤ Nat.card.{u_1} ↥(torsion K)
hcard₃ : Fintype.card.{u_1} ↥(torsion K) ≤ Nat.card.{u_1} ↥(torsion K)
hcard₄ hcard₅ : Fintype.card.{u_1} ↥(torsion K) ≤ Fintype.card.{u_1} ↥(torsion K)
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))

Tactic:
rw [Nat.card_eq_fintype_card, Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder,
      Nat.card_eq_fintype_card]

Premises used: NumberField.Units.torsionOrder, Nat.card_congr, Complex.card_rootsOfUnity, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
rw :
  orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) ∣
    torsionOrder K
⊢ Even (torsionOrder K)

Tactic:
rw [even_iff_two_dvd, ← this]

Premises used: even_iff_two_dvd
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) ∣
    torsionOrder K

Tactic:
orderOf_dvd_card

Premises used: NumberField.Units.torsionOrder, orderOf_dvd_card
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) ∣
    torsionOrder K

Tactic:
exact orderOf_dvd_card

Premises used: orderOf_dvd_card
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
suffices :
  orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
⊢ Even (torsionOrder K)

Tactic:
suffices orderOf (⟨-1, neg_one_mem_torsion⟩ : torsion K) = 2 by
    rw [even_iff_two_dvd, ← this]
    exact orderOf_dvd_card
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ¬Eq (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  orderOf.{u_1} (G := (𝓞 K)ˣ)
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) =
    2
rw₁ :
  orderOf.{u_1} (G := 𝓞 K)
      (↑(↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) :
        𝓞 K) =
    2
rw₂ : orderOf.{u_1} (G := 𝓞 K) (-(↑1 : 𝓞 K)) = 2
rw₃ : orderOf.{u_1} (G := 𝓞 K) (-1) = 2
rw₄ : Eq (α := ℕ) (if ringChar.{u_1} (𝓞 K) = 2 then 1 else 2) 2
rw₅ : Eq (α := ℕ) (if Eq (α := ℕ) 0 2 then 1 else 2) 2
rw₆ rw₇ : Eq (α := ℕ) 2 2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2

Tactic:
rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]

Premises used: orderOf_units, Units.val_neg, orderOf_neg_one, Units.val_one, if_neg, Subgroup.orderOf_coe, ringChar.eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
pos : ∀ (hc : 2 < orderOf (↑x : (𝓞 K)ˣ)), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
neg : ∀ (hc : orderOf (↑x : (𝓞 K)ˣ) ≤ 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1

Tactic:
by_cases! hc : 2 < orderOf (x : (𝓞 K)ˣ)

Premises used: orderOf, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : 2 < orderOf (↑x : (𝓞 K)ˣ)
⊢ 2 < orderOf (↑(↑(↑x : (𝓞 K)ˣ) : 𝓞 K) : K)

Tactic:
rw [← orderOf_units, ← orderOf_submonoid] at hc

Premises used: orderOf_units, orderOf_submonoid
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : 2 < orderOf (↑(↑(↑x : (𝓞 K)ˣ) : 𝓞 K) : K)
linarith : -1 + HSub.hSub (α := ℤ) (↑(nrRealPlaces K) : ℤ) 0 + (HAdd.hAdd (α := ℤ) 0 1 - (↑(nrRealPlaces K) : ℤ)) = 0
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1

Tactic:
linarith [IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt hc (IsPrimitiveRoot.orderOf (x.1 : K)),
        NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank h]

Premises used: Units.val, IsPrimitiveRoot.orderOf, Algebra.algebraMap, NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt, NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank, NumberField.RingOfIntegers, Subtype.val, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf (↑x : (𝓞 K)ˣ) ≤ 2
neg : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 0) (hc : LE.le (α := ℕ) 0 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
neg₁ : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 1) (hc : LE.le (α := ℕ) 1 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
neg₂ : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 2) (hc : LE.le (α := ℕ) 2 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1

Tactic:
interval_cases hi : orderOf (x : (𝓞 K)ˣ)

Premises used: orderOf, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf (↑x : (𝓞 K)ˣ) = 0
hc : LE.le (α := ℕ) 0 2
linarith :
  -1 + HSub.hSub (α := ℤ) (↑(orderOf (↑x : (𝓞 K)ˣ)) : ℤ) 0 + (HAdd.hAdd (α := ℤ) 0 1 - (↑(orderOf (↑x : (𝓞 K)ˣ)) : ℤ)) =
    0
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1

Tactic:
linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion _ x.1).1 x.2)]

Premises used: Iff.mpr, orderOf_pos_iff, Iff.mp, CommGroup.mem_torsion, Subtype.val, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf (↑x : (𝓞 K)ˣ) = 1
hc : LE.le (α := ℕ) 1 2
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1

Tactic:
Or.intro_left _ (orderOf_eq_one_iff.1 hi)

Premises used: Or.intro_left, Iff.mp, orderOf_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf (↑x : (𝓞 K)ˣ) = 1
hc : LE.le (α := ℕ) 1 2
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1

Tactic:
exact Or.intro_left _ (orderOf_eq_one_iff.1 hi)

Premises used: Or.intro_left, Iff.mp, orderOf_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf (↑(↑x : (𝓞 K)ˣ) : 𝓞 K) = 2
hc : LE.le (α := ℕ) 2 2
⊢ Ne (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf (↑x : (𝓞 K)ˣ) = 2
hc : LE.le (α := ℕ) 2 2
⊢ (↑(↑x : (𝓞 K)ˣ) : 𝓞 K) = -1

Tactic:
rw [← orderOf_units, CharP.orderOf_eq_two_iff 0 (by decide)] at hi

Premises used: orderOf_units, CharP.orderOf_eq_two_iff, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf (↑x : (𝓞 K)ˣ) = 2
hc : LE.le (α := ℕ) 2 2
hi₁ : (↑(↑x : (𝓞 K)ˣ) : 𝓞 K) = -1
⊢ LE.le (α := ℕ) 2 2

Tactic:
rw [← orderOf_units, CharP.orderOf_eq_two_iff 0 (by decide)] at hi

Premises used: orderOf_units, CharP.orderOf_eq_two_iff, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : (↑(↑x : (𝓞 K)ˣ) : 𝓞 K) = -1
hc : LE.le (α := ℕ) 2 2
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1

Tactic:
simp [← Units.val_inj, ← Units.val_inj, Units.val_neg, Units.val_one, hi]

Premises used: Units.val_inj, Units.val_neg, Units.val_one
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
⊢ Ne.{u_1 + 1} (α := ↥(torsion K)) 1
    (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯)

Tactic:
simp [← Subtype.coe_ne_coe]

Premises used: Subtype.coe_ne_coe
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
refine :
  ∀ (x : ↥(torsion K)),
    Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x →
      Membership.mem (γ := Finset ↥(torsion K))
        {1, Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯} x
⊢ torsionOrder K = 2

Tactic:
refine (Finset.card_eq_two.2 ⟨1, ⟨-1, neg_one_mem_torsion⟩,
    by simp [← Subtype.coe_ne_coe], Finset.ext fun x ↦ ⟨fun _ ↦ ?_, fun _ ↦ Finset.mem_univ _⟩⟩)

Premises used: Iff.mpr, Finset.mem_univ, Finset.ext, Finset.card_eq_two, And.intro, Iff.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
h_1 : Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x
rw :
  (↑x : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ∨
    (↑x : (𝓞 K)ˣ) =
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ)
⊢ Membership.mem (γ := Finset ↥(torsion K))
    {1, Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯} x

Tactic:
rw [Finset.mem_insert, Finset.mem_singleton, ← Subtype.val_inj, ← Subtype.val_inj]

Premises used: Finset.mem_singleton, Subtype.val_inj, Finset.mem_insert
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
h_1 : Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x
⊢ (↑x : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ∨
    (↑x : (𝓞 K)ˣ) =
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ)

Tactic:
torsion_eq_one_or_neg_one_of_odd_finrank h x

Premises used: NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
h_1 : Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x
⊢ (↑x : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ∨
    (↑x : (𝓞 K)ˣ) =
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ)

Tactic:
exact torsion_eq_one_or_neg_one_of_odd_finrank h x

Premises used: NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank