mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a + ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a

Tactic:
← sum_attach (filter ..)

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a +
      ∑ x ∈ {x ∈ s.powerset | ¬x.Nonempty}.attach, (-1) ^ #↑x • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ (s.biUnion S)ᶜ, f a = ∑ a, f a - ∑ a ∈ s.biUnion S, f a

Tactic:
eq_sub_iff_add_eq,

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ (s.biUnion S)ᶜ, f a + ∑ a ∈ s.biUnion S, f a = ∑ a, f a
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
s : Set ℝ
hn : s.Nonempty
⊢ sSup (-s) = -sInf s

Tactic:
by_cases hb : BddBelow s

Goal state after:
case pos
s : Set ℝ
hn : s.Nonempty
hb : BddBelow s
⊢ sSup (-s) = -sInf s

case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : ↑q ∈ Ioi x
⊢ ⨅ q, f ↑↑q ≤ f ↑q

Tactic:
mem_Ioi

Goal state after:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
⊢ ⨅ q, f ↑↑q ≤ f ↑q
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: x y : ℝ≥0∞
⊢ x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0

Tactic:
by
  simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff]

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

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1 + if y = 0 then 0 else 1

Tactic:
refine le_add_of_le_of_nonneg ?_ ?_

Goal state after:
case neg.refine_1
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1

case neg.refine_2
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ 0 ≤ if y = 0 then 0 else 1
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✝ p q : NonarchAddGroupSeminorm E
⊢ max (p 0) (q 0) = 0

Tactic:
← map_zero p,

Goal state after:
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✝ p q : NonarchAddGroupSeminorm E
⊢ max (p 0) (q 0) = p 0
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ p = ∞ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal

Tactic:
simpa using ENNReal.trichotomy₂ (Fact.out : 1 ≤ p)

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

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1 + if y = 1 then 0 else 1

Tactic:
refine le_add_of_le_of_nonneg ?_ ?_

Goal state after:
case neg.refine_1
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1

case neg.refine_2
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ 0 ≤ if y = 1 then 0 else 1
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
h : a * b ≠ ∞
ha : a ≠ 0
⊢ b * a ≠ ∞

Tactic:
by rwa [mul_comm]

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

Goal state before:
pp: a c : ℝ≥0∞
hac : a < c
⊢ ⨅ b, ⨅ (_ : a < b), b < c

Tactic:
obtain ⟨d, had, hdc⟩ := exists_between hac

Goal state after:
a c : ℝ≥0∞
hac : a < c
d : ℝ≥0∞
had : a < d
hdc : d < c
⊢ ⨅ b, ⨅ (_ : a < b), b < c
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x.toENNReal ≠ 0 ↔ 0 < x

Tactic:
by
  simp [toENNReal_eq_zero_iff.not]

Goal state after:
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

Tactic:
rw [if_pos (And.intro (pow_ne_zero n hI) hI), h, Nat.cast_add,
        Nat.cast_one]
      ring

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b * c
⊢ a < c * b

Tactic:
by rwa [mul_comm]

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
n : ℤ
⊢ count K v (↑v.asIdeal ^ n) = n

Tactic:
rw [count_zpow, count_self, mul_one]

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

Goal state before:
pp: y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
⊢ Ioo 0 ∞ = ⋃ n, Ico (y ^ n) (y ^ (n + 1))

Tactic:
ext x
  simp only [mem_iUnion, mem_Ioo, mem_Ico]
  constructor
  · rintro ⟨hx, h'x⟩
    exact exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y
  · rintro ⟨n, hn, h'n⟩
    constructor
    · apply lt_of_lt_of_le _ hn
      exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _
    · apply lt_trans h'n _
      exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝¹ : Subsingleton α
inst✝ : NeZero ε
⊢ IsEmpty ↑(sphere x ε)

Tactic:
rw [sphere_eq_empty_of_subsingleton (NeZero.ne ε)]

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝¹ : Subsingleton α
inst✝ : NeZero ε
⊢ IsEmpty ↑∅
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sSup s

Tactic:
rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sInf s

Tactic:
rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0

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
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ Ideal.span {∑ p ∈ s, a p} ≤ J

Tactic:
Ideal.span_singleton_le_iff_mem

Goal state after:
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
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ ∑ p ∈ s, a p ∈ J
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
this : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
exact UniformSpace.secondCountable_of_separable α

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

Goal state before:
pp: c : ℝ
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
by_cases! c_pos : 0 < c
  · convert! NNReal.ball_zero_eq_Ico' (NNReal.mk c c_pos.le)
    simp [Real.toNNReal, c_pos.le]
  simp [c_pos]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
i : PseudoMetricSpace (α × β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun x y ↦ max (dist x.1 y.1) (dist x.2 y.2)) ⋯ ⋯
s : Set (α × β)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
simp only [← isBounded_image_fst_and_snd, isBounded_iff_eventually, forall_mem_image, ←
      eventually_and, ← forall_and, ← max_le_iff]
    rfl

Goal state after:
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
⊢ closure[inst✝³] (Ico a b) ⊆ Icc a b

Tactic:
exact closure_minimal Ico_subset_Icc_self isClosed_Icc

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
simp [hd, dist_triangle]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
simp [hd, dist_triangle]

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

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ ↑(Ideal.span {↑c.den} * a.num) + ↑(Ideal.span {x}) = ↑(c.num * Ideal.span {↑a.den})

Tactic:
← hx,

Goal state after:
case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ ↑(Ideal.span {↑c.den} * a.num) + ↑(Ideal.span {x}) = ↑(Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x})
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u

Tactic:
rcases hx xs u hu with ⟨v, vs, xv, fvu⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x ∈ s, Iic x).Nonempty

Tactic:
rw [biInter_eq_iInter]

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x, Iic ↑x).Nonempty
Module: Mathlib.Topology.Order.IntermediateValue

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

Tactic:
by_cases hb : BddBelow s

Goal state after:
case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
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
⊢ Icc a b ⊆ s

Tactic:
intro y hy

Goal state after:
α : 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
⊢ y ∈ s
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:
intro y hy

Goal state after:
α : 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
y : α
hy : y ∈ Icc a b
⊢ y ∈ s
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
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 α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atTop
⊢ Ioi (f a) ⊆ f '' Ioi a

Tactic:
intro y hy

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atTop
y : δ
hy : y ∈ Ioi (f a)
⊢ y ∈ f '' Ioi a
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atBot
⊢ Iio (f a) ⊆ f '' Ioi a

Tactic:
intro y hy

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atBot
y : δ
hy : y ∈ Iio (f a)
⊢ y ∈ f '' Ioi a
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atBot
⊢ Iio (f a) ⊆ f '' Iio a

Tactic:
intro y hy

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atBot
y : δ
hy : y ∈ Iio (f a)
⊢ y ∈ f '' Iio a
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atTop
⊢ Ioi (f a) ⊆ f '' Iio a

Tactic:
intro y hy

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atTop
y : δ
hy : y ∈ Ioi (f a)
⊢ y ∈ f '' Iio a
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun a ↦ x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧ Bornology.IsBounded a)
    id

Tactic:
simp_rw [← and_assoc]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis
    (fun a ↦ (x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a) ∧ Bornology.IsBounded a) id
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 : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atBot

Tactic:
by simpa using hf.atTop_zsmul_const (neg_pos.2 hr)

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Ioi a)

Tactic:
rw [e.preimage_Ioi]
    apply isOpen_lt'

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
⊢ 0 ≤ U

Tactic:
obtain ⟨y, y_0, y_U⟩ := (h₁.and_eventually hU).exists

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
y : ι
y_0 : 0 ≤ u y
y_U : u y ≤ U
⊢ 0 ≤ U
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
⊢ ∃ᶠ (x' : S) in map f F, f l ≤ x'

Tactic:
refine fun ev ↦ freq_ge ?_
  simp only [not_le] at ev freq_ge ⊢
  filter_upwards [ev] with z hz
  by_contra con
  exact lt_irrefl (f l) <| lt_of_le_of_lt (f_incr <| not_lt.mp con) hz

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
⊢ ∀ (y : EReal), ↑x = y → recENNReal coe neg_coe y ≍ coe x

Tactic:
intro y hy

Goal state after:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
y : EReal
hy : ↑x = y
⊢ recENNReal coe neg_coe y ≍ coe x
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
h : ¬(Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ c

Tactic:
filter_upwards [(tendsto_order.1 h_limsup).2 b hb] with r hr
      contrapose! h
      exact ⟨limsup (u · r) cofinite, h, hr⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∃ a, ∀ (b : ℕ), a ≤ b → u b < x + ε
⊢ ∃ n, u ↑n < x + ε

Tactic:
obtain ⟨n, hn⟩ := h

Goal state after:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → u b < x + ε
⊢ ∃ n, u ↑n < x + ε