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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x ↦ max a (f x)

Tactic:
by
  simpa [max_comm] using (hf.max_const a)

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
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
x : α
hx : x ∈ s
⊢ f x = g x

Tactic:
refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
x : α
hx : x ∈ s
⊢ g x ≤ f x
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ -(-b ⊓ b)

Tactic:
neg_le_neg_iff,

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -b ⊓ b ≤ -a ⊓ a
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ ‖a‖ ≤ ‖b‖

Tactic:
apply solid
  rw [abs]
  nth_rw 1 [← neg_neg a]
  rw [← neg_inf]
  rw [abs]
  nth_rw 1 [← neg_neg b]
  rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|

Tactic:
inf_comm c,

Goal state after:
case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊓ c - c ⊓ d| ≤ |b - d|
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoMetricSpace M
inst✝ : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ dist (a / c) (b / c) = dist a b

Tactic:
simp only [div_eq_mul_inv, dist_mul_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ↑(ratio f)⁻¹ * ediam (⇑f '' s)

pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ratio f ≠ 0

Tactic:
exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : {x | f x ≠ g x}.Countable
t : Set β
ht : MeasurableSet t
this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (f ⁻¹' t ∩ {x | f x = g x})

Tactic:
exact (hf ht).inter h.measurableSet.of_compl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
inter_eq_compl_compl_union_compl

Goal state after:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet s

Tactic:
by rwa [← insert_eq_of_mem ha]

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : ¬x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
· simpa only [hx, ← preimage_compl, Prop.compl_singleton, not_true, preimage_singleton_false]
      using h.compl

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ μ (⋃ i, t i) = μ (⋃ i, disjointed t i)

Tactic:
by rw [iUnion_disjointed]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
⊢ μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0

Tactic:
by
  refine ⟨fun h i hi ↦ measure_mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩
  have _ := hI.to_subtype
  simpa [h] using measure_iUnion_le (μ := μ) fun x : I ↦ s x

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

Goal state before:
pp: case hbc
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖f (n • x)‖ < C

Tactic:
refine hC _ <| norm_nsmul_le.trans_lt ?_

Goal state after:
case hbc
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ↑n * ‖x‖ < δ
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
⊢ ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩

Tactic:
intro i j x hxi hxj

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
i j : ι
x : α
hxi : x ∈ t i
hxj : x ∈ t j
⊢ g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case refine_2
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
x : α
hx : x ∈ s
⊢ (∑ b ∈ univ.sigma fun a ↦ range (f ↑a).natAbs, if (fun a ↦ ↑a.fst) b = x then ↑((fun a ↦ sign (f ↑a.fst)) b) else 0) =
    f x

Tactic:
simp [sum_sigma, hx, ← Int.sign_eq_sign, Int.sign_mul_abs, mul_comm |f _|,
      sum_attach (s := s) (f := fun y => if y = x then f y else 0)]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
· simp [h, h.not_ge]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ sign a ≤ 0 ↔ a ≤ 0

pp: case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ sign a ≤ 0 ↔ a ≤ 0

pp: case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
· simp [h, h.not_ge]

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ sign a ≤ 0 ↔ a ≤ 0

case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
⊢ LowerSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
by
  simp [semicontinuousAt_iff_frequently]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
⊢ UpperSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≥ y) → f x ≥ y

Tactic:
by
  simp [semicontinuousAt_iff_frequently]

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

Goal state before:
pp: a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ a / b * b = a

Tactic:
mul_comm (a / b) b,

Goal state after:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ b * (a / b) = a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ - -(a' * b⁻¹) ≤ - -(a * b⁻¹)

Tactic:
neg_le_neg_iff,

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ -(a * b⁻¹) ≤ -(a' * b⁻¹)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : ⊤ ≠ ⊤ ∨ 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c

Tactic:
rw [ne_self_iff_false, false_or] at h₂; rw [top_mul_of_pos h₂] at hc; exact (not_top_lt hc).rec

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

Goal state before:
pp: ⊢ (range ENNReal.toEReal).OrdConnected

Tactic:
by
    rw [range_coe_ennreal]; exact ordConnected_Ici

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
⊢ μ (⋃ i, s i) ≤ ∑' (a : ℕ) (i : ℕ), m (f a i)

Tactic:
← ENNReal.tsum_prod,

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
⊢ μ (⋃ i, s i) ≤ ∑' (p : ℕ × ℕ), m (f p.1 p.2)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ 0 < ?m.77

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ c ≠ ⊤

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ 0 < ?m.121

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ 0 ≤ -c

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ -c ≠ ⊤

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ 0 ≤ c

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ c ≠ ⊤

Tactic:
by aesop

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

Goal state before:

Tactic:
y < f x + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (min_le_left _ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
have := aux_hasSum_of_le_geometric hr hu
  convert! dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n
  simp only [pow_add, mul_left_comm C, mul_div_right_comm]
  rw [mul_comm]
  exact (this.mul_left _).tsum_eq.symm

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

Goal state before:
pp: case insert
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : ι
s✝ : Finset ι
ia : a✝ ∉ s✝
IH : (∀ i ∈ s✝, LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun z ↦ ∑ i ∈ s✝, f i z) s x
ha : ∀ i ∈ insert a✝ s✝, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z ↦ f a✝ z + ∑ i ∈ s✝, f i z) s x

Tactic:
exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

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

Goal state before:
pp: R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun x ↦ ↑⌊a * x⌋₊ / x) atTop (𝓝 a)

Tactic:
have A : Tendsto (fun x : R ↦ a - x⁻¹) atTop (𝓝 (a - 0)) :=
    tendsto_const_nhds.sub tendsto_inv_atTop_zero

Goal state after:
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 (a - 0))
⊢ Tendsto (fun x ↦ ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' (s ∩ t)).Nonempty
⊢ f ⁻¹' (s ∩ t) ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ m (⋃ i, s i) = ∑' (i : ℕ), m (s i)

Tactic:
refine le_antisymm (measure_iUnion_le s) ?_

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), m (s i) ≤ m (⋃ i, s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case refine_3
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ ∑' (i : ℕ), m ((fun i ↦ f i ∩ s) i) + ∑' (i : ℕ), m ((fun i ↦ f i \ s) i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
rw [← ENNReal.tsum_add]
    exact ENNReal.tsum_le_tsum fun i => hs _

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

Goal state before:
pp: case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = sᶜ

Tactic:
(Tactic.tacticSeq1Indented
 [(Mathlib.Tactic.useSyntax
   "use"
   []
   (group)
   [(choice
     («term{_}» "{" [`False] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `False []) [])])
      (Term.optEllipsis [])
      []
      "}"))])])

Goal state after:
case h
α : Type u_1
s : Set α
⊢ (fun x ↦ x ∈ s) ⁻¹' {False} = sᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (trim 0) s = 0 s

Tactic:
exact nonpos_iff_eq_zero.1 <| (measure_mono (subset_univ s)).trans_eq <| trim_eq _ .univ

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

Goal state before:
pp: α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : c • 1 = 0 ∨ ν s = 0
⊢ c • 1 = 0 ∨ μ s = 0

Tactic:
exact hνs.imp_right fun hs ↦ h hs

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise Disjoint
h : ∀ s ∈ S, MeasurableSet s
⊢ μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion hs hd h]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
ht : ∀ t ∈ C, μ (s ∩ t) = 0
⊢ μ s = 0

Tactic:
obtain ⟨t, ht1, ht2⟩ := hC
  rw [show s = ⋃ n, s ∩ t n by rw [← inter_iUnion, ht2, inter_univ], measure_iUnion_null_iff]
  exact fun i => ht (t i) (ht1 i)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Tactic:
have hts : μ (t \ s) ≠ ∞ := (measure_lt_top_of_subset sdiff_subset ht').ne

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
y : α
⊢ y ∈ s ↔ y ∈ ⋃ x ∈ s, measurableAtom x

Tactic:
simp only [mem_iUnion, exists_prop]

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
y : α
⊢ y ∈ s ↔ ∃ i ∈ s, y ∈ measurableAtom i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), (μ.restrict t) (f i) = (ν.restrict t) (f i)
⊢ (μ.restrict t) (⋃ i, f i) = (ν.restrict t) (⋃ i, f i)

Tactic:
simp only [measure_iUnion hfd hfm, ihf]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
simp_rw [mem_map, mem_ae_iff]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ μ (s.indicator f ⁻¹' t)ᶜ = 0 ↔ (μ.restrict s) (f ⁻¹' t)ᶜ = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ MeasurableSet (measurableAtom x)

Tactic:
measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ MeasurableSet (countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
⊢ AEMeasurable f μ

Tactic:
have hvμ : μ v = 0 := (measure_biUnion_null_iff hSc).2 fun s hs ↦ ae_le_set.1 <|
    ((hUeq s hs).trans (hTeq s hs).symm).le

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ae μ = ⊥ ↔ μ = 0

Tactic:
rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on Iic) s

Tactic:
· exact directedOn_iff_directed.2 (hdir.directed_val.mono_comp _ fun x y => Iic_subset_Iic.2)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
this✝ : ∀ (s : Set α), MeasurableSet s
this : ∀ (s : Set α), MeasurableSet s
⊢ inst✝³ = borel α

Tactic:
by aesop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
h : OpensMeasurableSpace α
p : α → Prop
⊢ borel (Subtype p) ≤ instMeasurableSpace

Tactic:
borel_comap

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
h : OpensMeasurableSpace α
p : α → Prop
⊢ MeasurableSpace.comap val (borel α) ≤ instMeasurableSpace
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a ↦ (∏ c ∈ s, f c) a

Tactic:
exact Finset.prod_induction _ _ (fun _ _ => Measurable.mul) (@measurable_one M _ _ _ _) hf

Goal state after: