mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hfu : f ↑u < 1
n : ℕ
hn : f ↑u ^ n < r
⊢ ∃ d, f ↑d < r

Tactic:
use u ^ n

Goal state after:
case h
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := ⋯
hu : u = if g < 1 then g else g⁻¹
hfu : f ↑u < 1
n : ℕ
hn : f ↑u ^ n < r
⊢ f ↑(u ^ n) < r
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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
n : R
hn : n ≠ 0
d : ↥R⁰
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    spanSingleton R⁰ (mk' K n d)

Tactic:
have hd_ne_zero : (algebraMap R K) (d : R) ≠ 0 :=
    map_ne_zero_of_mem_nonZeroDivisors _ (IsFractionRing.injective R K) d.property

Goal state after:
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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    spanSingleton R⁰ (mk' K n d)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 (r + s) ≤ max (0 r) (0 s)

Tactic:
simp only [Pi.zero_apply]; rw [max_eq_right]; rfl

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

Goal state before:
pp: p q : ℝ≥0∞
hpq : p ≤ q
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))
  · simpa using q.trichotomy
  rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)
  · simpa using p.trichotomy
  have hq' : 0 < q := lt_of_lt_of_le hp hpq
  have hp' : p < ∞ := lt_of_le_of_lt hpq hq
  simp [ENNReal.toReal_mono hq.ne hpq, ENNReal.toReal_pos_iff, hp, hp', hq', hq]

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

Goal state before:
pp: 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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0

Tactic:
rw [ne_eq, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h_a_ne_zero

Goal state after:
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : ¬a = 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iSup f).toReal = ⨆ i, (f i).toReal

Tactic:
by
  simp only [ENNReal.toReal, toNNReal_iSup hf, NNReal.coe_iSup]

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

Goal state before:
pp: 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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible

Goal state after:
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v (I * I') = count K v I + count K v I'
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inl
a c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
· have hc : c ≠ 0 := h0.neg_resolve_left rfl
    simp [div_zero hc]

Goal state after:
case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case negSucc
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 : FractionalIdeal R⁰ K
n : ℕ
⊢ -count K v (I ^ (↑n + 1)) = -(↑n + 1) * count K v I

Tactic:
← Int.natCast_succ,

Goal state after:
case negSucc
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 : FractionalIdeal R⁰ K
n : ℕ
⊢ -count K v (I ^ ↑n.succ) = -↑n.succ * count K v I
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
⊢ count K v ↑w.asIdeal = 0

Tactic:
have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible

Goal state after:
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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v ↑w.asIdeal = 0
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, edist a b < δ → edist (f a) (f b) < ε

Tactic:
by
  simp [ContinuousOn, continuousWithinAt_iff]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' eball a r = eball (↑a) r ∩ {a | p a}

Tactic:
by
  rw [← preimage_eball, image_preimage_eq_inter_range, range_val_subtype]

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

Goal state before:
pp: case mk.mk
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h :
  { toPseudoEMetricSpace := toPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ }.toEDist =
    { toPseudoEMetricSpace := toPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist
⊢ toPseudoEMetricSpace✝¹ = toPseudoEMetricSpace✝

Tactic:
ext1

Goal state after:
case mk.mk
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h :
  { toPseudoEMetricSpace := toPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ }.toEDist =
    { toPseudoEMetricSpace := toPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist
⊢ toPseudoEMetricSpace✝¹.toEDist = toPseudoEMetricSpace✝.toEDist
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mk.mk
α : Type u_2
inst✝ : TopologicalSpace α
toWeakPseudoEMetricSpace✝¹ : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toWeakPseudoEMetricSpace✝ : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h :
  { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ }.toEDist =
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist
⊢ toWeakPseudoEMetricSpace✝¹ = toWeakPseudoEMetricSpace✝

Tactic:
ext1

Goal state after:
case mk.mk
α : Type u_2
inst✝ : TopologicalSpace α
toWeakPseudoEMetricSpace✝¹ : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toWeakPseudoEMetricSpace✝ : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h :
  { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ }.toEDist =
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist
⊢ toWeakPseudoEMetricSpace✝¹.toEDist = toWeakPseudoEMetricSpace✝.toEDist
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ toPseudoMetricSpace✝¹ = toPseudoMetricSpace✝

Tactic:
ext1

Goal state after:
case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ toPseudoMetricSpace✝¹.toDist = toPseudoMetricSpace✝.toDist
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d ≤ dist a b + dist b c + dist c d

Tactic:
exact dist_triangle4 a b c d

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε

Tactic:
by
  simp [ContinuousOn, continuousWithinAt_iff]

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

Goal state before:
pp: case inr.inr
α : 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
⊢ sSup (a • s) = a • sSup s

Tactic:
by_cases h : BddAbove s

Goal state after:
case pos
α : 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
⊢ sSup (a • s) = a • sSup s

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
⊢ sSup (a • s) = a • sSup s
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inr
α : 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
⊢ sInf (a • s) = a • sSup s

Tactic:
by_cases h : BddAbove s

Goal state after:
case pos
α : 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
⊢ sInf (a • s) = a • sSup s

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
⊢ sInf (a • s) = a • sSup s
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
rw [← neBot_iff]; exact uniformity_basis_edist.cauchy_iff

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✝³] (Ioo a b)
hab : a < b
this : Icc a b = Ioo a b
⊢ False

Tactic:
Icc_eq_Ioo_same_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx : b ≤ x
⊢ f b ≤ f x

Tactic:
rcases hbx.eq_or_lt with rfl | hbx

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
b : α
hb : b ∈ s
hx : ClusterPt b (𝓟 s)
h'x : ContinuousWithinAt f s b
this : (𝓝[s] b).NeBot
hbx : b ≤ b
⊢ f b ≤ f b

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx✝ : b ≤ x
hbx : b < x
⊢ f b ≤ f x
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : PreconnectedSpace α
x y : α
hxy : x < y
this : (Iio y ∩ Ioi x).Nonempty
⊢ ∃ a, x < a ∧ a < y

Tactic:
by grind [Set.inter_nonempty_iff_exists_left]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
y : β
hyK : y ∈ K
z : α
x' : γ
y' : β
hy' : (x', y').2 ∈ K
h2y : sSup (f x' '' K) = f x' y
hy : ∀ y_1 ∈ K, f x' y_1 ≤ f x' y
this : (∀ a' < f x' y, ∀ᶠ (b : γ) in 𝓝 x', a' < f b y) ∧ ∀ a' > f x' y, ∀ᶠ (b : γ) in 𝓝 x', f b y < a'
hz : z > f x' y
⊢ (x', y') ∈ ↿f ⁻¹' Iio z

Tactic:
exact (hy y' hy').trans_lt hz

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
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
have := mem_image_of_mem f hc
  rw [h.image_Icc (hc.1.trans hc.2)] at this
  exact this.2

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b c : E
⊢ ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

Tactic:
simpa using norm_mul_le' (a / b) (b / c)

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:
← norm_inv' u

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
⊢ sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s

Tactic:
rw [compl_subset_comm]

Goal state after:
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_false, id, zpowers_eq_closure]

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 = closure {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✝³, inst✝²] ⇑e

Tactic:
by
  rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]
  rintro s ⟨a, rfl | rfl⟩
  · rw [e.preimage_Ioi]
    apply isOpen_lt'
  · rw [e.preimage_Iio]
    apply isOpen_gt'

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∀ x ∈ s, f x = ↑(f x).toNNReal

Tactic:
intro x hx
    exact (coe_toNNReal (hf x hx)).symm

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

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s : Finset ι
hf : (↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih => ?_
  simp only [Finset.prod_cons, ← ih (hf.mono <| by simp)]
  refine ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
    (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)
  · exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀
  · exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

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

Tactic:
exact ⟨{a | u a ≤ b}, ⟨b, by rintro _ ⟨a, ha, rfl⟩; exact ha⟩, hb⟩

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

Goal state before:
pp: case bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤

Tactic:
exfalso; exact h (Eq.refl ⊥)

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

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊤
h2 : x ≠ ⊤ ∨ y ≠ ⊥
⊢ -(x + y) = -x - y

Tactic:
by
  induction x <;> induction y <;> try tauto
  rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']

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

Goal state before:
pp: case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Tactic:
exact neg_nonneg.2 h

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

Goal state before:
pp: α : Type u_3
⊢ ⨅ x, 𝓟 (Ici {x}) ≤ atTop

Tactic:
refine
    le_iInf fun s =>
      le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_

Goal state after:
α : Type u_3
s : Finset α
⊢ ⋂ i, Ici {↑i} ⊆ Ici s
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_zero
⊢ -⊤ * 0 = -(⊤ * 0)

Tactic:
simp only [zero_mul, mul_zero, neg_zero]

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

Goal state before:
pp: case zero_top
⊢ -0 * ⊤ = -(0 * ⊤)

Tactic:
simp only [zero_mul, mul_zero, neg_zero]

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

Goal state before:
pp: case zero_bot
⊢ -0 * ⊥ = -(0 * ⊥)

Tactic:
simp only [zero_mul, mul_zero, neg_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mp
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ (∃ a, ∀ (b : Finset β), a ⊆ b → b.preimage ⇑f ⋯ ∈ s) → ∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s

Tactic:
rintro ⟨t, ht⟩

Goal state after:
case mp
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage ⇑f ⋯ ∈ s
⊢ ∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mpr
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ (∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s) → ∃ a, ∀ (b : Finset β), a ⊆ b → b.preimage ⇑f ⋯ ∈ s

Tactic:
rintro ⟨t, ht⟩

Goal state after:
case mpr
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset γ
ht : ∀ (b : Finset γ), t ⊆ b → b ∈ s
⊢ ∃ a, ∀ (b : Finset β), a ⊆ b → b.preimage ⇑f ⋯ ∈ s
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal

Tactic:
induction x <;> induction y
    <;> try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

Goal state after:
case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
⊢ (⊤ * ↑a✝).toENNReal = ⊤.toENNReal * (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: b c : EReal
hb : 0 ≤ b
a : ℝ≥0∞
⊢ (↑a + b) * c = ↑a * c + b * c

Tactic:
lift b to ℝ≥0∞ using hb

Goal state after:
c : EReal
a b : ℝ≥0∞
⊢ (↑a + ↑b) * c = ↑a * c + ↑b * c
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
by
  by_cases H : ∃ (j : Subtype p), s j = ∅
  · rw [if_pos H]
    rcases H with ⟨j, hj⟩
    simp [hv.liminf_eq_sSup_univ_of_empty j j.2 hj]
  rw [if_neg H]
  by_cases H' : ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i))
  · have A : ∀ (j : Subtype p), ⋂ (i : s j), Iic (f i) = ∅ := by
      simp_rw [← not_nonempty_iff_eq_empty, nonempty_iInter_Iic_iff]
      exact H'
    simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]
  rw [if_neg H']
  apply hv.liminf_eq_ciSup_ciInf
  · push Not at H
    simpa only [nonempty_iff_ne_empty] using H
  · push Not at H'
    exact H'

Goal state after: