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
φ : K →+* ℂ
h : IsUnmixed k φ
pos :
  ∀ (hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))),
    ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))
neg :
  ∀ (hv : ¬ComplexEmbedding.IsReal (φ.comp (algebraMap k K))),
    ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))

Tactic:
by_cases hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))

Premises used: Algebra.algebraMap, NumberField.ComplexEmbedding.IsReal, RingHom.comp
-- 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
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
simp [embedding_mk_eq_of_isReal, h hv]

Premises used: NumberField.InfinitePlace.embedding_mk_eq_of_isReal
-- 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
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))

Tactic:
exact .inl <| by simp [embedding_mk_eq_of_isReal, h 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
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ¬ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ IsComplex ((mk φ).comap (algebraMap k K))

Tactic:
simpa using (isReal_mk_iff.not.2 hv)

Premises used: Iff.mpr, Iff.not, NumberField.InfinitePlace.isReal_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
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ¬ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))

Tactic:
exact .inr <| by simpa using (isReal_mk_iff.not.2 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
w : InfinitePlace K
h : w.IsReal
⊢ IsUnramified k w

Tactic:
isUnramified_iff.mpr (Or.inl h)

Premises used: Iff.mpr, NumberField.InfinitePlace.isUnramified_iff, Or.inl
-- 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)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
rw : IsUnramified k (mk φ) ↔ ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1
rw₁ : IsUnramified k (mk φ) ↔ ComplexEmbedding.IsReal φ
rw₂ : ¬IsUnramified k (mk φ) ↔ ¬ComplexEmbedding.IsReal φ
rw₃ : (mk φ).IsComplex ∧ IsReal ((mk φ).comap (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ
rw₄ : ¬(mk φ).IsReal ∧ IsReal ((mk φ).comap (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ
rw₅ : ¬(mk φ).IsReal ∧ IsReal (mk (φ.comp (algebraMap k K))) ↔ ¬ComplexEmbedding.IsReal φ
rw₆ : ¬ComplexEmbedding.IsReal φ ∧ IsReal (mk (φ.comp (algebraMap k K))) ↔ ¬ComplexEmbedding.IsReal φ
rw₇ : ¬ComplexEmbedding.IsReal φ ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ
rw₈ : ¬ComplexEmbedding.IsReal φ ∧ True ↔ ¬ComplexEmbedding.IsReal φ
rw₉ rw₁₀ : ¬ComplexEmbedding.IsReal φ ↔ ¬ComplexEmbedding.IsReal φ
⊢ IsUnramified k (mk φ) ↔ σ = 1

Tactic:
rw [h.ext_iff, ComplexEmbedding.isConj_one_iff, ← not_iff_not, not_isUnramified_iff,
    ← not_isReal_iff_isComplex, comap_mk, isReal_mk_iff, isReal_mk_iff, eq_true h.isReal_comp,
    and_true]

Premises used: not_iff_not, NumberField.InfinitePlace.comap_mk, and_true, NumberField.ComplexEmbedding.IsConj.isReal_comp, NumberField.InfinitePlace.isReal_mk_iff, NumberField.InfinitePlace.not_isUnramified_iff, NumberField.ComplexEmbedding.IsConj.ext_iff, eq_true, NumberField.InfinitePlace.not_isReal_iff_isComplex, NumberField.ComplexEmbedding.isConj_one_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 →+* ℂ
⊢ IsUnramified k (mk φ) ↔ ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1

Tactic:
⟨fun H σ hσ ↦ hσ.isUnramified_mk_iff.mp H,
    fun H ↦ ?_⟩

Premises used: Iff.intro, Iff.mp, NumberField.ComplexEmbedding.IsConj.isUnramified_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 →+* ℂ
refine : ∀ (H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1), IsUnramified k (mk φ)
⊢ IsUnramified k (mk φ) ↔ ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1

Tactic:
refine ⟨fun H σ hσ ↦ hσ.isUnramified_mk_iff.mp H,
    fun 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 →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
by_contra : ∀ (hφ : ¬IsUnramified k (mk φ)), False
⊢ IsUnramified k (mk φ)

Tactic:
by_contra 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 →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬IsUnramified k (mk φ)
⊢ (mk φ).IsComplex ∧ IsReal ((mk φ).comap (algebraMap k K))

Tactic:
rw [not_isUnramified_iff] at hφ

Premises used: NumberField.InfinitePlace.not_isUnramified_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 : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : (mk φ).IsComplex ∧ IsReal ((mk φ).comap (algebraMap k K))
⊢ ¬ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))

Tactic:
rw [comap_mk, isReal_mk_iff, ← not_isReal_iff_isComplex, isReal_mk_iff,
    ← ComplexEmbedding.isConj_one_iff (k := k)] at hφ

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.isReal_mk_iff, NumberField.InfinitePlace.not_isReal_iff_isComplex, NumberField.ComplexEmbedding.isConj_one_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 : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this : Algebra K ℂ := φ.toAlgebra
⊢ IsScalarTower k K ℂ

Tactic:
have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_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
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
r : k
⊢ (↑(↑(star φ) : K →* ℂ) : OneHom K ℂ).toFun ((algebraMap k K : (a : k) → K) r) = (algebraMap k ℂ : (a : k) → ℂ) r

Tactic:
simpa using RingHom.congr_fun hφ.2 r

Premises used: RingHom.congr_fun, And.right
-- 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 : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
φ' : K →ₐ[k] ℂ :=
  let __src := star φ;
  { toRingHom := __src, commutes' := ⋯ }
⊢ ComplexEmbedding.IsConj φ (φ'.restrictNormal' K)

Tactic:
have : ComplexEmbedding.IsConj φ (AlgHom.restrictNormal' φ' K) :=
    (RingHom.ext <| AlgHom.restrictNormal_commutes φ' K).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
inst_3 : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this_3 : IsScalarTower k K ℂ
φ' : K →ₐ[k] ℂ :=
  let __src := star φ;
  { toRingHom := __src, commutes' := ⋯ }
this : ComplexEmbedding.IsConj φ (φ'.restrictNormal' K)
⊢ False

Tactic:
hφ.1 (H _ this ▸ this)

Premises used: Eq.rec, And.left
-- 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 : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this_2 : Algebra K ℂ := φ.toAlgebra
this_3 : IsScalarTower k K ℂ
φ' : K →ₐ[k] ℂ :=
  let __src := star φ;
  { toRingHom := __src, commutes' := ⋯ }
this : ComplexEmbedding.IsConj φ (φ'.restrictNormal' K)
⊢ False

Tactic:
exact hφ.1 (H _ this ▸ this)

Premises used: Eq.rec, And.left
-- 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
φ : K →+* ℂ
σ : Gal(K/k)
simp : φ.comp (↑σ.symm : K →+* K) = φ ∨ conjugate (φ.comp (↑σ.symm : K →+* K)) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ
⊢ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) σ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Tactic:
simp only [MulAction.mem_stabilizer_iff, smul_mk, mk_eq_iff]

Premises used: NumberField.InfinitePlace.smul_mk, NumberField.InfinitePlace.mk_eq_iff, MulAction.mem_stabilizer_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
φ : K →+* ℂ
σ : Gal(K/k)
rw : φ.comp (↑σ.symm : K →+* K) = φ ∨ star φ = φ.comp (↑σ.symm : K →+* K) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm
⊢ φ.comp (↑σ.symm : K →+* K) = φ ∨ conjugate (φ.comp (↑σ.symm : K →+* K)) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Tactic:
rw [← ComplexEmbedding.isConj_symm, ComplexEmbedding.conjugate, star_eq_iff_star_eq]

Premises used: NumberField.ComplexEmbedding.conjugate, star_eq_iff_star_eq, NumberField.ComplexEmbedding.isConj_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
φ : K →+* ℂ
σ : Gal(K/k)
⊢ φ.comp (↑σ.symm : K →+* K) = φ ∨ star φ = φ.comp (↑σ.symm : K →+* K) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm

Tactic:
or_congr ⟨fun H ↦ ?_, fun H ↦ H ▸ rfl⟩ Iff.rfl

Premises used: or_congr, Iff.rfl, Eq.rec, Iff.intro, Eq.symm, 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
φ : K →+* ℂ
σ : Gal(K/k)
refine : ∀ (H : φ.comp (↑σ.symm : K →+* K) = φ), σ = 1
⊢ φ.comp (↑σ.symm : K →+* K) = φ ∨ star φ = φ.comp (↑σ.symm : K →+* K) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm

Tactic:
refine or_congr ⟨fun H ↦ ?_, fun H ↦ H ▸ rfl⟩ Iff.rfl

Premises used: or_congr, Iff.rfl, Iff.intro
-- 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
φ : K →+* ℂ
σ : Gal(K/k)
H : φ.comp (↑σ.symm : K →+* K) = φ
⊢ σ = 1

Tactic:
congr_arg AlgEquiv.symm
    (AlgEquiv.ext (g := AlgEquiv.refl) fun x ↦ φ.injective (RingHom.congr_fun H x))

Premises used: AlgEquiv.symm, RingHom.congr_fun, RingHom.injective, congr_arg, AlgEquiv.ext, Equiv.symm, AlgEquiv.refl, Equiv.refl
-- 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
φ : K →+* ℂ
σ : Gal(K/k)
H : φ.comp (↑σ.symm : K →+* K) = φ
⊢ σ = 1

Tactic:
exact congr_arg AlgEquiv.symm
    (AlgEquiv.ext (g := AlgEquiv.refl) fun x ↦ φ.injective (RingHom.congr_fun H x))

Premises used: AlgEquiv.symm, RingHom.congr_fun, RingHom.injective, congr_arg, AlgEquiv.ext
-- 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
h : IsUnramified k w
rw :
  ∀ ⦃x : Gal(K/k)⦄,
    Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk w.embedding)) x → Membership.mem (γ := Subgroup Gal(K/k)) ⊥ x
⊢ Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥

Tactic:
rw [eq_bot_iff, ← mk_embedding w, SetLike.le_def]

Premises used: NumberField.InfinitePlace.mk_embedding, SetLike.le_def, eq_bot_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
w : InfinitePlace K
h : IsUnramified k w
simp : ∀ (a : Gal(K/k)), ComplexEmbedding.IsConj w.embedding a → a = 1
⊢ ∀ ⦃x : Gal(K/k)⦄,
    Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk w.embedding)) x → Membership.mem (γ := Subgroup Gal(K/k)) ⊥ x

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

Premises used: forall_eq_or_imp, NumberField.InfinitePlace.mem_stabilizer_mk_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
h : IsUnramified k w
⊢ ∀ (a : Gal(K/k)), ComplexEmbedding.IsConj w.embedding a → a = 1

Tactic:
fun σ hσ ↦ hσ.isUnramified_mk_iff.mp ((mk_embedding w).symm ▸ h)

Premises used: NumberField.InfinitePlace.mk_embedding, Eq.rec, Iff.mp, Eq.symm, NumberField.ComplexEmbedding.IsConj.isUnramified_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
w : InfinitePlace K
h : IsUnramified k w
⊢ ∀ (a : Gal(K/k)), ComplexEmbedding.IsConj w.embedding a → a = 1

Tactic:
exact fun σ hσ ↦ hσ.isUnramified_mk_iff.mp ((mk_embedding w).symm ▸ 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
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
h₁ : ∀ (x : Gal(K/k)), x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
⊢ (↑(Stab (mk φ)) : Set Gal(K/k)) = {1, σ}

Tactic:
ext
-- 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)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
x : Gal(K/k)
h₁ : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
h₂ : x = 1 ∨ ComplexEmbedding.IsConj φ x ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
h₃ : x = 1 ∨ ComplexEmbedding.IsConj φ x ↔ x = 1 ∨ Membership.mem (γ := Set Gal(K/k)) {σ} x
h₄ : x = 1 ∨ ComplexEmbedding.IsConj φ x ↔ x = 1 ∨ x = σ
h₅ : x = 1 ∨ σ = x ↔ x = 1 ∨ x = σ
h₆ h₇ : x = 1 ∨ x = σ ↔ x = 1 ∨ x = σ
⊢ x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x

Tactic:
rw [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    ← h.ext_iff, eq_comm (a := σ)]

Premises used: eq_comm, Set.mem_singleton_iff, SetLike.mem_coe, NumberField.ComplexEmbedding.IsConj.ext_iff, NumberField.InfinitePlace.mem_stabilizer_mk_iff, Set.mem_insert_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
w : InfinitePlace K
rw :
  Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2
⊢ Nat.card.{u_2} ↥(Stab w) = 1 ∨ Nat.card.{u_2} ↥(Stab w) = 2

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

Premises used: SetLike.coe_sort_coe, NumberField.InfinitePlace.mk_embedding
-- 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
pos :
  ∀ (h : ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ),
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
      Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2
neg :
  ∀ (h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ),
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
      Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2
⊢ Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2

Tactic:
by_cases! h : ∃ σ, ComplexEmbedding.IsConj (k := k) (embedding 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
h : ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ
pos :
  ∀ (σ : Gal(K/k)) (hσ : ComplexEmbedding.IsConj w.embedding σ),
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
      Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2
⊢ Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2

Tactic:
obtain ⟨σ, 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
w : InfinitePlace K
σ : Gal(K/k)
hσ : ComplexEmbedding.IsConj w.embedding σ
pos : Nat.card.{u_2} (↑{1, σ} : Type u_2) = 1 ∨ Nat.card.{u_2} (↑{1, σ} : Type u_2) = 2
⊢ Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2

Tactic:
rw [hσ.coe_stabilizer_mk]

Premises used: NumberField.ComplexEmbedding.IsConj.coe_stabilizer_mk
-- 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
σ : Gal(K/k)
hσ : ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card.{u_2} (↑{1, σ} : Type u_2) = 1 ∨ Nat.card.{u_2} (↑{1, σ} : Type u_2) = 2

Tactic:
simp
-- 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
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
neg : Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1
⊢ Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2

Tactic:
left
-- 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
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
trans : Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = Nat.card.{u_2} (↑{1} : Type u_2)
trans₁ : Nat.card.{u_2} (↑{1} : Type u_2) = 1
⊢ Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1

Tactic:
trans Nat.card ({1} : Set Gal(K/k))

Premises used: Set.Elem, Nat.card, Singleton.singleton, OfNat.ofNat
-- 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
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
e_α : ∀ (x : Gal(K/k)), x ∈ (↑(Stab (mk w.embedding)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1} x
⊢ Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = Nat.card.{u_2} (↑{1} : Type u_2)

Tactic:
congr with x
-- 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
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
x : Gal(K/k)
⊢ x ∈ (↑(Stab (mk w.embedding)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1} x

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

Premises used: or_iff_left_iff_imp, Set.mem_singleton_iff, SetLike.mem_coe, NumberField.InfinitePlace.mem_stabilizer_mk_iff, IsEmpty.forall_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
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card.{u_2} (↑{1} : Type u_2) = 1

Tactic:
simp
-- 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
rw :
  Nat.card.{u_2} (↑(↑(Stab w) : Set Gal(K/k)) : Type u_2) = 1 ∨
    Nat.card.{u_2} (↑(↑(Stab w) : Set Gal(K/k)) : Type u_2) = 2
rw₁ rw₂ rw₃ :
  Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2
pos :
  ∀ (h : ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ),
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
      Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2
neg neg₁ :
  ∀ (h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ),
    Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1 ∨
      Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 2
⊢ Nat.card.{u_2} ↥(Stab w) = 1 ∨ Nat.card.{u_2} ↥(Stab w) = 2

Tactic:
classical
  rw [← SetLike.coe_sort_coe, ← mk_embedding w]
  by_cases! h : ∃ σ, ComplexEmbedding.IsConj (k := k) (embedding w) σ
  · obtain ⟨σ, hσ⟩ := h
    rw [hσ.coe_stabilizer_mk]
    simp
  · left
    trans Nat.card ({1} : Set Gal(K/k))
    · congr with x
      simp only [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_singleton_iff, or_iff_left_iff_imp,
        h x, IsEmpty.forall_iff]
    · simp

Premises used: SetLike.coe_sort_coe, or_iff_left_iff_imp, NumberField.InfinitePlace.mk_embedding, Set.Elem, Nat.card, Set.mem_singleton_iff, SetLike.mem_coe, NumberField.InfinitePlace.mem_stabilizer_mk_iff, Singleton.singleton, OfNat.ofNat, IsEmpty.forall_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
w : InfinitePlace K
inst_3 : IsGalois k K
rw :
  (∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔
    Eq (α := Subgroup Gal(K/k)) (Stab (mk w.embedding)) ⊥
⊢ IsUnramified k w ↔ Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥

Tactic:
rw [← mk_embedding w, isUnramified_mk_iff_forall_isConj]

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj