awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ Membership.mem (γ := Set ℚ_[p])
    (closure
      (Set.range (ι := WithVal (Rat.padicValuation p))
        (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
          (a : WithVal (Rat.padicValuation p)) → ℚ_[p])))
    x

Tactic:
simpa [-nhds_discrete] using Padic.denseRange_ratCast p _

Premises used: Padic.denseRange_ratCast, nhds_discrete
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : (Rat.padicValuation p).Completion
hp :
  IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {a : Completion (WithVal (Rat.padicValuation p)) |
      IsDenseInducing.extend ⋯ coe'
          ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
              (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
            a) =
        a}
ih :
  ∀ (a : WithVal (Rat.padicValuation p)),
    Eq (α := (Rat.padicValuation p).Completion)
      (IsDenseInducing.extend ⋯ coe'
        ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
            (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
          (↑a : Completion (WithVal (Rat.padicValuation p)))))
      (↑a : Completion (WithVal (Rat.padicValuation p)))
⊢ IsDenseInducing.extend ⋯ coe'
      ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
          (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
        y) =
    y

Tactic:
induction y using induction_on
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ IsOrderedMonoid (Multiplicative ℤ)

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
⊢ CharZero ℚ_[p]

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
⊢ IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
pf₂ :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
⊢ IsTopologicalRing (WithVal (Rat.padicValuation p))

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
pf₂ :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
⊢ IsUniformAddGroup (WithVal (Rat.padicValuation p))

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
pf₂ :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf₃ : IsUniformAddGroup (WithVal (Rat.padicValuation p))
⊢ IsUniformAddGroup ℚ_[p]

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
pf₂ :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf₃ : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf₄ : IsUniformAddGroup ℚ_[p]
⊢ IsTopologicalRing ℚ_[p]

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
pf₂ :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf₃ : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf₄ : IsUniformAddGroup ℚ_[p]
pf₅ : IsTopologicalRing ℚ_[p]
⊢ Continuous (X := WithVal (Rat.padicValuation p)) (Y := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
pf₂ :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf₃ : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf₄ : IsUniformAddGroup ℚ_[p]
pf₅ : IsTopologicalRing ℚ_[p]
pf₆ :
  Continuous (X := WithVal (Rat.padicValuation p)) (Y := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
⊢ CompleteSpace ℚ_[p]

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf₁ : CharZero ℚ_[p]
pf₂ :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf₃ : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf₄ : IsUniformAddGroup ℚ_[p]
pf₅ : IsTopologicalRing ℚ_[p]
pf₆ :
  Continuous (X := WithVal (Rat.padicValuation p)) (Y := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
pf₇ : CompleteSpace ℚ_[p]
⊢ T0Space ℚ_[p]

Tactic:
generalize_proofs _ _ _ H
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf_1 : CharZero ℚ_[p]
pf_2 :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf_3 : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf_4 : IsUniformAddGroup ℚ_[p]
pf_5 : IsTopologicalRing ℚ_[p]
pf_6 :
  Continuous (X := WithVal (Rat.padicValuation p)) (Y := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
pf_7 : CompleteSpace ℚ_[p]
pf_8 : T0Space ℚ_[p]
⊢ IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {a : Completion (WithVal (Rat.padicValuation p)) |
      pf_2.extend coe'
          ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) pf_6 :
              (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
            a) =
        a}

Tactic:
isClosed_eq ?_ continuous_id

Premises used: continuous_id, isClosed_eq
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf_1 : CharZero ℚ_[p]
pf_2 :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf_3 : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf_4 : IsUniformAddGroup ℚ_[p]
pf_5 : IsTopologicalRing ℚ_[p]
pf_6 :
  Continuous (X := WithVal (Rat.padicValuation p)) (Y := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
pf_7 : CompleteSpace ℚ_[p]
pf_8 : T0Space ℚ_[p]
hp :
  Continuous (Y := (Rat.padicValuation p).Completion) fun (a : Completion (WithVal (Rat.padicValuation p))) ↦
    pf_2.extend coe'
      ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) pf_6 :
          (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
        a)
⊢ IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {a : Completion (WithVal (Rat.padicValuation p)) |
      pf_2.extend coe'
          ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) pf_6 :
              (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
            a) =
        a}

Tactic:
refine isClosed_eq ?_ continuous_id

Premises used: continuous_id, isClosed_eq
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf_1 : CharZero ℚ_[p]
pf_2 :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf_3 : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf_4 : IsUniformAddGroup ℚ_[p]
pf_5 : IsTopologicalRing ℚ_[p]
pf_6 :
  Continuous (X := WithVal (Rat.padicValuation p)) (Y := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
pf_7 : CompleteSpace ℚ_[p]
pf_8 : T0Space ℚ_[p]
⊢ Continuous (Y := (Rat.padicValuation p).Completion) fun (a : Completion (WithVal (Rat.padicValuation p))) ↦
    pf_2.extend coe'
      ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) pf_6 :
          (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
        a)

Tactic:
(uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal
        Padic.isDenseInducing_cast_withVal.dense (uniformContinuous_coe _)).continuous.comp
        (continuous_extension)

Premises used: Classical.epsilon, Set.Mem, uniformContinuous_uniformly_extend, Continuous.comp, setOf, UniformContinuous.continuous, IsDenseInducing.dense, UniformSpace.Completion.continuous_extension, UniformSpace.Completion.uniformContinuous_coe, Padic.isUniformInducing_cast_withVal, Filter.lim, Filter.limUnder, IsDenseInducing.extend, Padic.isDenseInducing_cast_withVal
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
pf : IsOrderedMonoid (Multiplicative ℤ)
pf_1 : CharZero ℚ_[p]
pf_2 :
  IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
H : IsTopologicalRing (WithVal (Rat.padicValuation p))
pf_3 : IsUniformAddGroup (WithVal (Rat.padicValuation p))
pf_4 : IsUniformAddGroup ℚ_[p]
pf_5 : IsTopologicalRing ℚ_[p]
pf_6 :
  Continuous (X := WithVal (Rat.padicValuation p)) (Y := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
pf_7 : CompleteSpace ℚ_[p]
pf_8 : T0Space ℚ_[p]
⊢ Continuous (Y := (Rat.padicValuation p).Completion) fun (a : Completion (WithVal (Rat.padicValuation p))) ↦
    pf_2.extend coe'
      ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) pf_6 :
          (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
        a)

Tactic:
exact (uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal
        Padic.isDenseInducing_cast_withVal.dense (uniformContinuous_coe _)).continuous.comp
        (continuous_extension)

Premises used: uniformContinuous_uniformly_extend, Continuous.comp, UniformContinuous.continuous, IsDenseInducing.dense, UniformSpace.Completion.continuous_extension, UniformSpace.Completion.uniformContinuous_coe, Padic.isUniformInducing_cast_withVal, Padic.isDenseInducing_cast_withVal
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
ih :
  Eq (α := (Rat.padicValuation p).Completion)
    (IsDenseInducing.extend ⋯ coe'
      ((RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
          (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
        a))
    (↑a : Completion (WithVal (Rat.padicValuation p)))
⊢ Eq (α := (Rat.padicValuation p).Completion)
    (IsDenseInducing.extend ⋯ coe'
      ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
          (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
        (↑a : Completion (WithVal (Rat.padicValuation p)))))
    (↑a : Completion (WithVal (Rat.padicValuation p)))

Tactic:
rw [extensionHom_coe]

Premises used: UniformSpace.Completion.extensionHom_coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
ih : Continuous (X := WithVal (Rat.padicValuation p)) (Y := (Rat.padicValuation p).Completion) coe'
⊢ Eq (α := (Rat.padicValuation p).Completion)
    (IsDenseInducing.extend ⋯ coe'
      ((RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
          (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
        a))
    (↑a : Completion (WithVal (Rat.padicValuation p)))

Tactic:
apply IsDenseInducing.extend_eq

Premises used: IsDenseInducing.extend_eq
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
⊢ Continuous (X := WithVal (Rat.padicValuation p)) (Y := (Rat.padicValuation p).Completion) coe'

Tactic:
continuous_coe _

Premises used: UniformSpace.Completion.continuous_coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
⊢ Continuous (X := WithVal (Rat.padicValuation p)) (Y := (Rat.padicValuation p).Completion) coe'

Tactic:
exact continuous_coe _

Premises used: UniformSpace.Completion.continuous_coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : ℚ_[p]
hp :
  IsClosed (X := ℚ_[p])
    {x : ℚ_[p] |
      (extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
            (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
          (IsDenseInducing.extend ⋯ coe' x) =
        x}
h :
  ∀ (a : ℚ),
    Eq (α := ℚ_[p])
      ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
            (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
          (IsDenseInducing.extend ⋯ coe' (↑a : ℚ_[p])) :
        ℚ_[p])
      ((↑a : ℚ_[p]) : ℚ_[p])
⊢ (extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
        (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
      (IsDenseInducing.extend ⋯ coe' y) =
    y

Tactic:
induction y using isClosed_property (Padic.denseRange_ratCast p)

Premises used: Padic.denseRange_ratCast, isClosed_property
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ IsClosed (X := ℚ_[p])
    {x : ℚ_[p] |
      (extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
            (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
          (IsDenseInducing.extend ⋯ coe' x) =
        x}

Tactic:
isClosed_eq ?_ continuous_id

Premises used: continuous_id, isClosed_eq
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp :
  Continuous (Y := ℚ_[p]) fun (x : ℚ_[p]) ↦
    (extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
        (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
      (IsDenseInducing.extend ⋯ coe' x)
⊢ IsClosed (X := ℚ_[p])
    {x : ℚ_[p] |
      (extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
            (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
          (IsDenseInducing.extend ⋯ coe' x) =
        x}

Tactic:
refine isClosed_eq ?_ continuous_id

Premises used: continuous_id, isClosed_eq
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Continuous (Y := ℚ_[p]) fun (x : ℚ_[p]) ↦
    (extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
        (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
      (IsDenseInducing.extend ⋯ coe' x)

Tactic:
continuous_extension.comp ?_

Premises used: Continuous.comp, UniformSpace.Completion.extension, UniformSpace.Completion.continuous_extension, AbstractCompletion.extend, ite
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : Continuous (X := ℚ_[p]) (Y := Completion (WithVal (Rat.padicValuation p))) (IsDenseInducing.extend ⋯ coe')
⊢ Continuous (Y := ℚ_[p]) fun (x : ℚ_[p]) ↦
    (extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
        (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
      (IsDenseInducing.extend ⋯ coe' x)

Tactic:
refine continuous_extension.comp ?_

Premises used: Continuous.comp, UniformSpace.Completion.continuous_extension
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Continuous (X := ℚ_[p]) (Y := Completion (WithVal (Rat.padicValuation p))) (IsDenseInducing.extend ⋯ coe')

Tactic:
(uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal
        Padic.isDenseInducing_cast_withVal.dense (uniformContinuous_coe _)).continuous

Premises used: uniformContinuous_uniformly_extend, UniformContinuous.continuous, IsDenseInducing.dense, UniformSpace.Completion.uniformContinuous_coe, Padic.isUniformInducing_cast_withVal, Padic.isDenseInducing_cast_withVal
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Continuous (X := ℚ_[p]) (Y := Completion (WithVal (Rat.padicValuation p))) (IsDenseInducing.extend ⋯ coe')

Tactic:
exact (uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal
        Padic.isDenseInducing_cast_withVal.dense (uniformContinuous_coe _)).continuous

Premises used: uniformContinuous_uniformly_extend, UniformContinuous.continuous, IsDenseInducing.dense, UniformSpace.Completion.uniformContinuous_coe, Padic.isUniformInducing_cast_withVal, Padic.isDenseInducing_cast_withVal
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a q : ℚ
hf : Continuous (X := WithVal (Rat.padicValuation p)) (Y := Completion (WithVal (Rat.padicValuation p))) coe'
⊢ Eq (α := Completion (WithVal (Rat.padicValuation p))) (IsDenseInducing.extend ⋯ coe' (↑q : ℚ_[p]))
    (↑(((WithVal.equiv (Rat.padicValuation p)).symm : (a : ℚ) → WithVal (Rat.padicValuation p)) q) :
      Completion (WithVal (Rat.padicValuation p)))

Tactic:
apply IsDenseInducing.extend_eq

Premises used: IsDenseInducing.extend_eq
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a q : ℚ
⊢ Continuous (X := WithVal (Rat.padicValuation p)) (Y := Completion (WithVal (Rat.padicValuation p))) coe'

Tactic:
continuous_coe _

Premises used: UniformSpace.Completion.continuous_coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a q : ℚ
⊢ Continuous (X := WithVal (Rat.padicValuation p)) (Y := Completion (WithVal (Rat.padicValuation p))) coe'

Tactic:
exact continuous_coe _

Premises used: UniformSpace.Completion.continuous_coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℚ
⊢ ∀ (q : ℚ),
    Eq (α := Completion (WithVal (Rat.padicValuation p))) (IsDenseInducing.extend ⋯ coe' (↑q : ℚ_[p]))
      (↑(((WithVal.equiv (Rat.padicValuation p)).symm : (a : ℚ) → WithVal (Rat.padicValuation p)) q) :
        Completion (WithVal (Rat.padicValuation p)))

Tactic:
have : ∀ q : ℚ, Padic.isDenseInducing_cast_withVal.extend coe' q = coe'
        ((WithVal.equiv (Rat.padicValuation p)).symm q) := by
        intro q
        apply IsDenseInducing.extend_eq
        exact continuous_coe _
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℚ
this :
  ∀ (q : ℚ),
    Eq (α := Completion (WithVal (Rat.padicValuation p))) (IsDenseInducing.extend ⋯ coe' (↑q : ℚ_[p]))
      (↑(((WithVal.equiv (Rat.padicValuation p)).symm : (a : ℚ) → WithVal (Rat.padicValuation p)) q) :
        Completion (WithVal (Rat.padicValuation p)))
h :
  Eq (α := ℚ_[p])
    ((RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
          (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
        (((WithVal.equiv (Rat.padicValuation p)).symm : (a : ℚ) → WithVal (Rat.padicValuation p)) a) :
      ℚ_[p])
    ((↑a : ℚ_[p]) : ℚ_[p])
⊢ Eq (α := ℚ_[p])
    ((extensionHom (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯ :
          (a : Completion (WithVal (Rat.padicValuation p))) → ℚ_[p])
        (IsDenseInducing.extend ⋯ coe' (↑a : ℚ_[p])) :
      ℚ_[p])
    ((↑a : ℚ_[p]) : ℚ_[p])

Tactic:
rw [this, extensionHom_coe]

Premises used: UniformSpace.Completion.extensionHom_coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℚ
this :
  ∀ (q : ℚ),
    Eq (α := Completion (WithVal (Rat.padicValuation p))) (IsDenseInducing.extend ⋯ coe' (↑q : ℚ_[p]))
      (↑(((WithVal.equiv (Rat.padicValuation p)).symm : (a : ℚ) → WithVal (Rat.padicValuation p)) q) :
        Completion (WithVal (Rat.padicValuation p)))
⊢ Eq (α := ℚ_[p])
    ((RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
          (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
        (((WithVal.equiv (Rat.padicValuation p)).symm : (a : ℚ) → WithVal (Rat.padicValuation p)) a) :
      ℚ_[p])
    ((↑a : ℚ_[p]) : ℚ_[p])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := (a : (Rat.padicValuation p).Completion) → ℚ_[p])
    (⇑withValRingEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p])
    (Completion.extension
      (Rat.cast ∘ (⇑(WithVal.equiv (Rat.padicValuation p)) : (a : WithVal (Rat.padicValuation p)) → ℚ)))

Tactic:
rfl

Premises used: Set.Mem, setOf, CauSeq.Completion.ofRat, CauSeq.Completion.mk, UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := (a : ℚ_[p]) → (Rat.padicValuation p).Completion)
    (⇑(RingEquiv.symm withValRingEquiv) : (a : ℚ_[p]) → (Rat.padicValuation p).Completion)
    (IsDenseInducing.extend ⋯ Completion.coe')

Tactic:
rfl

Premises used: Classical.epsilon, Set.Mem, setOf, Filter.lim, Filter.limUnder, IsDenseInducing.extend, rfl
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑withValUniformEquiv : (Rat.padicValuation p).Completion ≃ ℚ_[p]) =
    (↑withValRingEquiv : (Rat.padicValuation p).Completion ≃ ℚ_[p])

Tactic:
rfl

Premises used: Classical.epsilon, UniformEquiv.symm, Padic.withValRingEquiv, Filter.lim, Filter.limUnder, EquivLike.toEquiv, IsDenseInducing.extend, rfl, Padic.withValUniformEquiv