mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.23
f : β → α
h : Monotone m ∨ Surjective f
⊢ m (f '' ∅) = 0

Tactic:
simp

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.23
f : β → α
h : Monotone m ∨ Surjective f
⊢ m ∅ = 0
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ ∑' (n : ℕ), 2⁻¹ ^ n = 2

Tactic:
simp

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

Goal state before:
pp: r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n < ∞ ↔ r < 1

Tactic:
simp

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)
p : EReal × EReal
⊢ p.1 * p.2 = ((fun x ↦ -x) ∘ (fun p ↦ p.1 * p.2) ∘ fun p ↦ (-p.1, p.2)) p

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ 2⁻¹ < 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m (∅ ∩ s) = 0

Tactic:
simp

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m ∅ = 0
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (comap f) (boundedBy m) = boundedBy fun s ↦ m (f '' s)

Tactic:
refine (comap_ofFunction _ ?_).trans ?_

Goal state after:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (Monotone fun s ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f

case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
| (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) i

Tactic:
simp

Goal state after:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
| if h : i ∈ s then f ⟨i, h⟩ else 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ : Type u_5
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_4
δ : Type u_5
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i ↦ f i y)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
ι : Sort u_4
δ : Type u_5
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousOn (f i) s
⊢ ∀ x ∈ s, BddAbove (range fun i ↦ f i x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_4
δ : Type u_5
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuous (f i)
⊢ ∀ (x : α), BddAbove (range fun i ↦ f i x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ ∀ (y : β), f a < y → ∀ᶠ (x' : α) in 𝓝[s] a, f x' < y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
n m : ℕ
hm : s m ⊆ dissipate s n
k : ℕ
hk : (fun x1 x2 ↦ x1 ⊇ x2) (s m) (s k) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (s (n + 1)) (s k)
⊢ s k ⊆ dissipate s (n + 1)

Tactic:
simp

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
n m : ℕ
hm : s m ⊆ dissipate s n
k : ℕ
hk : (fun x1 x2 ↦ x1 ⊇ x2) (s m) (s k) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (s (n + 1)) (s k)
⊢ s k ⊆ dissipate s n ∧ s k ⊆ s (n + 1)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
⊢ IsPiSystem (⋃ n, p n)

Tactic:
intro t1 ht1 t2 ht2 h
  rw [Set.mem_iUnion] at ht1 ht2 ⊢
  obtain ⟨n, ht1⟩ := ht1
  obtain ⟨m, ht2⟩ := ht2
  obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m
  exact ⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case singleton
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
a : Set α
ht : ∀ s ∈ {a}, s ∈ S
h' : (⋂ s ∈ {a}, s).Nonempty
⊢ ⋂ s ∈ {a}, s ∈ S

Tactic:
simpa using ht

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

Goal state before:
pp: case empty
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
h : ∀ i ∈ ↑∅, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ ↑∅, s i)

Tactic:
simp

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
x✝ : ∀ i < 0, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, ⋃ (_ : i < 0), s i)

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case a
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ generatePiSystem g, MeasurableSet t

Tactic:
exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t

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)
t : Set α
⊢ ∑ i ∈ Finset.range 0, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < 0), s i)

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ↑(Finset.image (fun x ↦ ↑x) T) ⊆ s

Tactic:
simp

Goal state after:
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)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
⊢ ∑ b, extend m (bif b then s₁ else s₂) = extend m s₁ + extend m s₂

Tactic:
simp

Goal state after:
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)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (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₂
Pu : P univ
⊢ 0 = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
Pu : P univ
s : Set α
x✝¹ : ℕ → Set α
x✝ : ∀ (i : ℕ), P (x✝¹ i)
⊢ 0 ≤ ∑' (i : ℕ), 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
Pu : P univ
s x✝¹ x✝ : Set α
⊢ P x✝¹ → P x✝ → x✝¹ ⊆ x✝ → 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
Pu : P univ
s : Set α
⊢ ⨅ (_ : s ⊆ univ), 0 ≤ 0 s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = μ.trim s

Tactic:
by
  rw [μ.trimmed, μ.coe_toOuterMeasure]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ {i} ⊆ S

Tactic:
intro j

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
⊢ j ∈ {i} → j ∈ S
Module: Mathlib.MeasureTheory.OuterMeasure.AE

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

Tactic:
simp

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 α
⊢ (∀ᵐ (x : α) ∂μ, x ∉ s) ↔ μ s = 0

Tactic:
by simp only [ae_iff, Classical.not_not, ofPred_mem_eq]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ s = sᶜᶜ

Tactic:
simp

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
M : Type u_4
inst✝ : One M
f : α → M
s : Set α
⊢ s.mulIndicator f =ᵐ[μ] 1 ↔ μ (s ∩ Function.mulSupport f) = 0

Tactic:
simp [EventuallyEq, eventually_iff, ae, compl_ofPred]

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
M : Type u_4
inst✝ : One M
f : α → M
s : Set α
⊢ ({a | a ∈ s ∧ ¬f a = 1} ∈ fun x ↦ μ x = 0) ↔ μ (s ∩ Function.mulSupport f) = 0
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case compl
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t u : Set α
hu : DynkinSystem.GenerateHas s u
ihu : C u ⋯
⊢ C uᶜ ⋯

Tactic:
| @compl u hu ihu =>

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : MeasurableSpace M
s : Set α
c : M
⊢ s ∈ {s}

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ i, s i)

Tactic:
simp

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

Goal state before:
pp: α : 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
n : ℕ
⊢ (↑n)⁻¹ ≠ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set α
hs : MeasurableSet s
⊢ ∀ (x : { x // x ∈ range Sum.inl }), x ∈ Subtype.val ⁻¹' Sum.inl '' s ↔ x ∈ ⇑(Equiv.Set.rangeInl α β) ⁻¹' s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
⊢ ∀ (x : { x // x ∈ range Sum.inr }), x ∈ Subtype.val ⁻¹' Sum.inr '' s ↔ x ∈ ⇑(Equiv.Set.rangeInr α β) ⁻¹' s

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
have : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r := by
      intro r hs
      have : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r := by simpa [ms, iInf_lt_iff] using hs
      rcases this with ⟨t, hmt, hin, hlt⟩
      exists t
    have : ∀ n : ℕ, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (n : ℝ≥0∞)⁻¹ := by
      intro n
      refine this _ (ENNReal.lt_add_right hs ?_)
      simp
    choose t hsub hm hm' using this
    refine ⟨⋂ n, t n, subset_iInter hsub, MeasurableSet.iInter hm, ?_⟩
    have : Tendsto (fun n : ℕ => ms + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0)) :=
      tendsto_const_nhds.add ENNReal.tendsto_inv_nat_nhds_zero
    rw [add_zero] at this
    refine le_antisymm (ge_of_tendsto' this fun n => ?_) ?_
    · exact le_trans (measure_mono <| iInter_subset t n) (hm' n).le
    · refine iInf_le_of_le (⋂ n, t n) ?_
      refine iInf_le_of_le (subset_iInter hsub) ?_
      exact iInf_le _ (MeasurableSet.iInter hm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
⊢ α ≃ᵐ β

Tactic:
have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ α ≃ᵐ β
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set α
ι : Sort u_3
inst✝ : Countable ι
t : ι → Set α
⊢ AEDisjoint μ s (⋃ i, t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)

Tactic:
by
  simp only [AEDisjoint, inter_iUnion, measure_iUnion_null_iff]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
⊢ map f (0 • μ) = 0 • map f μ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ (map f μ) s = μ s

pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ NullMeasurableSet s (map f μ)

Tactic:
hf

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ μ s = μ s

α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ NullMeasurableSet s (map f μ)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ NullMeasurableSet s (map f μ)

Tactic:
hf

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ NullMeasurableSet s μ
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
x✝¹ : Set α
x✝ : μ x✝¹ = 0
⊢ 0 x✝¹ = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
hs : ∑' (i : ℕ), μ (s i) ≠ ∞
⊢ μ (limsup s atTop) = 0

Tactic:
by
  rw [← Nat.cofinite_eq_atTop, measure_limsup_cofinite_eq_zero hs]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
⊢ comap f (0 • μ) = 0 • comap f μ

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ (comap f (c • μ)) s = (c • comap f μ) s

Tactic:
comap_apply₀ f _ h.1 _ hs.nullMeasurableSet,

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ (c • μ) (f '' s) = (c • comap f μ) s

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ ∑ x ∈ s, μ {x} = ∑ x ∈ s, μ (id ⁻¹' {x})

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ μ (id ⁻¹' ↑s) = μ ↑s

Tactic:
simp

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

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ ∀ y ∈ s, MeasurableSet (id ⁻¹' {y})

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nullsdiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Tactic:
have le23 : μ s₂ ≤ μ s₃ := measure_mono h23

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nullsdiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s✝ t : Set α
μ : Measure α
s : Set α
h : IsFiniteMeasure μ
⊢ (μ.restrict s) univ < ∞

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
⊢ 0 univ < ∞

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯) μ)
⊢ ((OuterMeasure.restrict s) μ.toOuterMeasure) t = μ (t ∩ s)

Tactic:
OuterMeasure.restrict_apply,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯) μ)
⊢ μ.toOuterMeasure (t ∩ s) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : IsEmpty ι
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), μ (s ∩ spanningSets μ n) ≤ 0) ↔ ∀ t ∈ range (spanningSets μ), μ (s ∩ t) = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Infinite
h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}
ε : ℝ≥0∞
hne : ε ≠ 0
hε : ∀ x ∈ s, ε ≤ μ {x}
this : Infinite ↑s
⊢ μ (⋃ x, {↑x}) = μ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < ∑' (i_1 : ℕ), (sfiniteSeq μ i_1) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ False

Tactic:
con

Goal state after:
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
hi : 0 < ∑' (i : ℕ), 0
⊢ False
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case e'_4.e'_5
α : 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) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ (μ (s \ t)).toReal = |(μ (s \ t)).toReal|

Tactic:
simp

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

Goal state before:
pp: case e'_4.e'_6
α : 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) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ (μ (t \ s)).toReal = |(μ (t \ s)).toReal|

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : m = ⊥
⊢ ∅ ∈ {D | D ⊆ C ∧ D.Countable}

Tactic:
simp

Goal state after: