awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : ComplexEmbedding.conjugate (mk φ).embedding = φ
inr :
  ∀ (hφ : ComplexEmbedding.IsReal (ComplexEmbedding.conjugate (mk φ).embedding))
    (h : ComplexEmbedding.conjugate (mk φ).embedding = φ), ComplexEmbedding.IsReal φ
inr₁ inr₂ inr₃ inr₄ :
  ∀ (hφ : ComplexEmbedding.IsReal φ) (h : ComplexEmbedding.conjugate (mk φ).embedding = φ), ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal φ

Tactic:
rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

Premises used: NumberField.ComplexEmbedding.isReal_conjugate_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
⊢ (mk φ).embedding = φ ∨ ComplexEmbedding.conjugate (mk φ).embedding = φ

Tactic:
cases mk_eq_iff.mp (mk_embedding (mk φ)) with
  | inl h => rwa [h] at hφ
  | inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_eq_iff, NumberField.InfinitePlace.mk, Iff.mp, NumberField.ComplexEmbedding.isReal_conjugate_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
h : w.IsReal
⊢ ComplexEmbedding.conjugate w.embedding = w.embedding

Tactic:
ComplexEmbedding.isReal_iff.mpr (isReal_iff.mp h)

Premises used: Iff.mpr, IsSelfAdjoint, NumberField.InfinitePlace.isReal_iff, Iff.mp, NumberField.ComplexEmbedding.isReal_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
rw : ¬w.IsReal ↔ ¬ComplexEmbedding.IsReal w.embedding
rw₁ rw₂ : ¬ComplexEmbedding.IsReal w.embedding ↔ ¬ComplexEmbedding.IsReal w.embedding
⊢ ¬w.IsReal ↔ w.IsComplex

Tactic:
rw [isComplex_iff, isReal_iff]

Premises used: NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isComplex_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
rw : ¬¬ComplexEmbedding.IsReal w.embedding ↔ w.IsReal
rw₁ : ¬¬ComplexEmbedding.IsReal w.embedding ↔ ComplexEmbedding.IsReal w.embedding
rw₂ rw₃ : ComplexEmbedding.IsReal w.embedding ↔ ComplexEmbedding.IsReal w.embedding
⊢ ¬w.IsComplex ↔ w.IsReal

Tactic:
rw [isComplex_iff, isReal_iff, not_not]

Premises used: Classical.not_not, NumberField.InfinitePlace.isReal_iff, NumberField.InfinitePlace.isComplex_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
rw : w.IsReal ∨ ¬w.IsReal
⊢ w.IsReal ∨ w.IsComplex

Tactic:
rw [← not_isReal_iff_isComplex]

Premises used: NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ ¬w.IsReal

Tactic:
em _

Premises used: em
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ ¬w.IsReal

Tactic:
exact em _

Premises used: em
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w w' : InfinitePlace K
h : w.IsReal
h' : w'.IsComplex
⊢ w ≠ w'

Tactic:
fun h_eq ↦ not_isReal_iff_isComplex.mpr h' (h_eq ▸ h)

Premises used: Iff.mpr, Eq.rec, NumberField.InfinitePlace.not_isReal_iff_isComplex, Not
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Disjoint.{u_1} (α := Set (InfinitePlace K))
    {x : InfinitePlace K |
      match (motive := InfinitePlace K → Prop) x with
      | w => w.IsReal}
    {x : InfinitePlace K |
      match (motive := InfinitePlace K → Prop) x with
      | w => w.IsComplex}

Tactic:
Set.disjoint_iff.2 <| fun _ hw ↦ not_isReal_iff_isComplex.2 hw.2 hw.1

Premises used: Iff.mpr, And.right, And.left, NumberField.InfinitePlace.not_isReal_iff_isComplex, Set.disjoint_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
⊢ (↑((embedding_of_isReal hw : (a : K) → ℝ) x) : ℂ) = (w.embedding : (a : K) → ℂ) x

Tactic:
ComplexEmbedding.IsReal.coe_embedding_apply (isReal_iff.mp hw) x

Premises used: NumberField.InfinitePlace.isReal_iff, NumberField.ComplexEmbedding.IsReal.coe_embedding_apply, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
rw : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ)
rw₁ : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = ‖(↑((embedding_of_isReal hw : (a : K) → ℝ) x) : ℂ)‖
rw₂ rw₃ :
  norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) =
    norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ)
⊢ norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = (w : (a : K) → ℝ) x

Tactic:
rw [← norm_embedding_eq, ← embedding_of_isReal_apply hw, Complex.norm_real]

Premises used: NumberField.InfinitePlace.norm_embedding_eq, Complex.norm_real, NumberField.InfinitePlace.embedding_of_isReal_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : (mk φ).IsReal
contrapose : ∀ (h : ¬ComplexEmbedding.IsReal φ), ¬(mk φ).IsReal
⊢ ComplexEmbedding.IsReal φ

Tactic:
contrapose h
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
rw : (mk φ).IsComplex
⊢ ¬(mk φ).IsReal

Tactic:
rw [not_isReal_iff_isComplex]

Premises used: NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ (mk φ).IsComplex

Tactic:
⟨φ, h, rfl⟩

Premises used: NumberField.InfinitePlace.IsComplex, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ (mk φ).IsComplex

Tactic:
exact ⟨φ, h, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ (mk φ).IsReal ↔ ComplexEmbedding.IsReal φ

Tactic:
⟨isReal_of_mk_isReal, fun H ↦ ⟨_, H, rfl⟩⟩

Premises used: NumberField.InfinitePlace.isReal_of_mk_isReal, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ (mk φ).IsComplex ↔ ¬ComplexEmbedding.IsReal φ

Tactic:
not_isReal_iff_isComplex.symm.trans isReal_mk_iff.not

Premises used: Iff.not, NumberField.InfinitePlace.isReal_mk_iff, Iff.trans, NumberField.InfinitePlace.not_isReal_iff_isComplex, Iff.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h rwa rwa₁ rwa₂ rwa₃ : (mk φ).IsComplex
⊢ ¬ComplexEmbedding.IsReal φ

Tactic:
rwa [← isComplex_mk_iff]

Premises used: NumberField.InfinitePlace.isComplex_mk_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsReal }
rw : Eq (α := ℕ) (if (↑w : InfinitePlace K).IsReal then 1 else 2) 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ (↑w : InfinitePlace K).mult = 1

Tactic:
rw [mult, if_pos w.prop]

Premises used: NumberField.InfinitePlace.mult, if_pos, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsComplex }
rw : Eq (α := ℕ) (if (↑w : InfinitePlace K).IsReal then 1 else 2) 2
rw₁ rw₂ : Eq (α := ℕ) 2 2
⊢ (↑w : InfinitePlace K).mult = 2

Tactic:
rw [mult, if_neg (not_isReal_iff_isComplex.mpr w.prop)]

Premises used: Iff.mpr, NumberField.InfinitePlace.mult, Subtype.prop, NumberField.InfinitePlace.not_isReal_iff_isComplex, if_neg
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
pos : w.IsReal → LT.lt (α := ℕ) 0 1
neg : ¬w.IsReal → LT.lt (α := ℕ) 0 2
⊢ LT.lt (α := ℕ) 0 (if w.IsReal then 1 else 2)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
h : w.IsReal
⊢ LT.lt (α := ℕ) 0 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
h : ¬w.IsReal
⊢ LT.lt (α := ℕ) 0 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.mult ≠ 0

Tactic:
ne_of_gt mult_pos

Premises used: ne_of_gt, NumberField.InfinitePlace.mult_pos
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ Ne (α := ℝ) (↑w.mult : ℝ) 0

Tactic:
Nat.cast_ne_zero.mpr mult_ne_zero

Premises used: Iff.mpr, NumberField.InfinitePlace.mult_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
rw : 1 ≤ w.mult
⊢ LE.le (α := ℝ) 1 (↑w.mult : ℝ)

Tactic:
rw [← Nat.cast_one, Nat.cast_le]

Premises used: Nat.cast_le, Nat.cast_one
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ 1 ≤ w.mult

Tactic:
mult_pos

Premises used: NumberField.InfinitePlace.mult_pos, Nat.lt
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ 1 ≤ w.mult

Tactic:
exact mult_pos

Premises used: NumberField.InfinitePlace.mult_pos
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : {φ : K →+* ℂ | mk φ = w}
| Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : fun (φ : K →+* ℂ) ↦ mk φ = w
s₁ : Finset.univ
congr : DecidablePred fun (x : K →+* ℂ) ↦ x = w.embedding ∨ x = star w.embedding
| {φ : K →+* ℂ | mk φ = w}

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : ∀ (x : K →+* ℂ), mk x = w
| fun (φ : K →+* ℂ) ↦ mk φ = w

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
x : K →+* ℂ
s : x = w.embedding ∨ x = star w.embedding
| mk x = w

Tactic:
rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]

Premises used: NumberField.ComplexEmbedding.conjugate, InvolutiveStar.star_involutive, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_eq_iff, Function.Involutive.eq_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : ∀ (x : K →+* ℂ), x = w.embedding ∨ x = star w.embedding
s₁ : Finset.univ
rw : DecidablePred fun (x : K →+* ℂ) ↦ x = w.embedding ∨ x = star w.embedding
| Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}

Tactic:
congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]

Premises used: NumberField.ComplexEmbedding.conjugate, InvolutiveStar.star_involutive, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_eq_iff, Function.Involutive.eq_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
conv_lhs : Finset.card.{u_1} (α := K →+* ℂ) {x : K →+* ℂ | x = w.embedding ∨ x = star w.embedding} = w.mult
⊢ Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w} = w.mult

Tactic:
conv_lhs =>
    congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]

Premises used: NumberField.ComplexEmbedding.conjugate, InvolutiveStar.star_involutive, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_eq_iff, Function.Involutive.eq_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
simp_rw :
  Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = if w.IsReal then 1 else 2
⊢ Finset.card.{u_1} (α := K →+* ℂ) {x : K →+* ℂ | x = w.embedding ∨ x = star w.embedding} = w.mult

Tactic:
simp_rw [Finset.filter_or, Finset.filter_eq' _ (embedding w),
    Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)),
    Finset.mem_univ, ite_true, mult]

Premises used: Finset.mem_univ, NumberField.ComplexEmbedding.conjugate, NumberField.InfinitePlace.mult, ite_true, Finset.filter_eq', NumberField.InfinitePlace.embedding, Finset.filter_or
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
pos : ∀ (hw : w.IsReal), Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1
neg : ∀ (hw : ¬w.IsReal), Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = if w.IsReal then 1 else 2

Tactic:
split_ifs with hw
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
pos : Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {w.embedding}) = 1
pos₁ : Finset.card (α := K →+* ℂ) {w.embedding} = 1
pos₂ pos₃ : Eq (α := ℕ) 1 1
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1

Tactic:
rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
      Finset.card_singleton]

Premises used: NumberField.InfinitePlace.isReal_iff, Finset.union_idempotent, Iff.mp, NumberField.ComplexEmbedding.isReal_iff, Finset.card_singleton
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2

Tactic:
Finset.card_pair ?_

Premises used: Finset.card_pair, List.foldr, Multiset.ndinsert, Multiset.ndunion, ite
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
neg : w.embedding ≠ ComplexEmbedding.conjugate w.embedding
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2

Tactic:
refine Finset.card_pair ?_

Premises used: Finset.card_pair
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
neg : ¬w.embedding = ComplexEmbedding.conjugate w.embedding
neg₁ : ¬ComplexEmbedding.conjugate w.embedding = w.embedding
neg₂ : ¬ComplexEmbedding.IsReal w.embedding
neg₃ neg₄ neg₅ neg₆ : ¬w.IsReal
⊢ w.embedding ≠ ComplexEmbedding.conjugate w.embedding

Tactic:
rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]

Premises used: NumberField.InfinitePlace.isReal_iff, Ne, eq_comm, NumberField.ComplexEmbedding.isReal_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
α : Type u_2
inst_1 : CommMonoid α
inst_2 : NumberField K
f : InfinitePlace K → α
rw :
  ∏ w : InfinitePlace K, f w =
    HMul.hMul (α := α) (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K))
      (∏ i : { x : InfinitePlace K // ¬x.IsReal },
        f
          (↑((Equiv.subtypeEquivRight (p := fun (x : InfinitePlace K) ↦ ¬x.IsReal) (q := fun (x : InfinitePlace K) ↦
                    x.IsComplex) ⋯ :
                  (a : { x : InfinitePlace K // ¬x.IsReal }) → { x : InfinitePlace K // x.IsComplex })
                i) :
            InfinitePlace K))
⊢ ∏ w : InfinitePlace K, f w =
    HMul.hMul (α := α) (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K))
      (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K))

Tactic:
rw [← Equiv.prod_comp (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex))]

Premises used: Equiv.subtypeEquivRight, Equiv.prod_comp, NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
α : Type u_2
inst_1 : CommMonoid α
inst_2 : NumberField K
f : InfinitePlace K → α
⊢ ∏ w : InfinitePlace K, f w =
    HMul.hMul (α := α) (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K))
      (∏ i : { x : InfinitePlace K // ¬x.IsReal },
        f
          (↑((Equiv.subtypeEquivRight (p := fun (x : InfinitePlace K) ↦ ¬x.IsReal) (q := fun (x : InfinitePlace K) ↦
                    x.IsComplex) ⋯ :
                  (a : { x : InfinitePlace K // ¬x.IsReal }) → { x : InfinitePlace K // x.IsComplex })
                i) :
            InfinitePlace K))

Tactic:
simp [Fintype.prod_subtype_mul_prod_subtype]

Premises used: Fintype.prod_subtype_mul_prod_subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ j : InfinitePlace K, ∑ i : K →+* ℂ with mk i = j, 1)
⊢ ∑ w : InfinitePlace K, w.mult = finrank ℚ K

Tactic:
rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]

Premises used: Finset.univ, Finset.card_eq_sum_ones, Fintype.card, NumberField.Embeddings.card, NumberField.InfinitePlace.mk, Finset.sum_fiberwise, Complex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
rw : x.mult = HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}) 1
rw₁ : x.mult = Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x} * 1
rw₂ : x.mult = Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}
rw₃ rw₄ : x.mult = x.mult
⊢ x.mult = ∑ i : K →+* ℂ with mk i = x, 1

Tactic:
rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq]

Premises used: NumberField.InfinitePlace.card_filter_mk_eq, 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
⊢ Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ j : InfinitePlace K, ∑ i : K →+* ℂ with mk i = j, 1)

Tactic:
exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : ∑ w : InfinitePlace K, w.mult = card.{u_1} (K →+* ℂ)
rw₁ : ∑ w : InfinitePlace K, w.mult = Finset.card.{u_1} (α := K →+* ℂ) Finset.univ
rw₂ : Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ x : K →+* ℂ, 1)
rw₃ rw₄ rw₅ : Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ j : InfinitePlace K, ∑ i : K →+* ℂ with mk i = j, 1)
⊢ ∑ w : InfinitePlace K, w.mult = finrank ℚ K

Tactic:
classical
  rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

Premises used: Finset.card_eq_sum_ones, Fintype.card, NumberField.Embeddings.card, Complex, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
refine_1 : ∀ (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }), (mk (↑φ : K →+* ℂ)).IsReal
refine_2 :
  ∀ (φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ })
    (h :
      Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
        ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
              { w : InfinitePlace K // w.IsReal }))
          φ)
        ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
              { w : InfinitePlace K // w.IsReal }))
          ψ)),
    φ = ψ
refine_3 :
  ∀ (w : { w : InfinitePlace K // w.IsReal }),
    ∃ (a : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }),
      (fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
              { w : InfinitePlace K // w.IsReal }))
          a =
        w
⊢ { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // w.IsReal }

Tactic:
refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)

Premises used: And.intro, Equiv.ofBijective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
⊢ (mk (↑φ : K →+* ℂ)).IsReal

Tactic:
⟨φ, φ.prop, rfl⟩

Premises used: NumberField.InfinitePlace.IsReal, Subtype.prop, And.intro, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
⊢ (mk (↑φ : K →+* ℂ)).IsReal

Tactic:
exact ⟨φ, φ.prop, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
h :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      φ)
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      ψ)
refine_2 : ∀ (h : mk (↑φ : K →+* ℂ) = mk (↑ψ : K →+* ℂ)), φ = ψ
refine_2₁ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ ComplexEmbedding.conjugate (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
refine_2₂ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
refine_2₃ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
refine_2₄ refine_2₅ refine_2₆ refine_2₇ : ∀ (h : φ = ψ), φ = ψ
⊢ φ = ψ

Tactic:
rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h

Premises used: NumberField.InfinitePlace.mk_eq_iff, Subtype.ext_iff, Subtype.prop, Subtype.mk.injEq, Iff.mp, NumberField.ComplexEmbedding.isReal_iff, or_self
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsReal }
⊢ (fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      (Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ComplexEmbedding.IsReal φ) (↑w : InfinitePlace K).embedding ⋯) =
    w

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsReal }
⊢ ∃ (a : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }),
    (fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
            { w : InfinitePlace K // w.IsReal }))
        a =
      w

Tactic:
exact ⟨⟨embedding w, isReal_iff.mp w.prop⟩, by simp⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
⊢ (↑((mkReal : (a : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) → { w : InfinitePlace K // w.IsReal }) φ) :
      InfinitePlace K) =
    mk (↑φ : K →+* ℂ)

Tactic:
rfl

Premises used: NumberField.InfinitePlace.mk, rfl