awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
rw : (σ • w).IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ IsUnramified k w
rw₁ : (σ • w).IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
rw₂ : w.IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
rw₃ :
  w.IsReal ∨
      IsComplex (w.comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ.symm : K →+* K) (algebraMap k K))) ↔
    w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w
have rw₄ : w.IsReal ∨
    IsComplex
      (w.comap
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(↑σ.symm : K →ₐ[k] K) : K →+* K) (algebraMap k K))) ↔
  w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
Tactic: rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
    ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
rw : (σ • w).IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ IsUnramified k w
rw₁ : (σ • w).IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
rw₂ : w.IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
rw₃ :
  w.IsReal ∨
      IsComplex (w.comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ.symm : K →+* K) (algebraMap k K))) ↔
    w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
rw₄ :
  w.IsReal ∨
      IsComplex
        (w.comap
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(↑σ.symm : K →ₐ[k] K) : K →+* K) (algebraMap k K))) ↔
    w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w
have rw₅ : w.IsReal ∨ IsComplex (w.comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
Tactic: rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
    ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
w : InfinitePlace K
⊢ IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w
have refine : ∀ (H : IsUnramified k w) (v : InfinitePlace K)
  (hv : Eq (α := InfinitePlace k) (v.comap (algebraMap k K)) (w.comap (algebraMap k K))), IsUnramified k v
Tactic: refine ⟨fun H ↦ H _ rfl, fun H v hv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
w : InfinitePlace K
H : IsUnramified k w
v : InfinitePlace K
hv : Eq (α := InfinitePlace k) (v.comap (algebraMap k K)) (w.comap (algebraMap k K))
⊢ IsUnramified k v
have obtain : ∀ (σ : Gal(K/k)) (H : IsUnramified k (σ • v))
  (hv : Eq (α := InfinitePlace k) (v.comap (algebraMap k K)) ((σ • v).comap (algebraMap k K))), IsUnramified k v
Tactic: obtain ⟨σ, rfl⟩ := exists_smul_eq_of_comap_eq hv
Cleared hypotheses: w, H, hv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
v : InfinitePlace K
σ : Gal(K/k)
H : IsUnramified k (σ • v)
hv : Eq (α := InfinitePlace k) (v.comap (algebraMap k K)) ((σ • v).comap (algebraMap k K))
⊢ IsUnramified k v
have rwa : ∀ (H : IsUnramified k v) (hv : Eq (α := InfinitePlace k) (v.comap (algebraMap k K)) ((σ • v).comap (algebraMap k K))),
  IsUnramified k v
Tactic: rwa [isUnramified_smul_iff] at H
Cleared hypotheses: H, hv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
w : InfinitePlace k
hw : ¬IsUnramifiedIn K w
⊢ Even (Nat.card.{u_2} Gal(K/k))
have obtain : ∀ (v : InfinitePlace K)
  (hw :
    ¬IsUnramifiedIn.{u_1, u_2} (k := k) K
        ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) v)),
  Even (Nat.card.{u_2} Gal(K/k))
Tactic: obtain ⟨v, rfl⟩ := comap_surjective (K := K) w
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
v : InfinitePlace K
hw :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) v)
⊢ Even (Nat.card.{u_2} Gal(K/k))
have hw₁ : ¬IsUnramified k v
Tactic: rw [isUnramifiedIn_comap] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
w : InfinitePlace k
hw : ¬IsUnramifiedIn K w
⊢ Even (finrank k K)
have obtain : ∀ (v : InfinitePlace K)
  (hw :
    ¬IsUnramifiedIn.{u_1, u_2} (k := k) K
        ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) v)),
  Even (finrank k K)
Tactic: obtain ⟨v, rfl⟩ := comap_surjective (K := K) w
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
v : InfinitePlace K
hw :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) v)
⊢ Even (finrank k K)
have hw₁ : ¬IsUnramified k v
Tactic: rw [isUnramifiedIn_comap] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
⊢ Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w} =
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w} * finrank k K
have rw : Eq (α := ℕ)
  (∑ b : InfinitePlace k with IsUnramifiedIn K b,
    Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = b}))
  (∑ _x : InfinitePlace k with IsUnramifiedIn K _x, Nat.card.{u_2} Gal(K/k))
Tactic: rw [← IsGalois.card_aut_eq_finrank,
    Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K)))
    (t := {w : InfinitePlace k | w.IsUnramifiedIn K}), ← smul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
rw :
  Eq (α := ℕ)
    (∑ b : InfinitePlace k with IsUnramifiedIn K b,
      Finset.card.{u_2} (α := InfinitePlace K)
        ({a ∈ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = b}))
    (∑ _x : InfinitePlace k with IsUnramifiedIn K _x, Nat.card.{u_2} Gal(K/k))
⊢ Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w} =
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w} * finrank k K
have rw₁ : Set.MapsTo (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K))
  (↑{w : InfinitePlace K | IsUnramified k w} : Set (InfinitePlace K))
  (↑{w : InfinitePlace k | IsUnramifiedIn K w} : Set (InfinitePlace k))
Tactic: rw [← IsGalois.card_aut_eq_finrank,
    Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K)))
    (t := {w : InfinitePlace k | w.IsUnramifiedIn K}), ← smul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
⊢ Eq (α := ℕ)
    (∑ b : InfinitePlace k with IsUnramifiedIn K b,
      Finset.card.{u_2} (α := InfinitePlace K)
        ({a ∈ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = b}))
    (∑ _x : InfinitePlace k with IsUnramifiedIn K _x, Nat.card.{u_2} Gal(K/k))
have refine : ∀ (w : InfinitePlace k)
  (hw : Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w} w),
  Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = w}) =
    Nat.card.{u_2} Gal(K/k)
Tactic: refine sum_congr rfl (fun w hw ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace k
hw : Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w} w
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = w}) =
    Nat.card.{u_2} Gal(K/k)
have obtain : ∀ (w : InfinitePlace K)
  (hw :
    Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w}
      ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)),
  Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    Nat.card.{u_2} Gal(K/k)
Tactic: obtain ⟨w, rfl⟩ := comap_surjective (K := K) w
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw :
  Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w}
    ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    Nat.card.{u_2} Gal(K/k)
have hw₁ : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
Tactic: rw [mem_filter_univ] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    Nat.card.{u_2} Gal(K/k)
have trans : Finset.card.{u_2} (α := InfinitePlace K)
    ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
      Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
        ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
  #(MulAction.orbit Gal(K/k) w).toFinset
Tactic: trans #(MulAction.orbit Gal(K/k) w).toFinset
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
trans :
  Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    #(MulAction.orbit Gal(K/k) w).toFinset
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    Nat.card.{u_2} Gal(K/k)
have trans₁ : #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card.{u_2} Gal(K/k)
Tactic: trans #(MulAction.orbit Gal(K/k) w).toFinset
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    #(MulAction.orbit Gal(K/k) w).toFinset
have e_s : {a ∈ {w : InfinitePlace K | IsUnramified k w} |
    Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
      ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)} =
  (MulAction.orbit Gal(K/k) w).toFinset
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ {a ∈ {w : InfinitePlace K | IsUnramified k w} |
      Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
        ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)} =
    (MulAction.orbit Gal(K/k) w).toFinset
have e_s : ∀ (w' : InfinitePlace K),
  Membership.mem (γ := Finset (InfinitePlace K))
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)})
      w' ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset
Tactic: ext w'
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
w' : InfinitePlace K
⊢ Membership.mem (γ := Finset (InfinitePlace K))
      ({a ∈ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)})
      w' ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset
have e_s : Eq (α := InfinitePlace k) ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
    (w'.comap (algebraMap k K)) →
  IsUnramified k w'
Tactic: rw [mem_filter, mem_filter_univ, Set.mem_toFinset, mem_orbit_iff, @eq_comm _ (comap w' _),
        and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
w' : InfinitePlace K
e :
  Eq (α := InfinitePlace k) ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
    (w'.comap (algebraMap k K))
⊢ IsUnramified k w'
have e_s : IsUnramifiedIn K (w'.comap (algebraMap k K))
Tactic: rwa [← isUnramifiedIn_comap, ← e]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card.{u_2} Gal(K/k)
have hc : IsUnramified k w
Tactic: rw [Nat.card_eq_fintype_card,
        ← 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
⊢ Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w}ᶜ =
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ * (finrank k K / 2)
have rw : Eq (α := ℕ)
  (∑ b ∈ {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ,
    Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∉ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = b}))
  (∑ _x ∈ {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ, Nat.card.{u_2} Gal(K/k) / 2)
Tactic: rw [← IsGalois.card_aut_eq_finrank,
    Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K)))
    (t := ({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ), ← smul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
rw :
  Eq (α := ℕ)
    (∑ b ∈ {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ,
      Finset.card.{u_2} (α := InfinitePlace K)
        ({a ∉ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = b}))
    (∑ _x ∈ {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ, Nat.card.{u_2} Gal(K/k) / 2)
⊢ Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w}ᶜ =
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ * (finrank k K / 2)
have rw₁ : Set.MapsTo (fun (x : InfinitePlace K) ↦ x.comap (algebraMap k K))
  (↑{w : InfinitePlace K | IsUnramified k w}ᶜ : Set (InfinitePlace K))
  (↑{w : InfinitePlace k | IsUnramifiedIn K w}ᶜ : Set (InfinitePlace k))
Tactic: rw [← IsGalois.card_aut_eq_finrank,
    Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K)))
    (t := ({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ), ← smul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
⊢ Eq (α := ℕ)
    (∑ b ∈ {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ,
      Finset.card.{u_2} (α := InfinitePlace K)
        ({a ∉ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = b}))
    (∑ _x ∈ {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ, Nat.card.{u_2} Gal(K/k) / 2)
have refine : ∀ (w : InfinitePlace k)
  (hw : Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ w),
  Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∉ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = w}) =
    Nat.card.{u_2} Gal(K/k) / 2
Tactic: refine sum_congr rfl (fun w hw ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace k
hw : Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ w
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∉ {w : InfinitePlace K | IsUnramified k w} | a.comap (algebraMap k K) = w}) =
    Nat.card.{u_2} Gal(K/k) / 2
have obtain : ∀ (w : InfinitePlace K)
  (hw :
    Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ
      ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)),
  Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∉ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    Nat.card.{u_2} Gal(K/k) / 2
Tactic: obtain ⟨w, rfl⟩ := comap_surjective (K := K) w
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw :
  Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ
    ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∉ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    Nat.card.{u_2} Gal(K/k) / 2
have hw₁ : ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
Tactic: rw [compl_filter, mem_filter_univ] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : NumberField K
inst_4 : NumberField k
inst_5 : IsGalois k K
w : InfinitePlace K
hw :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ Finset.card.{u_2} (α := InfinitePlace K)
      ({a ∉ {w : InfinitePlace K | IsUnramified k w} |
        Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
          ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
    Nat.card.{u_2} Gal(K/k) / 2
have trans : Finset.card.{u_2} (α := InfinitePlace K)
    ({a ∉ {w : InfinitePlace K | IsUnramified k w} |
      Eq (α := InfinitePlace k) (a.comap (algebraMap k K))
        ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)}) =
  #(MulAction.orbit Gal(K/k) w).toFinset
Tactic: trans Finset.card (MulAction.orbit Gal(K/k) w).toFinset