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
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsMixed k φ
have refine_1 : IsMixed k (star (star φ))
Tactic: rw [← star_star φ]
-- 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
φ : K →+* ℂ
h : IsMixed k φ
⊢ IsRamified k (mk φ)
have refine_2 : ¬ComplexEmbedding.IsReal (mk φ).embedding ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
Tactic: rw [isRamified_iff, isComplex_iff, comap_mk, isReal_iff, embedding_mk_eq_of_isReal h.1]
-- 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
φ : K →+* ℂ
h : IsMixed k φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding
have inl : (mk φ).embedding = φ → ¬ComplexEmbedding.IsReal (mk φ).embedding
Tactic: rcases embedding_mk_eq φ with (_ | _)
-- 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
φ : K →+* ℂ
h : IsMixed k φ
inl : (mk φ).embedding = φ → ¬ComplexEmbedding.IsReal (mk φ).embedding
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding
have inr : (mk φ).embedding = conjugate φ → ¬ComplexEmbedding.IsReal (mk φ).embedding
Tactic: rcases embedding_mk_eq φ with (_ | _)
-- 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
w : InfinitePlace K
h : IsUnramified k w
hw : ComplexEmbedding.IsReal (w.embedding.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal w.embedding
have hw₁ : IsReal (w.comap (algebraMap k K))
Tactic: rw [← isReal_mk_iff, ← comap_mk, mk_embedding] at hw
Cleared hypotheses: hw
-- 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
w : InfinitePlace K
h : IsUnramified k w
hw : ComplexEmbedding.IsReal ((conjugate w.embedding).comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)
have hw₁ : IsReal (w.comap (algebraMap k K))
Tactic: simp_rw [conjugate_comp, IsSelfAdjoint.star_iff, ← isReal_mk_iff, ← comap_mk, mk_embedding] at hw
Cleared hypotheses: 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
φ : K →+* ℂ
⊢ IsUnramified k (mk φ) ↔ IsUnmixed k φ
have refine_1 : ∀ (h : IsUnramified k (mk φ)), IsUnmixed k φ
Tactic: refine ⟨fun h ↦ ?_, fun 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
φ : K →+* ℂ
refine_1 : ∀ (h : IsUnramified k (mk φ)), IsUnmixed k φ
⊢ IsUnramified k (mk φ) ↔ IsUnmixed k φ
have refine_2 : ∀ (h : IsUnmixed k φ), IsUnramified k (mk φ)
Tactic: refine ⟨fun h ↦ ?_, fun 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
⊢ IsUnmixed k φ
have refine_1 : ∀ (hl : (mk φ).embedding = φ), IsUnmixed k φ
Tactic: rcases embedding_mk_eq φ with (hl | hr)
-- 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
refine_1 : ∀ (hl : (mk φ).embedding = φ), IsUnmixed k φ
⊢ IsUnmixed k φ
have refine_1₁ : ∀ (hr : (mk φ).embedding = conjugate φ), IsUnmixed k φ
Tactic: rcases embedding_mk_eq φ with (hl | hr)
-- 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
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k φ
have refine_1 : IsUnmixed k (star (star φ))
Tactic: rw [← star_star φ]
-- 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
φ : K →+* ℂ
h : IsUnmixed k φ
⊢ IsUnramified k (mk φ)
have refine_2 : ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))
Tactic: rw [isUnramified_iff, isReal_iff]
-- 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
φ : K →+* ℂ
h : IsUnmixed k φ
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))
have pos : ∀ (hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))),
  ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))
Tactic: by_cases hv : ComplexEmbedding.IsReal (φ.comp (algebraMap 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
φ : K →+* ℂ
h : IsUnmixed k φ
pos :
  ∀ (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))
have neg : ∀ (hv : ¬ComplexEmbedding.IsReal (φ.comp (algebraMap k K))),
  ComplexEmbedding.IsReal (mk φ).embedding ∨ IsComplex ((mk φ).comap (algebraMap k K))
Tactic: by_cases hv : ComplexEmbedding.IsReal (φ.comp (algebraMap 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)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw : IsUnramified k (mk φ) ↔ ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 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]
-- 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 φ σ
rw : IsUnramified k (mk φ) ↔ ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₁ : IsUnramified k (mk φ) ↔ ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
rw : IsUnramified k (mk φ) ↔ ComplexEmbedding.IsConj.{u_2, u_1} (k := k) φ 1
rw₁ : IsUnramified k (mk φ) ↔ ComplexEmbedding.IsReal φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₂ : ¬IsUnramified k (mk φ) ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
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 φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₃ : (mk φ).IsComplex ∧ IsReal ((mk φ).comap (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
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 φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₄ : ¬(mk φ).IsReal ∧ IsReal ((mk φ).comap (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
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 φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₅ : ¬(mk φ).IsReal ∧ IsReal (mk (φ.comp (algebraMap k K))) ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
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 φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₆ : ¬ComplexEmbedding.IsReal φ ∧ IsReal (mk (φ.comp (algebraMap k K))) ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
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 φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₇ : ¬ComplexEmbedding.IsReal φ ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
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 φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₈ : ¬ComplexEmbedding.IsReal φ ∧ True ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 φ σ
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 φ
⊢ IsUnramified k (mk φ) ↔ σ = 1
have rw₉ : ¬ComplexEmbedding.IsReal φ ↔ ¬ComplexEmbedding.IsReal φ
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]
-- 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 →+* ℂ
⊢ IsUnramified k (mk φ) ↔ ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
have refine : ∀ (H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1), IsUnramified k (mk φ)
Tactic: refine ⟨fun H σ hσ ↦ hσ.isUnramified_mk_iff.mp H,
    fun 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 : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
⊢ IsUnramified k (mk φ)
have by_contra : ∀ (hφ : ¬IsUnramified k (mk φ)), False
Tactic: by_contra hφ
-- 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 : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬IsUnramified k (mk φ)
⊢ False
have hφ₁ : (mk φ).IsComplex ∧ IsReal ((mk φ).comap (algebraMap k K))
Tactic: rw [not_isUnramified_iff] at hφ
Cleared hypotheses: hφ
-- 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 : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : (mk φ).IsComplex ∧ IsReal ((mk φ).comap (algebraMap k K))
⊢ False
have hφ₁ : ¬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φ
Cleared hypotheses: hφ
-- 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 : ∀ (σ : 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
⊢ False
have this₁ : IsScalarTower k K ℂ
Tactic: have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_eq' rfl
-- 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 : ∀ (σ : 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' := ⋯ }
⊢ False
have this₁ : ComplexEmbedding.IsConj φ (φ'.restrictNormal' K)
Tactic: have : ComplexEmbedding.IsConj φ (AlgHom.restrictNormal' φ' K) :=
    (RingHom.ext <| AlgHom.restrictNormal_commutes φ' K).symm
-- 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
φ : K →+* ℂ
σ : Gal(K/k)
⊢ Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) σ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ
have simp : φ.comp (↑σ.symm : K →+* K) = φ ∨ conjugate (φ.comp (↑σ.symm : K →+* K)) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ
Tactic: simp only [MulAction.mem_stabilizer_iff, smul_mk, mk_eq_iff]
-- 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
φ : K →+* ℂ
σ : Gal(K/k)
⊢ φ.comp (↑σ.symm : K →+* K) = φ ∨ conjugate (φ.comp (↑σ.symm : K →+* K)) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ
have rw : φ.comp (↑σ.symm : K →+* K) = φ ∨ star φ = φ.comp (↑σ.symm : K →+* K) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm
Tactic: rw [← ComplexEmbedding.isConj_symm, ComplexEmbedding.conjugate, star_eq_iff_star_eq]
-- 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
φ : K →+* ℂ
σ : Gal(K/k)
⊢ φ.comp (↑σ.symm : K →+* K) = φ ∨ star φ = φ.comp (↑σ.symm : K →+* K) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm
have refine : ∀ (H : φ.comp (↑σ.symm : K →+* K) = φ), σ = 1
Tactic: refine or_congr ⟨fun H ↦ ?_, fun H ↦ H ▸ rfl⟩ Iff.rfl
-- 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 : IsUnramified k w
⊢ Eq (α := Subgroup Gal(K/k)) (Stab w) ⊥
have rw : ∀ ⦃x : Gal(K/k)⦄,
  Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk w.embedding)) x → Membership.mem (γ := Subgroup Gal(K/k)) ⊥ x
Tactic: rw [eq_bot_iff, ← mk_embedding w, SetLike.le_def]
-- 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 : IsUnramified k w
⊢ ∀ ⦃x : Gal(K/k)⦄,
    Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk w.embedding)) x → Membership.mem (γ := Subgroup Gal(K/k)) ⊥ x
have simp : ∀ (a : Gal(K/k)), ComplexEmbedding.IsConj w.embedding a → a = 1
Tactic: simp only [mem_stabilizer_mk_iff, Subgroup.mem_bot, forall_eq_or_imp, true_and]
-- 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 φ σ
⊢ (↑(Stab (mk φ)) : Set Gal(K/k)) = {1, σ}
have h₁ : ∀ (x : Gal(K/k)), x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
Tactic: ext
-- 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)
⊢ x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
have h₁ : Membership.mem (γ := Subgroup Gal(K/k)) (Stab (mk φ)) x ↔ 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 := σ)]
-- 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
⊢ x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
have h₂ : x = 1 ∨ ComplexEmbedding.IsConj φ x ↔ 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 := σ)]
-- 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
⊢ x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
have h₃ : x = 1 ∨ ComplexEmbedding.IsConj φ x ↔ x = 1 ∨ Membership.mem (γ := Set Gal(K/k)) {σ} 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
⊢ x ∈ (↑(Stab (mk φ)) : Set Gal(K/k)) ↔ Membership.mem (γ := Set Gal(K/k)) {1, σ} x
have h₄ : x = 1 ∨ ComplexEmbedding.IsConj φ 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 := σ)]