mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

Tactic:
]

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

Tactic:
]

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖b⁻¹ * a‖ = ‖b⁻¹ * a‖

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
h.image_Icc (hc.1.trans hc.2)

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
h.image_Icc (hc.1.trans hc.2)

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a‖ = ‖a‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a‖ = 0 ↔ ‖a‖ = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖1⁻¹ * (a / b)‖ = ‖(b / a)⁻¹ * 1‖

Tactic:
]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖1⁻¹ * (a / b)‖ = ‖(b / a)⁻¹ * 1‖
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ⊓ ↑I ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') ⊓ ↑I

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ⊓ ↑I ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') ⊓ ↑I
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α✝
α : Type u_3
β : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : ProperSpace α
inst✝ : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall x r ×ˢ closedBall y r)

Tactic:
]

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α✝
α : Type u_3
β : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : ProperSpace α
inst✝ : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall x r ×ˢ closedBall y r)
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (univ.pi fun b ↦ closedBall (x b) r)

Tactic:
]

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (univ.pi fun b ↦ closedBall (x b) r)
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ n‖ = ‖a ^ n‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
⊢ ‖a‖ = ‖a‖

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε

Tactic:
]

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
h : ∀ᶠ (m : β × β) in atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε

Tactic:
]

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
h : ∀ᶠ (m : β × β) in atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ ‖(s.mulIndicator f x)⁻¹ * t.mulIndicator f x‖ = ‖s.mulIndicator f x / t.mulIndicator f x‖

Tactic:
]

Goal state after:
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ ‖(s.mulIndicator f x)⁻¹ * t.mulIndicator f x‖ = ‖s.mulIndicator f x / t.mulIndicator f x‖
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Icc (sInf s) (sSup s)
⊢ Icc (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Icc (sInf s) (sSup s)
⊢ Icc (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
⊢ ∃ a, ∀ (b : β × β), a ≤ b → ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u

Tactic:
]

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
⊢ ∃ a, ∀ (b : β × β), a ≤ b → ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ico (sInf s) (sSup s)
⊢ Ico (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ico (sInf s) (sSup s)
⊢ Ico (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioc (sInf s) (sSup s)
⊢ Ioc (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioc (sInf s) (sSup s)
⊢ Ioc (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioo (sInf s) (sSup s)
⊢ Ioo (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioo (sInf s) (sSup s)
⊢ Ioo (sInf s) (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ici (sInf s)
⊢ Ici (sInf s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ici (sInf s)
⊢ Ici (sInf s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1

Tactic:
]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioi (sInf s)
⊢ Ioi (sInf s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Ioi (sInf s)
⊢ Ioi (sInf s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : SeminormedGroup E
inst✝ : Subsingleton E
a : E
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Iic (sSup s)
⊢ Iic (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Iic (sSup s)
⊢ Iic (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
hx : x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'
⊢ x ∈ ↑(spanSingleton R⁰ (I'.divMod I J')⁻¹ * J')

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
hx : x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'
⊢ x ∈ ↑(spanSingleton R⁰ (I'.divMod I J')⁻¹ * J')
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Iio (sSup s)
⊢ Iio (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = Iio (sSup s)
⊢ Iio (sSup s) ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = univ
⊢ univ ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = univ
⊢ univ ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖

Tactic:
]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inr.inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s ∈ {∅}
⊢ ∅ ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
]

Goal state after:
case inr.inr.inr.inr.inr.inr.inr.inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s ∈ {∅}
⊢ ∅ ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ = ‖u‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖

Tactic:
]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖

Tactic:
]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ = ‖v‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u * v‖ + ‖u‖ = ‖u * v‖ + ‖u‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ = ‖y‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ = ‖x‖

pp: case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y⁻¹‖ = 0

Tactic:
]

Goal state after:
case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y⁻¹‖ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y‖ = 0

Tactic:
]

Goal state after:
case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y‖ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ ‖b⁻¹ * a‖ < r ↔ ‖b⁻¹ * a‖ < r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ ‖a⁻¹ * b‖ < r ↔ ‖a⁻¹ * b‖ < r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ ‖a‖ < r ↔ ‖a‖ < r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ ‖b⁻¹ * a‖ ≤ r ↔ ‖b⁻¹ * a‖ ≤ r

Tactic:
]

Goal state after: