mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
⊢ (∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ) →
    ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
⊢ (∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ) →
    ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

pp: case neg
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : ¬a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ ∀ x ∈ {x | v.restrict x < 0}, {x | v.restrict x < 0} ∈ 𝓝 x

pp: case inr
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ ∀ x ∈ {x | v.restrict x < r}, {x | v.restrict x < r} ∈ 𝓝 x

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ ∀ x ∈ {x | v.restrict x < 0}, {x | v.restrict x < 0} ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ IsClosed {a | (completion 0 ⋯) a = 0 a}

pp: case refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ ∀ (a : α), (completion 0 ⋯) ↑a = 0 ↑a

Tactic:
·

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ IsClosed {a | (completion 0 ⋯) a = 0 a}
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ ∀ (a : α), (completion 0 ⋯) ↑a = 0 ↑a

Tactic:
·

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ ∀ (a : α), (completion 0 ⋯) ↑a = 0 ↑a
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: case refine_1
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ IsClosed {a | ((f + g).completion ⋯) a = (f.completion hf + g.completion hg) a}

pp: case refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Tactic:
·

Goal state after:
case refine_1
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ IsClosed {a | ((f + g).completion ⋯) a = (f.completion hf + g.completion hg) a}
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: case refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Tactic:
·

Goal state after:
case refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x * (restrict₀ (ofClass v)) ↑r = (restrict₀ (ofClass v)) y * (restrict₀ (ofClass v)) ↑s

pp: case hb
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

pp: case hd
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0

Tactic:
·

Goal state after:
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x * (restrict₀ (ofClass v)) ↑r = (restrict₀ (ofClass v)) y * (restrict₀ (ofClass v)) ↑s
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] {x | v.restrict x < 0}

pp: case inr
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ IsClosed[_t] {x | v.restrict x < r}

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] {x | v.restrict x < 0}
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] {x | v.restrict x = 0}

pp: case inr
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ IsClosed[_t] {x | v.restrict x = r}

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] {x | v.restrict x = 0}
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (Filter.comap coe' (𝓝 y))

pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
·

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (Filter.comap coe' (𝓝 y))
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
·

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
      by_contra h
      exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_1
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ IsClosed {a | Completion.map (fun x ↦ r • x) a = ↑((algebraMap R A) r) * a}

pp: case refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun x ↦ r • x) ↑a = ↑((algebraMap R A) r) * ↑a

Tactic:
·

Goal state after:
case refine_1
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ IsClosed {a | Completion.map (fun x ↦ r • x) a = ↑((algebraMap R A) r) * a}
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun x ↦ r • x) ↑a = ↑((algebraMap R A) r) * ↑a

Tactic:
·

Goal state after:
case refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun x ↦ r • x) ↑a = ↑((algebraMap R A) r) * ↑a
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑x)⁻¹ = ↑x⁻¹

pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x)⁻¹ = ↑x⁻¹

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑x)⁻¹ = ↑x⁻¹
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x)⁻¹ = ↑x⁻¹

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x)⁻¹ = ↑x⁻¹
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
⊢ IsClosed {q | ⋯.extend (⇑f) (q.1 * q.2) = ⋯.extend (⇑f) q.1 * ⋯.extend (⇑f) q.2}

pp: case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a * i b) = ⋯.extend (⇑f) (i a) * ⋯.extend (⇑f) (i b)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
⊢ IsClosed {q | ⋯.extend (⇑f) (q.1 * q.2) = ⋯.extend (⇑f) q.1 * ⋯.extend (⇑f) q.2}
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x).hatInv = ↑x⁻¹

pp: case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑x = 0

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x).hatInv = ↑x⁻¹
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a * i b) = ⋯.extend (⇑f) (i a) * ⋯.extend (⇑f) (i b)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a * i b) = ⋯.extend (⇑f) (i a) * ⋯.extend (⇑f) (i b)
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑x = 0

Tactic:
·

Goal state after:
case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑x = 0
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
⊢ IsClosed {q | ⋯.extend (⇑f) (q.1 + q.2) = ⋯.extend (⇑f) q.1 + ⋯.extend (⇑f) q.2}

pp: case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a + i b) = ⋯.extend (⇑f) (i a) + ⋯.extend (⇑f) (i b)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
⊢ IsClosed {q | ⋯.extend (⇑f) (q.1 + q.2) = ⋯.extend (⇑f) q.1 + ⋯.extend (⇑f) q.2}
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a + i b) = ⋯.extend (⇑f) (i a) + ⋯.extend (⇑f) (i b)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a + i b) = ⋯.extend (⇑f) (i a) + ⋯.extend (⇑f) (i b)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))

pp: case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑r)) = 0

pp: case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑s)) = 0

Tactic:
·

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑r)) = 0

pp: case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑s)) = 0

Tactic:
·

Goal state after:
case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑r)) = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑s)) = 0

Tactic:
·

Goal state after:
case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑s)) = 0