-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma card_isUnramified_compl [NumberField k] [IsGalois k K] :
    #({w : InfinitePlace K | w.IsUnramified k} : Finset _)ᶜ =
      #({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ * (finrank k K / 2)

Proof state:
case intro
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K (w.comap (algebraMap k K))
⊢ #(filter (fun a => a.comap (algebraMap k K) = (fun x => x.comap (algebraMap k K)) w)
        (filter (fun w => IsUnramified k w) univ)ᶜ) =
    Fintype.card (K ≃ₐ[k] K) / 2

Tactic:
trans Finset.card (MulAction.orbit (K ≃ₐ[k] K) w).toFinset

Result:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K (w.comap (algebraMap k K))
⊢ #(filter (fun a => a.comap (algebraMap k K) = (fun x => x.comap (algebraMap k K)) w)
        (filter (fun w => IsUnramified k w) univ)ᶜ) =
    #(MulAction.orbit (K ≃ₐ[k] K) w).toFinset

k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K (w.comap (algebraMap k K))
⊢ #(MulAction.orbit (K ≃ₐ[k] K) w).toFinset = Fintype.card (K ≃ₐ[k] K) / 2

Proof state:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
⊢ ∀ x ∈ (filter (fun w => IsUnramified k w) univ)ᶜ,
    x.comap (algebraMap k K) ∈ (filter (fun w => IsUnramifiedIn K w) univ)ᶜ

Tactic:
simp [isUnramifiedIn_comap]

Result:
no goals

Proof state:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
⊢ ∑ b ∈ (filter (fun w => IsUnramifiedIn K w) univ)ᶜ,
      #(filter (fun a => a.comap (algebraMap k K) = b) (filter (fun w => IsUnramified k w) univ)ᶜ) =
    ∑ _x ∈ (filter (fun w => IsUnramifiedIn K w) univ)ᶜ, Fintype.card (K ≃ₐ[k] K) / 2

Tactic:
refine sum_congr rfl (fun w hw ↦ ?_)

Result:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
w : InfinitePlace k
hw : w ∈ (filter (fun w => IsUnramifiedIn K w) univ)ᶜ
⊢ #(filter (fun a => a.comap (algebraMap k K) = w) (filter (fun w => IsUnramified k w) univ)ᶜ) =
    Fintype.card (K ≃ₐ[k] K) / 2

Proof state:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
w : InfinitePlace k
hw : w ∈ (filter (fun w => IsUnramifiedIn K w) univ)ᶜ
⊢ #(filter (fun a => a.comap (algebraMap k K) = w) (filter (fun w => IsUnramified k w) univ)ᶜ) =
    Fintype.card (K ≃ₐ[k] K) / 2

Tactic:
obtain ⟨w, rfl⟩ := comap_surjective (K := K) w

Result:
case intro
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
this : Module.Finite k K := Finite.of_restrictScalars_finite ℚ k K
w : InfinitePlace K
hw : (fun x => x.comap (algebraMap k K)) w ∈ (filter (fun w => IsUnramifiedIn K w) univ)ᶜ
⊢ #(filter (fun a => a.comap (algebraMap k K) = (fun x => x.comap (algebraMap k K)) w)
        (filter (fun w => IsUnramified k w) univ)ᶜ) =
    Fintype.card (K ≃ₐ[k] K) / 2