awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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)) ⋯)
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))
⊢ DenseRange (X := adicCompletion L w) (α := adicCompletion K v ⊗[K] L)
    (⇑Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w)

Tactic:
apply (w.denseRange_algebraMap L).mono

Premises used: IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, Dense.mono
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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)) ⋯)
l : L
⊢ Eq.{u_3 + 1} (α := adicCompletion L w)
    ((Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w) (1 ⊗ₜ[K] l) : adicCompletion L w)
    ((algebraMap L (adicCompletion L w) : (a : L) → adicCompletion L w) l : adicCompletion L w)

Tactic:
simp [Φ, Algebra.algHom]

Premises used: Algebra.algHom
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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)) ⋯)
l : L
⊢ Membership.mem (α := adicCompletion L w) (γ := Set (adicCompletion L w))
    (Set.range (ι := adicCompletion K v ⊗[K] L) (⇑Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w))
    ((algebraMap L (adicCompletion L w) : (a : L) → adicCompletion L w) l : adicCompletion L w)

Tactic:
exact ⟨1 ⊗ₜ l, by simp [Φ, Algebra.algHom]⟩
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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)
rw : closure (↑Φ.range : Set (adicCompletion L w)) = Set.univ
⊢ Function.Surjective (α := adicCompletion K v ⊗[K] L) (β := adicCompletion L w)
    (⇑Φ : (a : adicCompletion K v ⊗[K] L) → adicCompletion L w)

Tactic:
rw [← Set.range_eq_univ, ← Φ.coe_range, ← Φ.range.closed_of_finiteDimensional.closure_eq]

Premises used: Set.range_eq_univ, Submodule.closed_of_finiteDimensional, IsClosed.closure_eq, LinearMap.range, LinearMap.coe_range
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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)
⊢ closure (↑Φ.range : Set (adicCompletion L w)) = Set.univ

Tactic:
h_dense.closure_range

Premises used: setOf, DenseRange.closure_range, Set.range
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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)
⊢ closure (↑Φ.range : Set (adicCompletion L w)) = Set.univ

Tactic:
exact h_dense.closure_range

Premises used: DenseRange.closure_range
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
x : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ norm (E := ℂ)
      ((v.embedding.comp (WithAbs.equiv (↑v : AbsoluteValue K ℝ)).toRingHom :
            (a : WithAbs (↑v : AbsoluteValue K ℝ)) → ℂ)
          x :
        ℂ) =
    ‖x‖

Tactic:
simpa using v.norm_embedding_eq (WithAbs.equiv v.1 x)

Premises used: NumberField.InfinitePlace.norm_embedding_eq, WithAbs.equiv, Subtype.val, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ norm (E := ℝ)
      (((embedding_of_isReal hv).comp (WithAbs.equiv (↑v : AbsoluteValue K ℝ)).toRingHom :
            (a : WithAbs (↑v : AbsoluteValue K ℝ)) → ℝ)
          x :
        ℝ) =
    ‖x‖

Tactic:
simpa using v.norm_embedding_of_isReal hv (WithAbs.equiv v.1 x)

Premises used: NumberField.InfinitePlace.norm_embedding_of_isReal, WithAbs.equiv, Subtype.val, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
x : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ norm (E := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
      (↑x : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) =
    (v : (a : K) → ℝ) ((WithAbs.equiv (↑v : AbsoluteValue K ℝ) : (a : WithAbs (↑v : AbsoluteValue K ℝ)) → K) x : K)

Tactic:
UniformSpace.Completion.norm_coe x

Premises used: UniformSpace.Completion.norm_coe
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
⊢ CompletableTopField.{u_1} (WithAbs (↑v : AbsoluteValue K ℝ))

Tactic:
v.isometry_embedding.isUniformInducing.completableTopField

Premises used: NumberField.InfinitePlace.isometry_embedding, IsUniformInducing.completableTopField, Isometry.isUniformInducing
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
⊢ IsTopologicalRing.{u_1} v.Completion

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
v : InfinitePlace ℚ
x : WithAbs (↑v : AbsoluteValue ℚ ℝ)
⊢ Eq (α := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ)))
    (↑((WithAbs.equiv (↑v : AbsoluteValue ℚ ℝ) : (a : WithAbs (↑v : AbsoluteValue ℚ ℝ)) → ℚ) x) :
      UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ)))
    (↑x : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue ℚ ℝ)))

Tactic:
(eq_ratCast (UniformSpace.Completion.coeRingHom.comp
    (WithAbs.equiv v.1).symm.toRingHom) _).symm

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.coeRingHom, WithAbs.equiv, RingHom.comp, SeparationQuotient.mk, RingEquiv.toRingHom, eq_ratCast, Eq.symm, Subtype.val, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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| : ℝ) : ℝ)
rw₄ rw₅ : Eq (α := ℝ) (↑|x| : ℝ) (↑|x| : ℝ)
⊢ norm (E := v.Completion) (↑x : v.Completion) = (↑|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]

Premises used: RingEquiv.apply_symm_apply, NumberField.InfinitePlace.Completion.norm_coe, WithAbs.equiv, Rat.infinitePlace_apply, NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
⊢ LocallyCompactSpace.{u_1} v.Completion

Tactic:
AbsoluteValue.Completion.locallyCompactSpace v.isometry_embedding

Premises used: NumberField.InfinitePlace.isometry_embedding, AbsoluteValue.Completion.locallyCompactSpace
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
x : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ Eq (α := ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) (↑x : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
    ((v.embedding : (a : K) → ℂ)
        ((WithAbs.equiv (↑v : AbsoluteValue K ℝ) : (a : WithAbs (↑v : AbsoluteValue K ℝ)) → K) x : K) :
      ℂ)

Tactic:
v.isometry_embedding.extensionHom_coe _

Premises used: Isometry.extensionHom_coe, NumberField.InfinitePlace.isometry_embedding
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ Eq (α := ℝ)
    ((extensionEmbeddingOfIsReal hv : (a : v.Completion) → ℝ)
        (↑x : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℝ)
    ((embedding_of_isReal hv : (a : K) → ℝ)
        ((WithAbs.equiv (↑v : AbsoluteValue K ℝ) : (a : WithAbs (↑v : AbsoluteValue K ℝ)) → K) x : K) :
      ℝ)

Tactic:
(v.isometry_embedding_of_isReal hv).extensionHom_coe _

Premises used: Isometry.extensionHom_coe, NumberField.InfinitePlace.isometry_embedding_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : v.Completion
⊢ ∀ (a : WithAbs (↑v : AbsoluteValue K ℝ)),
    (↑((extensionEmbeddingOfIsReal hv : (a : v.Completion) → ℝ)
            (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))) :
        ℂ) =
      (extensionEmbedding v : (a : v.Completion) → ℂ) (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : v.Completion
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}
⊢ (↑((extensionEmbeddingOfIsReal hv : (a : v.Completion) → ℝ) x) : ℂ) =
    (extensionEmbedding v : (a : v.Completion) → ℂ) x

Tactic:
refine UniformSpace.Completion.induction_on x ?_ (by simp)
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : v.Completion
⊢ Continuous Complex.ofReal

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : v.Completion
⊢ 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:
exact isClosed_eq (Continuous.comp' (by fun_prop) continuous_extension) continuous_extension

Premises used: Continuous.comp', isClosed_eq, UniformSpace.Completion.continuous_extension
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
⊢ Isometry (α := v.Completion) (β := ℂ) (⇑(extensionEmbedding v) : (a : v.Completion) → ℂ)

Tactic:
v.isometry_embedding.completion_extension

Premises used: NumberField.InfinitePlace.isometry_embedding, Set.Mem, setOf, Isometry.completion_extension, UniformSpace.Completion.extension, AbstractCompletion.extend, ite
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ Isometry (α := v.Completion) (β := ℝ) (⇑(extensionEmbeddingOfIsReal hv) : (a : v.Completion) → ℝ)

Tactic:
(v.isometry_embedding_of_isReal hv).completion_extension

Premises used: Set.Mem, setOf, Isometry.completion_extension, NumberField.InfinitePlace.isometry_embedding_of_isReal, UniformSpace.Completion.extension, AbstractCompletion.extend, ite
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
⊢ IsClosed (X := ℂ) (Set.range (ι := v.Completion) (⇑(extensionEmbedding v) : (a : v.Completion) → ℂ))

Tactic:
v.isometry_embedding.completion_extension.isClosedEmbedding.isClosed_range

Premises used: NumberField.InfinitePlace.isometry_embedding, Isometry.completion_extension, UniformSpace.Completion.extension, Isometry.isClosedEmbedding, AbstractCompletion.extend, Topology.IsClosedEmbedding.isClosed_range, ite
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed (X := ℝ) (Set.range (ι := v.Completion) (⇑(extensionEmbeddingOfIsReal hv) : (a : v.Completion) → ℝ))

Tactic:
(v.isometry_embedding_of_isReal hv).completion_extension.isClosedEmbedding.isClosed_range

Premises used: Isometry.completion_extension, NumberField.InfinitePlace.isometry_embedding_of_isReal, UniformSpace.Completion.extension, Isometry.isClosedEmbedding, AbstractCompletion.extend, Topology.IsClosedEmbedding.isClosed_range, ite
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
contrapose : ∀ (hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange), ¬v.IsComplex
⊢ (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange

Tactic:
contrapose hv
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
simp : ComplexEmbedding.IsReal v.embedding
⊢ ¬v.IsComplex

Tactic:
simp only [not_isComplex_iff_isReal, isReal_iff]

Premises used: NumberField.InfinitePlace.not_isComplex_iff_isReal, NumberField.InfinitePlace.isReal_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
a : ∀ (x : K), Eq (α := ℂ) ((star v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
⊢ ComplexEmbedding.IsReal v.embedding

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
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 : ℂ)
⊢ 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)
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (α := ℂ) ((Complex.ofRealHom : (a : ℝ) → ℂ) r : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)

Tactic:
rw [extensionEmbedding_coe, ← WithAbs.equiv_symm_apply, RingEquiv.apply_symm_apply] at hr

Premises used: RingEquiv.apply_symm_apply, NumberField.InfinitePlace.Completion.extensionEmbedding_coe, WithAbs.equiv_symm_apply
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)
⊢ Eq (α := ℂ) ((star v.embedding : (a : K) → ℂ) x : ℂ) ((v.embedding : (a : K) → ℂ) x : ℂ)

Tactic:
simp [ComplexEmbedding.conjugate_coe_eq, ← hr, Complex.conj_ofReal]

Premises used: Complex.conj_ofReal, NumberField.ComplexEmbedding.conjugate_coe_eq
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
rw : (extensionEmbedding v).fieldRange = ⊤
⊢ Function.Surjective (α := v.Completion) (β := ℂ) (⇑(extensionEmbedding v) : (a : v.Completion) → ℂ)

Tactic:
rw [← RingHom.fieldRange_eq_top_iff]

Premises used: RingHom.fieldRange_eq_top_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤

Tactic:
(Complex.subfield_eq_of_closed <| isClosed_image_extensionEmbedding v).resolve_left <|
    subfield_ne_real_of_isComplex hv

Premises used: Or.resolve_left, NumberField.InfinitePlace.Completion.subfield_ne_real_of_isComplex, Complex.subfield_eq_of_closed
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤

Tactic:
exact (Complex.subfield_eq_of_closed <| isClosed_image_extensionEmbedding v).resolve_left <|
    subfield_ne_real_of_isComplex hv

Premises used: Or.resolve_left, NumberField.InfinitePlace.Completion.subfield_ne_real_of_isComplex, Complex.subfield_eq_of_closed
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ Function.Bijective (α := v.Completion) (β := ℂ) (⇑(extensionEmbedding v) : (a : v.Completion) → ℂ)

Tactic:
⟨(extensionEmbedding v).injective, surjective_extensionEmbedding_of_isComplex hv⟩

Premises used: NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isComplex, RingHom.injective, And.intro, NumberField.InfinitePlace.Completion.extensionEmbedding, Function.Bijective
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsComplex
x : v.Completion
⊢ Eq (α := ℂ) ((ringEquivComplexOfIsComplex hv : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)

Tactic:
rfl

Premises used: UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, ite