mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, dissipate s x ⊆ ⋂ x, s x

pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, s x ⊆ ⋂ x, dissipate s x

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, dissipate s x ⊆ ⋂ x, s x

case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋂ x, s x ⊆ ⋂ x, dissipate s x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
k : ℕ
hn : 0 < k.succ
⊢ ∀ i ∈ Finset.range k, 0 ≤ (↑i + 1 + 1) * (↑k + 1)⁻¹

pp: case refine_2
k : ℕ
hn : 0 < k.succ
⊢ ∀ i ∈ Finset.range k, (↑i + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
<;>

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
⊢ ∀ i ∈ Finset.range k, 0 ≤ (↑i + 1 + 1) * (↑k + 1)⁻¹

case refine_2
k : ℕ
hn : 0 < k.succ
⊢ ∀ i ∈ Finset.range k, (↑i + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
<;>

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.MeasureTheory.PiSystem

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

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

Tactic:
<;>

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

case inl.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s = univ
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

pp: case neg
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

case neg
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

pp: case neg
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

case neg
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) ≤ generateFrom g

pp: case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom g ≤ generateFrom (generatePiSystem g)

Tactic:
<;>

Goal state after:
case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) ≤ generateFrom g

case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom g ≤ generateFrom (generatePiSystem g)
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
hs : a ∈ s
⊢ (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
hs : a ∉ s
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
hs : a ∈ s
⊢ (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
hs : a ∉ s
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mp
α : 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)
a : α
⊢ a ∈ ⋂ b ∈ T, f b → a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

pp: case refine_1.mpr
α : 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)
a : α
⊢ a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b → a ∈ ⋂ b ∈ T, f b

Tactic:
<;>

Goal state after:
case refine_1.mp
α : 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)
a : α
⊢ a ∈ ⋂ b ∈ T, f b → a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

case refine_1.mpr
α : 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)
a : α
⊢ a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b → a ∈ ⋂ b ∈ T, f b
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ μ₁ = μ₂ → ∀ (s : Set α), μ₁ s = μ₂ s

Tactic:
rintro rfl s; rfl

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

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

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

Tactic:
· rw [← compl_empty_iff, ← not_nonempty_iff_eq_empty]
    rintro ⟨a, ha⟩
    exact h _ <| measure_mono_null (singleton_subset_iff.2 ha) hs

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

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

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

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ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated.3664957871._hygCtx._hyg.200.«0»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : True ∈ x
⊢ True ∈ ∅

pp: case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated.3664957871._hygCtx._hyg.200.«1»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : False ∈ x
⊢ False ∈ ∅

Tactic:
<;>

Goal state after:
case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated.3664957871._hygCtx._hyg.200.«0»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : True ∈ x
⊢ True ∈ ∅

case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated.3664957871._hygCtx._hyg.200.«1»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : False ∈ x
⊢ False ∈ ∅
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
⊢ MeasurableSet (⇑(Equiv.Set.rangeInl α β) ⁻¹' s)

Tactic:
by
    refine ⟨_, hs.inl_image, Set.ext ?_⟩
    simp

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

Goal state before:
pp: case inl
α✝ : 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 γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
a : α
⊢ (Sum.inl a, c) ∈ univ → (Sum.inl a, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ

pp: case inr
α✝ : 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 γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
b : β
⊢ (Sum.inr b, c) ∈ univ → (Sum.inr b, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ

Tactic:
<;>

Goal state after:
case inl
α✝ : 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 γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
a : α
⊢ (Sum.inl a, c) ∈ univ → (Sum.inl a, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ

case inr
α✝ : 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 γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
b : β
⊢ (Sum.inr b, c) ∈ univ → (Sum.inr b, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
by
  rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f 0
⊢ map f 0 = 0

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬AEMeasurable f 0
⊢ map f 0 = 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f 0
⊢ map f 0 = 0

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬AEMeasurable f 0
⊢ map f 0 = 0
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: case hn
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ Pairwise (Disjoint on fun x ↦ {(x, y)})

pp: case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ ∀ (i : α), MeasurableSet {(i, y)}

Tactic:
<;>

Goal state after:
case hn
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ Pairwise (Disjoint on fun x ↦ {(x, y)})

case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ ∀ (i : α), MeasurableSet {(i, y)}
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ ¬g = 1

Tactic:
inv_mul_eq_one

Goal state after:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ ¬g₂ = g₁
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e.symm

pp: case hf
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e

Tactic:
<;>

Goal state after:
case hg
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e.symm

case hf
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable ⇑e
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 α
⊢ (μ univ)⁻¹ * μ univ < ∞

Tactic:
← ENNReal.div_eq_inv_mul

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
⊢ μ univ / μ univ < ∞
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) ↔ μ s = 0

Tactic:
by
  nth_rw 2 [show s = ⋃ n, s ∩ spanningSets μ n by
      rw [← inter_iUnion, iUnion_spanningSets, inter_univ]]
  rw [measure_iUnion_null_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
inst✝ : IsFiniteMeasure (map f μ)
⊢ μ univ < ∞

Tactic:
rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]
    exact IsFiniteMeasure.measure_univ_lt_top

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
by
  simp [← restrict_union_add_inter₀ s ht, restrict_zero_set h]

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

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

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

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|
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
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D

Tactic:
let m := ⨆ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)

Goal state after:
α : 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)
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

Tactic:
union_comm t s

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

Goal state before:
pp: case mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
⊢ IsFiniteMeasure μ → IsFiniteMeasureOnCompacts μ

pp: case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
⊢ IsFiniteMeasureOnCompacts μ → IsFiniteMeasure μ

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
⊢ IsFiniteMeasure μ → IsFiniteMeasureOnCompacts μ

case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
⊢ IsFiniteMeasureOnCompacts μ → IsFiniteMeasure μ
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

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

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

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
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
⊢ μ Set.univ < ∞

pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
⊢ (μ.trim ⋯) Set.univ < ∞

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
⊢ μ Set.univ < ∞

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
⊢ (μ.trim ⋯) Set.univ < ∞
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' ∩ f n ≠ v
⊢ Disjoint (u' ∩ f n) v

pp: case succ.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' \ f n ≠ v
⊢ Disjoint (u' \ f n) v

Tactic:
<;>

Goal state after:
case succ.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' ∩ f n ≠ v
⊢ Disjoint (u' ∩ f n) v

case succ.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' \ f n ≠ v
⊢ Disjoint (u' \ f n) v
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
⊢ (c • μ) {a | ¬p a} = 0

Tactic:
rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]

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

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ t = μ (toMeasurable (μ + ν) t)

Tactic:
refine
      measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
        (measure_toMeasurable t).symm

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ (μ + ν) (toMeasurable (μ + ν) t) ≠ ∞