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 →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // w.IsReal }
have refine_1 : ∀ (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }), (mk (↑φ : K →+* ℂ)).IsReal
Tactic: refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
refine_1 : ∀ (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }), (mk (↑φ : K →+* ℂ)).IsReal
⊢ { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // w.IsReal }
have refine_2 : ∀ (φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ })
  (h :
    Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
      ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) sorry :
            { w : InfinitePlace K // w.IsReal }))
        φ)
      ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) sorry :
            { w : InfinitePlace K // w.IsReal }))
        ψ)),
  φ = ψ
Tactic: refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
refine_1 : ∀ (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }), (mk (↑φ : K →+* ℂ)).IsReal
refine_2 :
  ∀ (φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ })
    (h :
      Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
        ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
              { w : InfinitePlace K // w.IsReal }))
          φ)
        ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
              { w : InfinitePlace K // w.IsReal }))
          ψ)),
    φ = ψ
⊢ { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // w.IsReal }
have refine_3 : ∀ (w : { w : InfinitePlace K // w.IsReal }),
  ∃ (a : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }),
    (fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) sorry :
            { w : InfinitePlace K // w.IsReal }))
        a =
      w
Tactic: refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
h :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      φ)
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      ψ)
⊢ φ = ψ
have refine_2 : ∀ (h : mk (↑φ : K →+* ℂ) = mk (↑ψ : K →+* ℂ)), φ = ψ
Tactic: rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
h :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      φ)
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      ψ)
refine_2 : ∀ (h : mk (↑φ : K →+* ℂ) = mk (↑ψ : K →+* ℂ)), φ = ψ
⊢ φ = ψ
have refine_2₁ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ ComplexEmbedding.conjugate (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
Tactic: rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
h :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      φ)
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      ψ)
refine_2 : ∀ (h : mk (↑φ : K →+* ℂ) = mk (↑ψ : K →+* ℂ)), φ = ψ
refine_2₁ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ ComplexEmbedding.conjugate (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
⊢ φ = ψ
have refine_2₂ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
Tactic: rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
h :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      φ)
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      ψ)
refine_2 : ∀ (h : mk (↑φ : K →+* ℂ) = mk (↑ψ : K →+* ℂ)), φ = ψ
refine_2₁ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ ComplexEmbedding.conjugate (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
refine_2₂ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
⊢ φ = ψ
have refine_2₃ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
Tactic: rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ ψ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
h :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal })
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      φ)
    ((fun (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) ↦
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (mk (↑φ : K →+* ℂ)) ⋯ :
          { w : InfinitePlace K // w.IsReal }))
      ψ)
refine_2 : ∀ (h : mk (↑φ : K →+* ℂ) = mk (↑ψ : K →+* ℂ)), φ = ψ
refine_2₁ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ ComplexEmbedding.conjugate (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
refine_2₂ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ) ∨ (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
refine_2₃ : ∀ (h : (↑φ : K →+* ℂ) = (↑ψ : K →+* ℂ)), φ = ψ
⊢ φ = ψ
have refine_2₄ : ∀ (h : φ = ψ), φ = ψ
Tactic: rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have h : ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
  norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)
Tactic: convert! (congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
    norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have h₁ : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
  norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
Tactic: convert! (congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
    norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)
have h : Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
  (∏ x_1 : K →+* ℂ, norm (E := ℂ) ((x_1 : (a : K) → ℂ) x : ℂ))
Tactic: rw [norm_prod, ← Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ x_1 : K →+* ℂ, norm (E := ℂ) ((x_1 : (a : K) → ℂ) x : ℂ))
have h : Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
  (∏ j : InfinitePlace K, ∏ i : K →+* ℂ with mk i = j, norm (E := ℂ) ((i : (a : K) → ℂ) x : ℂ))
Tactic: rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
w : InfinitePlace K
φ : K →+* ℂ
hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ
⊢ norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
have rw : norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
Tactic: rw [← (Finset.mem_filter.mp hφ).2, apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
w : InfinitePlace K
φ : K →+* ℂ
hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ
rw : norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
⊢ norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
have rw₁ : norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
Tactic: rw [← (Finset.mem_filter.mp hφ).2, apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ j : InfinitePlace K, ∏ i : K →+* ℂ with mk i = j, norm (E := ℂ) ((i : (a : K) → ℂ) x : ℂ))
have this : ∀ (w : InfinitePlace K) (φ : K →+* ℂ) (hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ),
  norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
Tactic: have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
        ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
this :
  ∀ (w : InfinitePlace K) (φ : K →+* ℂ) (hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ),
    norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ j : InfinitePlace K, ∏ i : K →+* ℂ with mk i = j, norm (E := ℂ) ((i : (a : K) → ℂ) x : ℂ))
have h : Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
  (∏ x_1 : InfinitePlace K, ∏ x_2 : K →+* ℂ with mk x_2 = x_1, (x_1 : (a : K) → ℝ) x)
Tactic: simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, 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 : K
this :
  ∀ (w : InfinitePlace K) (φ : K →+* ℂ) (hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ),
    norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
h :
  Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ x_1 : InfinitePlace K, ∏ x_2 : K →+* ℂ with mk x_2 = x_1, (x_1 : (a : K) → ℝ) x)
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ j : InfinitePlace K, ∏ i : K →+* ℂ with mk i = j, norm (E := ℂ) ((i : (a : K) → ℂ) x : ℂ))
have h₁ : Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
  (∏ x_1 : InfinitePlace K,
    HPow.hPow (α := ℝ) ((x_1 : (a : K) → ℝ) x : ℝ) (Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x_1}))
Tactic: simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, 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 : K
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
have h : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
Tactic: rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
have h₁ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ)| = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
Tactic: rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₁ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ)| = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
have h₂ : norm (E := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
Tactic: rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₁ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ)| = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₂ : norm (E := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
have h₃ : ‖(↑(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ) : ℂ)‖ = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
Tactic: rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₁ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ)| = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₂ : norm (E := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₃ : ‖(↑(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ) : ℂ)‖ = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
have h₄ : norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
Tactic: rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have h : ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
  norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)
Tactic: classical
  convert! (congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm
  · rw [norm_prod, ← Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]
    rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]
    have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
        ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]
    simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]
  · rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
    norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have h₁ : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
  norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
Tactic: classical
  convert! (congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm
  · rw [norm_prod, ← Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]
    rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]
    have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
        ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]
    simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]
  · rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]
-- 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
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ)
⊢ LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ)
have contrapose! : ∀ (this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)),
  LT.lt (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) 1
Tactic: contrapose! this
Cleared hypotheses: this
-- 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
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) 1
have rw : LT.lt (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) w.mult)
  (∏ _x : InfinitePlace K, 1)
Tactic: rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]
-- 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
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
rw :
  LT.lt (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) w.mult)
    (∏ _x : InfinitePlace K, 1)
rw₁ : Type u_1
⊢ LT.lt (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) 1
have rw₂ : Finset (InfinitePlace K)
Tactic: rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]
-- 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
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
⊢ Ne (α := ℕ) (if z.IsReal then 1 else 2) 0
have pos : z.IsReal → Ne (α := ℕ) 1 0
Tactic: split_ifs
-- 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
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
pos : z.IsReal → Ne (α := ℕ) 1 0
⊢ Ne (α := ℕ) (if z.IsReal then 1 else 2) 0
have neg : ¬z.IsReal → Ne (α := ℕ) 2 0
Tactic: split_ifs
-- 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
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
⊢ HPow.hPow (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) z.mult < 1
have refine_2 : LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
Tactic: refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)
-- 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
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
⊢ LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
have pos : ∀ (hz : z = w), LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
Tactic: by_cases hz : z = w