awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : w.IsReal
main₁ : w.embedding = ψ.toRingHom
⊢ w.IsReal

Tactic:
rw [conjugate_embedding_eq_of_isReal hw, or_self] at main

Premises used: NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal, or_self
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom
hw : w.IsReal
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
congr_arg RingHom.toRatAlgHom main

Premises used: RingHom.toRatAlgHom, congr_arg
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom
hw : w.IsReal
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
exact congr_arg RingHom.toRatAlgHom main

Premises used: RingHom.toRatAlgHom, congr_arg
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)

Premises used: RingHom.toRatAlgHom, congr_arg, Or.resolve_right, LT.lt.not_ge
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
inr :
  ∀ (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom), 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)

Premises used: RingHom.toRatAlgHom, congr_arg, Or.resolve_right, LT.lt.not_ge
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
rw :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
⊢ Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0

Tactic:
rw [← Complex.conj_eq_iff_im]

Premises used: Complex.conj_eq_iff_im
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ Eq (α := ℂ) ((ComplexEmbedding.conjugate w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
    ((ψ.toRingHom : (a : K) → ℂ) (↑x : K) : ℂ)

Tactic:
have := RingHom.congr_fun h' x
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
rw : Eq (α := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
⊢ Eq (α := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)

Tactic:
hψ.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
⊢ Eq (α := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)

Tactic:
exact hψ.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0

Tactic:
have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
inl : ∀ (hw : w.IsReal), w.embedding.toRatAlgHom = ψ
inr : ∀ (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1), w.embedding.toRatAlgHom = ψ
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
cases h₃ with
    | inl hw =>
      rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
      exact congr_arg RingHom.toRatAlgHom main
    | inr hw =>
      refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
      have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
      rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h

Premises used: NumberField.InfinitePlace.norm_embedding_eq, MulZeroClass.zero_mul, NumberField.RingOfIntegers.val, Complex.norm_real, NumberField.InfinitePlace.embedding, Complex.ofReal_zero, or_self, Complex.re_add_im, add_zero, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
⊢ ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits

Tactic:
fun x ↦ IsAlgClosed.splits _

Premises used: Algebra.algebraMap, Rat, minpoly, IsAlgClosed.splits, Polynomial.map, Complex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
⊢ ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits

Tactic:
exact fun x ↦ IsAlgClosed.splits _

Premises used: IsAlgClosed.splits
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
rw : Eq (α := Subalgebra ℚ K) (IntermediateField.toSubalgebra ℚ⟮(↑x : K)⟯) ⊤
⊢ Eq (α := Subalgebra ℚ K) ℚ[(↑x : K)] ⊤

Tactic:
rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite ℚ _)]

Premises used: IsAlgebraic.of_finite, Rat, IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
⊢ Eq (α := Subalgebra ℚ K) (IntermediateField.toSubalgebra ℚ⟮(↑x : K)⟯) ⊤

Tactic:
congr_arg IntermediateField.toSubalgebra <|
    NumberField.is_primitive_element_of_infinitePlace_lt h₁ h₂ h₃

Premises used: NumberField.is_primitive_element_of_infinitePlace_lt, congr_arg, IntermediateField.toSubalgebra, Subalgebra.copy
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
⊢ Eq (α := Subalgebra ℚ K) (IntermediateField.toSubalgebra ℚ⟮(↑x : K)⟯) ⊤

Tactic:
exact congr_arg IntermediateField.toSubalgebra <|
    NumberField.is_primitive_element_of_infinitePlace_lt h₁ h₂ h₃

Premises used: NumberField.is_primitive_element_of_infinitePlace_lt, congr_arg, IntermediateField.toSubalgebra
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } = nrRealPlaces K

Tactic:
Fintype.card_congr mkReal

Premises used: Fintype.card_congr, NumberField.InfinitePlace.mkReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ card.{u_1} { x : InfinitePlace K // x.IsReal ∨ x.IsComplex } =
    card.{u_1} { x : InfinitePlace K // x.IsReal } + card.{u_1} { x : InfinitePlace K // x.IsComplex }

Tactic:
Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K))
      (disjoint_isReal_isComplex K)

Premises used: NumberField.InfinitePlace.IsComplex, Fintype.card_subtype_or_disjoint, NumberField.InfinitePlace.IsReal, NumberField.InfinitePlace.disjoint_isReal_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : card.{u_1} (InfinitePlace K) = card.{u_1} { x : InfinitePlace K // x.IsReal ∨ x.IsComplex }
⊢ card.{u_1} (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

Tactic:
convert!
    Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K))
      (disjoint_isReal_isComplex K) using 1

Premises used: NumberField.InfinitePlace.IsComplex, Fintype.card_subtype_or_disjoint, NumberField.InfinitePlace.IsReal, NumberField.InfinitePlace.disjoint_isReal_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : w.IsReal ∨ w.IsComplex
⊢ Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ card.{u_1} (InfinitePlace K) = card.{u_1} { x : InfinitePlace K // x.IsReal ∨ x.IsComplex }

Tactic:
exact (Fintype.card_of_subtype _ (fun w ↦ ⟨fun _ ↦ isReal_or_isComplex w, fun _ ↦ by simp⟩)).symm

Premises used: NumberField.InfinitePlace.isReal_or_isComplex, Iff.intro, Fintype.card_of_subtype, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : card.{u_1} (InfinitePlace K) = card.{u_1} { x : InfinitePlace K // x.IsReal ∨ x.IsComplex }
⊢ card.{u_1} (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

Tactic:
classical
  convert!
    Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K))
      (disjoint_isReal_isComplex K) using 1
  exact (Fintype.card_of_subtype _ (fun w ↦ ⟨fun _ ↦ isReal_or_isComplex w, fun _ ↦ by simp⟩)).symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  ∀ (w : { w : InfinitePlace K // w.IsComplex }),
    Finset.card.{u_1} (α := { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })
        {φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } | mkComplex φ = w} =
      2
rw :
  ∑ j : { w : InfinitePlace K // w.IsComplex },
      ∑ i : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } with mkComplex i = j, 1 =
    2 * nrComplexPlaces K
⊢ card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

Tactic:
rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]

Premises used: Finset.card_eq_sum_ones, Fintype.card, NumberField.InfinitePlace.mkComplex, Finset.sum_fiberwise
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  ∀ (w : { w : InfinitePlace K // w.IsComplex }),
    Finset.card.{u_1} (α := { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })
        {φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } | mkComplex φ = w} =
      2
simp_rw :
  ∑ x : { w : InfinitePlace K // w.IsComplex },
      HSMul.hSMul (β := ℕ)
        (Finset.card.{u_1} (α := { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })
          {i : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } | mkComplex i = x})
        1 =
    2 * nrComplexPlaces K
simp_rw₁ : ∑ x : { w : InfinitePlace K // w.IsComplex }, HSMul.hSMul (α := ℕ) (β := ℕ) 2 1 = 2 * nrComplexPlaces K
simp_rw₂ : ∑ x : { w : InfinitePlace K // w.IsComplex }, HMul.hMul (α := ℕ) 2 1 = 2 * nrComplexPlaces K
simp_rw₃ : ∑ x : { w : InfinitePlace K // w.IsComplex }, 2 = 2 * nrComplexPlaces K
simp_rw₄ :
  ∑ x : { w : InfinitePlace K // w.IsComplex }, 2 =
    2 * Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) Finset.univ
simp_rw₅ :
  ∑ x : { w : InfinitePlace K // w.IsComplex }, 2 =
    HMul.hMul (α := ℕ) 2 (∑ x : { w : InfinitePlace K // w.IsComplex }, 1)
simp_rw₆ :
  Eq (α := ℕ) (∑ x : { w : InfinitePlace K // w.IsComplex }, 2)
    (∑ i : { w : InfinitePlace K // w.IsComplex }, HMul.hMul (α := ℕ) 2 1)
simp_rw₇ :
  HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) Finset.univ) 2 =
    Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) Finset.univ • HMul.hMul (α := ℕ) 2 1
simp_rw₈ :
  Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) Finset.univ * 2 =
    Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) Finset.univ * HMul.hMul (α := ℕ) 2 1
⊢ ∑ j : { w : InfinitePlace K // w.IsComplex },
      ∑ i : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } with mkComplex i = j, 1 =
    2 * nrComplexPlaces K

Tactic:
simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones,
      Finset.mul_sum, Finset.sum_const, smul_eq_mul, mul_one]

Premises used: Finset.mul_sum, Finset.card_eq_sum_ones, Fintype.card, smul_eq_mul, mul_one, Finset.sum_const
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
suffices :
  ∀ (w : { w : InfinitePlace K // w.IsComplex }),
    Finset.card.{u_1} (α := { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })
        {φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } | mkComplex φ = w} =
      2
⊢ card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

Tactic:
suffices ∀ w : { w : InfinitePlace K // IsComplex w },
     #{φ : {φ //¬ ComplexEmbedding.IsReal φ} | mkComplex φ = w} = 2 by
    rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
    simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones,
      Finset.mul_sum, Finset.sum_const, smul_eq_mul, mul_one]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w} = w.mult

Tactic:
card_filter_mk_eq w

Premises used: NumberField.InfinitePlace.card_filter_mk_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
h :
  Finset.card.{u_1} (α := { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })
      {φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } |
        mkComplex φ = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw} =
    Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}
h₁ : 2 = w.mult
⊢ Finset.card.{u_1} (α := { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })
      {φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } |
        mkComplex φ = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw} =
    2

Tactic:
convert! card_filter_mk_eq w

Premises used: NumberField.InfinitePlace.card_filter_mk_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
h :
  card.{u_1}
      { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
        mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } =
    card.{u_1} { x : K →+* ℂ // mk x = w }
⊢ Finset.card.{u_1} (α := { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })
      {φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } |
        mkComplex φ = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw} =
    Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}

Tactic:
rw [← Fintype.card_subtype, ← Fintype.card_subtype]

Premises used: Fintype.card_subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ card.{u_1}
      { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
        mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } =
    card.{u_1} { x : K →+* ℂ // mk x = w }

Tactic:
Fintype.card_congr (Equiv.ofBijective ?_ ⟨fun _ _ h => ?_, fun ⟨φ, hφ⟩ => ?_⟩)

Premises used: Fintype.card_congr, Exists, And.intro, Equiv.ofBijective, _private.0.NumberField.InfinitePlace.card_complex_embeddings.match_2, Eq