awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
this : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ (mk φ).embedding = φ
have rwa : ∀ (this : (mk φ).embedding = φ ∨ (mk φ).embedding = φ), (mk φ).embedding = φ
Tactic: rwa [ComplexEmbedding.isReal_iff.mp h, or_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
this : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
rwa : ∀ (this : (mk φ).embedding = φ ∨ (mk φ).embedding = φ), (mk φ).embedding = φ
⊢ (mk φ).embedding = φ
have rwa₁ : ∀ (this : (mk φ).embedding = φ), (mk φ).embedding = φ
Tactic: rwa [ComplexEmbedding.isReal_iff.mp h, or_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.IsReal ↔ ComplexEmbedding.IsReal w.embedding
have refine : w.IsReal → ComplexEmbedding.IsReal w.embedding
Tactic: refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding
have refine : w.IsComplex → ¬ComplexEmbedding.IsReal w.embedding
Tactic: refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding
have contrapose : ∀ (hφ : ComplexEmbedding.IsReal (mk φ).embedding), ComplexEmbedding.IsReal φ
Tactic: contrapose hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : (mk φ).embedding = φ
⊢ ComplexEmbedding.IsReal φ
have inl : ∀ (hφ : ComplexEmbedding.IsReal φ) (h : (mk φ).embedding = φ), ComplexEmbedding.IsReal φ
Tactic: rwa [h] at hφ
Cleared hypotheses: hφ, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : ComplexEmbedding.conjugate (mk φ).embedding = φ
⊢ ComplexEmbedding.IsReal φ
have inr : ∀ (hφ : ComplexEmbedding.IsReal (ComplexEmbedding.conjugate (mk φ).embedding))
  (h : ComplexEmbedding.conjugate (mk φ).embedding = φ), ComplexEmbedding.IsReal φ
Tactic: rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
Cleared hypotheses: hφ, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : ComplexEmbedding.conjugate (mk φ).embedding = φ
inr :
  ∀ (hφ : ComplexEmbedding.IsReal (ComplexEmbedding.conjugate (mk φ).embedding))
    (h : ComplexEmbedding.conjugate (mk φ).embedding = φ), ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal φ
have inr₁ : ∀ (hφ : ComplexEmbedding.IsReal φ) (h : ComplexEmbedding.conjugate (mk φ).embedding = φ), ComplexEmbedding.IsReal φ
Tactic: rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
Cleared hypotheses: hφ, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
⊢ ComplexEmbedding.IsReal φ
have x : (mk φ).embedding = φ ∨ ComplexEmbedding.conjugate (mk φ).embedding = φ
Tactic: cases mk_eq_iff.mp (mk_embedding (mk φ)) with
  | inl h => rwa [h] at hφ
  | inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ ¬w.IsReal ↔ w.IsComplex
have rw : ¬w.IsReal ↔ ¬ComplexEmbedding.IsReal w.embedding
Tactic: rw [isComplex_iff, isReal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
rw : ¬w.IsReal ↔ ¬ComplexEmbedding.IsReal w.embedding
⊢ ¬w.IsReal ↔ w.IsComplex
have rw₁ : ¬ComplexEmbedding.IsReal w.embedding ↔ ¬ComplexEmbedding.IsReal w.embedding
Tactic: rw [isComplex_iff, isReal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ ¬w.IsComplex ↔ w.IsReal
have rw : ¬¬ComplexEmbedding.IsReal w.embedding ↔ w.IsReal
Tactic: rw [isComplex_iff, isReal_iff, not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
rw : ¬¬ComplexEmbedding.IsReal w.embedding ↔ w.IsReal
⊢ ¬w.IsComplex ↔ w.IsReal
have rw₁ : ¬¬ComplexEmbedding.IsReal w.embedding ↔ ComplexEmbedding.IsReal w.embedding
Tactic: rw [isComplex_iff, isReal_iff, not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
rw : ¬¬ComplexEmbedding.IsReal w.embedding ↔ w.IsReal
rw₁ : ¬¬ComplexEmbedding.IsReal w.embedding ↔ ComplexEmbedding.IsReal w.embedding
⊢ ¬w.IsComplex ↔ w.IsReal
have rw₂ : ComplexEmbedding.IsReal w.embedding ↔ ComplexEmbedding.IsReal w.embedding
Tactic: rw [isComplex_iff, isReal_iff, not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ w.IsComplex
have rw : w.IsReal ∨ ¬w.IsReal
Tactic: rw [← not_isReal_iff_isComplex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
⊢ norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = (w : (a : K) → ℝ) x
have rw : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ)
Tactic: rw [← norm_embedding_eq, ← embedding_of_isReal_apply hw, Complex.norm_real]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
rw : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ)
⊢ norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = (w : (a : K) → ℝ) x
have rw₁ : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = ‖(↑((embedding_of_isReal hw : (a : K) → ℝ) x) : ℂ)‖
Tactic: rw [← norm_embedding_eq, ← embedding_of_isReal_apply hw, Complex.norm_real]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
rw : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ)
rw₁ : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = ‖(↑((embedding_of_isReal hw : (a : K) → ℝ) x) : ℂ)‖
⊢ norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) = (w : (a : K) → ℝ) x
have rw₂ : norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ) =
  norm (E := ℝ) ((embedding_of_isReal hw : (a : K) → ℝ) x : ℝ)
Tactic: rw [← norm_embedding_eq, ← embedding_of_isReal_apply hw, Complex.norm_real]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : (mk φ).IsReal
⊢ ComplexEmbedding.IsReal φ
have contrapose : ∀ (h : ¬ComplexEmbedding.IsReal φ), ¬(mk φ).IsReal
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ ¬(mk φ).IsReal
have rw : (mk φ).IsComplex
Tactic: rw [not_isReal_iff_isComplex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsReal }
⊢ (↑w : InfinitePlace K).mult = 1
have rw : Eq (α := ℕ) (if (↑w : InfinitePlace K).IsReal then 1 else 2) 1
Tactic: rw [mult, if_pos w.prop]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsReal }
rw : Eq (α := ℕ) (if (↑w : InfinitePlace K).IsReal then 1 else 2) 1
⊢ (↑w : InfinitePlace K).mult = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [mult, if_pos w.prop]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsComplex }
⊢ (↑w : InfinitePlace K).mult = 2
have rw : Eq (α := ℕ) (if (↑w : InfinitePlace K).IsReal then 1 else 2) 2
Tactic: rw [mult, if_neg (not_isReal_iff_isComplex.mpr w.prop)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : { w : InfinitePlace K // w.IsComplex }
rw : Eq (α := ℕ) (if (↑w : InfinitePlace K).IsReal then 1 else 2) 2
⊢ (↑w : InfinitePlace K).mult = 2
have rw₁ : Eq (α := ℕ) 2 2
Tactic: rw [mult, if_neg (not_isReal_iff_isComplex.mpr w.prop)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ LT.lt (α := ℕ) 0 (if w.IsReal then 1 else 2)
have pos : w.IsReal → LT.lt (α := ℕ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
pos : w.IsReal → LT.lt (α := ℕ) 0 1
⊢ LT.lt (α := ℕ) 0 (if w.IsReal then 1 else 2)
have neg : ¬w.IsReal → LT.lt (α := ℕ) 0 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ LE.le (α := ℝ) 1 (↑w.mult : ℝ)
have rw : 1 ≤ w.mult
Tactic: rw [← Nat.cast_one, Nat.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
| Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}
have s : {φ : K →+* ℂ | mk φ = w}
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
| {φ : K →+* ℂ | mk φ = w}
have s : fun (φ : K →+* ℂ) ↦ mk φ = w
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : fun (φ : K →+* ℂ) ↦ mk φ = w
| {φ : K →+* ℂ | mk φ = w}
have s₁ : Finset.univ
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : fun (φ : K →+* ℂ) ↦ mk φ = w
s₁ : Finset.univ
| {φ : K →+* ℂ | mk φ = w}
have congr : DecidablePred fun (x : K →+* ℂ) ↦ x = w.embedding ∨ x = star w.embedding
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
| fun (φ : K →+* ℂ) ↦ mk φ = w
have s : ∀ (x : K →+* ℂ), mk x = w
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
x : K →+* ℂ
| mk x = w
have s : x = w.embedding ∨ x = star w.embedding
Tactic: rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
| Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}
have s : ∀ (x : K →+* ℂ), x = w.embedding ∨ x = star w.embedding
Tactic: congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : ∀ (x : K →+* ℂ), x = w.embedding ∨ x = star w.embedding
| Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}
have s₁ : Finset.univ
Tactic: congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
s : ∀ (x : K →+* ℂ), x = w.embedding ∨ x = star w.embedding
s₁ : Finset.univ
| Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w}
have rw : DecidablePred fun (x : K →+* ℂ) ↦ x = w.embedding ∨ x = star w.embedding
Tactic: congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
⊢ Finset.card.{u_1} (α := K →+* ℂ) {φ : K →+* ℂ | mk φ = w} = w.mult
have conv_lhs : Finset.card.{u_1} (α := K →+* ℂ) {x : K →+* ℂ | x = w.embedding ∨ x = star w.embedding} = w.mult
Tactic: conv_lhs =>
    congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
⊢ Finset.card.{u_1} (α := K →+* ℂ) {x : K →+* ℂ | x = w.embedding ∨ x = star w.embedding} = w.mult
have simp_rw : Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = if w.IsReal then 1 else 2
Tactic: simp_rw [Finset.filter_or, Finset.filter_eq' _ (embedding w),
    Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)),
    Finset.mem_univ, ite_true, mult]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = if w.IsReal then 1 else 2
have pos : ∀ (hw : w.IsReal), Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
pos : ∀ (hw : w.IsReal), Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = if w.IsReal then 1 else 2
have neg : ∀ (hw : ¬w.IsReal), Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1
have pos : Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {w.embedding}) = 1
Tactic: rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
      Finset.card_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
pos : Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {w.embedding}) = 1
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1
have pos₁ : Finset.card (α := K →+* ℂ) {w.embedding} = 1
Tactic: rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
      Finset.card_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
pos : Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {w.embedding}) = 1
pos₁ : Finset.card (α := K →+* ℂ) {w.embedding} = 1
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1
have pos₂ : Eq (α := ℕ) 1 1
Tactic: rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
      Finset.card_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ Finset.card (α := K →+* ℂ) ({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2
have neg : w.embedding ≠ ComplexEmbedding.conjugate w.embedding
Tactic: refine Finset.card_pair ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ w.embedding ≠ ComplexEmbedding.conjugate w.embedding
have neg : ¬w.embedding = ComplexEmbedding.conjugate w.embedding
Tactic: rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
neg : ¬w.embedding = ComplexEmbedding.conjugate w.embedding
⊢ w.embedding ≠ ComplexEmbedding.conjugate w.embedding
have neg₁ : ¬ComplexEmbedding.conjugate w.embedding = w.embedding
Tactic: rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
neg : ¬w.embedding = ComplexEmbedding.conjugate w.embedding
neg₁ : ¬ComplexEmbedding.conjugate w.embedding = w.embedding
⊢ w.embedding ≠ ComplexEmbedding.conjugate w.embedding
have neg₂ : ¬ComplexEmbedding.IsReal w.embedding
Tactic: rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
α : Type u_2
inst_1 : CommMonoid α
inst_2 : NumberField K
f : InfinitePlace K → α
⊢ ∏ w : InfinitePlace K, f w =
    HMul.hMul (α := α) (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K))
      (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K))
have rw : ∏ w : InfinitePlace K, f w =
  HMul.hMul (α := α) (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K))
    (∏ i : { x : InfinitePlace K // ¬x.IsReal },
      f
        (↑((Equiv.subtypeEquivRight (p := fun (x : InfinitePlace K) ↦ ¬x.IsReal) (q := fun (x : InfinitePlace K) ↦
                  x.IsComplex) sorry :
                (a : { x : InfinitePlace K // ¬x.IsReal }) → { x : InfinitePlace K // x.IsComplex })
              i) :
          InfinitePlace K))
Tactic: rw [← Equiv.prod_comp (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ∑ w : InfinitePlace K, w.mult = finrank ℚ K
have rw : Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ j : InfinitePlace K, ∑ i : K →+* ℂ with mk i = j, 1)
Tactic: rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
⊢ x.mult = ∑ i : K →+* ℂ with mk i = x, 1
have rw : x.mult = HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}) 1
Tactic: rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
rw : x.mult = HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}) 1
⊢ x.mult = ∑ i : K →+* ℂ with mk i = x, 1
have rw₁ : x.mult = Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x} * 1
Tactic: rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
rw : x.mult = HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}) 1
rw₁ : x.mult = Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x} * 1
⊢ x.mult = ∑ i : K →+* ℂ with mk i = x, 1
have rw₂ : x.mult = Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}
Tactic: rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
rw : x.mult = HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}) 1
rw₁ : x.mult = Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x} * 1
rw₂ : x.mult = Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x}
⊢ x.mult = ∑ i : K →+* ℂ with mk i = x, 1
have rw₃ : x.mult = x.mult
Tactic: rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ∑ w : InfinitePlace K, w.mult = finrank ℚ K
have rw : ∑ w : InfinitePlace K, w.mult = card.{u_1} (K →+* ℂ)
Tactic: classical
  rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : ∑ w : InfinitePlace K, w.mult = card.{u_1} (K →+* ℂ)
⊢ ∑ w : InfinitePlace K, w.mult = finrank ℚ K
have rw₁ : ∑ w : InfinitePlace K, w.mult = Finset.card.{u_1} (α := K →+* ℂ) Finset.univ
Tactic: classical
  rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : ∑ w : InfinitePlace K, w.mult = card.{u_1} (K →+* ℂ)
rw₁ : ∑ w : InfinitePlace K, w.mult = Finset.card.{u_1} (α := K →+* ℂ) Finset.univ
⊢ ∑ w : InfinitePlace K, w.mult = finrank ℚ K
have rw₂ : Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ x : K →+* ℂ, 1)
Tactic: classical
  rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : ∑ w : InfinitePlace K, w.mult = card.{u_1} (K →+* ℂ)
rw₁ : ∑ w : InfinitePlace K, w.mult = Finset.card.{u_1} (α := K →+* ℂ) Finset.univ
rw₂ : Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ x : K →+* ℂ, 1)
⊢ ∑ w : InfinitePlace K, w.mult = finrank ℚ K
have rw₃ : Eq (α := ℕ) (∑ w : InfinitePlace K, w.mult) (∑ j : InfinitePlace K, ∑ i : K →+* ℂ with mk i = j, 1)
Tactic: classical
  rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])