-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
rw₁₁ : card.{u_1} (InfinitePlace k) * finrank k K = 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 = 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₁₇ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₁₈ rw₁₉ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₂₀ : ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x
⊢ card.{u_2} (InfinitePlace 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

Premises used: Iff.mpr, Finset.mem_univ, Finset.card_univ, forall_true_left, NumberField.InfinitePlace.isUnramifiedIn, MulZeroClass.zero_mul, NumberField.InfinitePlace.card_eq_card_isUnramifiedIn, Finset.compl_univ, Finset.filter_true_of_mem, Finset.card_eq_zero, add_zero