mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case right
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ (↑n)⁻¹ * a < b

Tactic:
rw [← ENNReal.div_eq_inv_mul]

Goal state after:
case right
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ a / ↑n < b
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case e_toUniformSpace
α : Type u_2
ed : EDist α
edist_self✝¹ : ∀ (x : α), edist x x = 0
edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
ed' : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := ed, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    { toEDist := ed', edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U', uniformity_edist := hU' }.toEDist
⊢ U = U'

Tactic:
exact UniformSpace.ext (((show ed = ed' from h) ▸ hU).trans hU'.symm)

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α✝
α : Type u
edist : α → α → ℝ≥0∞
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
inst✝ : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle

Tactic:
by rfl

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

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
by
  lift x to ℝ≥0 using h'x
  lift y to ℝ≥0 using h'y
  have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
  obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) := by
    refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx
  refine ⟨n, ?_, ?_⟩
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
⊢ Continuous[(uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace,
      (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace]
    f

Tactic:
refine @Continuous.mk α β hα.toUniformSpace.toTopologicalSpace
      hβ.toUniformSpace.toTopologicalSpace f fun s hs ↦ ?_

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (f ⁻¹' s)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : ι → ℝ≥0∞
c : R
⊢ c • ⨆ i, f i = ⨆ i, c • f i

Tactic:
by
  simp only [← smul_one_mul c (f _), ← smul_one_mul c (iSup _), ENNReal.mul_iSup]

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddAbove s
⊢ 0 = a • sSup s

Tactic:
Real.sSup_of_not_bddAbove h,

Goal state after:
case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddAbove s
⊢ 0 = a • 0
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddAbove s
⊢ 0 = a • sSup s

Tactic:
Real.sSup_of_not_bddAbove h,

Goal state after:
case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddAbove s
⊢ 0 = a • 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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
⊢ ⊥ < J * ∏ x ∈ s \ {p}, x.asIdeal

Tactic:
bot_lt_iff_ne_bot,

Goal state after:
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
⊢ J * ∏ x ∈ s \ {p}, x.asIdeal ≠ ⊥
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)

Tactic:
rcases hab.lt_or_gt with hab | hab

Goal state after:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)

case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ico a b)

Tactic:
apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ι : Sort u_3
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (c i)
hc₂ : s ⊆ ⋃ i, c i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i

Tactic:
simpa only [ball, UniformSpace.ball, preimage_ofPred_eq, dist_comm]
    using uniformity_basis_dist.lebesgue_number_lemma hs hc₁ hc₂

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ico a b)
hab : a < b
this : closure[inst✝³] (Ico a b) = Ico a b
⊢ False

Tactic:
closure_Ico hab.ne,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ico a b)
hab : a < b
this : Icc a b = Ico a b
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by
  have hnonempty : (Ioo y x ∩ s).Nonempty := by
    obtain ⟨z, hyz, hzx⟩ := hs.exists_between hy
    exact ⟨z, mem_inter hzx hyz⟩
  have hx : IsLUB (Ioo y x ∩ s) x := hs.isLUB_inter_iff isOpen_Ioo |>.mpr <| isLUB_Ioo hy
  apply hx.exists_seq_strictMono_tendsto_of_notMem (by simp) hnonempty |>.imp
  simp_all

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

Goal state before:
pp: case h'
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
⊢ x c < y (f (x c))

Tactic:
rw [hfx _ hc]

Goal state after:
case h'
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
⊢ x c < y c
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous[inst✝⁴, inst✝²] f
hg : Continuous[inst✝⁴, inst✝²] g
ha : f a ≤ g a
hb : g b ≤ f b
⊢ ∃ x, f x = g x

Tactic:
obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty :=
    isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg)
      (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩

Goal state after:
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous[inst✝⁴, inst✝²] f
hg : Continuous[inst✝⁴, inst✝²] g
ha : f a ≤ g a
hb : g b ≤ f b
x : X
left✝ : x ∈ univ
hfg : f x ≤ g x
hgf : g x ≤ f x
⊢ ∃ x, f x = g x
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
rcases (hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
⊢ ∃ x ∈ s, IsMinOn f s x
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 : α × β) (r : ℝ), IsCompact (closedBall x r)

Tactic:
rintro ⟨x, y⟩ r

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, y) r)
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]

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

Goal state before:
pp: case refine_4
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Surjective
    ⇑((Submodule.comap (↑I).subtype ↑J).mapQ (Submodule.comap (↑I').subtype ↑J')
        (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ⋯)

Tactic:
have H : Submodule.map (Algebra.lsmul R R K (I'.divMod I J')) ↑I =
        (spanSingleton R⁰ (I'.divMod I J') * I) := by
      ext x
      simp [Submodule.mem_span_singleton_mul]

Goal state after:
case refine_4
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ Surjective
    ⇑((Submodule.comap (↑I).subtype ↑J).mapQ (Submodule.comap (↑I').subtype ↑J')
        (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ⋯)
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y

Tactic:
grind [inter_assoc, inter_eq_self_of_subset_right, Icc_subset_Icc_right]

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
⊢ Icc a b ⊆ s

Tactic:
by
  intro y hy
  have : IsClosed (s ∩ Icc y b) := by
    suffices s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b from this ▸ hs.inter isClosed_Icc
    grind [Icc_subset_Icc_left, inter_eq_self_of_subset_right, inter_assoc]
  exact IsClosed.mem_of_ge_of_forall_exists_lt this hb hy.2 fun x hx ↦
    hgt x ⟨hx.1, Ioc_subset_Ioc_left hy.1 hx.2⟩ y hx.2.1

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
⊢ map (algebraMap S R) p = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

Tactic:
have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
  rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
  let hF : Fintype {v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} :=
    (finite_factors h).fintype
  rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
  · let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF
    refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
    have : v.asIdeal.LiesOver p := by rwa [Ideal.liesOver_iff_dvd_map v.2.ne_top]
    simp [maxPowDividing_eq_pow_multiset_count _ h, ramificationIdx_eq_factors_count p v h]
  · intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv

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

Goal state before:
pp: case pos
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
u : α
hu : u ∈ Ioo ⊥ a ∧ f u = f b
⊢ False

Tactic:
hf_i hu.2

Goal state after:
case pos
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
u : α
hu : b ∈ Ioo ⊥ a ∧ f b = f b
⊢ False
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedCancelAddMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atTop

Tactic:
by
  refine tendsto_atTop.mpr fun s => ?_
  obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul_left hr.le ha)

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
replace hn : s ≤ (n : ℤ) • r := by simpa

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ ↑n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
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
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
hd : Dense ↑s
⊢ Xor (Dense ↑s) (∃ a, s = zpowers a)

Tactic:
simp only [hd, xor_true]

Goal state after:
G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
hd : Dense ↑s
⊢ ¬∃ a, s = zpowers a
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ Continuous[inst✝³, Preorder.topology β] ⇑e

Tactic:
continuous_generateFrom_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[inst✝³] (⇑e ⁻¹' s)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
constructor
  · rintro ⟨b, hb⟩
    exact ⟨{a | u a ≤ b}, ⟨b, by rintro _ ⟨a, ha, rfl⟩; exact ha⟩, hb⟩
  · rintro ⟨s, ⟨b, hb⟩, hs⟩
    exact ⟨b, hs.mono <| by simpa [upperBounds] using hb⟩

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

Goal state before:
pp: x y : EReal
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
simp [bot_lt_iff_ne_bot]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SupConvergenceClass α

Tactic:
refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, b < ↑b_1

case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, ↑b_1 < b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
a c : EReal
b : ℝ
hb : ↑b ≠ ⊥ ∨ c ≠ ⊥
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ↑b ↔ a + ↑b ≤ c

Tactic:
rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]

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

Goal state before:
pp: a b c : EReal
hb : b ≠ ⊥ ∨ c ≠ ⊥
ht : b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - b ↔ a + b ≤ c

Tactic:
induction b with

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

Goal state before:
pp: a b c : EReal
hc : c < a + b
⊢ ∃ a' < a, c < a' + b

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (sub_lt_of_lt_add hc)
  refine ⟨a', ha', (sub_lt_iff (.inl ?_) (.inr hc.ne_top)).1 hc'⟩
  contrapose! hc
  exact hc ▸ (add_bot a).symm ▸ bot_le

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

Goal state before:
pp: x : EReal
h : 0 < x
⊢ x * ⊤ = ⊤

Tactic:
exact mul_top_of_pos h

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
⊢ Tendsto Finset.powerset atTop atTop

Tactic:
refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩
  exact Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu

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

Goal state before:
pp: a b : EReal
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
by
  nth_rw 1 [← neg_zero]
  rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]

Goal state after: