mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hp₀
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
exps : HeightOneSpectrum R → ℤ
⊢ count K v 1 = 0

pp: case hp₁
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
exps : HeightOneSpectrum R → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0

pp: case hp₂
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
exps : HeightOneSpectrum R → ℤ
⊢ ∀ x ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0

Tactic:
· exact count_one K v

Goal state after:
case hp₁
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
exps : HeightOneSpectrum R → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0

case hp₂
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
exps : HeightOneSpectrum R → ℤ
⊢ ∀ x ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u_3
m' : PseudoMetricSpace α
toDist✝ : Dist α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h :
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
        edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
        toBornology := toBornology✝, cobounded_sets := hB }.toDist =
    m'.toDist
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB }.toDist
⊢ { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB } =
    m'

Tactic:
let d' := m'.toDist

Goal state after:
α : Type u_3
m' : PseudoMetricSpace α
toDist✝ : Dist α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h :
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
        edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
        toBornology := toBornology✝, cobounded_sets := hB }.toDist =
    m'.toDist
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB }.toDist
d' : Dist α := m'.toDist
⊢ { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB } =
    m'
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal

Tactic:
rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ (a / b).toReal = a.toReal / b.toReal

Tactic:
rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ ball y ε ↔ y ∈ ball x ε

Tactic:
mem_ball',

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ dist y x < ε ↔ y ∈ ball x ε
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (a • ∅) = a • sInf ∅

Tactic:
rw [smul_set_empty, Real.sInf_empty, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ (J * ∏ x ∈ s \ {p}, x.asIdeal) * p.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1

Tactic:
refine mul_lt_mul_of_pos_left ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ p.asIdeal < 1

case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ 0 < J * ∏ x ∈ s \ {p}, x.asIdeal
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨆ i, f i) * r = ⨅ i, f i * r

Tactic:
by
  simp only [Real.mul_iSup_of_nonpos ha, mul_comm]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
⊢ Inseparable x y ↔ edist x y = 0

Tactic:
by
  simp [inseparable_iff_mem_closure, mem_closure_iff, edist_comm, forall_gt_iff_le]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
by
  obtain hr | rfl | hr := lt_trichotomy r 0
  · simp [hr]
  · cases x
    simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
  · ext ⟨x', y'⟩
    simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq,
      max_eq_iff]
    refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))
    all_goals rintro rfl; rfl

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ frontier (Ioc a b) = {a, b}

Tactic:
rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_sdiff_Ioo_same h.le]

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

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
⊢ ⨆ s, f ↑s = ⨆ i, f i

Tactic:
by_cases h : BddAbove (range (fun x : S ↦ f x))
  · refine hS.ciSup hf <| h.closure.mono ?_
    simpa [← Function.comp_def, range_comp] using hf.range_subset_closure_image_dense hS
  · suffices ¬ BddAbove (range f) by simp [ciSup_of_not_bddAbove, this, h]
    contrapose h
    grind [h.mono]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 < r
⊢ dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r

Tactic:
lift r to ℝ≥0 using hr.le

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g < ↑r ↔ ∀ (b : β), dist (f b) (g b) < ↑r
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 < r
⊢ dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr.le

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g = ↑r ↔ (∃ i, dist (f i) (g i) = ↑r) ∧ ∀ (b : β), dist (f b) (g b) ≤ ↑r
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (Pi.single i a k) (Pi.single j b k) ≤ max (nndist a 0) (nndist b 0)

pp: case refine_2
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist a 0 ≤ nndist (Pi.single i a) (Pi.single j b)

pp: case refine_3
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist b 0 ≤ nndist (Pi.single i a) (Pi.single j b)

Tactic:
· simp only [Pi.single_apply]
    by_cases hki : k = i <;> by_cases hkj : k = j <;> simp_all [nndist_comm]

Goal state after:
case refine_2
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist a 0 ≤ nndist (Pi.single i a) (Pi.single j b)

case refine_3
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist b 0 ≤ nndist (Pi.single i a) (Pi.single j b)
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
hx' : a < x
⊢ False

Tactic:
· exact hx (ha hx'.le)

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ε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
h : ∀ᶠ (m : β × β) in atTop ×ˢ 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:
rw [prod_atTop_atTop_eq] at h

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.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
have S0m : ∀ n, (0 : ℝ) ∈ S n := fun n => ⟨⟨n, n⟩, ⟨le_rfl, le_rfl⟩, dist_self _⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
mem_ball',

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ dist a b < r ↔ ‖a⁻¹ * b‖ < r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

Tactic:
by
  simp only [← ofReal_norm']
  refine ⟨fun h ↦ ?_, fun h ↦ by congr⟩
  exact (Real.toNNReal_eq_toNNReal_iff (norm_nonneg' _) (norm_nonneg' _)).mp (ENNReal.coe_inj.mp h)

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖a / b‖ < r

Tactic:
mem_ball',

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ dist a b < r ↔ ‖a / b‖ < r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x ↦ b * x) ⁻¹' ball a r = ball (a / b) r

Tactic:
by
  ext c
  simp [dist_eq_norm_inv_mul, Set.mem_preimage, mem_ball, div_eq_mul_inv, mul_comm, mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ ∀ (t t' : Set α),
    IsClosed[inst✝³] t →
      IsClosed[inst✝³] t' →
        Icc a b ⊆ t ∪ t' → (Icc a b ∩ t).Nonempty → (Icc a b ∩ t').Nonempty → (Icc a b ∩ (t ∩ t')).Nonempty

Tactic:
by
      rintro s t hs ht hab ⟨x, hx⟩ ⟨y, hy⟩
      -- This used to use `wlog`, but it was causing timeouts.
      rcases le_total x y with h | h
      · exact isPreconnected_Icc_aux x y s t h hs ht hab hx hy
      · rw [inter_comm s t]
        rw [union_comm s t] at hab
        exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
m : ℤ
hm : g ^ m ∈ Ioc a (a * g)
⊢ ∃ c ∈ ↑S, c ∈ Ioo a b

Tactic:
refine ⟨g ^ m, zpow_mem hgS _, hm.1, hm.2.trans_lt ?_⟩

Goal state after:
case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
m : ℤ
hm : g ^ m ∈ Ioc a (a * g)
⊢ a * g < b
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 1 < g} a
⊢ Dense ↑S

Tactic:
by
  refine S.dense_of_not_isolated_one fun ε ε1 => ?_
  contrapose! H
  exact exists_isLeast_one_lt hbot ε1 (disjoint_left.2 H)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderInf α
inst✝ : InfConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ i, f i))

Tactic:
by convert! tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + t

Tactic:
by
  rcases h'.eq_or_lt with (rfl | hlt)
  · rcases eq_or_ne z ⊤ with (rfl | hz)
    · obtain rfl := htop rfl rfl
      simpa
    lift z to ℝ using ⟨hz, hbot⟩
    exact add_lt_add_right_coe h z
  · exact add_lt_add h hlt

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
⊢ -a ≤ 0 ↔ 0 ≤ a

Tactic:
EReal.neg_le,

Goal state after:
a : EReal
⊢ -0 ≤ a ↔ 0 ≤ a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x ↦ False) = ⊥

Tactic:
simp [blimsup_eq]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ emultiplicity p.asIdeal (I none ⊔ ⨆ b, I (some b)) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
emultiplicity_sup p ..,

Goal state after:
case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ min (emultiplicity p.asIdeal (I none)) (emultiplicity p.asIdeal (⨆ b, I (some b))) =
    ⨅ i, emultiplicity p.asIdeal (I i)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊥ ↔ ⊥ ≤ ⊥

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊥ - ↑a✝ ↔ ↑a✝ ≤ ⊥

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊤ ↔ ⊤ ≤ ⊥

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊥ ↔ ⊥ ≤ ↑a✝

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ↑a✝¹ - ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊤ ↔ ⊤ ≤ ↑a✝

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊥ ↔ ⊥ ≤ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊤ - ↑a✝ ↔ ↑a✝ ≤ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊤ ↔ ⊤ ≤ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊥ - ⊥ < 0 ↔ ⊥ < ⊥

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊥ - ↑a✝ < 0 ↔ ⊥ < ↑a✝

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊥ - ⊤ < 0 ↔ ⊥ < ⊤

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ↑a✝ - ⊥ < 0 ↔ ↑a✝ < ⊥

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ↑a✝¹ - ↑a✝ < 0 ↔ ↑a✝¹ < ↑a✝

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ↑a✝ - ⊤ < 0 ↔ ↑a✝ < ⊤

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊤ - ⊥ < 0 ↔ ⊤ < ⊥

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊤ - ↑a✝ < 0 ↔ ⊤ < ↑a✝

Tactic:
simp_all [← EReal.coe_sub]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊤ - ⊤ < 0 ↔ ⊤ < ⊤

Tactic:
simp_all [← EReal.coe_sub]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
⊢ limsup u f ≤ liminf u f

Tactic:
by_contra! hlt

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
⊢ False