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
inst_3 : NumberField k
inst_4 : NumberField K
inst_5 : IsGalois k K
inst_6 : IsUnramifiedAtInfinitePlaces k K
rw :
  Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w} * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) {w : InfinitePlace k | InfinitePlace.IsUnramifiedIn K w}ᶜ *
        (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₁ :
  Finset.card.{u_1} (α := InfinitePlace k) Finset.univ * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₂ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₃ :
  card.{u_1} (InfinitePlace k) * finrank k K +
      Finset.card.{u_1} (α := InfinitePlace k) Finset.univᶜ * (finrank k K / 2) =
    card.{u_1} (InfinitePlace k) * finrank k K
rw₄ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₅ : card.{u_1} (InfinitePlace k) * finrank k K + 0 * (finrank k K / 2) = card.{u_1} (InfinitePlace k) * finrank k K
rw₆ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₇ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₈ : card.{u_1} (InfinitePlace k) * finrank k K + 0 = card.{u_1} (InfinitePlace k) * finrank k K
rw₉ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₁₀ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₁₁ : card.{u_1} (InfinitePlace k) * finrank k K = card.{u_1} (InfinitePlace k) * finrank k K
rw₁₂ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₁₃ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₁₄ : card.{u_1} (InfinitePlace k) * finrank k K = card.{u_1} (InfinitePlace k) * finrank k K
rw₁₅ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₁₆ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
rw₁₇ : Eq.{u_1 + 1} (α := Finset (InfinitePlace k)) Finset.univᶜ ∅
rw₁₈ rw₁₉ :
  ∀ (x : InfinitePlace k),
    Membership.mem (γ := Finset (InfinitePlace k)) Finset.univ x → InfinitePlace.IsUnramifiedIn K x
⊢ card.{u_2} (InfinitePlace K) = card.{u_1} (InfinitePlace k) * finrank k K
have rw₂₀ : ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x
Tactic: classical
  rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
⊢ w.comap (algebraMap K L) = v
have h : ∀ (k : K), Eq (α := ℝ) ((w.comap (algebraMap K L) : (a : K) → ℝ) k : ℝ) ((v : (a : K) → ℝ) k : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
⊢ mk (w.embedding.comp (algebraMap K L)) = v
have rw : (mk w.embedding).comap (algebraMap K L) = v
Tactic: rw [← comap_mk, w.mk_embedding, comap_eq w v]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
rw : (mk w.embedding).comap (algebraMap K L) = v
⊢ mk (w.embedding.comp (algebraMap K L)) = v
have rw₁ : w.comap (algebraMap K L) = v
Tactic: rw [← comap_mk, w.mk_embedding, comap_eq w v]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
rw : (mk w.embedding).comap (algebraMap K L) = v
rw₁ : w.comap (algebraMap K L) = v
⊢ mk (w.embedding.comp (algebraMap K L)) = v
have rw₂ : v = v
Tactic: rw [← comap_mk, w.mk_embedding, comap_eq w v]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding
have x : Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L)) ∨
  Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (conjugate (w.embedding.comp (algebraMap K L)))
Tactic: cases embedding_mk_eq (w.embedding.comp (algebraMap K L)) with
  | inl hl => exact .inl (hl ▸ congrArg embedding (mk_embedding_comp w v))
  | inr hr => simpa using .inr (hr ▸ congrArg embedding (mk_embedding_comp w v))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hv : v.IsComplex
⊢ w.IsComplex
have rw : ∀ (hv : ∃ (x : K), ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)),
  ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)
Tactic: rw [isComplex_iff, ComplexEmbedding.isReal_iff, RingHom.ext_iff, not_forall] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hv : ∃ (x : K), ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
⊢ ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)
have obtain : ∀ (x : K) (hx : ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)),
  ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)
Tactic: obtain ⟨x, hx⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx : ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
⊢ ∃ (x : L), ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) x : ℂ) ((w.embedding : (a : L) → ℂ) x : ℂ)
have h : ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
    ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
Tactic: use algebraMap K L x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx : ¬Eq (α := ℂ) ((conjugate v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
⊢ ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
have hx₁ : ¬Eq (α := ℂ) ((conjugate (embedding (mk (w.embedding.comp (algebraMap K L)))) : (a : K) → ℂ) x : ℂ)
    ((embedding (mk (w.embedding.comp (algebraMap K L))) : (a : K) → ℂ) x : ℂ)
Tactic: rw [← comap_eq w v, ← mk_embedding w, comap_mk] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx :
  ¬Eq (α := ℂ) ((conjugate (embedding (mk (w.embedding.comp (algebraMap K L)))) : (a : K) → ℂ) x : ℂ)
      ((embedding (mk (w.embedding.comp (algebraMap K L))) : (a : K) → ℂ) x : ℂ)
⊢ ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
have h : Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L)) →
  ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
Tactic: rcases embedding_mk_eq (w.embedding.comp (algebraMap K L)) with (_ | _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
hx :
  ¬Eq (α := ℂ) ((conjugate (embedding (mk (w.embedding.comp (algebraMap K L)))) : (a : K) → ℂ) x : ℂ)
      ((embedding (mk (w.embedding.comp (algebraMap K L))) : (a : K) → ℂ) x : ℂ)
h :
  Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (w.embedding.comp (algebraMap K L)) →
    ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
        ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
⊢ ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
have h₁ : Eq (α := K →+* ℂ) (embedding (mk (w.embedding.comp (algebraMap K L)))) (conjugate (w.embedding.comp (algebraMap K L))) →
  ¬Eq (α := ℂ) ((conjugate w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
      ((w.embedding : (a : L) → ℂ) ((algebraMap K L : (a : K) → L) x : L) : ℂ)
Tactic: rcases embedding_mk_eq (w.embedding.comp (algebraMap K L)) with (_ | _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : w.IsReal
⊢ v.IsReal
have rw : ∀ (hw : ¬w.IsComplex), ¬v.IsComplex
Tactic: rw [← not_isComplex_iff_isReal] at hw ⊢
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (mixedEmbeddingsOver L v.embedding) ψ
⊢ Membership.mem (γ := Set (L →+* ℂ))
    (Sum.elim embedding (conjugate ∘ embedding) ''
      (OrderIso.symm Set.sumEquiv :
          (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
        (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
    ψ
have x : (mk ψ).embedding = ψ ∨ (mk ψ).embedding = conjugate ψ
Tactic: cases embedding_mk_eq ψ with
        | inl hl => simpa using .inl ⟨mk ψ, mk_mem_ramifiedPlacesOver h, hl⟩
        | inr hr => simpa using .inr ⟨mk ψ, mk_mem_ramifiedPlacesOver h, by aesop⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
⊢ 2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    Set.ncard (α := L →+* ℂ) (mixedEmbeddingsOver L v.embedding)
have rw : 2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
  Set.ncard.{u_5} (α := InfinitePlace L ⊕ InfinitePlace L)
    ((OrderIso.symm Set.sumEquiv :
        (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
      (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
Tactic: rw [← (bijOn_sumElim_conjugate L v).ncard_eq, two_mul, Set.ncard_sumEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
rw :
  2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    Set.ncard.{u_5} (α := InfinitePlace L ⊕ InfinitePlace L)
      ((OrderIso.symm Set.sumEquiv :
          (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
        (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
⊢ 2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    Set.ncard (α := L →+* ℂ) (mixedEmbeddingsOver L v.embedding)
have rw₁ : Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) + Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
  Set.ncard.{u_5} (α := InfinitePlace L ⊕ InfinitePlace L)
    ((OrderIso.symm Set.sumEquiv :
        (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
      (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
Tactic: rw [← (bijOn_sumElim_conjugate L v).ncard_eq, two_mul, Set.ncard_sumEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
rw :
  2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    Set.ncard.{u_5} (α := InfinitePlace L ⊕ InfinitePlace L)
      ((OrderIso.symm Set.sumEquiv :
          (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
        (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
rw₁ :
  Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) +
      Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    Set.ncard.{u_5} (α := InfinitePlace L ⊕ InfinitePlace L)
      ((OrderIso.symm Set.sumEquiv :
          (a : Set (InfinitePlace L) × Set (InfinitePlace L)) → Set (InfinitePlace L ⊕ InfinitePlace L))
        (ramifiedPlacesOver L v, ramifiedPlacesOver L v))
⊢ 2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    Set.ncard (α := L →+* ℂ) (mixedEmbeddingsOver L v.embedding)
have rw₂ : Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) + Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
  Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) + Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v)
Tactic: rw [← (bijOn_sumElim_conjugate L v).ncard_eq, two_mul, Set.ncard_sumEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
left : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : IsUnramified K w
⊢ Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) (v.embeddingConjugateIte w)
have pos : ∀ (h : ComplexEmbedding.LiesOver w.embedding v.embedding),
  Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) (v.embeddingConjugateIte w)
Tactic: by_cases h : ComplexEmbedding.LiesOver w.embedding v.embedding
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
left : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
hw : IsUnramified K w
pos :
  ∀ (h : ComplexEmbedding.LiesOver w.embedding v.embedding),
    Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) (v.embeddingConjugateIte w)
⊢ Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) (v.embeddingConjugateIte w)
have neg : ∀ (h : ¬ComplexEmbedding.LiesOver w.embedding v.embedding),
  Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) (v.embeddingConjugateIte w)
Tactic: by_cases h : ComplexEmbedding.LiesOver w.embedding v.embedding
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
⊢ Set.SurjOn (α := InfinitePlace L) v.embeddingConjugateIte (unramifiedPlacesOver L v)
    (unmixedEmbeddingsOver L v.embedding)
have refine : ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ),
  v.embeddingConjugateIte (mk ψ) = ψ
Tactic: refine fun ψ h ↦ ⟨mk ψ, mk_mem_unramifiedPlacesOver h, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ
have inl : (mk ψ).embedding = ψ → v.embeddingConjugateIte (mk ψ) = ψ
Tactic: rcases embedding_mk_eq ψ with (_ | hψ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ
inl : (mk ψ).embedding = ψ → v.embeddingConjugateIte (mk ψ) = ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ
have inr : ∀ (hψ : (mk ψ).embedding = conjugate ψ), v.embeddingConjugateIte (mk ψ) = ψ
Tactic: rcases embedding_mk_eq ψ with (_ | hψ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ
hψ : (mk ψ).embedding = conjugate ψ
h_1 : ComplexEmbedding.LiesOver (conjugate ψ) v.embedding
over : (conjugate ψ).comp (algebraMap K L) = v.embedding
⊢ ComplexEmbedding.IsReal (ψ.comp (algebraMap K L))
have this : ψ.comp (algebraMap K L) = v.embedding
Tactic: have := h.1.over
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
⊢ Set.SurjOn (α := InfinitePlace L) v.embeddingConjugateIte (unramifiedPlacesOver L v)
    (unmixedEmbeddingsOver L v.embedding)
have refine : ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ),
  v.embeddingConjugateIte (mk ψ) = ψ
Tactic: classical
  refine fun ψ h ↦ ⟨mk ψ, mk_mem_unramifiedPlacesOver h, ?_⟩
  rcases embedding_mk_eq ψ with (_ | hψ)
  · aesop (add simp [embeddingConjugateIte, unmixedEmbeddingsOver])
  · simpa [embeddingConjugateIte, hψ] using fun ⟨_⟩ ↦
      h.2.isReal_iff_isReal.1 <| by have := h.1.over; aesop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
refine :
  ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ),
    v.embeddingConjugateIte (mk ψ) = ψ
⊢ Set.SurjOn (α := InfinitePlace L) v.embeddingConjugateIte (unramifiedPlacesOver L v)
    (unmixedEmbeddingsOver L v.embedding)
have inl : ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ),
  (mk ψ).embedding = ψ → v.embeddingConjugateIte (mk ψ) = ψ
Tactic: classical
  refine fun ψ h ↦ ⟨mk ψ, mk_mem_unramifiedPlacesOver h, ?_⟩
  rcases embedding_mk_eq ψ with (_ | hψ)
  · aesop (add simp [embeddingConjugateIte, unmixedEmbeddingsOver])
  · simpa [embeddingConjugateIte, hψ] using fun ⟨_⟩ ↦
      h.2.isReal_iff_isReal.1 <| by have := h.1.over; aesop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
refine :
  ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ),
    v.embeddingConjugateIte (mk ψ) = ψ
inl :
  ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ),
    (mk ψ).embedding = ψ → v.embeddingConjugateIte (mk ψ) = ψ
⊢ Set.SurjOn (α := InfinitePlace L) v.embeddingConjugateIte (unramifiedPlacesOver L v)
    (unmixedEmbeddingsOver L v.embedding)
have inr : ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ)
  (hψ : (mk ψ).embedding = conjugate ψ), v.embeddingConjugateIte (mk ψ) = ψ
Tactic: classical
  refine fun ψ h ↦ ⟨mk ψ, mk_mem_unramifiedPlacesOver h, ?_⟩
  rcases embedding_mk_eq ψ with (_ | hψ)
  · aesop (add simp [embeddingConjugateIte, unmixedEmbeddingsOver])
  · simpa [embeddingConjugateIte, hψ] using fun ⟨_⟩ ↦
      h.2.isReal_iff_isReal.1 <| by have := h.1.over; aesop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) =
    Set.ncard (α := L →+* ℂ) (unmixedEmbeddingsOver L v.embedding)
have rw : Set.ncard (α := L →+* ℂ) (unmixedEmbeddingsOver L v.embedding) =
  Set.ncard (α := L →+* ℂ) (unmixedEmbeddingsOver L v.embedding)
Tactic: rw [(bijOn_extensionIte L v).ncard_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
have rw : Finset.card.{u_5} (α := L →+* ℂ)
    (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) sorry) =
  Fintype.card.{u_5} (L →ₐ[K] ℂ)
Tactic: rw [← AlgHom.card K L ℂ, ramifiedPlacesOver_ncard, unramifiedPlacesOver_ncard,
    ← Set.ncard_union_eq (disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver L v.embedding),
    union_unmixedEmbeddingsOver_mixedEmbeddingsOver, Set.ncard_eq_toFinset_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ Finset.card.{u_5} (α := L →+* ℂ)
      (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) =
    Fintype.card.{u_5} (L →ₐ[K] ℂ)
have apply : ∀ (ψ : L →+* ℂ)
  (hψ : ψ ∈ (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) sorry) : Set (L →+* ℂ))),
  ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
Tactic: apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm