awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 1 ⋯ = 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
x y : M
simp :
  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
      (HMul.hMul (α := K) (β := K) ((f : (a : M) → K) x : K) ((f : (a : M) → K) y : K)) ⋯ =
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) x) ⋯ :
        ↥(integralClosure ℤ K))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) y) ⋯ :
        ↥(integralClosure ℤ K))
⊢ restrict (⇑f : (a : M) → K) h (x * y) = restrict (⇑f : (a : M) → K) h x * restrict (⇑f : (a : M) → K) h y

Tactic:
simp only [restrict, map_mul]

Premises used: NumberField.RingOfIntegers.restrict, map_mul
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
x y : M
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
      (HMul.hMul (α := K) (β := K) ((f : (a : M) → K) x : K) ((f : (a : M) → K) y : K)) ⋯ =
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) x) ⋯ :
        ↥(integralClosure ℤ K))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) y) ⋯ :
        ↥(integralClosure ℤ K))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
inst_2 : NumberField K_1
M : Type u_3
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
⊢ IsScalarTower.{u_4, u_5, u_5} (𝓞 K) (𝓞 L) L

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
inst_2 : NumberField K_1
M : Type u_3
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
⊢ IsIntegralClosure.{u_5, u_4, u_5} (𝓞 L) (𝓞 K) L

Tactic:
IsIntegralClosure.tower_top (R := ℤ)

Premises used: IsIntegralClosure.tower_top
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
inst_2 : NumberField K_1
M : Type u_3
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
⊢ Algebra.IsIntegral.{u_4, u_5} (𝓞 K) (𝓞 L)

Tactic:
IsIntegralClosure.isIntegral_algebra (𝓞 K) L

Premises used: IsIntegralClosure.isIntegral_algebra, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
inst_2 : NumberField K_1
M : Type u_3
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
inst_6 : NumberField K
inst_7 : NumberField L
⊢ IsNoetherian.{u_4, u_5} (𝓞 K) (𝓞 L)

Tactic:
IsIntegralClosure.isNoetherian (𝓞 K) K L (𝓞 L)

Premises used: NumberField.RingOfIntegers, IsIntegralClosure.isNoetherian
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
hx : Eq.{u_5 + 1} (α := 𝓞 L) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x : 𝓞 L) (0 : 𝓞 L)
⊢ Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑x : K) : L)
    ((↑((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) : L) : L)

Tactic:
have h : (algebraMap K L) x = (algebraMap (𝓞 K) (𝓞 L)) x := rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
hx : Eq.{u_5 + 1} (α := 𝓞 L) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x : 𝓞 L) (0 : 𝓞 L)
h :
  Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑x : K) : L)
    ((↑((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) : L) : L)
⊢ x = 0

Tactic:
simp only [hx, map_zero, map_eq_zero, RingOfIntegers.coe_eq_zero_iff] at h

Premises used: NumberField.RingOfIntegers.coe_eq_zero_iff, map_zero, map_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
hx : Eq.{u_5 + 1} (α := 𝓞 L) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x : 𝓞 L) (0 : 𝓞 L)
h : x = 0
⊢ x = 0

Tactic:
h
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
hx : Eq.{u_5 + 1} (α := 𝓞 L) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x : 𝓞 L) (0 : 𝓞 L)
h : x = 0
⊢ x = 0

Tactic:
exact h
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
⊢ Injective.{u_4 + 1, u_5 + 1} (α := 𝓞 K) (β := 𝓞 L) (⇑(algebraMap (𝓞 K) (𝓞 L)) : (a : 𝓞 K) → 𝓞 L)

Tactic:
(RingHom.injective_iff_ker_eq_bot (algebraMap (𝓞 K) (𝓞 L))).mpr (ker_algebraMap_eq_bot K L)

Premises used: Iff.mpr, Algebra.algebraMap, NumberField.RingOfIntegers.ker_algebraMap_eq_bot, RingHom.injective_iff_ker_eq_bot, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
inst_2 : NumberField K_1
M : Type u_3
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
⊢ IsTorsionFree.{u_4, u_5} (𝓞 K) (𝓞 L)

Tactic:
isTorsionFree_iff_algebraMap_injective.mpr <| algebraMap.injective K L

Premises used: Iff.mpr, Module.isTorsionFree_iff_algebraMap_injective, NumberField.RingOfIntegers.algebraMap.injective
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
inst_2 : NumberField K_1
M : Type u_3
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
⊢ IsTorsionFree.{u_4, u_5} (𝓞 K) L

Tactic:
.trans_faithfulSMul (𝓞 K) (𝓞 L) L

Premises used: Module.IsTorsionFree.trans_faithfulSMul, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := K)
    (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (((RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)
            i :
          𝓞 K) :
      K)

Tactic:
Basis.localizationLocalization_apply ℚ (nonZeroDivisors ℤ) K (RingOfIntegers.basis K) i

Premises used: Rat, Module.Basis.localizationLocalization_apply, nonZeroDivisors, Int, NumberField.RingOfIntegers.basis
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := ℚ)
    (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) :
            Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
        i :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (((((Basis.repr (RingOfIntegers.basis K) : 𝓞 K ≃ₗ[ℤ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
                    (a : 𝓞 K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ)
                  x :
                Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℤ)
            i :
          ℤ) :
      ℚ)

Tactic:
Basis.localizationLocalization_repr_algebraMap ℚ (nonZeroDivisors ℤ) K _ x i

Premises used: Set.Mem, Rat, setOf, nonZeroDivisors, Int, Module.Basis.localizationLocalization_repr_algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Membership.mem (γ := Submodule ℤ K)
      (Submodule.span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
      x ↔
    Membership.mem (γ := Subring K) (RingHom.range (R := 𝓞 K) (algebraMap (𝓞 K) K)) x

Tactic:
simp [integralBasis, Basis.localizationLocalization_span]

Premises used: NumberField.integralBasis, Module.Basis.localizationLocalization_span
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ finrank.{0, u_1} ℤ (𝓞 K) = finrank ℚ K

Tactic:
IsIntegralClosure.rank ℤ ℚ K (𝓞 K)

Premises used: IsIntegralClosure.rank, Rat, Int, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
z : 𝓞 ℚ
obtain :
  ∀ (z : ℤ),
    Eq (α := ℚ)
      ((↑((ringOfIntegersEquiv : (a : 𝓞 ℚ) → ℤ) ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) z : 𝓞 ℚ)) : ℚ) : ℚ)
      ((algebraMap (𝓞 ℚ) ℚ : (a : 𝓞 ℚ) → ℚ) ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) z : 𝓞 ℚ) : ℚ)
⊢ Eq (α := ℚ) ((↑((ringOfIntegersEquiv : (a : 𝓞 ℚ) → ℤ) z) : ℚ) : ℚ) ((algebraMap (𝓞 ℚ) ℚ : (a : 𝓞 ℚ) → ℚ) z : ℚ)

Tactic:
obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z

Premises used: RingEquiv.surjective, Rat.ringOfIntegersEquiv, RingEquiv.symm, rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
z : ℤ
⊢ Eq (α := ℚ) ((↑((ringOfIntegersEquiv : (a : 𝓞 ℚ) → ℤ) ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) z : 𝓞 ℚ)) : ℚ) : ℚ)
    ((algebraMap (𝓞 ℚ) ℚ : (a : 𝓞 ℚ) → ℚ) ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) z : 𝓞 ℚ) : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
x : ℤ
⊢ Eq (α := ℚ) (↑((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) x) : ℚ) (↑x : ℚ)

Tactic:
eq_intCast ringOfIntegersEquiv.symm _ ▸ rfl

Premises used: Rat.ringOfIntegersEquiv, Eq.rec, eq_intCast, Eq.symm, RingEquiv.symm, rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
f : Polynomial ℚ
hf : Fact (Irreducible f)
⊢ Module.Finite ℚ (AdjoinRoot f)

Tactic:
(AdjoinRoot.powerBasis hf.out.ne_zero).finite

Premises used: PowerBasis.finite, Irreducible.ne_zero, Fact.out, AdjoinRoot.powerBasis
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
f : Polynomial ℚ
hf : Fact (Irreducible f)
⊢ FiniteDimensional ℚ (AdjoinRoot f)

Tactic:
convert! (AdjoinRoot.powerBasis hf.out.ne_zero).finite

Premises used: PowerBasis.finite, Irreducible.ne_zero, Fact.out, AdjoinRoot.powerBasis
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
⊢ IsQuadraticExtension (↥K⁺) K

Tactic:
IsCMField.is_quadratic

Premises used: NumberField.IsCMField.is_quadratic
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
⊢ IsTotallyComplex K

Tactic:
IsCMField.to_isTotallyComplex

Premises used: NumberField.IsCMField.to_isTotallyComplex
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
rw₆ : Module.finrank.{0, u_1} ℚ ↥K⁺ = nrComplexPlaces K
rw₇ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = 2 * nrComplexPlaces K
rw₈ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank ℚ K
rw₉ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank.{0, u_1} ℚ ↥K⁺ * Module.finrank (↥K⁺) K
rw₁₀ : Module.finrank.{0, u_1} ℚ ↥K⁺ * 2 = Module.finrank.{0, u_1} ℚ ↥K⁺ * Module.finrank (↥K⁺) K
rw₁₁ rw₁₂ : Module.finrank.{0, u_1} ℚ ↥K⁺ * 2 = Module.finrank.{0, u_1} ℚ ↥K⁺ * 2
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)

Tactic:
rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]

Premises used: Nat.mul_left_cancel_iff, NumberField.IsTotallyComplex.finrank, NumberField.IsTotallyReal.finrank, zero_add, Algebra.IsQuadraticExtension.finrank_eq_two, mul_comm, NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces, zero_lt_two, add_zero, NumberField.IsTotallyComplex.nrRealPlaces_eq_zero, NumberField.IsTotallyReal.nrComplexPlaces_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
w : InfinitePlace K
⊢ Eq (α := InfinitePlace ↥K⁺) ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
    (w.comap (algebraMap (↥K⁺) K) : InfinitePlace ↥K⁺)

Tactic:
rfl

Premises used: NumberField.InfinitePlace.comap, rfl
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
w : InfinitePlace ↥K⁺
x : ↥K⁺
rw :
  Eq (α := ℝ)
    ((comap ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w) (algebraMap (↥K⁺) K) :
          (a : ↥K⁺) → ℝ)
        x :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺)
              ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w) :
            InfinitePlace ↥K⁺) :
          (a : ↥K⁺) → ℝ)
        x :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
rw₂ rw₃ : Eq (α := ℝ) ((w : (a : ↥K⁺) → ℝ) x : ℝ) ((w : (a : ↥K⁺) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w : InfinitePlace K) :
          (a : K) → ℝ)
        ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) x : K) :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)

Tactic:
rw [← comap_apply, ← equivInfinitePlace_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, NumberField.InfinitePlace.comap_apply, NumberField.IsCMField.equivInfinitePlace_apply
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw : Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1 = Units.rank K
rw₁ : Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
rw₂ rw₃ : Fintype.card.{u_1} (InfinitePlace K) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
⊢ Units.rank.{u_1} ↥K⁺ = Units.rank K

Tactic:
rw [Units.rank, Units.rank, card_infinitePlace_eq_card_infinitePlace K]

Premises used: NumberField.Units.rank, NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsAlgebraic ℚ K
φ : K →+* ℂ
⊢ ∃ (σ : Gal(K/↥K⁺)), ComplexEmbedding.IsConj φ σ

Tactic:
exists_isConj_of_isRamified <|
    isRamified_iff.mpr ⟨IsTotallyComplex.isComplex _, IsTotallyReal.isReal _⟩

Premises used: Iff.mpr, NumberField.InfinitePlace.exists_isConj_of_isRamified, NumberField.InfinitePlace.isRamified_iff, NumberField.IsTotallyComplex.isComplex, And.intro, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
⊢ Nat.card.{u_1} Gal(K/↥K⁺) = 2

Tactic:
have : Nat.card (K ≃ₐ[K⁺] K) = 2 :=
    (IsQuadraticExtension.finrank_eq_two K⁺ K) ▸ IsGalois.card_aut_eq_finrank K⁺ K
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : Nat.card.{u_1} Gal(K/↥K⁺) = 2
⊢ ∃! y : Gal(K/↥K⁺), y ≠ 1

Tactic:
rw [Nat.card_eq_two_iff' 1] at this

Premises used: Nat.card_eq_two_iff', OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : ∃! y : Gal(K/↥K⁺), y ≠ 1
⊢ σ = τ

Tactic:
ExistsUnique.unique this
    ((isConj_ne_one_iff hφ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ)
    ((isConj_ne_one_iff hψ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal ψ)

Premises used: Iff.mpr, NumberField.ComplexEmbedding.isConj_ne_one_iff, NumberField.IsTotallyComplex.complexEmbedding_not_isReal, ExistsUnique.unique
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : ∃! y : Gal(K/↥K⁺), y ≠ 1
⊢ σ = τ

Tactic:
exact ExistsUnique.unique this
    ((isConj_ne_one_iff hφ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ)
    ((isConj_ne_one_iff hψ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal ψ)

Premises used: Iff.mpr, NumberField.ComplexEmbedding.isConj_ne_one_iff, NumberField.IsTotallyComplex.complexEmbedding_not_isReal, ExistsUnique.unique
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
obtain : ∀ (σ : Gal(K/↥K⁺)) (hσ : ComplexEmbedding.IsConj φ σ), ComplexEmbedding.IsConj φ (complexConj K)
⊢ ComplexEmbedding.IsConj φ (complexConj K)

Tactic:
obtain ⟨σ, hσ⟩ := exists_isConj _ φ

Premises used: NumberField.IsCMField.exists_isConj
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
σ : Gal(K/↥K⁺)
hσ : ComplexEmbedding.IsConj φ σ
⊢ ComplexEmbedding.IsConj (Classical.choice ⋯) (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice ⋯)) ⋯)

Tactic:
have := (exists_isConj K (Classical.choice (inferInstance : Nonempty (K →+* ℂ)))).choose_spec
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
σ : Gal(K/↥K⁺)
hσ : ComplexEmbedding.IsConj φ σ
this :
  ComplexEmbedding.IsConj (Classical.choice ⋯) (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice ⋯)) ⋯)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hσ : ComplexEmbedding.IsConj φ (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice ⋯)) ⋯))
    (this :
      ComplexEmbedding.IsConj (Classical.choice ⋯)
        (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice ⋯)) ⋯)),
    ComplexEmbedding.IsConj φ (complexConj K)
⊢ ComplexEmbedding.IsConj φ (complexConj K)

Tactic:
rwa [isConj_eq_isConj K hσ this] at hσ

Premises used: NumberField.IsCMField.isConj_eq_isConj
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
x : K
rw : Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
rw₁ rw₂ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
⊢ Eq (α := ℂ) ((φ : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)

Tactic:
rw [IsConj.eq (isConj_complexConj K φ), RCLike.star_def]

Premises used: NumberField.IsCMField.isConj_complexConj, RCLike.star_def, NumberField.ComplexEmbedding.IsConj.eq
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
rw : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ) = (w : (a : K) → ℝ) x
rw₁ : Norm.norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) : ℂ) = (w : (a : K) → ℝ) x
rw₂ : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
rw₃ rw₄ : Eq (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) ((w : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((complexConj K : (a : K) → K) x : K) : ℝ) ((w : (a : K) → ℝ) x : ℝ)

Tactic:
rw [← norm_embedding_eq, complexEmbedding_complexConj, Complex.norm_conj, norm_embedding_eq]

Premises used: Complex.norm_conj, NumberField.InfinitePlace.norm_embedding_eq, NumberField.IsCMField.complexEmbedding_complexConj
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
x : K
φ : K →+* ℂ := Classical.choice ⋯
⊢ (complexConj K : (a : K) → K) ((complexConj K : (a : K) → K) x : K) = x

Tactic:
isConj_apply_apply (isConj_complexConj K φ) x

Premises used: NumberField.IsCMField.isConj_complexConj, NumberField.ComplexEmbedding.isConj_apply_apply
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
x : K
φ : K →+* ℂ := Classical.choice ⋯
⊢ (complexConj K : (a : K) → K) ((complexConj K : (a : K) → K) x : K) = x

Tactic:
exact isConj_apply_apply (isConj_complexConj K φ) x

Premises used: NumberField.IsCMField.isConj_complexConj, NumberField.ComplexEmbedding.isConj_apply_apply
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
⊢ Ne (α := Gal(K/↥K⁺)) (complexConj K) 1

Tactic:
(isConj_ne_one_iff
    (exists_isConj K (Classical.choice (inferInstance : Nonempty _))).choose_spec).mpr <|
      IsTotallyComplex.complexEmbedding_not_isReal _

Premises used: Iff.mpr, NumberField.ComplexEmbedding.isConj_ne_one_iff, Exists.choose_spec, Classical.choice, NumberField.IsTotallyComplex.complexEmbedding_not_isReal, inferInstance, NumberField.IsCMField.exists_isConj, NumberField.IsCMField.complexConj
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
x : ↥K⁺
⊢ (complexConj K : (a : K) → K) (↑x : K) = (↑x : K)

Tactic:
AlgEquiv.commutes _ x

Premises used: AlgEquiv.commutes
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
h :
  ∀ (a : K),
    Eq (α := K) ((HPow.hPow (α := Gal(K/↥K⁺)) (β := ℕ) (complexConj K) 2 : (a : K) → K) a : K) ((1 : (a : K) → K) a : K)
⊢ HPow.hPow (α := Gal(K/↥K⁺)) (β := ℕ) (complexConj K) 2 = 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
a : K
⊢ Eq (α := K) ((HPow.hPow (α := Gal(K/↥K⁺)) (β := ℕ) (complexConj K) 2 : (a : K) → K) a : K) ((1 : (a : K) → K) a : K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : Algebra.IsIntegral ℚ K
⊢ Eq (α := Subgroup Gal(K/↥K⁺)) (Subgroup.zpowers (complexConj K)) ⊤

Tactic:
Subgroup.eq_top_of_card_eq _ ?_

Premises used: Subgroup.eq_top_of_card_eq