awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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))
rw₂ 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)
⊢ 2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    Set.ncard (α := L →+* ℂ) (mixedEmbeddingsOver L v.embedding)

Tactic:
rw [← (bijOn_sumElim_conjugate L v).ncard_eq, two_mul, Set.ncard_sumEquiv_symm_apply]

Premises used: two_mul, Set.ncard_sumEquiv_symm_apply, NumberField.InfinitePlace.bijOn_sumElim_conjugate, Set.BijOn.ncard_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
h : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ v.embeddingConjugateIte w = w.embedding

Tactic:
simp [embeddingConjugateIte, h]

Premises used: _private.0.NumberField.InfinitePlace.embeddingConjugateIte
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
h : ¬ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ v.embeddingConjugateIte w = conjugate w.embedding

Tactic:
simp [embeddingConjugateIte, h]

Premises used: _private.0.NumberField.InfinitePlace.embeddingConjugateIte
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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)
neg :
  ∀ (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)

Tactic:
by_cases h : ComplexEmbedding.LiesOver w.embedding v.embedding

Premises used: NumberField.InfinitePlace.embedding, NumberField.ComplexEmbedding.LiesOver
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
h : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) (v.embeddingConjugateIte w)

Tactic:
simpa [embeddingConjugateIte_pos h] using ⟨h, hw.isUnmixed⟩

Premises used: _private.0.NumberField.InfinitePlace.embeddingConjugateIte_pos
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
h : ¬ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) (v.embeddingConjugateIte w)

Tactic:
simpa [embeddingConjugateIte_neg h] using
      ⟨⟨(LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq w v).resolve_left
        (liesOver_iff.not.1 h)⟩, hw.isUnmixed_conjugate⟩

Premises used: _private.0.NumberField.InfinitePlace.embeddingConjugateIte_neg
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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)

Tactic:
fun ψ h ↦ ⟨mk ψ, mk_mem_unramifiedPlacesOver h, ?_⟩

Premises used: Set.Mem, setOf, Set.SurjOn, NumberField.InfinitePlace.mk, Set.Subset, And.intro, Exists.intro, NumberField.InfinitePlace.mk_mem_unramifiedPlacesOver, Set.image
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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)

Tactic:
refine fun ψ h ↦ ⟨mk ψ, mk_mem_unramifiedPlacesOver h, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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 ψ) = ψ
inr : ∀ (hψ : (mk ψ).embedding = conjugate ψ), v.embeddingConjugateIte (mk ψ) = ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

Tactic:
rcases embedding_mk_eq ψ with (_ | hψ)

Premises used: NumberField.InfinitePlace.embedding_mk_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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_1 : (mk ψ).embedding = ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

Tactic:
aesop (add simp [embeddingConjugateIte, unmixedEmbeddingsOver])

Premises used: _private.0.NumberField.InfinitePlace.embeddingConjugateIte, NumberField.ComplexEmbedding.unmixedEmbeddingsOver
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
⊢ ψ.comp (algebraMap K L) = v.embedding

Tactic:
have := h.1.over
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
this : ψ.comp (algebraMap K L) = v.embedding
⊢ ComplexEmbedding.IsReal (ψ.comp (algebraMap K L))

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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 ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

Tactic:
simpa [embeddingConjugateIte, hψ] using fun ⟨_⟩ ↦
      h.2.isReal_iff_isReal.1 <| by have := h.1.over; aesop

Premises used: _private.0.NumberField.InfinitePlace.embeddingConjugateIte
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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 ψ) = ψ
inr inr₁ :
  ∀ (ψ : L →+* ℂ) (h : Membership.mem (γ := Set (L →+* ℂ)) (unmixedEmbeddingsOver L v.embedding) ψ)
    (hψ : (mk ψ).embedding = conjugate ψ), v.embeddingConjugateIte (mk ψ) = ψ
⊢ Set.SurjOn (α := InfinitePlace L) v.embeddingConjugateIte (unramifiedPlacesOver L v)
    (unmixedEmbeddingsOver L v.embedding)

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

Premises used: _private.0.NumberField.InfinitePlace.embeddingConjugateIte, NumberField.ComplexEmbedding.unmixedEmbeddingsOver
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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.BijOn (α := InfinitePlace L) v.embeddingConjugateIte (unramifiedPlacesOver L v)
    (unmixedEmbeddingsOver L v.embedding)

Tactic:
⟨mapsTo_embeddingConjugateIte L v, ((embedding_injective _).ite (star_injective.comp
    (embedding_injective _)) (fun _ _ ↦ eq_of_embedding_eq_conjugate L)).injOn,
      surjOn_embeddingConjugateIte L v⟩

Premises used: NumberField.InfinitePlace.eq_of_embedding_eq_conjugate, Function.Injective.injOn, _private.0.NumberField.InfinitePlace.mapsTo_embeddingConjugateIte, star_injective, Function.Injective.ite, _private.0.NumberField.InfinitePlace.surjOn_embeddingConjugateIte, Function.Injective.comp, And.intro, Set.BijOn, NumberField.InfinitePlace.embedding_injective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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 rw₁ :
  Set.ncard (α := L →+* ℂ) (unmixedEmbeddingsOver L v.embedding) =
    Set.ncard (α := L →+* ℂ) (unmixedEmbeddingsOver L v.embedding)
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) =
    Set.ncard (α := L →+* ℂ) (unmixedEmbeddingsOver L v.embedding)

Tactic:
rw [(bijOn_extensionIte L v).ncard_eq]

Premises used: Set.BijOn.ncard_eq, _private.0.NumberField.InfinitePlace.bijOn_extensionIte
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
rw :
  Finset.card.{u_5} (α := L →+* ℂ)
      (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) =
    Fintype.card.{u_5} (L →ₐ[K] ℂ)
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L

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]

Premises used: NumberField.ComplexEmbedding.union_unmixedEmbeddingsOver_mixedEmbeddingsOver, NumberField.InfinitePlace.ramifiedPlacesOver_ncard, Set.ncard_union_eq, NumberField.ComplexEmbedding.disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver, NumberField.InfinitePlace.embedding, AlgHom.card, Set.ncard_eq_toFinset_card, Complex, NumberField.InfinitePlace.unramifiedPlacesOver_ncard
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
σ : L →ₐ[K] ℂ
h : σ ∈ (↑univ : Set (L →ₐ[K] ℂ))
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ : L →+* ℂ) (algebraMap K L) = v.embedding

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
σ : L →ₐ[K] ℂ
h : σ ∈ (↑univ : Set (L →ₐ[K] ℂ))
⊢ σ.toRingHom ∈
    (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) : Set (L →+* ℂ))

Tactic:
simpa using ⟨by aesop⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
apply :
  ∀ (ψ : L →+* ℂ)
    (hψ :
      ψ ∈ (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) : Set (L →+* ℂ))),
    ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
⊢ Finset.card.{u_5} (α := L →+* ℂ)
      (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) =
    Fintype.card.{u_5} (L →ₐ[K] ℂ)

Tactic:
apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm

Premises used: AlgHom.coe_ringHom_injective, Function.Injective.injOn, AlgHom.toRingHom, Finset.card_nbij, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
ψ : L →+* ℂ
hψ : ψ ∈ (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) : Set (L →+* ℂ))
⊢ ComplexEmbedding.LiesOver ψ v.embedding

Tactic:
simp only [Set.Finite.toFinset_setOf, coe_filter, mem_univ, true_and, Set.mem_setOf_eq] at hψ

Premises used: Set.Finite.toFinset_setOf, Finset.mem_univ, Finset.coe_filter, Set.mem_setOf_eq, true_and
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
ψ : L →+* ℂ
hψ : ComplexEmbedding.LiesOver ψ v.embedding
x : K
⊢ (↑(↑ψ : L →* ℂ) : OneHom L ℂ).toFun ((algebraMap K L : (a : K) → L) x) = (algebraMap K ℂ : (a : K) → ℂ) x

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← hψ.over]

Premises used: RingHom.algebraMap_toAlgebra, NumberField.ComplexEmbedding.LiesOver.over
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
ψ : L →+* ℂ
hψ : ComplexEmbedding.LiesOver ψ v.embedding
⊢ { toRingHom := ψ, commutes' := ⋯ } ∈ (↑univ : Set (L →ₐ[K] ℂ)) ∧
    AlgHom.toRingHom.{u_4, u_5, 0} (R := K) { toRingHom := ψ, commutes' := ⋯ : L →ₐ[K] ℂ } = ψ

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
ψ : L →+* ℂ
hψ : ComplexEmbedding.LiesOver ψ v.embedding
⊢ ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))

Tactic:
exact ⟨⟨ψ, fun _ ↦ by simp [RingHom.algebraMap_toAlgebra, ← hψ.over]⟩, by simp⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
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
let let₁ let₂ :
  Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
let₃ :
  let this := v.embedding.toAlgebra;
  Finset.card.{u_5} (α := L →+* ℂ)
      (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) =
    Fintype.card.{u_5} (L →ₐ[K] ℂ)
let₄ :
  let this := v.embedding.toAlgebra;
  ∀ (ψ : L →+* ℂ)
    (hψ :
      ψ ∈ (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) : Set (L →+* ℂ))),
    ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
let₅ :
  let this := v.embedding.toAlgebra;
  ∀ (ψ : L →+* ℂ) (hψ : ComplexEmbedding.LiesOver ψ v.embedding), ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L

Tactic:
classical
  let : Algebra K ℂ := v.embedding.toAlgebra
  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]
  apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm
  simp only [Set.Finite.toFinset_setOf, coe_filter, mem_univ, true_and, Set.mem_setOf_eq] at hψ
  exact ⟨⟨ψ, fun _ ↦ by simp [RingHom.algebraMap_toAlgebra, ← hψ.over]⟩, by simp⟩

Premises used: Set.Finite.toFinset_setOf, Finset.mem_univ, AlgHom.coe_ringHom_injective, NumberField.ComplexEmbedding.union_unmixedEmbeddingsOver_mixedEmbeddingsOver, Finset.coe_filter, Function.Injective.injOn, NumberField.InfinitePlace.ramifiedPlacesOver_ncard, Set.ncard_union_eq, NumberField.ComplexEmbedding.disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver, Set.mem_setOf_eq, NumberField.InfinitePlace.embedding, AlgHom.toRingHom, Set.ncard_eq_toFinset_card, Finset.card_nbij, Eq.symm, NumberField.InfinitePlace.unramifiedPlacesOver_ncard, true_and
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
⊢ nrComplexPlaces K = 0 ↔ IsTotallyReal K

Tactic:
simp [Fintype.card_eq_zero_iff, isEmpty_subtype, isTotallyReal_iff]

Premises used: NumberField.isTotallyReal_iff, Fintype.card_eq_zero_iff, isEmpty_subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : IsTotallyReal K
φ : K →+* ℂ
⊢ ComplexEmbedding.IsReal φ

Tactic:
isReal_mk_iff.mp <| isReal (InfinitePlace.mk φ)

Premises used: NumberField.InfinitePlace.mk, NumberField.InfinitePlace.isReal_mk_iff, Iff.mp, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : IsTotallyReal K
w : InfinitePlace K
⊢ w.mult = 1

Tactic:
mult_isReal ⟨w, isReal w⟩

Premises used: Subtype.mk, NumberField.InfinitePlace.mult_isReal, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
inst_3 : Algebra F K
inst_4 : Algebra.IsAlgebraic F K
w : InfinitePlace F
⊢ ∃ (W : InfinitePlace K), W.comap (algebraMap F K) = w

Tactic:
comap_surjective w

Premises used: NumberField.InfinitePlace.comap_surjective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
inst_3 : Algebra F K
inst_4 : Algebra.IsAlgebraic F K
w : InfinitePlace F
obtain : ∀ (W : InfinitePlace K), IsReal (W.comap (algebraMap F K))
⊢ w.IsReal

Tactic:
obtain ⟨W, rfl⟩ : ∃ W : InfinitePlace K, W.comap (algebraMap F K) = w := comap_surjective w

Premises used: NumberField.InfinitePlace, NumberField.InfinitePlace.comap_surjective, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
inst_3 : Algebra F K
inst_4 : Algebra.IsAlgebraic F K
W : InfinitePlace K
⊢ IsReal (W.comap (algebraMap F K))

Tactic:
IsReal.comap _ (IsTotallyReal.isReal W)

Premises used: NumberField.InfinitePlace.IsReal.comap, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
inst_3 : Algebra F K
inst_4 : Algebra.IsAlgebraic F K
W : InfinitePlace K
⊢ IsReal (W.comap (algebraMap F K))

Tactic:
exact IsReal.comap _ (IsTotallyReal.isReal W)

Premises used: NumberField.InfinitePlace.IsReal.comap, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
f : F ≃+* K
⊢ IsTotallyReal F ↔ IsTotallyReal K

Tactic:
⟨fun _ ↦ .ofRingEquiv f, fun _ ↦ .ofRingEquiv f.symm⟩

Premises used: Iff.intro, NumberField.IsTotallyReal.ofRingEquiv, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
⊢ IsTotallyReal.{u_2} ↥⊤ ↔ IsTotallyReal K

Tactic:
isTotallyReal_iff_ofRingEquiv Subfield.topEquiv

Premises used: NumberField.isTotallyReal_iff_ofRingEquiv, Subfield.topEquiv
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F_1 : Type u_1
inst : Field F_1
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
inst_3 : CharZero K
F : IntermediateField ℚ K
inst_4 : Algebra.IsAlgebraic (↥F) K
⊢ IsTotallyReal.{u_2} ↥F

Tactic:
IsTotallyReal.of_algebra F K

Premises used: NumberField.IsTotallyReal.of_algebra, Membership.mem, Subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F_1 : Type u_1
inst : Field F_1
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
F : Subfield K
inst_3 : Algebra.IsAlgebraic (↥F) K
⊢ IsTotallyReal.{u_2} ↥F

Tactic:
IsTotallyReal.of_algebra F K

Premises used: NumberField.IsTotallyReal.of_algebra, Membership.mem, Subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyReal K
⊢ nrComplexPlaces K = 0

Tactic:
nrComplexPlaces_eq_zero_iff.mpr h

Premises used: Iff.mpr, NumberField.nrComplexPlaces_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyReal K
rw : nrRealPlaces K + 2 * nrComplexPlaces K = nrRealPlaces K
rw₁ : nrRealPlaces K + HMul.hMul (α := ℕ) 2 0 = nrRealPlaces K
rw₂ : nrRealPlaces K + 0 = nrRealPlaces K
rw₃ rw₄ : nrRealPlaces K = nrRealPlaces K
⊢ finrank ℚ K = nrRealPlaces K

Tactic:
rw [← card_add_two_mul_card_eq_rank, nrComplexPlaces_eq_zero_iff.mpr h, mul_zero, add_zero]

Premises used: Iff.mpr, MulZeroClass.mul_zero, NumberField.nrComplexPlaces_eq_zero_iff, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank, add_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
v : InfinitePlace ℚ
rw : Rat.infinitePlace.IsReal
⊢ v.IsReal

Tactic:
rw [Subsingleton.elim v Rat.infinitePlace]

Premises used: Rat.infinitePlace, Subsingleton.elim
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
v : InfinitePlace ℚ
⊢ Rat.infinitePlace.IsReal

Tactic:
Rat.isReal_infinitePlace

Premises used: Rat.isReal_infinitePlace
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
v : InfinitePlace ℚ
⊢ Rat.infinitePlace.IsReal

Tactic:
exact Rat.isReal_infinitePlace

Premises used: Rat.isReal_infinitePlace