awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
⊢ CompactSpace.{u_1} ↥𝒪[K] ↔ CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]

Tactic:
⟨fun h ↦ ?_, fun ⟨_, _, h⟩ ↦ ⟨?_⟩⟩

Premises used: Valued.integer, Membership.mem, Subtype, CompactSpace, CompactSpace.mk, Iff.intro, _private.0.Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.match_1
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
refine_1 :
  ∀ (h : CompactSpace.{u_1} ↥𝒪[K]),
    CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
refine_2 :
  CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K] →
    CompleteSpace.{u_1} ↥𝒪[K] →
      IsDiscreteValuationRing.{u_1} ↥𝒪[K] → ∀ (h : Finite.{u_1 + 1} 𝓀[K]), IsCompact.{u_1} (X := ↥𝒪[K]) Set.univ
⊢ CompactSpace.{u_1} ↥𝒪[K] ↔ CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨_, _, h⟩ ↦ ⟨?_⟩⟩
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
⊢ IsDiscreteValuationRing.{u_1} ↥𝒪[K]

Tactic:
have : IsDiscreteValuationRing 𝒪[K] := isDiscreteValuationRing_of_compactSpace
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
⊢ IsDiscreteValuationRing.{u_1} ↥𝒪[K]

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
refine_1 : Finite.{u_1 + 1} 𝓀[K]
⊢ CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]

Tactic:
refine ⟨complete_of_compact, by assumption, ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
⊢ Finite.{u_1 + 1} 𝓀[K] ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ

Tactic:
rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete,
        totallyBounded_iff_finite_residueField] at h

Premises used: isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete, Valued.integer.totallyBounded_iff_finite_residueField
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h₁ : Finite.{u_1 + 1} 𝓀[K] ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ
⊢ IsDiscreteValuationRing.{u_1} ↥𝒪[K]

Tactic:
rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete,
        totallyBounded_iff_finite_residueField] at h

Premises used: isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete, Valued.integer.totallyBounded_iff_finite_residueField
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : Finite.{u_1 + 1} 𝓀[K] ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
⊢ Finite.{u_1 + 1} 𝓀[K]

Tactic:
h.left

Premises used: And.left
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : Finite.{u_1 + 1} 𝓀[K] ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
⊢ Finite.{u_1 + 1} 𝓀[K]

Tactic:
exact h.left

Premises used: And.left
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h_1 : CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
left : CompleteSpace.{u_1} ↥𝒪[K]
left_1 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ

Tactic:
rw [← totallyBounded_iff_finite_residueField] at h

Premises used: Valued.integer.totallyBounded_iff_finite_residueField
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h_1 : CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
left : CompleteSpace.{u_1} ↥𝒪[K]
left_1 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
refine_2 : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ
⊢ IsCompact.{u_1} (X := ↥𝒪[K]) Set.univ

Tactic:
rw [isCompact_iff_totallyBounded_isComplete]

Premises used: isCompact_iff_totallyBounded_isComplete
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h_1 : CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
left : CompleteSpace.{u_1} ↥𝒪[K]
left_1 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ

Tactic:
⟨h, completeSpace_iff_isComplete_univ.mp ‹_›⟩

Premises used: completeSpace_iff_isComplete_univ, And.intro, Iff.mp
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h_1 : CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
left : CompleteSpace.{u_1} ↥𝒪[K]
left_1 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ

Tactic:
exact ⟨h, completeSpace_iff_isComplete_univ.mp ‹_›⟩
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
simp : ProperSpace K ↔ IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)
⊢ ProperSpace K ↔ CompactSpace.{u_1} ↥𝒪[K]

Tactic:
simp only [← isCompact_univ_iff, Subtype.isCompact_iff, Set.image_univ, Subtype.range_coe_subtype,
             toNormedField.setOf_mem_integer_eq_closedBall]

Premises used: Set.image_univ, Subtype.isCompact_iff, Subtype.range_coe_subtype, isCompact_univ_iff, Valued.toNormedField.setOf_mem_integer_eq_closedBall
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
mp : ProperSpace K → IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)
mpr : IsCompact.{u_1} (X := K) (Metric.closedBall 0 1) → ProperSpace K
⊢ ProperSpace K ↔ IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : ProperSpace K
⊢ IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)

Tactic:
isCompact_closedBall 0 1

Premises used: ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : ProperSpace K
⊢ IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)

Tactic:
exact isCompact_closedBall 0 1

Premises used: ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)
mpr : LocallyCompactSpace K
⊢ ProperSpace K

Tactic:
suffices LocallyCompactSpace K from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace K
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)
⊢ LocallyCompactSpace K

Tactic:
IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup h <|
      Metric.closedBall_mem_nhds 0 zero_lt_one

Premises used: Metric.closedBall_mem_nhds, zero_lt_one, IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : IsCompact.{u_1} (X := K) (Metric.closedBall 0 1)
⊢ LocallyCompactSpace K

Tactic:
exact IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup h <|
      Metric.closedBall_mem_nhds 0 zero_lt_one

Premises used: Metric.closedBall_mem_nhds, zero_lt_one, IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
⊢ ProperSpace K ↔ CompleteSpace K ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]

Tactic:
simp only [properSpace_iff_compactSpace_integer,
      compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField,
      toNormedField.setOf_mem_integer_eq_closedBall,
      completeSpace_iff_isComplete_univ (α := 𝒪[K]), Subtype.isComplete_iff,
      NormedField.completeSpace_iff_isComplete_closedBall, Set.image_univ,
      Subtype.range_coe_subtype]

Premises used: Set.image_univ, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, completeSpace_iff_isComplete_univ, Subtype.range_coe_subtype, Subtype.isComplete_iff, NormedField.completeSpace_iff_isComplete_closedBall, Valued.integer.properSpace_iff_compactSpace_integer, Valued.toNormedField.setOf_mem_integer_eq_closedBall
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : ContinuousConstVAdd R R
h₀ :
  ∀ (s : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) s ↔
      ∃ (γ : (ValueGroupWithZero R)ˣ),
        {z : R | (v : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆ s
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) '' {z : R | (v : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆ s

Tactic:
simpa [← vadd_mem_nhds_vadd_iff (t := s) (-x), ← image_vadd, ← image_subset_iff] using
      h₀ ((x + ·) ⁻¹' s)

Premises used: Set.image_vadd, Set.preimage, HAdd.hAdd, Set.image_subset_iff, vadd_mem_nhds_vadd_iff, Neg.neg
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
inst_2 : TopologicalSpace R_1
inst_3 : IsValuativeTopology R_1
R : Type u_2
inst_4 : CommRing R
inst_5 : ValuativeRel R
inst_6 : UniformSpace R
inst_7 : IsUniformAddGroup R
inst_8 : IsValuativeTopology R
simp_rw :
  ∀ (s : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) s ↔
      ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v)ˣ),
        {x : R |
            LT.lt (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
              ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ v) → ValueGroupWithZero R)
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ v) :
                ValueGroupWithZero R)} ⊆
          s
⊢ ∀ (s : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) s ↔
      ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v)ˣ),
        {x : R |
            (Valuation.restrict v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑v : R →*₀ ValueGroupWithZero R)) x <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)} ⊆
          s

Tactic:
simp_rw [Valuation.restrict_lt_iff_lt_embedding]

Premises used: Valuation.restrict_lt_iff_lt_embedding
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
inst_2 : TopologicalSpace R_1
inst_3 : IsValuativeTopology R_1
R : Type u_2
inst_4 : CommRing R
inst_5 : ValuativeRel R
inst_6 : UniformSpace R
inst_7 : IsUniformAddGroup R
inst_8 : IsValuativeTopology R
⊢ ∀ (s : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) s ↔
      ∃ (γ : (ValueGroupWithZero R)ˣ),
        {x : R | (v : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)} ⊆ s

Tactic:
mem_nhds_zero_iff (R := R)

Premises used: IsValuativeTopology.mem_nhds_zero_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
inst_2 : TopologicalSpace R_1
inst_3 : IsValuativeTopology R_1
R : Type u_2
inst_4 : CommRing R
inst_5 : ValuativeRel R
inst_6 : UniformSpace R
inst_7 : IsUniformAddGroup R
inst_8 : IsValuativeTopology R
h :
  ∀ (a : Set R),
    (∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v)ˣ),
        {x : R |
            LT.lt (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
              ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ v) → ValueGroupWithZero R)
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ v) :
                ValueGroupWithZero R)} ⊆
          a) ↔
      ∃ (γ : (ValueGroupWithZero R)ˣ),
        {x : R | (v : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)} ⊆ a
⊢ ∀ (s : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) s ↔
      ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v)ˣ),
        {x : R |
            LT.lt (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
              ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ v) → ValueGroupWithZero R)
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ v) :
                ValueGroupWithZero R)} ⊆
          s

Tactic:
convert! mem_nhds_zero_iff (R := R)

Premises used: IsValuativeTopology.mem_nhds_zero_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
inst_2 : TopologicalSpace R_1
inst_3 : IsValuativeTopology R_1
R : Type u_2
inst_4 : CommRing R
inst_5 : ValuativeRel R
inst_6 : UniformSpace R
inst_7 : IsUniformAddGroup R
inst_8 : IsValuativeTopology R
a : Set R
⊢ (∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v)ˣ),
      {x : R |
          LT.lt (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
            ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ v) → ValueGroupWithZero R)
                (↑γ : MonoidWithZeroHom.ValueGroup₀ v) :
              ValueGroupWithZero R)} ⊆
        a) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ), {x : R | (v : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)} ⊆ a

Tactic:
simpa [← Valuation.restrict_lt_iff_lt_embedding] using
      (valuation R).exists_setOf_restrict_le_iff 0 _

Premises used: Valuation.restrict_lt_iff_lt_embedding, ValuativeRel.valuation, OfNat.ofNat, Valuation.exists_setOf_restrict_le_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
⊢ Valued.v = v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
simp :
  ∀ (x : R),
    Tendsto (β := ValueGroupWithZero R) ((⇑v : (a : R) → ValueGroupWithZero R) : (a : R) → ValueGroupWithZero R) (𝓝 x)
      (𝓝 ((v : (a : R) → ValueGroupWithZero R) x) : Filter (ValueGroupWithZero R))
⊢ Continuous[inst_2, _] (⇑v : (a : R) → ValueGroupWithZero R)

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt]

Premises used: ContinuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
pos :
  ∀
    (hx :
      Eq (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
        (0 : ValueGroupWithZero R)),
    Tendsto (β := ValueGroupWithZero R) ((⇑v : (a : R) → ValueGroupWithZero R) : (a : R) → ValueGroupWithZero R) (𝓝 x)
      (𝓝 ((v : (a : R) → ValueGroupWithZero R) x) : Filter (ValueGroupWithZero R))
neg :
  ∀
    (hx :
      ¬Eq (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
          (0 : ValueGroupWithZero R)),
    Tendsto (β := ValueGroupWithZero R) ((⇑v : (a : R) → ValueGroupWithZero R) : (a : R) → ValueGroupWithZero R) (𝓝 x)
      (𝓝 ((v : (a : R) → ValueGroupWithZero R) x) : Filter (ValueGroupWithZero R))
⊢ Tendsto (β := ValueGroupWithZero R) ((⇑v : (a : R) → ValueGroupWithZero R) : (a : R) → ValueGroupWithZero R) (𝓝 x)
    (𝓝 ((v : (a : R) → ValueGroupWithZero R) x) : Filter (ValueGroupWithZero R))

Tactic:
by_cases hx : v x = 0
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
hx :
  Eq (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)
i : ValueGroupWithZero R
hi : ¬i = 0
y : R
⊢ LT.lt (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ ValueGroupWithZero R) (↑v : R →*₀ ValueGroupWithZero R))
      ((Valuation.restrict v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑v : R →*₀ ValueGroupWithZero R)) (y - x) :
        MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ ValueGroupWithZero R) (↑v : R →*₀ ValueGroupWithZero R))
      ((↑((Units.mapEquiv
                  (↑(ValueGroupWithZero.orderMonoidIso v) : ValueGroupWithZero R ≃* MonoidWithZeroHom.ValueGroup₀ v) :
                (a : (ValueGroupWithZero R)ˣ) → (MonoidWithZeroHom.ValueGroup₀ v)ˣ)
              (Units.mk0 i hi)) :
          MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v) →
    (v : (a : R) → ValueGroupWithZero R) y < i

Tactic:
simp [Valuation.map_sub_of_right_eq_zero _ hx]

Premises used: Valuation.map_sub_of_right_eq_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
hx :
  Eq (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)
⊢ Tendsto (β := ValueGroupWithZero R) ((⇑v : (a : R) → ValueGroupWithZero R) : (a : R) → ValueGroupWithZero R) (𝓝 x)
    (𝓝 ((v : (a : R) → ValueGroupWithZero R) x) : Filter (ValueGroupWithZero R))

Tactic:
simpa [hx, ((valuation R).hasBasis_nhds _).tendsto_iff WithZeroTopology.hasBasis_nhds_zero]
      using fun i hi ↦ ⟨(Units.mk0 i hi).mapEquiv (ValueGroupWithZero.orderMonoidIso (valuation R)),
        fun y ↦ by simp [Valuation.map_sub_of_right_eq_zero _ hx]⟩

Premises used: Filter.HasBasis.tendsto_iff, WithZeroTopology.hasBasis_nhds_zero, Valuation.hasBasis_nhds, ValuativeRel.valuation
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
hx :
  ¬Eq (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
      (0 : ValueGroupWithZero R)
x_1 : R
⊢ LT.lt (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ ValueGroupWithZero R) (↑v : R →*₀ ValueGroupWithZero R))
      ((Valuation.restrict v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑v : R →*₀ ValueGroupWithZero R)) (x_1 - x) :
        MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ ValueGroupWithZero R) (↑v : R →*₀ ValueGroupWithZero R))
      ((↑((Units.mapEquiv
                  (↑(ValueGroupWithZero.orderMonoidIso v) : ValueGroupWithZero R ≃* MonoidWithZeroHom.ValueGroup₀ v) :
                (a : (ValueGroupWithZero R)ˣ) → (MonoidWithZeroHom.ValueGroup₀ v)ˣ)
              (Units.mk0 ((v : (a : R) → ValueGroupWithZero R) x) hx)) :
          MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) v) →
    Eq (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x_1 : ValueGroupWithZero R)
      ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)

Tactic:
simpa [← (valuation R).restrict_def] using Valuation.map_eq_of_sub_lt _

Premises used: Valuation.restrict_def, Valuation.map_eq_of_sub_lt, ValuativeRel.valuation
-- Module: Mathlib.Topology.Algebra.Valued.ValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
hx :
  ¬Eq (α := ValueGroupWithZero R) ((v : (a : R) → ValueGroupWithZero R) x : ValueGroupWithZero R)
      (0 : ValueGroupWithZero R)
⊢ Tendsto (β := ValueGroupWithZero R) ((⇑v : (a : R) → ValueGroupWithZero R) : (a : R) → ValueGroupWithZero R) (𝓝 x)
    (𝓝 ((v : (a : R) → ValueGroupWithZero R) x) : Filter (ValueGroupWithZero R))

Tactic:
simpa [((valuation R).hasBasis_nhds _).tendsto_iff (hasBasis_nhds_of_ne_zero hx)]
      using ⟨(Units.mk0 (v x) hx).mapEquiv (ValueGroupWithZero.orderMonoidIso (valuation R)),
        fun _ ↦ by simpa [← (valuation R).restrict_def] using Valuation.map_eq_of_sub_lt _⟩

Premises used: Filter.HasBasis.tendsto_iff, WithZeroTopology.hasBasis_nhds_of_ne_zero, Valuation.hasBasis_nhds, ValuativeRel.valuation
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
U V W : Opens (↑X : Type u)
down : U ≤ V
a₂ : U ⟶ V
h :
  Eq.{u + 1} (α := (a : ↥U) → ↥V)
    ((fun (f : U ⟶ V) ↦ Set.inclusion (s := (↑U : Set (↑X : Type u))) (t := (↑V : Set (↑X : Type u))) ⋯)
      { down := { down := down } })
    ((fun (f : U ⟶ V) ↦ Set.inclusion (s := (↑U : Set (↑X : Type u))) (t := (↑V : Set (↑X : Type u))) ⋯) a₂)
⊢ { down := { down := down : PLift (U ≤ V) } : ULift.{u, 0} (PLift (U ≤ V)) } = a₂

Tactic:
congr!
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U V : Opens (↑X : Type u)
f : U ⟶ V
x : ↥U
⊢ (f : (a : ↥U) → ↥V) x = Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ V) (↑x : (↑X : Type u)) ⋯

Tactic:
rfl

Premises used: rfl