-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma even_nat_card_aut_of_not_isUnramified [IsGalois k K] (hw : ¬ IsUnramified k w) :
    Even (Nat.card <| K ≃ₐ[k] K)

Proof state:
case pos.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : Finite (K ≃ₐ[k] K)
val✝ : Fintype (K ≃ₐ[k] K)
⊢ Even (Nat.card (K ≃ₐ[k] K))

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

Result:
case pos.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : Finite (K ≃ₐ[k] K)
val✝ : Fintype (K ≃ₐ[k] K)
⊢ Nat.card ↥(Stab w) ∣ Nat.card (K ≃ₐ[k] K)

Proof state:
case pos.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : Finite (K ≃ₐ[k] K)
val✝ : Fintype (K ≃ₐ[k] K)
⊢ Nat.card ↥(Stab w) ∣ Nat.card (K ≃ₐ[k] K)

Tactic:
exact Subgroup.card_subgroup_dvd_card (Stab w)

Result:
no goals

Proof state:
case h.e'_3
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite (K ≃ₐ[k] K)
⊢ Nat.card (K ≃ₐ[k] K) = 0

Tactic:
by_contra e

Result:
case h.e'_3
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite (K ≃ₐ[k] K)
e : ¬Nat.card (K ≃ₐ[k] K) = 0
⊢ False

Proof state:
case pos
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : Finite (K ≃ₐ[k] K)
⊢ Even (Nat.card (K ≃ₐ[k] K))

Tactic:
cases nonempty_fintype (K ≃ₐ[k] K)

Result:
case pos.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : Finite (K ≃ₐ[k] K)
val✝ : Fintype (K ≃ₐ[k] K)
⊢ Even (Nat.card (K ≃ₐ[k] K))

Proof state:
case neg
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite (K ≃ₐ[k] K)
⊢ Even (Nat.card (K ≃ₐ[k] K))

Tactic:
convert Even.zero

Result:
case h.e'_3
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite (K ≃ₐ[k] K)
⊢ Nat.card (K ≃ₐ[k] K) = 0

Proof state:
case h.e'_3
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite (K ≃ₐ[k] K)
e : ¬Nat.card (K ≃ₐ[k] K) = 0
⊢ False

Tactic:
exact H (Nat.finite_of_card_ne_zero e)

Result:
no goals

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
⊢ Even (Nat.card (K ≃ₐ[k] K))

Tactic:
by_cases H : Finite (K ≃ₐ[k] K)

Result:
case pos
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : Finite (K ≃ₐ[k] K)
⊢ Even (Nat.card (K ≃ₐ[k] K))

case neg
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : ¬Finite (K ≃ₐ[k] K)
⊢ Even (Nat.card (K ≃ₐ[k] K))