awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
rw : IsClosed (↑(extensionEmbeddingOfIsReal hv).fieldRange : Set ℝ)
⊢ Function.Surjective (α := v.Completion) (β := ℝ) (⇑(extensionEmbeddingOfIsReal hv) : (a : v.Completion) → ℝ)

Tactic:
rw [← RingHom.fieldRange_eq_top_iff, ← Real.subfield_eq_of_closed]

Premises used: RingHom.fieldRange_eq_top_iff, Real.subfield_eq_of_closed
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed (↑(extensionEmbeddingOfIsReal hv).fieldRange : Set ℝ)

Tactic:
isClosed_image_extensionEmbeddingOfIsReal hv

Premises used: setOf, NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbeddingOfIsReal, Set.range
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed (↑(extensionEmbeddingOfIsReal hv).fieldRange : Set ℝ)

Tactic:
exact isClosed_image_extensionEmbeddingOfIsReal hv

Premises used: NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbeddingOfIsReal
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ Function.Bijective (α := v.Completion) (β := ℝ) (⇑(extensionEmbeddingOfIsReal hv) : (a : v.Completion) → ℝ)

Tactic:
⟨(extensionEmbeddingOfIsReal hv).injective, surjective_extensionEmbeddingOfIsReal hv⟩

Premises used: RingHom.injective, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal, And.intro, Function.Bijective, NumberField.InfinitePlace.Completion.surjective_extensionEmbeddingOfIsReal
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
hv : v.IsReal
x : v.Completion
⊢ Eq (α := ℝ) ((ringEquivRealOfIsReal hv : (a : v.Completion) → ℝ) x : ℝ)
    ((extensionEmbeddingOfIsReal hv : (a : v.Completion) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (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
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (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

Premises used: UniformSpace.Completion.algebraMap_def
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 ℝ)) (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)
⊢ 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 ℝ)))

Tactic:
simp [this, algebraMap_def, Algebra.algebraMap_self]

Premises used: Algebra.algebraMap_self, UniformSpace.Completion.algebraMap_def
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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
a :
  ∀ (x : v.Completion),
    Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
      ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
⊢ (extensionEmbedding w).comp (algebraMap v.Completion w.Completion) = extensionEmbedding v

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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
x : v.Completion
a :
  IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
    {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
      Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a : ℂ)
        ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}
a₁ :
  ∀ (a : WithAbs (↑v : AbsoluteValue K ℝ)),
    Eq (α := ℂ)
      (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
          (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
        ℂ)
      ((extensionEmbedding v : (a : v.Completion) → ℂ)
          (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
        ℂ)
⊢ Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)

Tactic:
induction x using induction_on
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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
⊢ IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
    {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
      Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a : ℂ)
        ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}

Tactic:
isClosed_eq
        (continuous_extension.comp (continuous_algebraMap v.Completion w.Completion))
        continuous_extension

Premises used: Continuous.comp, continuous_algebraMap, NumberField.InfinitePlace.Completion, isClosed_eq, UniformSpace.Completion.continuous_extension
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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
⊢ IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
    {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
      Eq (α := ℂ) (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a : ℂ)
        ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}

Tactic:
exact isClosed_eq
        (continuous_extension.comp (continuous_algebraMap v.Completion w.Completion))
        continuous_extension

Premises used: Continuous.comp, continuous_algebraMap, NumberField.InfinitePlace.Completion, isClosed_eq, UniformSpace.Completion.continuous_extension
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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
a : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ Eq (α := ℂ)
    (((extensionEmbedding w).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)

Tactic:
simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply,
        ← ComplexEmbedding.LiesOver.over w.embedding v.embedding]

Premises used: WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply, NumberField.InfinitePlace.embedding, NumberField.ComplexEmbedding.LiesOver.over
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (conjugate w.embedding) v.embedding
a :
  ∀ (x : v.Completion),
    Eq (α := ℂ)
      (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
      ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)
⊢ (conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) = extensionEmbedding v

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (conjugate w.embedding) v.embedding
x : v.Completion
a :
  IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
    {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
      Eq (α := ℂ)
        (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a :
          ℂ)
        ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}
a₁ :
  ∀ (a : WithAbs (↑v : AbsoluteValue K ℝ)),
    Eq (α := ℂ)
      (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
          (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
        ℂ)
      ((extensionEmbedding v : (a : v.Completion) → ℂ)
          (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
        ℂ)
⊢ Eq (α := ℂ)
    (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) x : ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)

Tactic:
induction x using induction_on
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (conjugate w.embedding) v.embedding
⊢ Continuous (X := ℂ) (Y := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (conjugate w.embedding) v.embedding
⊢ IsClosed.{u_1} (X := UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))
    {a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)) |
      Eq (α := ℂ)
        (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ) a :
          ℂ)
        ((extensionEmbedding v : (a : v.Completion) → ℂ) a : ℂ)}

Tactic:
simpa using isClosed_eq (.comp (by fun_prop)
        (continuous_extension.comp <| continuous_algebraMap v.Completion w.Completion))
        continuous_extension

Premises used: Continuous.comp, continuous_algebraMap, NumberField.InfinitePlace.Completion, isClosed_eq, UniformSpace.Completion.continuous_extension
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 (conjugate w.embedding) v.embedding
a : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ Eq (α := ℂ)
    (((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) (↑a : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      ℂ)

Tactic:
simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply,
        ← ComplexEmbedding.LiesOver.over (conjugate w.embedding) v.embedding]

Premises used: WithAbs.algebraMap_left_apply, NumberField.ComplexEmbedding.conjugate, WithAbs.algebraMap_right_apply, NumberField.InfinitePlace.embedding, NumberField.ComplexEmbedding.LiesOver.over
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
w : InfinitePlace L
v : InfinitePlace K
inst_2 : Algebra.{u_1, u_2} v.Completion w.Completion
φ : w.Completion →+* ℂ
inst_3 : ComplexEmbedding.LiesOver φ (extensionEmbedding v)
x : v.Completion
⊢ Eq (α := ℂ)
    ((φ : (a : w.Completion) → ℂ)
        ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion) x : w.Completion) :
      ℂ)
    ((extensionEmbedding v : (a : v.Completion) → ℂ) x : ℂ)

Tactic:
simp_all [liesOver_iff, RingHom.ext_iff]

Premises used: RingHom.ext_iff, NumberField.ComplexEmbedding.liesOver_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : WithAbs (↑v : AbsoluteValue K ℝ)
⊢ norm.{u_2} (E := WithAbs (↑w : AbsoluteValue L ℝ))
      ((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) (WithAbs (↑w : AbsoluteValue L ℝ)) :
            (a : WithAbs (↑v : AbsoluteValue K ℝ)) → WithAbs (↑w : AbsoluteValue L ℝ))
          x :
        WithAbs (↑w : AbsoluteValue L ℝ)) =
    ‖x‖

Tactic:
simpa [WithAbs.norm_eq_apply_ofAbs] using
      WithAbs.ofAbs_algebraMap v.1 w.1 x ▸ comp_of_comap_eq (comap_eq w v) x.ofAbs

Premises used: WithAbs.norm_eq_apply_ofAbs
-- Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
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 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
inst_4 : Algebra.{u_1, u_2} v.Completion w.Completion
inst_5 : IsScalarTower.{u_1, u_1, u_2} K v.Completion w.Completion
inst_6 : ContinuousSMul.{u_1, u_2} v.Completion w.Completion
h : v.IsReal
⊢ ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)

Tactic:
let := embedding_liesOver_of_isReal w h; liesOver_extensionEmbedding w v

Premises used: NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding, NumberField.InfinitePlace.LiesOver.embedding_liesOver_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
simp_rw :
  Eq.{u_2 + 1} (α := w.Completion)
    ((↑((algebraMap K (WithAbs (↑w : AbsoluteValue L ℝ)) : (a : K) → WithAbs (↑w : AbsoluteValue L ℝ)) x) :
        UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
    ((↑((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) (WithAbs (↑w : AbsoluteValue L ℝ)) :
              (a : WithAbs (↑v : AbsoluteValue K ℝ)) → WithAbs (↑w : AbsoluteValue L ℝ))
            ((algebraMap K (WithAbs (↑v : AbsoluteValue K ℝ)) : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) x)) :
        UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
⊢ Eq.{u_2 + 1} (α := w.Completion) ((algebraMap K w.Completion : (a : K) → w.Completion) x : w.Completion)
    ((algebraMap v.Completion w.Completion : (a : v.Completion) → w.Completion)
        ((algebraMap K v.Completion : (a : K) → v.Completion) x) :
      w.Completion)

Tactic:
simp_rw [RingHom.algebraMap_toAlgebra, UniformSpace.Completion.algebraMap_def,
      Isometry.mapRingHom_coe]

Premises used: UniformSpace.Completion.algebraMap_def, RingHom.algebraMap_toAlgebra, Isometry.mapRingHom_coe
-- Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
x : K
⊢ Eq.{u_2 + 1} (α := w.Completion)
    ((↑((algebraMap K (WithAbs (↑w : AbsoluteValue L ℝ)) : (a : K) → WithAbs (↑w : AbsoluteValue L ℝ)) x) :
        UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))
    ((↑((algebraMap (WithAbs (↑v : AbsoluteValue K ℝ)) (WithAbs (↑w : AbsoluteValue L ℝ)) :
              (a : WithAbs (↑v : AbsoluteValue K ℝ)) → WithAbs (↑w : AbsoluteValue L ℝ))
            ((algebraMap K (WithAbs (↑v : AbsoluteValue K ℝ)) : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) x)) :
        UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ))) :
      UniformSpace.Completion (WithAbs (↑w : AbsoluteValue L ℝ)))

Tactic:
simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply]

Premises used: WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsRamified K w
⊢ w.IsComplex ∧ IsReal (w.comap (algebraMap K L))

Tactic:
have H := NumberField.InfinitePlace.isRamified_iff.mp h
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsRamified K w
H : w.IsComplex ∧ IsReal (w.comap (algebraMap K L))
⊢ w.IsComplex ∧ v.IsReal

Tactic:
rw [NumberField.InfinitePlace.LiesOver.comap_eq w v] at H

Premises used: NumberField.InfinitePlace.LiesOver.comap_eq
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
⊢ ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)

Tactic:
have := LiesOver.extensionEmbedding_liesOver_of_isReal w H.2
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
a :
  ∀ (x : v.Completion),
    Eq (α := ℂ) ((RingHom.comp (algebraMap ℝ ℂ) (ringEquivRealOfIsReal ⋯).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
      (((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
          x :
        ℂ)
⊢ RingHom.comp (algebraMap ℝ ℂ) (ringEquivRealOfIsReal ⋯).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x : v.Completion
⊢ Eq (α := ℂ) ((RingHom.comp (algebraMap ℝ ℂ) (ringEquivRealOfIsReal ⋯).toRingHom : (a : v.Completion) → ℂ) x : ℂ)
    (((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion) : (a : v.Completion) → ℂ)
        x :
      ℂ)

Tactic:
simp