mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ a / f b = 1 / f b * a

Tactic:
div_mul_eq_mul_div,

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ a / f b = 1 * a / f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), (s₁, s₂) ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
g : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ 1 < ∏'[L] (i : ι), g i

Tactic:
rw [← tprod_one (L := L)]

Goal state after:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
g : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏'[L] (x : ι), 1 < ∏'[L] (i : ι), g i
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∏'[L] (b : β), f b = f b

Tactic:
by
  rw [tprod_eq_prod (s := {b}), prod_singleton]
  exact fun b' hb' ↦ hf b' (by simpa using hb')

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
a✝ : ℕ
hx : Int.negSucc a✝ ∈ u
⊢ a✝ ∈ u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯

Tactic:
by simpa using Or.inr hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
⊢ mulSupport f = g '' mulSupport (f ∘ g)

Tactic:
rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
| fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b

Tactic:
ext _

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
x✝ : Finset ι
| ∏ b ∈ x✝, (fun x ↦ 1 + f x) b
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ pkg.extend f = g

Tactic:
apply pkg.funext pkg.continuous_extend hg.continuous

Goal state after:
α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ ∀ (a : α), pkg.extend f (pkg.coe a) = g (pkg.coe a)
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
y : α
⊢ BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)

Tactic:
rcases hs with ⟨z, hz⟩

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
⊢ BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
K : ℝ≥0
h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
x y : E
⊢ dist x y ≤ ↑K * dist (f x) (f y)

Tactic:
simpa only [dist_eq_norm_inv_mul, map_inv, map_mul] using h (x⁻¹ * y)

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x ↦ TProd.mk l (TProd.elim' h x)) ⁻¹' Set.tprod l t = Set.tprod l t

Tactic:
simp only [TProd.mk_elim hnd h]

Goal state after:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x ↦ x) ⁻¹' Set.tprod l t = Set.tprod l t
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ Measurable f

Tactic:
apply measurable_to_countable'

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x : β
⊢ x ∈ measurableAtom x

Tactic:
by
  simp +contextual [measurableAtom]

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
⊢ ↑n * ‖x‖ < δ

Tactic:
simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ

Goal state after:
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:
rcases eq_or_ne i j with rfl | hij

Goal state after:
case inl
α : 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 : ι
x : α
hxi hxj : x ∈ t i
⊢ g' i ⟨x, hxi⟩ = g' i ⟨x, hxj⟩

case inr
α : 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
hij : i ≠ j
⊢ g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
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 α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableSet (diagonal α)

Tactic:
← Set.range_diag,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableSet (range Function.diag)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑univ) (x_1 : ↑(t ↑x)), f ↑x_1

Tactic:
← ENNReal.tsum_biUnion' h,

Goal state after:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑(⋃ i ∈ univ, t i)), f ↑x
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.neg
x y : EReal
h : ↑neg * ↑x.abs ≤ ↑neg * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs

Tactic:
left; simpa using h

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

Goal state before:
pp: a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
⊢ ∃ m, ↑a * ↑n ≤ ↑m

Tactic:
obtain ⟨m, an_m⟩ := exists_nat_ge (a * n)

Goal state after:
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ ∃ m, ↑a * ↑n ≤ ↑m
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hf : Summable f
i : α
⊢ ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x

Tactic:
refine (NNReal.summable_of_le (fun i' => ?_) hf).tsum_eq_add_tsum_ite' i
  rw [Function.update_apply]
  split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), (∃ᶠ (x' : α) in 𝓝[s] x, x_1ᶜ ∉ 𝓝ˢ (f x')) → x_1ᶜ ∉ 𝓝ˢ (f x)) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
simp [← subset_interior_iff_mem_nhdsSet, not_subset, forall_isClosed_iff, inter_nonempty]

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
rcases eq_or_ne b ⊤ with rfl | b_top
  · rcases eq_or_lt_of_le ha with rfl | ha
    · rw [zero_mul] at h
      exact (not_le_of_gt h hc).rec
    · obtain ⟨a', a0', aa'⟩ := exists_between ha
      use a', mem_Ioo.2 ⟨a0', aa'⟩
      rw [mul_top_of_pos ha] at h
      rwa [mul_top_of_pos a0']
  · have b0 : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
    obtain ⟨a', ha', aa'⟩ := exists_between ((div_lt_iff b0 b_top).2 h)
    exact ⟨a', ⟨(div_nonneg hc b0.le).trans_lt ha', aa'⟩, (div_lt_iff b0 b_top).1 ha'⟩

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

Goal state before:
pp: case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ ∑' (i : ℕ), m (t i) = ∞

Tactic:
push Not at ht

Goal state after:
case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∃ i, ¬P (t i)
⊢ ∑' (i : ℕ), m (t i) = ∞
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case a
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n)

Tactic:
· simp_rw [le_iInf_iff]
    refine fun t ht_subset ↦ iInf_le_of_le t ?_
    by_cases ht : ∀ i, P (t i)
    · exact iInf_le_of_le ht (iInf_le_of_le ht_subset le_rfl)
    · simp only [ht, not_false_eq_true, iInf_neg, top_le_iff]
      push Not at ht
      obtain ⟨i, hti_notMem⟩ := ht
      have hfi_top : m (t i) = ∞ := m_top _ hti_notMem
      exact ENNReal.tsum_eq_top_of_eq_top ⟨i, hfi_top⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ 2 * C / 2 ^ n

Tactic:
simp only [div_eq_mul_inv, ENNReal.inv_pow] at *

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * C * 2⁻¹ ^ n
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s

case inr
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s

case inr
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i ↦ ε' ↑i) c ∧ c ≤ ε

Tactic:
have := hs.toEncodable
  rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
  refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
  · conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]
  · simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]

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

Goal state before:
pp: α : Type u_2
f : Filter α
m : α → EReal
a b : EReal
hm : Tendsto m f (𝓝 a)
h₁ : a ≠ 0 ∨ b ≠ ⊥
h₂ : a ≠ 0 ∨ b ≠ ⊤
⊢ Tendsto (fun x ↦ m x * b) f (𝓝 (a * b))

Tactic:
by
  simpa only [mul_comm] using EReal.Tendsto.const_mul hm h₁.symm h₂.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
⊢ (inducedOuterMeasure m ⋯ m0) s ≤ m s hs

Tactic:
inducedOuterMeasure_eq m0 mU hs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
⊢ m s hs ≤ m s hs
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ MeasurableSet s ↔
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
rw [isCaratheodory_iff_le]

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t) ↔
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ⨅ (_ : MeasurableSet (⋂ n, t n)), m (⋂ n, t n) ≤ m (⋂ n, t n)

Tactic:
exact iInf_le _ (MeasurableSet.iInter hm)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∑' (i : ι), extend (fun t _ht ↦ μ t) (f i) = ∑' (i : ι), μ (f i)

pp: ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ μ ∅ = 0

pp: ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → μ (⋃ i, f i) = ∑' (i : ℕ), μ (f i)

Tactic:
· simp [measure_eq_extend, h]

Goal state after:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ μ ∅ = 0

ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → μ (⋃ i, f i) = ∑' (i : ℕ), μ (f i)
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
h : μ ≪ ν
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (map f ν) s = 0 → (map f μ) s = 0

Tactic:
simpa [hf, hs] using @h _

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
s : Set α
hs : MeasurableSet s
⊢ (comap f (comap g μ)) s = (comap (g ∘ f) μ) s

Tactic:
rw [comap_apply _ hf hf' _ hs, comap_apply _ hg hg' _ (hf' _ hs),
      comap_apply _ (hg.comp hf) (fun t ht ↦ image_comp g f _ ▸ hg' _ <| hf' _ ht) _ hs, image_comp]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Ioc b a → P x

Tactic:
simp only [uIoc_eq_union, mem_union, or_imp, eventually_and]

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 (AEDisjoint μ)
h : ∀ s ∈ S, NullMeasurableSet s μ
⊢ μ (⋃ i ∈ S, i) = ∑' (s : ↑S), μ ↑s

Tactic:
measure_biUnion₀ hs hd h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise (AEDisjoint μ)
h : ∀ s ∈ S, NullMeasurableSet s μ
⊢ ∑' (p : ↑S), μ ↑p = ∑' (s : ↑S), μ ↑s
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
by
  rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)
  · have : IsEmpty s := ⟨fun x => hb'.subset (hsb x.2)⟩
    rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
  · rw [← comap_coe_nhdsLT_of_Ioo_subset hsb (fun _ => hs a ha) hb, map_comap_of_mem]
    rw [Subtype.range_val]
    exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ ((μ.restrict t).restrict s) u = (μ.restrict (s ∩ t)) u

Tactic:
by simp only [restrict_apply hu, restrict_apply₀' ht, inter_assoc]

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Tactic:
split_ifs with h <;> exact ⟨ih, h⟩

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

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f / g =ᵐ[μ] 1
x : α
hx : (f / g) x = 1 x
⊢ f x = g x

pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᵐ[μ] g
x : α
hx : f x = g x
⊢ (f / g) x = 1 x

Tactic:
· rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᵐ[μ] g
x : α
hx : f x = g x
⊢ (f / g) x = 1 x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case h₁
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ f ⁻¹' t ⊆ {a | ¬f a = b}

Tactic:
exact fun x hx hfx ↦ ht (hfx ▸ hx)

Goal state after: