awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
w : InfinitePlace k
hw : Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w} w
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)
⊢ 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:
obtain ⟨w, rfl⟩ := comap_surjective (K := K) w

Premises used: NumberField.InfinitePlace.comap_surjective, rfl
-- 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
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)
⊢ 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

Premises used: Finset.mem_filter_univ
-- 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
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
trans₁ : #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card.{u_2} Gal(K/k)
⊢ 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:
trans #(MulAction.orbit Gal(K/k) w).toFinset

Premises used: Set.toFinset, MulAction.orbit, AlgEquiv
-- 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
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
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
⊢ 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:
congr
-- 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
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
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
⊢ {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:
ext w'
-- 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
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_s :
  Eq (α := InfinitePlace k) ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
      (w'.comap (algebraMap k K)) →
    IsUnramified k w'
⊢ 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:
rw [mem_filter, mem_filter_univ, Set.mem_toFinset, mem_orbit_iff, @eq_comm _ (comap w' _),
        and_iff_right_iff_imp]

Premises used: Finset.mem_filter_univ, eq_comm, and_iff_right_iff_imp, Finset.mem_filter, NumberField.InfinitePlace.mem_orbit_iff, Set.mem_toFinset
-- 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
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))
e_s : IsUnramifiedIn K (w'.comap (algebraMap k K))
e_s₁ e_s₂ e_s₃ e_s₄ :
  IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ IsUnramified k w'

Tactic:
rwa [← isUnramifiedIn_comap, ← e]

Premises used: NumberField.InfinitePlace.isUnramifiedIn_comap
-- 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
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
hc : IsUnramified k w
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card.{u_2} Gal(K/k)

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]

Premises used: NumberField.InfinitePlace.card_stabilizer, Set.toFinset_card, if_pos, mul_one, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, Nat.card_eq_fintype_card
-- 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
w : InfinitePlace K
hw : IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
hc hc₁ hc₂ hc₃ : IsUnramifiedIn K (w.comap (algebraMap k K))
⊢ IsUnramified k w

Tactic:
rwa [← isUnramifiedIn_comap]

Premises used: NumberField.InfinitePlace.isUnramifiedIn_comap
-- 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
⊢ 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:
simp [Set.MapsTo, isUnramifiedIn_comap]

Premises used: Set.MapsTo, NumberField.InfinitePlace.isUnramifiedIn_comap
-- 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
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)
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))
⊢ 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 [← 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]

Premises used: IsGalois.card_aut_eq_finrank, Finset.card_eq_sum_card_fiberwise, smul_eq_mul, Finset.sum_const
-- 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
⊢ 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:
sum_congr rfl (fun w hw ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- 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
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
⊢ 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:
refine sum_congr rfl (fun w hw ↦ ?_)
-- 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
w : InfinitePlace k
hw : Membership.mem (γ := Finset (InfinitePlace k)) {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ w
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
⊢ 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:
obtain ⟨w, rfl⟩ := comap_surjective (K := K) w

Premises used: NumberField.InfinitePlace.comap_surjective, rfl
-- 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
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)
⊢ ¬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

Premises used: Finset.mem_filter_univ, Finset.compl_filter
-- 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
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
trans₁ : #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card.{u_2} Gal(K/k) / 2
⊢ 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:
trans Finset.card (MulAction.orbit Gal(K/k) w).toFinset

Premises used: Set.toFinset, MulAction.orbit, AlgEquiv, Finset.card
-- 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
w : InfinitePlace K
hw :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
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
⊢ 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:
congr
-- 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
w : InfinitePlace K
hw :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
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
⊢ {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:
ext w'
-- 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
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_s :
  Eq (α := InfinitePlace k) ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
      (w'.comap (algebraMap k K)) →
    ¬IsUnramified k w'
⊢ 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:
rw [mem_filter, compl_filter, mem_filter_univ, @eq_comm _ (comap w' _), Set.mem_toFinset,
        mem_orbit_iff, and_iff_right_iff_imp]

Premises used: Finset.mem_filter_univ, Finset.compl_filter, eq_comm, and_iff_right_iff_imp, Finset.mem_filter, NumberField.InfinitePlace.mem_orbit_iff, Set.mem_toFinset
-- 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
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))
e_s : ¬IsUnramifiedIn K (w'.comap (algebraMap k K))
e_s₁ e_s₂ e_s₃ e_s₄ :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
⊢ ¬IsUnramified k w'

Tactic:
rwa [← isUnramifiedIn_comap, ← e]

Premises used: NumberField.InfinitePlace.isUnramifiedIn_comap
-- 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
w : InfinitePlace K
hw :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
hnc : ¬IsUnramified k w
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card.{u_2} Gal(K/k) / 2

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]

Premises used: NumberField.InfinitePlace.card_stabilizer, Nat.mul_div_cancel, Set.toFinset_card, zero_lt_two, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, if_neg, Nat.card_eq_fintype_card
-- 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
w : InfinitePlace K
hw :
  ¬IsUnramifiedIn.{u_1, u_2} (k := k) K ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap k K) : InfinitePlace k)) w)
hnc hnc₁ hnc₂ hnc₃ : ¬IsUnramifiedIn K (w.comap (algebraMap k K))
⊢ ¬IsUnramified k w

Tactic:
rwa [← isUnramifiedIn_comap]

Premises used: NumberField.InfinitePlace.isUnramifiedIn_comap
-- 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
⊢ 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:
simp [Set.MapsTo, isUnramifiedIn_comap]

Premises used: Set.MapsTo, NumberField.InfinitePlace.isUnramifiedIn_comap
-- 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
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}ᶜ
rw₂ rw₃ : card.{u_2} (InfinitePlace K) = card.{u_2} (InfinitePlace 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)

Tactic:
rw [← card_isUnramified, ← card_isUnramified_compl, Finset.card_add_card_compl]

Premises used: Finset.card_add_card_compl, NumberField.InfinitePlace.card_isUnramified, NumberField.InfinitePlace.card_isUnramified_compl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
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)
⊢ InfinitePlace.IsUnramified k w

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

Premises used: NumberField.InfinitePlace.comap_surjective, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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 F
⊢ InfinitePlace.IsUnramified.{u_1, u_2} k (K := K)
    ((fun (x : InfinitePlace F) ↦ (x.comap (algebraMap K F) : InfinitePlace K)) w)

Tactic:
(h₁.1 w).comap K

Premises used: IsUnramifiedAtInfinitePlaces.isUnramified, NumberField.InfinitePlace.IsUnramified.comap
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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 F
⊢ InfinitePlace.IsUnramified.{u_1, u_2} k (K := K)
    ((fun (x : InfinitePlace F) ↦ (x.comap (algebraMap K F) : InfinitePlace K)) w)

Tactic:
exact (h₁.1 w).comap K

Premises used: IsUnramifiedAtInfinitePlaces.isUnramified, NumberField.InfinitePlace.IsUnramified.comap
-- 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 : IsUnramifiedAtInfinitePlaces k K
w : InfinitePlace K
⊢ IsUnramified k w

Tactic:
IsUnramifiedAtInfinitePlaces.isUnramified w

Premises used: IsUnramifiedAtInfinitePlaces.isUnramified
-- 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 : IsUnramifiedAtInfinitePlaces k K
w : InfinitePlace k
⊢ IsUnramifiedIn K w

Tactic:
fun v _ ↦ v.isUnramified k

Premises used: NumberField.InfinitePlace.isUnramified, NumberField.InfinitePlace.IsUnramifiedIn