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
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) / 2
have trans₁ : #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card.{u_2} Gal(K/k) / 2
Tactic: trans Finset.card (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, compl_filter, mem_filter_univ, @eq_comm _ (comap w' _), Set.mem_toFinset,
        mem_orbit_iff, 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) / 2
have hnc : ¬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), InfinitePlace.card_stabilizer, if_neg,
        Nat.mul_div_cancel _ zero_lt_two, 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
⊢ card.{u_2} (InfinitePlace K) =
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ * (finrank k K / 2)
have rw : card.{u_2} (InfinitePlace 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)
Tactic: rw [← card_isUnramified, ← card_isUnramified_compl, Finset.card_add_card_compl]
-- 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 :
  card.{u_2} (InfinitePlace 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)
⊢ card.{u_2} (InfinitePlace K) =
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ * (finrank k K / 2)
have rw₁ : card.{u_2} (InfinitePlace K) =
  Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w} +
    Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w}ᶜ
Tactic: rw [← card_isUnramified, ← card_isUnramified_compl, Finset.card_add_card_compl]
-- 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 :
  card.{u_2} (InfinitePlace 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)
rw₁ :
  card.{u_2} (InfinitePlace K) =
    Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w} +
      Finset.card.{u_2} (α := InfinitePlace K) {w : InfinitePlace K | IsUnramified k w}ᶜ
⊢ card.{u_2} (InfinitePlace K) =
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ * (finrank k K / 2)
have rw₂ : card.{u_2} (InfinitePlace K) = card.{u_2} (InfinitePlace K)
Tactic: rw [← card_isUnramified, ← card_isUnramified_compl, Finset.card_add_card_compl]
-- 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
F : Type u_3
inst_2 : Field F
inst_3 : Algebra k K
inst_4 : Algebra k F
inst_5 : Algebra K F
inst_6 : IsScalarTower k K F
h₁ : IsUnramifiedAtInfinitePlaces k F
inst_7 : Algebra.IsAlgebraic K F
w : InfinitePlace K
⊢ InfinitePlace.IsUnramified k w
have obtain : ∀ (w : InfinitePlace F),
  InfinitePlace.IsUnramified.{u_1, u_2} k (K := K)
    ((fun (x : InfinitePlace F) ↦ (x.comap (algebraMap K F) : InfinitePlace K)) w)
Tactic: obtain ⟨w, rfl⟩ := InfinitePlace.comap_surjective (K := F) w
Cleared hypotheses: 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
Tactic: rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₁ : ∀ (x : InfinitePlace k), Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
Tactic: rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
have simp : ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x
Tactic: simp only [Finset.mem_univ, forall_true_left]
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw : Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
    Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
      (finrank k K / 2) =
  card.{u_1} (InfinitePlace k) * finrank k K
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₁ : Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
    Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
  card.{u_1} (InfinitePlace k) * finrank k K
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₁ :
  Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₂ : ∀ (x : InfinitePlace k), Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₁ :
  Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₂ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₃ : card.{u_1} (InfinitePlace k) * finrank k K + Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
  card.{u_1} (InfinitePlace k) * finrank k K
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₁ :
  Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₂ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₃ :
  card.{u_1} (InfinitePlace k) * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₄ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₅ : card.{u_1} (InfinitePlace k) * finrank k K + 0 * (finrank k K / 2) = card.{u_1} (InfinitePlace k) * finrank k K
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₁ :
  Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₂ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₃ :
  card.{u_1} (InfinitePlace k) * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₄ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₅ : card.{u_1} (InfinitePlace k) * finrank k K + 0 * (finrank k K / 2) = card.{u_1} (InfinitePlace k) * finrank k K
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₆ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₁ :
  Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₂ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₃ :
  card.{u_1} (InfinitePlace k) * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₄ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₅ : card.{u_1} (InfinitePlace k) * finrank k K + 0 * (finrank k K / 2) = card.{u_1} (InfinitePlace k) * finrank k K
rw₆ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₇ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₈ : card.{u_1} (InfinitePlace k) * finrank k K + 0 = card.{u_1} (InfinitePlace k) * finrank k K
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- 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
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₁ :
  Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₂ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₃ :
  card.{u_1} (InfinitePlace k) * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₄ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₅ : card.{u_1} (InfinitePlace k) * finrank k K + 0 * (finrank k K / 2) = card.{u_1} (InfinitePlace k) * finrank k K
rw₆ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₇ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₈ : card.{u_1} (InfinitePlace k) * finrank k K + 0 = card.{u_1} (InfinitePlace k) * finrank k K
rw₉ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₁₀ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₁₁ : card.{u_1} (InfinitePlace k) * finrank k K = card.{u_1} (InfinitePlace k) * finrank k K
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K