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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ closure[inst✝¹] s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
← seqClosure_eq_closure

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ seqClosure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst✝¹] s
⊢ a ∈ closure[inst✝²] (f ⁻¹' s) → b ∈ s

Tactic:
← seqClosure_eq_closure

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst✝¹] s
⊢ a ∈ seqClosure (f ⁻¹' s) → b ∈ s
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
by_cases! hm : ∃ m, ∃ᶠ n in atTop, y n ∈ closure {x m}

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∃ m, ∃ᶠ (n : ℕ) in atTop, y n ∈ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : m ∈ s
⊢ m ≤ l.length

Tactic:
rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : m ∈ s
⊢ ¬L.length ≤ m
Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝³ : SMul M X
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul M X
⊢ Continuous[instTopologicalSpaceProd, _] ((fun p ↦ p.1 • p.2) ∘ Prod.map id mk)

Tactic:
exact continuous_mk.comp continuous_smul

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
induction a with
  | top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb]
  | coe a =>
    induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩

Goal state after:
case inl.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, x i < ↑q

case inl.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, ↑(q + 1) < x i
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hxa : x < a
⊢ IccExtend h (f ∘ Subtype.val) x = f x

Tactic:
simp [IccExtend_of_le_left _ _ hxa.le, ha x hxa]

Goal state after:
Module: Mathlib.Topology.Bornology.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
f g : LocallyBoundedMap α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    cases f
    cases g
    congr

Goal state after:
Module: Mathlib.Topology.Algebra.UniformMulAction

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ m • n • x = n • m • x

Tactic:
rw [hmn, hnm, map_comp, map_comp]

Goal state after:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ Completion.map (SMul.smul m ∘ SMul.smul n) x = Completion.map (SMul.smul n ∘ SMul.smul m) x

case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)

case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)

case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)

case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
⊢ limsup (fun i ↦ c - f i) F = c - liminf f F

Tactic:
by
  rcases F.eq_or_neBot with rfl | _
  · simp
  · exact (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z - ↑K * dist y z ≤ f ↑t + ↑K * dist y ↑t

Tactic:
rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z ≤ f ↑t + ↑K * (dist y z + dist y ↑t)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b c : E
⊢ dist a (b / c) = dist (a * c) b

Tactic:
← dist_mul_right _ _ c,

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b c : E
⊢ dist (a * c) (b / c * c) = dist (a * c) b
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵢ Y
⊢ ∀ (x y : X), edist (e.toFun x) (e.toFun y) = ↑1 * edist x y

Tactic:
by simpa using! e.isometry

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃₀ s)

Tactic:
sUnion_eq_biUnion

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃ i ∈ s, i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
p : α → Prop
inst✝ : MeasurableSingletonClass α
x : Subtype p
⊢ val ⁻¹' {↑x} = {x}

Tactic:
rw [← image_singleton, preimage_image_eq _ Subtype.val_injective]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ ⊤ (f '' s) = ⊤ s

Tactic:
top_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ ⊤ (f '' s) = ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤ MeasurableSpace.comap (fun b c ↦ g c b) pi

Tactic:
by
  simpa only [pi, comap_iSup] using le_iSup_of_le a <| by measurability

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

Goal state before:
pp: case hf
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)

pp: case hd
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ Summable d

Tactic:
· exact_mod_cast hf

Goal state after:
case hd
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ Summable d
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∀ (i : ι), p i a}

Tactic:
by
    rw [ofPred_forall]; exact MeasurableSet.iInter fun i ↦ (hp i).setOf

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a b : SignType
⊢ Decidable (a ≤ b)

Tactic:
cases a <;> cases b <;> first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (x y : SignType), -x * y = -(x * y)

Tactic:
rintro ⟨_⟩ ⟨_⟩ <;> rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (x y : SignType), x * -y = -(x * y)

Tactic:
rintro ⟨_⟩ ⟨_⟩ <;> rfl

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

Goal state before:
pp: case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ ↑(sign x) * ↑x.abs = ↑(sign y) * ↑y.abs

Tactic:
habs,

Goal state after:
case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ ↑(sign x) * ↑y.abs = ↑(sign y) * ↑y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ {i | ε ≤ a i}.Finite

Tactic:
by_contra h
  have := Infinite.to_subtype h
  refine tsum_ne_top (top_unique ?_)
  calc ∞ = ∑' _ : { i | ε ≤ a i }, ε := (tsum_const_eq_top_of_ne_zero ε_ne_zero).symm
  _ ≤ ∑' i, a i := ENNReal.summable.tsum_le_tsum_of_inj (↑)
    Subtype.val_injective (fun _ _ => zero_le) (fun i => i.2) ENNReal.summable

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

Goal state before:
pp: a : EReal
⊢ a / 0 = 0

Tactic:
change a * 0⁻¹ = 0

Goal state after:
a : EReal
⊢ a * 0⁻¹ = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ b * a = a * b

Tactic:
mul_comm a b

Goal state after:
case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ b * a = b * a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ a * b ≤ c

Tactic:
mul_comm a b

Goal state after:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ a * b < c

Tactic:
mul_comm a b

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
hfs : LowerSemicontinuousOn f s
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
rw [lowerSemicontinuousOn_iff_preimage_Iic] at hfs
  obtain ⟨v, hv, hv'⟩ := hfs c
  exact hv' ▸ ks.inter_right hv

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h'
⊢ ∀ (i' : ℝ), ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ ↑i'

Tactic:
refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩

Goal state after:
case h'
x✝¹ : ℝ
x : EReal
x✝ : x ∈ Iic ↑x✝¹ ∩ {⊥}ᶜ
h1 : x ≤ ↑x✝¹
h2 : x ∈ {⊥}ᶜ
⊢ x ∈ Ioc ⊥ ↑x✝¹
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x : EReal
h_top : x = ⊤
⊢ ContinuousAt toENNReal x

Tactic:
simp only [ContinuousAt, h_top, toENNReal_top]
    refine ENNReal.tendsto_nhds_top fun n ↦ ?_
    filter_upwards [eventually_gt_nhds (coe_lt_top n)] with y hy
    exact toENNReal_coe (x := n) ▸ toENNReal_lt_toENNReal (coe_ennreal_nonneg _) hy

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
⊢ ∃ a, b ≤ |r| ^ a

Tactic:
obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_gt hr_le) hr))

Goal state after:
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
n : ℕ
hn : b < |r| ^ n
⊢ ∃ a, b ≤ |r| ^ a
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

Tactic:
simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Tactic:
exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
· positivity

Goal state after:
case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case h
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n

Tactic:
split_ifs with hn1 hn2 h

Goal state after:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
⊢ f1 n ∩ f2 n ∈ π n

case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∉ p2
⊢ f1 n ∩ univ ∈ π n

case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n

case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), d.Has (f i)
⊢ d.Has (⋃ i, disjointed f i)

Tactic:
exact
      d.has_iUnion (disjoint_disjointed _) fun n =>
        disjointedRec (fun (t : Set α) i h => h_inter _ _ h <| d.has_compl <| hf i) (hf n)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : x ∈ s i → ∀ x_1 ∈ {i}ᶜ, x ∉ s x_1
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)

Tactic:
exact (hU hi j hne.symm hj).elim

Goal state after:
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃₀ s) μ

Tactic:
sUnion_eq_biUnion

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃ i ∈ s, i) μ
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Fintype α
μ : Measure (α × β)
y : β
⊢ μ (Prod.snd ⁻¹' {y}) = ∑ x, μ {(x, y)}

Tactic:
rw [measure_preimage_snd_singleton_eq_tsum μ y, tsum_fintype]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ ν s = 0 → μ s = 0

Tactic:
by
    rw [measure_eq_zero_iff_ae_notMem, measure_eq_zero_iff_ae_notMem]
    exact fun hs => h hs

Goal state after: