-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma nat_card_stabilizer_eq_one_or_two :
    Nat.card (Stab w) = 1 ∨ Nat.card (Stab w) = 2

Proof state:
case neg.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : ¬1 = σ
⊢ #{1, σ} = 2

Tactic:
simp [*]

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
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑{1} = 1

Tactic:
simp

Result:
no goals

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
h : ¬∃ σ, ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
push_neg at h

Result:
case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ Nat.card ↥(Stab w) = 1 ∨ Nat.card ↥(Stab w) = 2

Tactic:
rw [← SetLike.coe_sort_coe, ← mk_embedding w]

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = Nat.card ↑{1}

Tactic:
congr with x

Result:
case e_α.e_s.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
x : K ≃ₐ[k] K
⊢ x ∈ ↑(Stab (mk w.embedding)) ↔ x ∈ {1}

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
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : ¬1 = σ
⊢ #{1, σ} = 1 ∨ #{1, σ} = 2

Tactic:
right

Result:
case neg.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : ¬1 = σ
⊢ #{1, σ} = 2

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
by_cases h : ∃ σ, ComplexEmbedding.IsConj (k := k) (embedding w) σ

Result:
case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∃ σ, ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ¬∃ σ, ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Proof state:
case neg.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1

Tactic:
trans Nat.card ({1} : Set (K ≃ₐ[k] K))

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = Nat.card ↑{1}

k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑{1} = 1

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
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : 1 = σ
⊢ #{1, σ} = 1 ∨ #{1, σ} = 2

Tactic:
left

Result:
case pos.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : 1 = σ
⊢ #{1, σ} = 1

Proof state:
case pos.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : 1 = σ
⊢ #{1, σ} = 1

Tactic:
simp [*]

Result:
no goals

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
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
left

Result:
case neg.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1

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
h : ∃ σ, ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
obtain ⟨σ, hσ⟩ := h

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
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

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
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
⊢ #{1, σ} = 1 ∨ #{1, σ} = 2

Tactic:
by_cases 1 = σ

Result:
case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : 1 = σ
⊢ #{1, σ} = 1 ∨ #{1, σ} = 2

case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
h✝ : ¬1 = σ
⊢ #{1, σ} = 1 ∨ #{1, σ} = 2

Proof state:
case e_α.e_s.h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : K ≃ₐ[k] K), ¬ComplexEmbedding.IsConj w.embedding σ
x : K ≃ₐ[k] K
⊢ x ∈ ↑(Stab (mk w.embedding)) ↔ x ∈ {1}

Tactic:
simp only [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_singleton_iff, or_iff_left_iff_imp,
  h x, IsEmpty.forall_iff]

Result:
no goals

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
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
simp only [hσ.coe_stabilzer_mk, Nat.card_eq_fintype_card, card_ofFinset, Set.toFinset_singleton]

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
σ : K ≃ₐ[k] K
hσ : ComplexEmbedding.IsConj w.embedding σ
⊢ #{1, σ} = 1 ∨ #{1, σ} = 2