awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
h : ∀ (p : T.CompleteType α), p ∈ T.typesWith (φ ⊓ ψ) ↔ p ∈ T.typesWith φ ∩ T.typesWith ψ
⊢ T.typesWith (φ ⊓ ψ) = T.typesWith φ ∩ T.typesWith ψ

Tactic:
ext p
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
p : T.CompleteType α
h :
  (∀ (M : ModelType (↑p : Set L[[α]].Sentence)) (v : Empty → (↑M : Type (max (max u w) v)))
      (xs : Fin 0 → (↑M : Type (max (max u w) v))), BoundedFormula.Realize (φ ⊓ ψ) v xs) ↔
    ∀ (x : ModelType (↑p : Set L[[α]].Sentence)) (x_1 : Empty → (↑x : Type (max (max u w) v)))
      (x_2 : Fin 0 → (↑x : Type (max (max u w) v))), BoundedFormula.Realize φ x_1 x_2 ∧ BoundedFormula.Realize ψ x_1 x_2
⊢ p ∈ T.typesWith (φ ⊓ ψ) ↔ p ∈ T.typesWith φ ∩ T.typesWith ψ

Tactic:
simp only [mem_typesWith_iff, mem_inter_iff, ← SetLike.mem_coe, p.isMaximal.mem_iff_models,
    ModelsBoundedFormula, ← forall_and]

Premises used: Set.mem_inter_iff, FirstOrder.Language.Theory.ModelsBoundedFormula, SetLike.mem_coe, FirstOrder.Language.Theory.IsMaximal.mem_iff_models, FirstOrder.Language.Theory.CompleteType.isMaximal, forall_and, FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
p : T.CompleteType α
⊢ (∀ (M : ModelType (↑p : Set L[[α]].Sentence)) (v : Empty → (↑M : Type (max (max u w) v)))
      (xs : Fin 0 → (↑M : Type (max (max u w) v))), BoundedFormula.Realize (φ ⊓ ψ) v xs) ↔
    ∀ (x : ModelType (↑p : Set L[[α]].Sentence)) (x_1 : Empty → (↑x : Type (max (max u w) v)))
      (x_2 : Fin 0 → (↑x : Type (max (max u w) v))), BoundedFormula.Realize φ x_1 x_2 ∧ BoundedFormula.Realize ψ x_1 x_2

Tactic:
forall₃_congr fun _ _ _ ↦ BoundedFormula.realize_inf

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, forall₃_congr
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
p : T.CompleteType α
⊢ (∀ (M : ModelType (↑p : Set L[[α]].Sentence)) (v : Empty → (↑M : Type (max (max u w) v)))
      (xs : Fin 0 → (↑M : Type (max (max u w) v))), BoundedFormula.Realize (φ ⊓ ψ) v xs) ↔
    ∀ (x : ModelType (↑p : Set L[[α]].Sentence)) (x_1 : Empty → (↑x : Type (max (max u w) v)))
      (x_2 : Fin 0 → (↑x : Type (max (max u w) v))), BoundedFormula.Realize φ x_1 x_2 ∧ BoundedFormula.Realize ψ x_1 x_2

Tactic:
exact forall₃_congr fun _ _ _ ↦ BoundedFormula.realize_inf

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, forall₃_congr
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
hφ : φ ∈ (L.lhomWithConstants α).onTheory T
⊢ T.typesWith φ = Set.univ

Tactic:
univ_subset_iff.mp fun p _ ↦ p.subset hφ

Premises used: Set.univ_subset_iff, Iff.mp, FirstOrder.Language.Theory.CompleteType.subset
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
⊢ Eq (α := Set (T.CompleteType α)) (T.typesWith ⊤) Set.univ

Tactic:
univ_subset_iff.mp fun p _ ↦ p.isMaximal.mem_of_models (φ := ⊤) (fun _ _ _ a ↦ a)

Premises used: Set.univ_subset_iff, FirstOrder.Language.Theory.IsMaximal.mem_of_models, Iff.mp, FirstOrder.Language.Theory.CompleteType.isMaximal
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ T.typesWith ∼φ = (T.typesWith φ)ᶜ

Tactic:
Eq.symm compl_setOf_mem

Premises used: FirstOrder.Language.Theory.CompleteType.compl_setOf_mem, Eq.symm
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ T.typesWith ∼φ = (T.typesWith φ)ᶜ

Tactic:
exact Eq.symm compl_setOf_mem

Premises used: FirstOrder.Language.Theory.CompleteType.compl_setOf_mem, Eq.symm
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
obtain :
  ∀ (M : ModelType (↑p : Set L[[α]].Sentence)), ∃ (M : T.ModelType), p ∈ T.realizedTypes (↑M : Type (max (max u v) w)) α
⊢ ∃ (M : T.ModelType), p ∈ T.realizedTypes (↑M : Type (max (max u v) w)) α

Tactic:
obtain ⟨M⟩ := p.isMaximal.1

Premises used: And.left, FirstOrder.Language.Theory.CompleteType.isMaximal
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
⊢ ∃ (M : T.ModelType), p ∈ T.realizedTypes (↑M : Type (max (max u v) w)) α

Tactic:
⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), ?_⟩

Premises used: FirstOrder.Language.Theory.ModelType.reduct, FirstOrder.Language.con, Exists.intro, FirstOrder.Language.constantMap, FirstOrder.Language.lhomWithConstants, FirstOrder.Language.Theory.CompleteType.subset, FirstOrder.Language.Theory.ModelType.subtheoryModel
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
refine :
  (T.typeOf (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w)))) =
    p
⊢ ∃ (M : T.ModelType), p ∈ T.realizedTypes (↑M : Type (max (max u v) w)) α

Tactic:
refine ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), ?_⟩
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
⊢ (T.typeOf (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w)))) =
    p

Tactic:
SetLike.ext fun φ => ?_

Premises used: SetLike.ext
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
refine :
  ∀ (φ : L[[α]].Sentence),
    Membership.mem (γ := T.CompleteType α)
        (T.typeOf (M :=
          (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
                (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
            Type (max (max u v) w)))
          fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w))))
        φ ↔
      φ ∈ p
⊢ (T.typeOf (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w)))) =
    p

Tactic:
refine SetLike.ext fun φ => ?_

Premises used: SetLike.ext
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
φ : L[[α]].Sentence
simp :
  (Formula.Realize (L := L) (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      ((_root_.Equiv.symm Formula.equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ) fun (a : α) ↦
      (↑(L.con a) : (↑M : Type (max (max u v) w)))) ↔
    φ ∈ p
⊢ Membership.mem (γ := T.CompleteType α)
      (T.typeOf (M :=
        (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
              (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
          Type (max (max u v) w)))
        fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w))))
      φ ↔
    φ ∈ p

Tactic:
simp only [CompleteType.mem_typeOf]

Premises used: FirstOrder.Language.Theory.CompleteType.mem_typeOf
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
φ : L[[α]].Sentence
⊢ (Formula.Realize (L := L) (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      ((_root_.Equiv.symm Formula.equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ) fun (a : α) ↦
      (↑(L.con a) : (↑M : Type (max (max u v) w)))) ↔
    φ ∈ p

Tactic:
(@Formula.realize_equivSentence_symm_con _
      ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc _ φ).trans
      (_root_.trans (_root_.trans ?_ (p.isMaximal.isComplete.realize_sentence_iff φ M))
        (p.isMaximal.mem_iff_models φ).symm)

Premises used: trans, setOf, FirstOrder.Language.Theory.ModelType.reduct, FirstOrder.Language.Formula.realize_equivSentence_symm_con, FirstOrder.Language.Theory.IsMaximal.mem_iff_models, FirstOrder.Language.Theory.IsMaximal.isComplete, FirstOrder.Language.Theory.ModelType.Carrier, Iff.trans, FirstOrder.Language.Theory.IsComplete.realize_sentence_iff, Set.image, FirstOrder.Language.lhomWithConstants, FirstOrder.Language.Theory.CompleteType.isMaximal, Iff.symm, FirstOrder.Language.Theory.CompleteType.subset, FirstOrder.Language.Theory.ModelType.subtheoryModel, FirstOrder.Language.LHom.onTheory
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
φ : L[[α]].Sentence
_ :
  (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)) ⊨
      φ ↔
    (↑M : Type (max (max u v) w)) ⊨ φ
⊢ (Formula.Realize (L := L) (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      ((_root_.Equiv.symm Formula.equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ) fun (a : α) ↦
      (↑(L.con a) : (↑M : Type (max (max u v) w)))) ↔
    φ ∈ p

Tactic:
refine
    (@Formula.realize_equivSentence_symm_con _
      ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc _ φ).trans
      (_root_.trans (_root_.trans ?_ (p.isMaximal.isComplete.realize_sentence_iff φ M))
        (p.isMaximal.mem_iff_models φ).symm)

Premises used: trans, FirstOrder.Language.Theory.ModelType.reduct, FirstOrder.Language.Formula.realize_equivSentence_symm_con, FirstOrder.Language.Theory.IsMaximal.mem_iff_models, FirstOrder.Language.Theory.IsMaximal.isComplete, FirstOrder.Language.Theory.ModelType.Carrier, Iff.trans, FirstOrder.Language.Theory.IsComplete.realize_sentence_iff, FirstOrder.Language.lhomWithConstants, FirstOrder.Language.Theory.CompleteType.isMaximal, Iff.symm, FirstOrder.Language.Theory.CompleteType.subset, FirstOrder.Language.Theory.ModelType.subtheoryModel
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
φ : L[[α]].Sentence
⊢ (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)) ⊨
      φ ↔
    (↑M : Type (max (max u v) w)) ⊨ φ

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
Goal:
⊢ MDiff (jacobiTheta ∘ UpperHalfPlane.coe)

Tactic:
fun τ => (differentiableAt_jacobiTheta τ.2).mdifferentiableAt.comp τ τ.mdifferentiable_coe

Premises used: UpperHalfPlane.mdifferentiable_coe, MDifferentiableAt.comp, MDifferentiable, DifferentiableAt.mdifferentiableAt, UpperHalfPlane.coe_im_pos, differentiableAt_jacobiTheta
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
⊢ Ne (α := ℕ) 3 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) = hζ.toInteger

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ HPow.hPow (β := ℕ) hζ.toInteger 3 = 1

Tactic:
hζ.toInteger_isPrimitiveRoot.pow_eq_one

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ LT.lt (α := ℕ) 2 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
rw : Nat.totient 3 / 2 - 1 = 0
⊢ Fintype.card.{u_1} (InfinitePlace K) - 1 = 0

Tactic:
rw [card_eq_nrRealPlaces_add_nrComplexPlaces, nrRealPlaces_eq_zero (n := 3) K (by decide),
      zero_add, nrComplexPlaces_eq_totient_div_two (n := 3)]

Premises used: IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two, zero_add, IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero, NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ Nat.totient 3 / 2 - 1 = 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ rank K = 0

Tactic:
have hrank : rank K = 0 := by
    dsimp only [rank]
    rw [card_eq_nrRealPlaces_add_nrComplexPlaces, nrRealPlaces_eq_zero (n := 3) K (by decide),
      zero_add, nrComplexPlaces_eq_totient_div_two (n := 3)]
    rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
obtain :
  ∀ (x : ↥(torsion K)) (e : Fin (rank K) → ℤ)
    (hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
obtain ⟨⟨x, e⟩, hxu, -⟩ := exist_unique_eq_mul_prod _ u

Premises used: NumberField.Units.exist_unique_eq_mul_prod
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
rw : (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i = (↑x : (𝓞 K)ˣ) * 1
⊢ u = (↑x : (𝓞 K)ˣ)

Tactic:
rw [← mul_one x.1, hxu]

Premises used: mul_one, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
h : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i) 1
⊢ (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i = (↑x : (𝓞 K)ˣ) * 1

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
h :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i)
    (∏ x_1 ∈ ∅, fundSystem K x_1 ^ (x, e).2 x_1)
rw : Type
rw₁ : Fin (rank K) → (𝓞 K)ˣ
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i) 1

Tactic:
rw [← Finset.prod_empty]

Premises used: Finset.prod_empty
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
h : IsEmpty (Fin 0)
⊢ Eq (α := Finset (Fin (rank K))) Finset.univ ∅

Tactic:
rw [Finset.univ_eq_empty_iff, hrank]

Premises used: Finset.univ_eq_empty_iff
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ IsEmpty (Fin 0)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ u = (↑x : (𝓞 K)ˣ)

Tactic:
replace hxu : u = x := by
    rw [← mul_one x.1, hxu]
    apply congr_arg
    rw [← Finset.prod_empty]
    congr
    rw [Finset.univ_eq_empty_iff, hrank]
    infer_instance
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
obtain :
  ∀ (n : ℕ) (hnpos : 0 < n) (hn : (↑x : (𝓞 K)ˣ) ^ n = 1),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
obtain ⟨n, hnpos, hn⟩ := isOfFinOrder_iff_pow_eq_one.1 <| (CommGroup.mem_torsion _ _).1 x.2

Premises used: Iff.mp, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn : (↑x : (𝓞 K)ˣ) ^ n = 1
rw :
  Eq (α := K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((↑u : 𝓞 K) ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ)) : K)
    (1 : K)
⊢ HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1

Tactic:
rw [← map_pow]

Premises used: map_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn : (↑x : (𝓞 K)ˣ) ^ n = 1
⊢ Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 1 : K) (1 : K)

Tactic:
map_one (algebraMap (𝓞 K) K)

Premises used: Algebra.algebraMap, map_one, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn : (↑x : (𝓞 K)ˣ) ^ n = 1
h : (↑u : 𝓞 K) ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) = 1
⊢ Eq (α := K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((↑u : 𝓞 K) ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ)) : K)
    (1 : K)

Tactic:
convert! map_one (algebraMap (𝓞 K) K)

Premises used: Algebra.algebraMap, map_one, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn : (↑x : (𝓞 K)ˣ) ^ n = 1
h : ∀ (hn : x ^ n = 1), Eq.{u_1 + 1} (α := 𝓞 K) (↑(↑1 : (𝓞 K)ˣ) : 𝓞 K) 1
⊢ (↑u : 𝓞 K) ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) = 1

Tactic:
rw_mod_cast [hxu, hn]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn : x ^ n = 1
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (↑(↑1 : (𝓞 K)ˣ) : 𝓞 K) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn : (↑x : (𝓞 K)ˣ) ^ n = 1
⊢ HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1

Tactic:
replace hn : (↑u : K) ^ ((⟨n, hnpos⟩ : ℕ+) : ℕ) = 1 := by
    rw [← map_pow]
    convert! map_one (algebraMap (𝓞 K) K)
    rw_mod_cast [hxu, hn]
    simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
⊢ Odd (α := ℕ) 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
obtain :
  ∀ (r : ℕ) (hr3 : r < 3)
    (hru :
      (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r ∨
        (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
obtain ⟨r, hr3, hru⟩ := hζ.exists_pow_or_neg_mul_pow_of_isOfFinOrder (by decide)
    (isOfFinOrder_iff_pow_eq_one.2 ⟨n, hnpos, hn⟩)

Premises used: Iff.mpr, IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one