awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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 = σ
⊢ x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
have h₅ : x = 1 ∨ σ = x ↔ x = 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 := σ)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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 = σ
⊢ x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
have h₆ : x = 1 ∨ x = σ ↔ x = 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 := σ)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
w : InfinitePlace K
⊢ Nat.card.{u_2} ↥(Stab w) = 1 ∨ Nat.card.{u_2} ↥(Stab w) = 2
have 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
Tactic: rw [← SetLike.coe_sort_coe, ← mk_embedding w]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
w : InfinitePlace K
⊢ 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
have 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
Tactic: by_cases! h : ∃ σ, ComplexEmbedding.IsConj (k := k) (embedding w) σ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ 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
have 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
Tactic: by_cases! h : ∃ σ, ComplexEmbedding.IsConj (k := k) (embedding w) σ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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} (↑(↑(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
have 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
Tactic: obtain ⟨σ, hσ⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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} (↑(↑(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
have pos : Nat.card.{u_2} (↑{1, σ} : Type u_2) = 1 ∨ Nat.card.{u_2} (↑{1, σ} : Type u_2) = 2
Tactic: rw [hσ.coe_stabilizer_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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} (↑(↑(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
have neg : Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1
have trans : Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = Nat.card.{u_2} (↑{1} : Type u_2)
Tactic: trans Nat.card ({1} : Set Gal(K/k))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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)
⊢ Nat.card.{u_2} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = 1
have trans₁ : Nat.card.{u_2} (↑{1} : Type u_2) = 1
Tactic: trans Nat.card ({1} : Set Gal(K/k))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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} (↑(↑(Stab (mk w.embedding)) : Set Gal(K/k)) : Type u_2) = Nat.card.{u_2} (↑{1} : Type u_2)
have e_α : ∀ (x : Gal(K/k)), x ∈ (↑(Stab (mk w.embedding)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1} x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
k : Type u_1
inst : Field k
K : Type u_2
inst_1 : Field K
inst_2 : Algebra k K
w : InfinitePlace K
⊢ Nat.card.{u_2} ↥(Stab w) = 1 ∨ Nat.card.{u_2} ↥(Stab w) = 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ Nat.card.{u_2} ↥(Stab w) = 1 ∨ Nat.card.{u_2} ↥(Stab w) = 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ Nat.card.{u_2} ↥(Stab w) = 1 ∨ Nat.card.{u_2} ↥(Stab w) = 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ Nat.card.{u_2} ↥(Stab w) = 1 ∨ Nat.card.{u_2} ↥(Stab w) = 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ IsUnramified k w ↔ Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥
have rw : (∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔
  Eq (α := Subgroup Gal(K/k)) (Stab (mk w.embedding)) ⊥
Tactic: rw [← mk_embedding w, isUnramified_mk_iff_forall_isConj]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ IsUnramified k w ↔ Nat.card.{u_2} ↥(Stab w) = 1
have rw : Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥ ↔ Nat.card.{u_2} ↥(Stab w) = 1
Tactic: rw [isUnramified_iff_stabilizer_eq_bot, Subgroup.card_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ IsUnramified k w ↔ Nat.card.{u_2} ↥(Stab w) = 1
have rw₁ : Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥ ↔ Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥
Tactic: rw [isUnramified_iff_stabilizer_eq_bot, Subgroup.card_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ¬IsUnramified k w ↔ Nat.card.{u_2} ↥(Stab w) = 2
have rw : ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
Tactic: rw [isUnramified_iff_card_stabilizer_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
have inl : ∀ (e : Nat.card.{u_2} ↥(Stab w) = 1), ¬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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
have inr : ∀ (e : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
have inl : ¬Eq (α := ℕ) 1 1 ↔ Eq (α := ℕ) 1 2
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ¬Nat.card.{u_2} ↥(Stab w) = 1 ↔ Nat.card.{u_2} ↥(Stab w) = 2
have inr : ¬Eq (α := ℕ) 2 1 ↔ Eq (α := ℕ) 2 2
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
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 φ)
⊢ ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ
have 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 φ σ
Tactic: obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, h₁, -⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ ∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ
have 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 φ σ
Tactic: rw [mem_stabilizer_mk_iff] at hx hy
Cleared hypotheses: y, hy, h₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ Nat.card.{u_2} ↥(Stab w) = if IsUnramified k w then 1 else 2
have isTrue : IsUnramified k w → Nat.card.{u_2} ↥(Stab w) = 1
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ Nat.card.{u_2} ↥(Stab w) = if IsUnramified k w then 1 else 2
have isFalse : ¬IsUnramified k w → Nat.card.{u_2} ↥(Stab w) = 2
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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))
have pos : ∀ (H : Finite.{u_2 + 1} Gal(K/k)), Even (Nat.card.{u_2} Gal(K/k))
Tactic: by_cases H : Finite Gal(K/k)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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))
⊢ Even (Nat.card.{u_2} Gal(K/k))
have neg : ∀ (H : ¬Finite.{u_2 + 1} Gal(K/k)), Even (Nat.card.{u_2} Gal(K/k))
Tactic: by_cases H : Finite Gal(K/k)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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 (Nat.card.{u_2} Gal(K/k))
have pos : ∀ (val : Fintype Gal(K/k)), Even (Nat.card.{u_2} Gal(K/k))
Tactic: cases nonempty_fintype Gal(K/k)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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)
⊢ Even (Nat.card.{u_2} Gal(K/k))
have pos : Nat.card.{u_2} ↥(Stab w) ∣ Nat.card.{u_2} Gal(K/k)
Tactic: rw [even_iff_two_dvd, ← not_isUnramified_iff_card_stabilizer_eq_two.mp hw]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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 (Nat.card.{u_2} Gal(K/k))
have h : Nat.card.{u_2} Gal(K/k) = 0
Tactic: convert! Even.zero
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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)
⊢ Nat.card.{u_2} Gal(K/k) = 0
have h : ∀ (e : ¬Nat.card.{u_2} Gal(K/k) = 0), False
Tactic: by_contra e
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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 (finrank k K)
have pos : FiniteDimensional k K → Even (finrank k K)
Tactic: by_cases FiniteDimensional k K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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)
⊢ Even (finrank k K)
have neg : ¬FiniteDimensional k K → Even (finrank k K)
Tactic: by_cases FiniteDimensional k K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w
have rw : (σ • w).IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ IsUnramified k w
Tactic: rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
    ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w
have rw₁ : (σ • w).IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
Tactic: rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
    ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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))
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w
have rw₂ : w.IsReal ∨ IsComplex ((σ • w).comap (algebraMap k K)) ↔ w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
Tactic: rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
    ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
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))
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w
have rw₃ : w.IsReal ∨
    IsComplex (w.comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ.symm : K →+* K) (algebraMap k K))) ↔
  w.IsReal ∨ IsComplex (w.comap (algebraMap k K))
Tactic: rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
    ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]