mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
u : Set ↑s
hs : MeasurableSet (Subtype.val ⁻¹' s)
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' u)

Tactic:
rcases hu with ⟨u, hu, rfl⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' Subtype.val ⁻¹' u)
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
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt (C / ε)

Goal state after:
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
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x

Tactic:
apply compl_subset_compl.1
      intro z hz
      simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
      exact ⟨z, hz, (hs z hz).2.2⟩

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
t : β
ht : t ∈ Icc 0 1
⊢ 1 - t ∈ Icc 0 1

Tactic:
rw [mem_Icc] at *
  exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s = ∅
⊢ ⊤ s = ⨅ (_ : s = ∅), 0

Tactic:
simp [h]

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
rcases (pi s t).eq_empty_or_nonempty with h | h

Goal state after:
case inl
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : s.pi t = ∅
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

case inr
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case inl
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : s.pi t = ∅
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
β : Type u
t : Finset β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
ht : #t = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card ↥t = ∑ a ∈ s, (f a).natAbs

Tactic:
simp [ht]

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
⊢ (if 0 < a then 1 else if a < 0 then -1 else 0) ≤ if 0 < b then 1 else if b < 0 then -1 else 0

Tactic:
split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ 1 ≤ 1

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ -1 ≤ 1

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : b < 0
⊢ -1 ≤ -1

case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : ¬b < 0
⊢ -1 ≤ 0

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ 0 ≤ 1

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1

case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 0 ≤ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ Summable fun b ↦ f ↑b

Tactic:
exact NNReal.summable_comp_injective (tsum_coe_ne_top_iff_summable.1 hf) Subtype.coe_injective

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

Goal state before:
pp: case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
simp [h]

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

Goal state before:
pp: case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
simp [h]

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

Goal state before:
pp: case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f ↔ (∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩

Tactic:
constructor
  · simp only [← NNReal.summable_coe, NNReal.coe_tsum]
    exact fun h => ⟨h.sigma_factor, h.sigma⟩
  · rintro ⟨h₁, h₂⟩
    simpa only [← ENNReal.tsum_coe_ne_top_iff_summable, ENNReal.tsum_sigma',
      ENNReal.coe_tsum (h₁ _)] using h₂

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

Goal state before:
pp: f : ℕ → ℝ≥0
⊢ Tendsto (fun i ↦ ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

Tactic:
by
  rw [← tendsto_coe]
  convert! _root_.tendsto_sum_nat_add fun i => (f i : ℝ)
  norm_cast

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

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

Tactic:
rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]

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

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ b ≤ -0

Tactic:
simp [h]

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
x✝² : Nonempty α
x✝¹ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
⊢ ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False

Tactic:
filter_upwards [(hf a ha (f x) hxa).filter_mono (inf_le_inf_left _ hℱs),
    (hℱ x hx).filter_mono (inf_le_right : 𝓝 a ⊓ ℱ ≤ ℱ)] using fun y h₁ h₂ ↦ not_le_of_gt h₁ h₂

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ liminf (u + v) f = ⊤

Tactic:
apply top_le_iff.1 (le_trans _ le_liminf_add)
  rw [h, top_add_of_ne_bot h']

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

Goal state before:
pp: a b : EReal
h : ContinuousAt (fun p ↦ p.1 * p.2) (a, b)
this : (fun p ↦ p.1 * p.2) = (fun x ↦ -x) ∘ (fun p ↦ p.1 * p.2) ∘ fun p ↦ (-p.1, p.2)
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (Prod.map (fun a ↦ -a) id (-a, b))

Tactic:
simp [h]

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

Goal state before:
pp: case h.refine_1
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
⊢ ↑x < p.1 * p.2

Tactic:
have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)

Goal state after:
case h.refine_1
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 * 1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ (c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s

Tactic:
simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul,
  iInf_subtype']

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ c * ⨅ x, ∑' (n : ℕ), m (↑x n) = ⨅ x, c * ∑' (i : ℕ), m (↑x i)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
t : Set α
⊢ (boundedBy (sInfGen m)) t ≤ μ t

Tactic:
exact le_trans (boundedBy_le t) (iInf₂_le μ hμ)

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

Goal state before:
pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S

Tactic:
simp [ht]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∨ b ∈ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
⊢ ∅ ∈ g b

Tactic:
apply False.elim (h_b.elim hbs hbt)

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

Goal state before:
pp: case e'_4
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : t = ∅
⊢ ⊤ (t ∩ s) + ⊤ (t \ s) ≤ ⊤ t

Tactic:
simp [ht]

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

Goal state before:
pp: 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)

pp: 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)

Tactic:
swap

Goal state after:
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)

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)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: 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)

Tactic:
simp [ht]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
⊢ (∀ (s : Set α), μ sᶜ = 0 ↔ s = univ) ↔ ∀ (a : α), ¬μ {a} = 0

Tactic:
refine ⟨fun h a ha ↦ by simpa [ha] using (h {a}ᶜ).1, fun h s ↦ ⟨fun hs ↦ ?_, ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ s = univ

case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h✝ : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
h : x ∈ s
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ

Tactic:
simp [h]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h✝ : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
h : x ∉ s
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ t'

Tactic:
refine (measure_mono htt').trans ?_

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim (sᶜ ∪ t') ≤ μ t'
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ.trim (t ∩ s) ≤ ((restrict s) μ) t

Tactic:
trim_eq _ (ht.inter hs),

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) ≤ ((restrict s) μ) t
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ s \ t

Tactic:
by
      simpa using ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩

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

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

Tactic:
iUnion_singleton_eq_range,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable β
μ : Measure (α × β)
x : α
⊢ μ (Prod.fst ⁻¹' {x}) = μ (range (Prod.mk x))
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ : Measure α
⊢ ∀ ⦃a₂ : Measure α⦄, map (⇑e) μ₁ = map (⇑e) a₂ → μ₁ = a₂

Tactic:
μ₂

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
⊢ map (⇑e) μ₁ = map (⇑e) μ₂ → μ₁ = μ₂
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ f '' s =ᵐ[μ] f '' toMeasurable (comap f μ) s

pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ

Tactic:
swap

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ

case refine_1
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ f '' s =ᵐ[μ] f '' toMeasurable (comap f μ) 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
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ b ≤ a

Tactic:
by simpa using ha

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)
⊢ μ (⋃ i, s i) ≤ μ (⋃ i, t i)

Tactic:
gcongr; apply hsub

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

Goal state before:

Tactic:
μ univ = μ univ - μ s + μ s := (tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm
    _ ≤ μ univ - μ s + (μ t + ε) := by gcongr
    _ = _ := by rw [add_right_comm, add_assoc]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ∅ < ∞

Tactic:
simp only [measure_empty, zero_lt_top]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst✝ : Decidable (x ∈ t)
h : x ∈ t
⊢ μ s = t.indicator (fun x ↦ μ s) x

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst✝ : Decidable (x ∈ t)
h : x ∉ t
⊢ μ ∅ = t.indicator (fun x ↦ μ s) x

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Finset ι
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x

Tactic:
by
  simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), (f i) t = (f i) s
⊢ ∑' (i : ι), (f i) t = ∑' (i : ι), (f i) s

Tactic:
simp [ht]

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

Goal state before:
pp: case refine_1
α : 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
⊢ Measurable (v.domRestrict (v.piecewise (fun x ↦ default) f))

Tactic:
rw [domRestrict_piecewise]
    apply measurable_const

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : IsEmpty ι
μ : ι → Measure α
⊢ sum μ = 0

Tactic:
by
  rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty]

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
n : ?m.90
⊢ ?m.93 n

Tactic:
apply normal_exists_closure_subset t_cl (T_open (g n).1 (g n).2)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
n : ℕ
⊢ t ⊆ ↑(g n)
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case nil
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
hl : ∀ f ∈ [], Measurable f
⊢ Measurable [].prod

Tactic:
exact measurable_one

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

Goal state before:
pp: γ : Type u_3
inst✝² : TopologicalSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
x y : γ
h✝ : Inseparable x y
s : Set γ
hs : MeasurableSet s
x✝² : ℕ → Set γ
x✝¹ : Pairwise (Function.onFun Disjoint x✝²)
x✝ : ∀ (i : ℕ), MeasurableSet (x✝² i)
h : ∀ (i : ℕ), x ∈ x✝² i ↔ y ∈ x✝² i
⊢ x ∈ ⋃ i, x✝² i ↔ y ∈ ⋃ i, x✝² i

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)ᶜ

Tactic:
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)ᶜ

Tactic:
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Goal state after: