-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma card_isUnramified [NumberField k] [IsGalois k K] :
    #{w : InfinitePlace K | w.IsUnramified k} =
      #{w : InfinitePlace k | w.IsUnramifiedIn K} * finrank k K

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 : (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)

Tactic:
simp only [mem_univ, forall_true_left, mem_filter, true_and] at hw

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 : 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)

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)

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)

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)

Tactic:
trans #(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)

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
⊢ #(filter (fun w => IsUnramified k w) univ) = #(filter (fun w => IsUnramifiedIn K w) univ) * finrank k K

Tactic:
letI := Module.Finite.of_restrictScalars_finite ℚ k K

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
⊢ #(filter (fun w => IsUnramified k w) univ) = #(filter (fun w => IsUnramifiedIn K w) univ) * finrank k K

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:
case e_s.h
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))
w' : InfinitePlace K
⊢ w' ∈
      filter (fun a => a.comap (algebraMap k K) = (fun x => x.comap (algebraMap k K)) w)
        (filter (fun w => IsUnramified k w) univ) ↔
    w' ∈ (MulAction.orbit (K ≃ₐ[k] K) w).toFinset

Tactic:
simp only [mem_univ, forall_true_left, filter_congr_decidable, mem_filter, true_and,
  Set.mem_toFinset, mem_orbit_iff, @eq_comm _ (comap w' _), and_iff_right_iff_imp]

Result:
case e_s.h
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))
w' : InfinitePlace K
⊢ w.comap (algebraMap k K) = w'.comap (algebraMap k K) → IsUnramified k w'

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 : IsUnramifiedIn K (w.comap (algebraMap k K))
⊢ #(MulAction.orbit (K ≃ₐ[k] K) w).toFinset = Fintype.card (K ≃ₐ[k] K)

Tactic:
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w,
  ← Nat.card_eq_fintype_card (α := Stab w), card_stabilizer, if_pos,
  mul_one, Set.toFinset_card]

Result:
case hc
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))
⊢ IsUnramified k w

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 : 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

Tactic:
congr

Result:
case e_s
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

Proof state:
case hc
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))
⊢ IsUnramified k w

Tactic:
rwa [← isUnramifiedIn_comap]

Result:
no goals