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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ {0}ᶜ ⊆ {x | (fun x ↦ ∃ c, Tendsto (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Tactic:
intro y y_ne

Goal state after:
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}ᶜ
⊢ y ∈ {x | (fun x ↦ ∃ c, Tendsto (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}
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:
exact fun H => h (isDenseEmbedding_coe.injective H)

Goal state after:
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case e'_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
⊢ 0 = i 0

pp: case e'_3
α : 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
⊢ 0 = f 0

Tactic:
<;>

Goal state after:
case e'_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
⊢ 0 = i 0

case e'_3
α : 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
⊢ 0 = f 0
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ {0}ᶜ ⊆ {y | y.hatInv = y⁻¹}

Tactic:
intro y y_ne

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {y | y.hatInv = y⁻¹}
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I ↑(span {a}) = R ∙ y
⊢ I ≤ R ∙ x * y

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I ↑(span {a}) = R ∙ y
⊢ R ∙ x * y ≤ I

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I ↑(span {a}) = R ∙ y
⊢ I ≤ R ∙ x * y

case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I ↑(span {a}) = R ∙ y
⊢ R ∙ x * y ≤ I
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH.ofNat.refine_1
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ ¬(MonoidWithZeroHom.ofClass v) 1 = 0

pp: case hH.ofNat.refine_2
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ (MonoidWithZeroHom.ofClass v) 1 * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n) = (MonoidWithZeroHom.ofClass v) (π ^ n)

Tactic:
<;>

Goal state after:
case hH.ofNat.refine_1
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ ¬(MonoidWithZeroHom.ofClass v) 1 = 0

case hH.ofNat.refine_2
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ (MonoidWithZeroHom.ofClass v) 1 * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n) = (MonoidWithZeroHom.ofClass v) (π ^ n)
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH.negSucc.refine_1
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n = n✝
⊢ ¬(MonoidWithZeroHom.ofClass v) (π ^ (n + 1)) = 0

pp: case hH.negSucc.refine_2
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n = n✝
⊢ (MonoidWithZeroHom.ofClass v) (π ^ (n + 1)) * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n) =
    (MonoidWithZeroHom.ofClass v) 1

Tactic:
<;>

Goal state after:
case hH.negSucc.refine_1
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n = n✝
⊢ ¬(MonoidWithZeroHom.ofClass v) (π ^ (n + 1)) = 0

case hH.negSucc.refine_2
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n = n✝
⊢ (MonoidWithZeroHom.ofClass v) (π ^ (n + 1)) * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n) =
    (MonoidWithZeroHom.ofClass v) 1
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : π = 0
⊢ False

Tactic:
h0,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer 0
h0 : π = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addXYZ P Q = (P x * Q z) • Q

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
    smul_fin3]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case pos
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : WithVal v
hb : v b.ofVal = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v)) (if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩) =
    if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩

pp: case neg
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : WithVal v
hb : ¬v b.ofVal = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v)) (if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩) =
    if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩

Tactic:
<;>

Goal state after:
case pos
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : WithVal v
hb : v b.ofVal = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v)) (if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩) =
    if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩

case neg
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : WithVal v
hb : ¬v b.ofVal = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v)) (if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩) =
    if h : (valuation v) b = 0 then 0 else ↑⟨Units.mk0 ((valuation v) b) ⋯, ⋯⟩
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case pos
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : R
hb : v b = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) (if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩) =
    if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩

pp: case neg
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : R
hb : ¬v b = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) (if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩) =
    if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩

Tactic:
<;>

Goal state after:
case pos
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : R
hb : v b = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) (if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩) =
    if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩

case neg
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : R
hb : ¬v b = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) (if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩) =
    if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case IJ
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
⊢ x ∈ span {π.val}

Tactic:
by_cases hx₀ : x = 0

Goal state after:
case pos
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
hx₀ : x = 0
⊢ x ∈ span {π.val}

case neg
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
hx₀ : ¬x = 0
⊢ x ∈ span {π.val}
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ ContinuousAt (⇑(equiv v)) 0

Tactic:
ContinuousAt,

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ Filter.Tendsto (⇑(equiv v)) (nhds 0) (nhds ((equiv v) 0))
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ ContinuousAt (⇑(equiv v).symm) 0

Tactic:
ContinuousAt,

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ Filter.Tendsto (⇑(equiv v).symm) (nhds 0) (nhds ((equiv v).symm 0))
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ ContinuousAt (⇑(RingHom.id R)) 0

Tactic:
ContinuousAt,

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ Filter.Tendsto (⇑(RingHom.id R)) (nhds 0) (nhds ((RingHom.id R) 0))
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz'✝ : z < y
hz0 : ⊥ < ↑z
hz' : (↑z).unbot ⋯ < (↑y).unbot ⋯
⊢ (↑z).unbot ⋯ ∈ some ⁻¹' s

pp: case refine_2
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz'✝ : z < y
hz0 : ⊥ < ↑z
hz' : (↑z).unbot ⋯ < (↑y).unbot ⋯
⊢ (↑y).unbot ⋯ ∈ some ⁻¹' s

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz'✝ : z < y
hz0 : ⊥ < ↑z
hz' : (↑z).unbot ⋯ < (↑y).unbot ⋯
⊢ (↑z).unbot ⋯ ∈ some ⁻¹' s

case refine_2
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz'✝ : z < y
hz0 : ⊥ < ↑z
hz' : (↑z).unbot ⋯ < (↑y).unbot ⋯
⊢ (↑y).unbot ⋯ ∈ some ⁻¹' s
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz'✝ : z < y
hz0 : ⊥ < ↑z
hz' : (↑z).unbot ⋯ < (↑y).unbot ⋯
⊢ False

Tactic:
refine absurd (this ?_ ?_) hz'.ne <;>
    simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ContinuousAt (⇑v.restrict) 0

Tactic:
ContinuousAt,

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto (⇑v.restrict) (𝓝 0) (𝓝 (v.restrict 0))
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ ContinuousAt (⇑v.restrict) x

Tactic:
ContinuousAt,

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ Tendsto (⇑v.restrict) (𝓝 x) (𝓝 (v.restrict x))
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
⊢ ContinuousAt (⇑v) 0

Tactic:
ContinuousAt,

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
⊢ Tendsto (⇑v) (𝓝 0) (𝓝 (v 0))
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
h0 : v x ≠ 0
⊢ ContinuousAt (⇑v) x

Tactic:
ContinuousAt,

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
h0 : v x ≠ 0
⊢ Tendsto (⇑v) (𝓝 x) (𝓝 (v x))
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
⊢ AddEquiv.refl ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

pp: case inr
⊢ AddEquiv.neg ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

Tactic:
<;>

Goal state after:
case inl
⊢ AddEquiv.refl ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

case inr
⊢ AddEquiv.neg ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h✝ : max x x⁻¹ = x ∧ x⁻¹ ≤ x
⊢ closure {x} = closure {x'}

pp: case inr
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h✝ : max x x⁻¹ = x⁻¹ ∧ x < x⁻¹
⊢ closure {x} = closure {x'}

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h✝ : max x x⁻¹ = x ∧ x⁻¹ ≤ x
⊢ closure {x} = closure {x'}

case inr
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h✝ : max x x⁻¹ = x⁻¹ ∧ x < x⁻¹
⊢ closure {x} = closure {x'}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
h✝ : max y y⁻¹ = y ∧ y⁻¹ ≤ y
⊢ closure {y} = closure {y'}

pp: case inr
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
h✝ : max y y⁻¹ = y⁻¹ ∧ y < y⁻¹
⊢ closure {y} = closure {y'}

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
h✝ : max y y⁻¹ = y ∧ y⁻¹ ≤ y
⊢ closure {y} = closure {y'}

case inr
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
h✝ : max y y⁻¹ = y⁻¹ ∧ y < y⁻¹
⊢ closure {y} = closure {y'}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b → b = |a|ₘ ∧ 1 < b

pp: case mpr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ b = |a|ₘ ∧ 1 < b → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Tactic:
<;>

Goal state after:
case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b → b = |a|ₘ ∧ 1 < b

case mpr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ b = |a|ₘ ∧ 1 < b → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
this : Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').1 * (x, x').2⁻¹ ∈ V
⊢ ∃ V' ∈ 𝓝 1, 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V

Tactic:
let hatKstar := ({0}ᶜ : Set <| hat K)

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
this : Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').1 * (x, x').2⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
⊢ ∃ V' ∈ 𝓝 1, 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V