-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem card_complex_embeddings :
    card { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mkComplex x = ⟨w, hw⟩ }
φ : { φ // ¬ComplexEmbedding.IsReal φ }
hφ : mkComplex φ = ⟨w, hw⟩
⊢ mk ↑φ = w

Tactic:
rwa [Subtype.ext_iff] at hφ

Result:
no goals

Proof state:
case h.e'_2.refine_1
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ { x // mkComplex x = ⟨w, hw⟩ } → { x // mk x = w }

Tactic:
exact fun ⟨φ, hφ⟩ => ⟨φ.val, by rwa [Subtype.ext_iff] at hφ⟩

Result:
no goals

Proof state:
case h.e'_3
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ 2 = w.mult

Tactic:
simp_rw [mult, not_isReal_iff_isComplex.mpr hw, ite_false]

Result:
no goals

Proof state:
case h.e'_2.refine_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h :
  (match x✝¹ with
    | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩) =
    match x✝ with
    | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩
⊢ x✝¹ = x✝

Tactic:
rwa [Subtype.mk_eq_mk, ← Subtype.ext_iff, ← Subtype.ext_iff] at h

Result:
no goals

Proof state:
case h.e'_2.refine_3
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ a,
    (match a with
      | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩) =
      ⟨φ, hφ⟩

Tactic:
refine ⟨⟨⟨φ, not_isReal_of_mk_isComplex (hφ.symm ▸ hw)⟩, ?_⟩, rfl⟩

Result:
case h.e'_2.refine_3
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ mkComplex ⟨φ, ⋯⟩ = ⟨w, hw⟩

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #(Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
⊢ card { φ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

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

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #(Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
⊢ ∑ j : { w // w.IsComplex }, ∑ i ∈ Finset.filter (fun i => mkComplex i = j) Finset.univ, 1 = 2 * nrComplexPlaces K

Proof state:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ card { x // mkComplex x = ⟨w, hw⟩ } = card { x // mk x = w }

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

Result:
case h.e'_2.refine_1
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ { x // mkComplex x = ⟨w, hw⟩ } → { x // mk x = w }

case h.e'_2.refine_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : ?h.e'_2.refine_1 x✝¹ = ?h.e'_2.refine_1 x✝
⊢ x✝¹ = x✝

case h.e'_2.refine_3
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ a, ?h.e'_2.refine_1 a = ⟨φ, hφ⟩

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∀ (w : { w // w.IsComplex }), #(Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2

Tactic:
rintro ⟨w, hw⟩

Result:
case mk
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #(Finset.filter (fun φ => mkComplex φ = ⟨w, hw⟩) Finset.univ) = 2

Proof state:
case mk
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #(Finset.filter (fun φ => mkComplex φ = ⟨w, hw⟩) Finset.univ) = 2

Tactic:
convert card_filter_mk_eq w

Result:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #(Finset.filter (fun φ => mkComplex φ = ⟨w, hw⟩) Finset.univ) = #(Finset.filter (fun φ => mk φ = w) Finset.univ)

case h.e'_3
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ 2 = w.mult

Proof state:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #(Finset.filter (fun φ => mkComplex φ = ⟨w, hw⟩) Finset.univ) = #(Finset.filter (fun φ => mk φ = w) Finset.univ)

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

Result:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ card { x // mkComplex x = ⟨w, hw⟩ } = card { x // mk x = w }

Proof state:
case h.e'_2.refine_3
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ mkComplex ⟨φ, ⋯⟩ = ⟨w, hw⟩

Tactic:
rwa [Subtype.ext_iff, mkComplex_coe]

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #(Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
⊢ ∑ j : { w // w.IsComplex }, ∑ i ∈ Finset.filter (fun i => mkComplex i = j) Finset.univ, 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]

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ¬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]

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∀ (w : { w // w.IsComplex }), #(Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2