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
w : InfinitePlace K
inst_3 : IsGalois k K
⊢ (∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔
    Eq (α := Subgroup Gal(K/k)) (Stab (mk w.embedding)) ⊥

Tactic:
simp only [eq_bot_iff, SetLike.le_def, mem_stabilizer_mk_iff,
    Subgroup.mem_bot, forall_eq_or_imp, true_and]

Premises used: SetLike.le_def, forall_eq_or_imp, NumberField.InfinitePlace.mem_stabilizer_mk_iff, eq_bot_iff, Subgroup.mem_bot, true_and
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
rw : Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥ ↔ Nat.card.{u_2} ↥(Stab w) = 1
rw₁ rw₂ : Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥ ↔ Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥
⊢ IsUnramified k w ↔ Nat.card.{u_2} ↥(Stab w) = 1

Tactic:
rw [isUnramified_iff_stabilizer_eq_bot, Subgroup.card_eq_one]

Premises used: Subgroup.card_eq_one, NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
rw : ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
⊢ ¬IsUnramified k w ↔ Nat.card.{u_2} ↥(Stab w) = 2

Tactic:
rw [isUnramified_iff_card_stabilizer_eq_one]

Premises used: NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
inl : ∀ (e : Nat.card.{u_2} ↥(Stab w) = 1), ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
inr : ∀ (e : Nat.card.{u_2} ↥(Stab w) = 2), ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
⊢ ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2

Tactic:
obtain (e | e) := nat_card_stabilizer_eq_one_or_two k w

Premises used: NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
e : Nat.card.{u_2} ↥(Stab w) = 1
inl : ¬Eq (α := ℕ) 1 1 ↔ Eq (α := ℕ) 1 2
⊢ ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2

Tactic:
rw [e]
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
e : Nat.card.{u_2} ↥(Stab w) = 2
inr : ¬Eq (α := ℕ) 2 1 ↔ Eq (α := ℕ) 2 2
⊢ ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2

Tactic:
rw [e]
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
e : Nat.card.{u_2} ↥(Stab w) = 1
⊢ ¬Eq (α := ℕ) 1 1 ↔ Eq (α := ℕ) 1 2

Tactic:
decide
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
e : Nat.card.{u_2} ↥(Stab w) = 2
⊢ ¬Eq (α := ℕ) 2 1 ↔ Eq (α := ℕ) 2 2

Tactic:
decide
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
⊢ IsRamified k w ↔ Nat.card.{u_2} ↥(Stab w) = 2

Tactic:
not_isUnramified_iff_card_stabilizer_eq_two

Premises used: NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two
-- 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 : IsGalois k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
⊢ ∃ (x : ↥(Stab (mk φ))) (y : ↥(Stab (mk φ))), x ≠ y ∧ Eq (α := Set ↥(Stab (mk φ))) {x, y} Set.univ

Tactic:
rw [isRamified_iff_card_stabilizer_eq_two, Nat.card_eq_two_iff] at h

Premises used: NumberField.InfinitePlace.isRamified_iff_card_stabilizer_eq_two, Nat.card_eq_two_iff
-- 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 : IsGalois k K
φ : K →+* ℂ
h : ∃ (x : ↥(Stab (mk φ))) (y : ↥(Stab (mk φ))), x ≠ y ∧ Eq (α := Set ↥(Stab (mk φ))) {x, y} Set.univ
obtain :
  ∀ (x : Gal(K/k)) (hx : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) (y : Gal(K/k))
    (hy : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) y)
    (h₁ :
      Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) x hx ≠
        Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) y hy),
    ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ
⊢ ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ

Tactic:
obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, h₁, -⟩ := h
-- 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 : IsGalois k K
φ : K →+* ℂ
x : Gal(K/k)
hx : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x
y : Gal(K/k)
hy : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) y
h₁ :
  Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) x hx ≠
    Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) y hy
rw :
  ∀ (hx_1 : x = 1 ∨ ComplexEmbedding.IsConj φ x) (y : Gal(K/k))
    (hy : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) y) (hy_1 : y = 1 ∨ ComplexEmbedding.IsConj φ y)
    (h₁ :
      Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) x hx ≠
        Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) y hy),
    ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ
⊢ ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ

Tactic:
rw [mem_stabilizer_mk_iff] at hx hy

Premises used: NumberField.InfinitePlace.mem_stabilizer_mk_iff
-- 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 : IsGalois k K
φ : K →+* ℂ
x : Gal(K/k)
hx_1 : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x
hx : x = 1 ∨ ComplexEmbedding.IsConj φ x
y : Gal(K/k)
hy_1 : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) y
hy : y = 1 ∨ ComplexEmbedding.IsConj φ y
h₁ :
  Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) x hx_1 ≠
    Subtype.mk (p := fun (x : Gal(K/k)) ↦ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x) y hy_1
⊢ ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ

Tactic:
grind
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
isTrue : IsUnramified k w → Nat.card.{u_2} ↥(Stab w) = 1
isFalse : ¬IsUnramified k w → Nat.card.{u_2} ↥(Stab w) = 2
⊢ Nat.card.{u_2} ↥(Stab w) = if IsUnramified k w then 1 else 2

Tactic:
split
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
h isTrue isTrue₁ isTrue₂ isTrue₃ : IsUnramified k w
⊢ Nat.card.{u_2} ↥(Stab w) = 1

Tactic:
rwa [← isUnramified_iff_card_stabilizer_eq_one]

Premises used: NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
h isFalse isFalse₁ isFalse₂ isFalse₃ : ¬IsUnramified k w
⊢ Nat.card.{u_2} ↥(Stab w) = 2

Tactic:
rwa [← not_isUnramified_iff_card_stabilizer_eq_two]

Premises used: NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
pos : ∀ (H : Finite.{u_2 + 1} Gal(K/k)), Even (Nat.card.{u_2} Gal(K/k))
neg : ∀ (H : ¬Finite.{u_2 + 1} Gal(K/k)), Even (Nat.card.{u_2} Gal(K/k))
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
by_cases H : Finite Gal(K/k)

Premises used: Finite, 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : Finite.{u_2 + 1} Gal(K/k)
pos : ∀ (val : Fintype Gal(K/k)), Even (Nat.card.{u_2} Gal(K/k))
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
cases nonempty_fintype Gal(K/k)

Premises used: nonempty_fintype, 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : Finite.{u_2 + 1} Gal(K/k)
val : Fintype Gal(K/k)
pos : Nat.card.{u_2} ↥(Stab w) ∣ Nat.card.{u_2} Gal(K/k)
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
rw [even_iff_two_dvd, ← not_isUnramified_iff_card_stabilizer_eq_two.mp hw]

Premises used: NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two, Iff.mp, even_iff_two_dvd
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : Finite.{u_2 + 1} Gal(K/k)
val : Fintype Gal(K/k)
⊢ Nat.card.{u_2} ↥(Stab w) ∣ Nat.card.{u_2} Gal(K/k)

Tactic:
Subgroup.card_subgroup_dvd_card (Stab w)

Premises used: Subgroup.card_subgroup_dvd_card, AlgEquiv, MulAction.stabilizer
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : Finite.{u_2 + 1} Gal(K/k)
val : Fintype Gal(K/k)
⊢ Nat.card.{u_2} ↥(Stab w) ∣ Nat.card.{u_2} Gal(K/k)

Tactic:
exact Subgroup.card_subgroup_dvd_card (Stab 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite.{u_2 + 1} Gal(K/k)
⊢ Even (α := ℕ) 0

Tactic:
Even.zero

Premises used: Even.zero
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite.{u_2 + 1} Gal(K/k)
h : Nat.card.{u_2} Gal(K/k) = 0
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
convert! Even.zero

Premises used: Even.zero
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite.{u_2 + 1} Gal(K/k)
h : ∀ (e : ¬Nat.card.{u_2} Gal(K/k) = 0), False
⊢ Nat.card.{u_2} Gal(K/k) = 0

Tactic:
by_contra e
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite.{u_2 + 1} Gal(K/k)
e : ¬Nat.card.{u_2} Gal(K/k) = 0
⊢ False

Tactic:
H (Nat.finite_of_card_ne_zero e)

Premises used: Nat.finite_of_card_ne_zero
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite.{u_2 + 1} Gal(K/k)
e : ¬Nat.card.{u_2} Gal(K/k) = 0
⊢ False

Tactic:
exact H (Nat.finite_of_card_ne_zero e)

Premises used: Nat.finite_of_card_ne_zero
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
even_nat_card_aut_of_not_isUnramified hw

Premises used: NumberField.InfinitePlace.even_nat_card_aut_of_not_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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
pos : FiniteDimensional k K → Even (finrank k K)
neg : ¬FiniteDimensional k K → Even (finrank k K)
⊢ Even (finrank k K)

Tactic:
by_cases FiniteDimensional k K

Premises used: FiniteDimensional
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
h : FiniteDimensional k K
⊢ Even (finrank k K)

Tactic:
IsGalois.card_aut_eq_finrank k K ▸ even_card_aut_of_not_isUnramified hw

Premises used: IsGalois.card_aut_eq_finrank, NumberField.InfinitePlace.even_card_aut_of_not_isUnramified, Eq.rec
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
h : FiniteDimensional k K
⊢ Even (finrank k K)

Tactic:
exact IsGalois.card_aut_eq_finrank k K ▸ even_card_aut_of_not_isUnramified 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
h : ¬FiniteDimensional k K
⊢ Even (finrank k K)

Tactic:
finrank_of_not_finite ‹_› ▸ Even.zero

Premises used: Even.zero, Eq.rec, Module.finrank_of_not_finite, Eq.symm
-- 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
w : InfinitePlace K
inst_3 : IsGalois k K
hw : ¬IsUnramified k w
h : ¬FiniteDimensional k K
⊢ Even (finrank k K)

Tactic:
exact finrank_of_not_finite ‹_› ▸ Even.zero
-- 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
σ : 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))
rw₅ rw₆ : w.IsReal ∨ IsComplex (w.comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w

Tactic:
rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
    ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap, NumberField.InfinitePlace.isUnramified_iff, NumberField.InfinitePlace.isReal_smul_iff, NumberField.InfinitePlace.comap_smul
-- 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 : IsGalois k K
w : InfinitePlace K
⊢ IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w

Tactic:
⟨fun H ↦ H _ rfl, fun H v hv ↦ ?_⟩

Premises used: Iff.intro, 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 : IsGalois k K
w : InfinitePlace K
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
⊢ IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w

Tactic:
refine ⟨fun H ↦ H _ rfl, fun H v hv ↦ ?_⟩
-- 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 : 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))
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
⊢ IsUnramified k v

Tactic:
obtain ⟨σ, rfl⟩ := exists_smul_eq_of_comap_eq hv

Premises used: NumberField.InfinitePlace.exists_smul_eq_of_comap_eq, 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 : 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))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (H : IsUnramified k v) (hv : Eq (α := InfinitePlace k) (v.comap (algebraMap k K)) ((σ • v).comap (algebraMap k K))),
    IsUnramified k v
⊢ IsUnramified k v

Tactic:
rwa [isUnramified_smul_iff] at H

Premises used: NumberField.InfinitePlace.isUnramified_smul_iff
-- 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 : IsGalois k K
w : InfinitePlace k
hw : ¬IsUnramifiedIn K w
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))
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
obtain ⟨v, 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 : 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)
⊢ ¬IsUnramified k v

Tactic:
rw [isUnramifiedIn_comap] at hw

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 : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
even_card_aut_of_not_isUnramified hw

Premises used: NumberField.InfinitePlace.even_card_aut_of_not_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 : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (Nat.card.{u_2} Gal(K/k))

Tactic:
exact even_card_aut_of_not_isUnramified hw

Premises used: NumberField.InfinitePlace.even_card_aut_of_not_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 : IsGalois k K
w : InfinitePlace k
hw : ¬IsUnramifiedIn K w
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)
⊢ Even (finrank k K)

Tactic:
obtain ⟨v, 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 : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (finrank k K)

Tactic:
even_finrank_of_not_isUnramified hw

Premises used: NumberField.InfinitePlace.even_finrank_of_not_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 : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (finrank k K)

Tactic:
exact even_finrank_of_not_isUnramified hw

Premises used: NumberField.InfinitePlace.even_finrank_of_not_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 : 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))
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

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]

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 : 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:
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)
⊢ 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:
refine sum_congr rfl (fun w hw ↦ ?_)