mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 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)⁻¹ * C < (C / ε)⁻¹ * C

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ m (f '' x✝¹) ≤ m (f '' x✝)

Tactic:
by gcongr

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:
x

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.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
⊢ Summable f

Tactic:
refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_
  rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
  exact lt_irrefl _ (hn.trans_le (h n))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| fun x ↦ a = f x

Tactic:
x

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
| a = f x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
rw [← Fintype.coe_image_univ, univ_eq]

Goal state after:
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

Tactic:
simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
    exact Finset.sum_neg h hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
⊢ SemicontinuousWithinAt r' s a

Tactic:
intro b hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
b : β
hb : r' a b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
b : β
hb' : r' x b
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (r ⊔ r') x' b

Tactic:
· exact (h' b hb').mono fun _ hx ↦ Or.inr hx

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
b : β
hb' : r' x b
⊢ ∀ᶠ (x' : α) in 𝓝 x, (r ⊔ r') x' b

Tactic:
· exact (h' b hb').mono fun _ hx ↦ Or.inr hx

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

Goal state before:
pp: case coe
x : ℝ
⊢ ⊥ < (↑x)⁻¹

Tactic:
exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ ∃ a ∈ s, IsMinOn f s a

Tactic:
simp only [isMinOn_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
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_neg (a * b⁻¹),

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a' * b⁻¹ ≤ - -(a * b⁻¹)
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), 0 < ε → ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
intro ε hε (hb : (∑' i, μ (s i)) < ∞)

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) < ∞
⊢ μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
⊢ ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
x

Goal state after:
case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
x : α
⊢ x ∈ s → ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : f a > z
⊢ (g ∘ f) a > y

Tactic:
calc
      y < g (min (f x) (f a)) := hz (by simp [zlt, ha])
      _ ≤ g (f a) := gmon (min_le_right _ _)

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : f '' s ⊆ iUnion t
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
Set.image_subset_iff,

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ f ⁻¹' iUnion t
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
by
  simp only [ContinuousAt, EReal.top_mul_top, EReal.tendsto_nhds_top_iff_real]
  intro x
  rw [_root_.eventually_nhds_iff]
  use (Set.Ioi ((max x 0) : EReal)) ×ˢ (Set.Ioi 1)
  split_ands
  · intro p p_in_prod
    simp only [Set.mem_prod, Set.mem_Ioi, max_lt_iff] at p_in_prod
    rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
    have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)
    rw [mul_one p.1] at this
    exact lt_of_lt_of_le p1_gt_x this
  · exact IsOpen.prod isOpen_Ioi isOpen_Ioi
  · simp
  · rw [Set.mem_Ioi, ← EReal.coe_one]; exact EReal.coe_lt_top 1

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
⊢ LowerSemicontinuousWithinAt (fun x ↦ max (f x) (g x)) s a

Tactic:
intro b hb

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : (fun x ↦ max (f x) (g x)) a > b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, (fun x1 x2 ↦ (fun x ↦ max (f x) (g x)) x1 > x2) x' b
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
⊢ LowerSemicontinuousWithinAt (fun x ↦ min (f x) (g x)) s a

Tactic:
intro b hb

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : (fun x ↦ min (f x) (g x)) a > b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, (fun x1 x2 ↦ (fun x ↦ min (f x) (g x)) x1 > x2) x' b
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
by_cases ht : a ∈ t

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)
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
⊢ ∀ ⦃a : α⦄,
    a ∈ s i → a ∉ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j) → a ∈ s j → a ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)

Tactic:
x

Goal state after:
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 : α
⊢ x ∈ s i → x ∉ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j) → x ∈ s j → x ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ hf.equivRange.symm ⟨f x, ⋯⟩ = x

Tactic:
nth_rw 3 [← hf.equivRange.symm_apply_apply x]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ hf.equivRange.symm ⟨f x, ⋯⟩ = hf.equivRange.symm (hf.equivRange x)
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, f i) = ∑' (i : ι), μ (f i)

Tactic:
by
  rw [measure_eq_extend (MeasurableSet.iUnion h),
    extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
  · simp [measure_eq_extend, h]
  · exact μ.empty
  · exact μ.m_iUnion

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : μ s' = μ s
hs'm : NullMeasurableSet s' μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t)

Tactic:
by gcongr

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ range f ∈ ae (map f μ)

Tactic:
mem_ae_map_iff h hf

Goal state after:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ f ⁻¹' range f ∈ ae μ
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ (map f μ) s ≤ (map f μ) t

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [← measure_inter_add_sdiff (s ∪ t) ht, Set.union_inter_cancel_right, union_sdiff_right, ←
    measure_inter_add_sdiff s ht]
  ac_rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ b, s b) =ᵐ[μ] M (t b)

Tactic:
refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≤ μ (M (t b) ∩ M (⋃ b, s b))

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
b : ι
⊢ NullMeasurableSet (M (t b) ∩ M (⋃ b, s b)) μ

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ (s ∩ t).Nonempty

Tactic:
rw [← Set.not_disjoint_iff_nonempty_inter]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ ¬Disjoint s t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (Function.extend f m 0 (f i))

Tactic:
rw [hf.extend_apply]
    infer_instance

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ - μ s + μ s ≤ μ univ - μ s + (μ t + ε)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
⊢ {i | 0 < μ (As i)}.Countable

Tactic:
set posmeas := { i : ι | 0 < μ (As i) } with posmeas_def
  rcases exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ≥0∞) < 1) with
    ⟨as, _, as_mem, as_lim⟩
  set fairmeas := fun n : ℕ => { i : ι | as n ≤ μ (As i) }
  have countable_union : posmeas = ⋃ n, fairmeas n := by
    have fairmeas_eq : ∀ n, fairmeas n = (fun i => μ (As i)) ⁻¹' Ici (as n) := fun n => by
      simp only [fairmeas]
      rfl
    simpa only [fairmeas_eq, posmeas_def, ← preimage_iUnion,
      iUnion_Ici_eq_Ioi_of_lt_of_tendsto (fun n => (as_mem n).1) as_lim]
  rw [countable_union]
  refine countable_iUnion fun n => Finite.countable ?_
  exact finite_const_le_meas_of_disjoint_iUnion₀ μ (as_mem n).1 As_mble As_disj Union_As_finite

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

Goal state before:
pp: α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirectedOrder ι
i j : ι
hij : i ≤ j
⊢ μ (accumulate f i) ≤ μ (accumulate f j)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
⊢ μ (t ∩ u) ≤ μ ((⋂ n, w n) ∩ u)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ∞
⊢ μ (t ∩ s) ≤ μ (u ∩ s)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ∞
⊢ μ (t ∩ s) + μ (t \ s) ≤ μ (t ∩ s) + μ (u \ s)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ μ (t ∩ u) ≤ μ (t' ∩ u)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = (sum fun i ↦ μ.restrict (s i)) t

Tactic:
by simp only [sum_apply _ ht, restrict_iUnion_apply_ae hd hm ht]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ∞
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ μ s + ν s ≤ μ s + ν t

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝³ : SMul R ℝ≥0∞
inst✝² : LE R
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsOrderedSMul R ℝ≥0∞
μ ν : Measure α
hμν : μ ≤ ν
a : R
s : Set α
⊢ (a • μ) s ≤ (a • ν) s

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : α) ∂Measure.map Subtype.val (Measure.comap Subtype.val μ), p x) ↔
    ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x

Tactic:
(MeasurableEmbedding.subtype_coe hs).ae_map_iff

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : { x // x ∈ s }) ∂Measure.comap Subtype.val μ, p ↑x) ↔ ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), (if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) = 0

Tactic:
simp only [ite_eq_left_iff]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), ¬x = 1 → ¬x = 0 → min (μ (t' x)) (ν (t' x)) = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∈ s
⊢ s.indicator f x = s.indicator g x

pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.indicator f x = s.indicator g x

Tactic:
· simp [hxs, hx hxs]

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.indicator f x = s.indicator g x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ CountablySeparated α

Tactic:
rcases h with ⟨b, hbc, hb⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst✝¹ = generateFrom b
⊢ CountablySeparated α
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
i : ι
⊢ ∀ x ∉ s i, f x = mk f ⋯ x

Tactic:
x

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
i : ι
x : α
⊢ x ∉ s i → f x = mk f ⋯ x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
⊢ (sum fun x ↦ 0) = 0

Tactic:
ext s hs
  simp [Measure.sum_apply _ hs]

Goal state after: