awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
hb_1 : Membership.mem (γ := Submonoid (𝓞 K)) (nonZeroDivisors (𝓞 K)) b
ha : ¬a = 0
hb : ¬b = 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) ((w : (a : K) → ℝ) (↑b : K) : ℝ)
have funProp : a ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
hb_1 : Membership.mem (γ := Submonoid (𝓞 K)) (nonZeroDivisors (𝓞 K)) b
ha : ¬a = 0
hb : ¬b = 0
funProp : a ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) ((w : (a : K) → ℝ) (↑b : K) : ℝ)
have funProp₁ : b ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x y : K
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x + y) : ℝ) (max ((v : (a : K) → ℝ) x) ((v : (a : K) → ℝ) y) : ℝ)
have obtain : ∀ (w : HeightOneSpectrum (𝓞 K)) (hw : place (A := adicCompletion K w) (embedding w) = (↑v : AbsoluteValue K ℝ)),
  LE.le (α := ℝ) ((v : (a : K) → ℝ) (x + y) : ℝ) (max ((v : (a : K) → ℝ) x) ((v : (a : K) → ℝ) y) : ℝ)
Tactic: obtain ⟨w, hw⟩ := v.prop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (A := adicCompletion K w) (embedding w) = (↑v : AbsoluteValue K ℝ)
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x + y) : ℝ) (max ((v : (a : K) → ℝ) x) ((v : (a : K) → ℝ) y) : ℝ)
have H : ∀ (x : K), Eq (α := ℝ) ((v : (a : K) → ℝ) x : ℝ) ((HeightOneSpectrum.adicAbv K w : (a : K) → ℝ) x : ℝ)
Tactic: have H x : v x = NumberField.HeightOneSpectrum.adicAbv K w x := by
    rw [show v x = v.val x from rfl]
    grind only [place_apply, norm_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
| I
have rw : ∏ᶠ (p : HeightOneSpectrum (𝓞 K)), p.asIdeal ^ multiplicity p.asIdeal I
Tactic: rw [← finprod_heightOneSpectrum_pow_multiplicity hI]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
⊢ ∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I
have conv_rhs : Eq.{u_1 + 1} (α := Ideal (𝓞 K)) (∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I)
  (∏ᶠ (p : HeightOneSpectrum (𝓞 K)), p.asIdeal ^ multiplicity p.asIdeal I)
Tactic: conv_rhs => rw [← finprod_heightOneSpectrum_pow_multiplicity hI]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
⊢ HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (↑x : K) : ℝ)
      (HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.maximalIdeal.asIdeal) : ℝ)
        (multiplicity v.maximalIdeal.asIdeal (span {x}))) =
    1
have hnz : Ne (α := Ideal (𝓞 K)) (span {x}) ⊥
Tactic: have hnz : span {x} ≠ ⊥ := mt Submodule.span_singleton_eq_bot.mp hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : Ne (α := Ideal (𝓞 K)) (span {x}) ⊥
⊢ HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (↑x : K) : ℝ)
      (HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.maximalIdeal.asIdeal) : ℝ)
        (multiplicity v.maximalIdeal.asIdeal (span {x}))) =
    1
have rw : norm (E := adicCompletion K v.maximalIdeal)
      ((embedding v.maximalIdeal : (a : K) → adicCompletion K v.maximalIdeal) (↑x : K) :
        adicCompletion K v.maximalIdeal) *
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maximalIdeal.maxPowDividing (span {x}))) : ℝ) =
  1
Tactic: rw [← norm_embedding_eq v x, ← Nat.cast_pow, ← map_pow, ← maxPowDividing_eq_pow_multiplicity hnz]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v_1 : HeightOneSpectrum R
L : Type u_3
inst_5 : NumberField K
inst_6 : Field L
inst_7 : NumberField L
inst_8 : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst_9 : Algebra.{u_1, u_3} (adicCompletion K v) (adicCompletion L w)
inst_10 : ContinuousSMul.{u_1, u_3} (adicCompletion K v) (adicCompletion L w)
inst_11 : IsScalarTower.{u_1, u_1, u_3} K (adicCompletion K v) (adicCompletion L w)
Φ : LinearMap (R := adicCompletion K v) (RingHom.id (adicCompletion K v)) (adicCompletion K v ⊗[K] L)
  (adicCompletion L w) :=
  AlgHom.toLinearMap
    (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯)
⊢ DenseRange (X := adicCompletion L w) (α := adicCompletion K v ⊗[K] L)
    (⇑Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w)
have apply : Subset (α := Set (adicCompletion L w))
  (Set.range (ι := L) (⇑(algebraMap L (adicCompletion L w)) : (a : L) → adicCompletion L w))
  (Set.range (ι := adicCompletion K v ⊗[K] L) (⇑Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w))
Tactic: apply (w.denseRange_algebraMap L).mono
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v_1 : HeightOneSpectrum R
L : Type u_3
inst_5 : NumberField K
inst_6 : Field L
inst_7 : NumberField L
inst_8 : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst_9 : Algebra.{u_1, u_3} (adicCompletion K v) (adicCompletion L w)
inst_10 : ContinuousSMul.{u_1, u_3} (adicCompletion K v) (adicCompletion L w)
inst_11 : IsScalarTower.{u_1, u_1, u_3} K (adicCompletion K v) (adicCompletion L w)
Φ : LinearMap (R := adicCompletion K v) (RingHom.id (adicCompletion K v)) (adicCompletion K v ⊗[K] L)
  (adicCompletion L w) :=
  AlgHom.toLinearMap
    (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯)
h_dense :
  DenseRange (X := adicCompletion L w) (α := adicCompletion K v ⊗[K] L)
    (⇑Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w)
⊢ Function.Surjective (α := adicCompletion K v ⊗[K] L) (β := adicCompletion L w)
    (⇑Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w)
have rw : closure (↑Φ.range : Set (adicCompletion L w)) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← Φ.coe_range, ← Φ.range.closed_of_finiteDimensional.closure_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
v : InfinitePlace ℚ
x : ℚ
⊢ norm (E := v.Completion) (↑x : v.Completion) = (↑|x| : ℝ)
have rw : norm (E := v.Completion)
    (↑((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
          (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
            WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
      v.Completion) =
  (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
          (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
            WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
    ℝ)
Tactic: rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
    norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
v : InfinitePlace ℚ
x : ℚ
rw :
  norm (E := v.Completion)
      (↑((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
        v.Completion) =
    (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ)
⊢ norm (E := v.Completion) (↑x : v.Completion) = (↑|x| : ℝ)
have rw₁ : norm (E := v.Completion)
    ((↑(((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x) :
        UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
      UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) =
  (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
          (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
            WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
    ℝ)
Tactic: rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
    norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
v : InfinitePlace ℚ
x : ℚ
rw :
  norm (E := v.Completion)
      (↑((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
        v.Completion) =
    (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ)
rw₁ :
  norm (E := v.Completion)
      ((↑(((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x) :
          UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
        UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) =
    (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ)
⊢ norm (E := v.Completion) (↑x : v.Completion) = (↑|x| : ℝ)
have rw₂ : Eq (α := ℝ)
  ((v : (a : ℚ) → ℝ)
      ((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
          (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
            WithAbs (↑v : AbsoluteValue ℚ ℝ)) :
        ℚ) :
    ℝ)
  ((↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ) :
    ℝ)
Tactic: rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
    norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
v : InfinitePlace ℚ
x : ℚ
rw :
  norm (E := v.Completion)
      (↑((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
        v.Completion) =
    (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ)
rw₁ :
  norm (E := v.Completion)
      ((↑(((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x) :
          UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
        UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) =
    (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ)
rw₂ :
  Eq (α := ℝ)
    ((v : (a : ℚ) → ℝ)
        ((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ)) :
          ℚ) :
      ℝ)
    ((↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
              (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
                WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
        ℝ) :
      ℝ)
⊢ norm (E := v.Completion) (↑x : v.Completion) = (↑|x| : ℝ)
have rw₃ : Eq (α := ℝ) ((v : (a : ℚ) → ℝ) x : ℝ) ((↑|x| : ℝ) : ℝ)
Tactic: rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
    norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
v : InfinitePlace ℚ
x : ℚ
rw :
  norm (E := v.Completion)
      (↑((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
        v.Completion) =
    (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ)
rw₁ :
  norm (E := v.Completion)
      ((↑(((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x) :
          UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) :
        UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ))) =
    (↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
      ℝ)
rw₂ :
  Eq (α := ℝ)
    ((v : (a : ℚ) → ℝ)
        ((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
            (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
              WithAbs (↑v : AbsoluteValue ℚ ℝ)) :
          ℚ) :
      ℝ)
    ((↑|(WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ)
              (((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ)).symm : (a : ℚ) → WithAbs (↑v : AbsoluteValue ℚ ℝ)) x :
                WithAbs (↑v : AbsoluteValue ℚ ℝ))| :
        ℝ) :
      ℝ)
rw₃ : Eq (α := ℝ) ((v : (a : ℚ) → ℝ) x : ℝ) ((↑|x| : ℝ) : ℝ)
⊢ norm (E := v.Completion) (↑x : v.Completion) = (↑|x| : ℝ)
have rw₄ : Eq (α := ℝ) (↑|x| : ℝ) (↑|x| : ℝ)
Tactic: rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
    norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : v.Completion
⊢ (↑((extensionEmbeddingOfIsReal hv : (a : v.Completion) → ℝ) x) : ℂ) =
    (extensionEmbedding v : (a : v.Completion) → ℂ) x
have refine : IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
  {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
    (↑((extensionEmbeddingOfIsReal hv : (a : v.Completion) → ℝ) a) : ℂ) =
      (extensionEmbedding v : (a : v.Completion) → ℂ) a}
Tactic: refine UniformSpace.Completion.induction_on x ?_ (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange
have contrapose : ∀ (hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange), ¬v.IsComplex
Tactic: contrapose hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
⊢ ¬v.IsComplex
have simp : ComplexEmbedding.IsReal v.embedding
Tactic: simp only [not_isComplex_iff_isReal, isReal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
⊢ ComplexEmbedding.IsReal v.embedding
have a : ∀ (x : K), Eq (α := ℂ) ((star v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
⊢ Eq (α := ℂ) ((star v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
have a : ∀ (r : ℝ)
  (hr :
    Eq (α := ℂ) ((Complex.ofRealHom : (a : ℝ) → ℂ) r : ℂ)
      ((extensionEmbedding v : (a : v.Completion) → ℂ)
          (↑(WithAbs.toAbs (↑v : AbsoluteValue K ℝ) x) : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
        ℂ)),
  Eq (α := ℂ) ((star v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
Tactic: obtain ⟨r, hr⟩ := hv ▸ RingHom.mem_fieldRange_self (extensionEmbedding v) (x : v.Completion)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr :
  Eq (α := ℂ) ((Complex.ofRealHom : (a : ℝ) → ℂ) r : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ)
        (↑(WithAbs.toAbs (↑v : AbsoluteValue K ℝ) x) : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
⊢ Eq (α := ℂ) ((star v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
have hr₁ : Eq (α := ℂ) ((Complex.ofRealHom : (a : ℝ) → ℂ) r : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
Tactic: rw [extensionEmbedding_coe, ← WithAbs.equiv_symm_apply, RingEquiv.apply_symm_apply] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ Function.Surjective (α := v.Completion) (β := ℂ) (⇑(extensionEmbedding v) : (a : v.Completion) → ℂ)
have rw : (extensionEmbedding v).fieldRange = ⊤
Tactic: rw [← RingHom.fieldRange_eq_top_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ Function.Surjective (α := v.Completion) (β := ℝ) (⇑(extensionEmbeddingOfIsReal hv) : (a : v.Completion) → ℝ)
have rw : IsClosed (↑(extensionEmbeddingOfIsReal hv).fieldRange : Set ℝ)
Tactic: rw [← RingHom.fieldRange_eq_top_iff, ← Real.subfield_eq_of_closed]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
x : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ Eq.{u_2 + 1} (α := w.Completion)
    ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion)
        (↑x : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      w.Completion)
    ((↑((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) (WithAbs (↑w : AbsoluteValue L ℝ)) :
              (a : WithAbs (↑v : AbsoluteValue K ℝ)) → WithAbs (↑w : AbsoluteValue L ℝ))
            x) :
        UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
have this : Eq.{u_2 + 1} (α := w.Completion)
  ((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) w.Completion : (a : WithAbs (↑v : AbsoluteValue K ℝ)) → w.Completion)
      x :
    w.Completion)
  ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion)
      ((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) v.Completion :
          (a : WithAbs (↑v : AbsoluteValue K ℝ)) → v.Completion)
        x) :
    w.Completion)
Tactic: have := IsScalarTower.algebraMap_apply (WithAbs v.1) v.Completion w.Completion x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
x : WithAbs (↑v : AbsoluteValue K ℝ)
this :
  Eq.{u_2 + 1} (α := w.Completion)
    ((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) w.Completion :
          (a : WithAbs (↑v : AbsoluteValue K ℝ)) → w.Completion)
        x :
      w.Completion)
    ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion)
        ((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) v.Completion :
            (a : WithAbs (↑v : AbsoluteValue K ℝ)) → v.Completion)
          x) :
      w.Completion)
⊢ Eq.{u_2 + 1} (α := w.Completion)
    ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion)
        (↑x : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      w.Completion)
    ((↑((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) (WithAbs (↑w : AbsoluteValue L ℝ)) :
              (a : WithAbs (↑v : AbsoluteValue K ℝ)) → WithAbs (↑w : AbsoluteValue L ℝ))
            x) :
        UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
have this₁ : Eq.{u_2 + 1} (α := w.Completion)
  ((↑((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) (WithAbs (↑w : AbsoluteValue L ℝ)) :
            (a : WithAbs (↑v : AbsoluteValue K ℝ)) → WithAbs (↑w : AbsoluteValue L ℝ))
          x) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
    UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
  ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion)
      ((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) v.Completion :
          (a : WithAbs (↑v : AbsoluteValue K ℝ)) → v.Completion)
        x) :
    w.Completion)
Tactic: rw [algebraMap_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst_3 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_4 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
inst_5 : ContinuousSMul.{u_1, u_2} v.Completion w.Completion
inst_6 : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ (extensionEmbedding w).comp (algebraMap v.Completion w.Completion) = extensionEmbedding v
have a : ∀ (x : v.Completion),
  Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
Tactic: ext x