mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case coe.top
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : ↑a ≠ 0 ∨ ∞ ≠ ∞
hb : ∞ ≠ 0 ∨ ↑a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (↑a, ∞)) (𝓝 (↑a * ∞))

Tactic:
simp only [ne_eq, or_false, not_true_eq_false] at ha

Goal state after:
case coe.top
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
hb : ∞ ≠ 0 ∨ ↑a ≠ ∞
ha : ¬↑a = 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (↑a, ∞)) (𝓝 (↑a * ∞))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 ↦ x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))
⊢ x ≤ y

Tactic:
rw [one_mul] at this

Goal state after:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist (↑x) a + edist (↑y) a < r + r

Tactic:
exact ENNReal.add_lt_add x.2 y.2

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case neg
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
h : ¬∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n

Tactic:
push Not at h

Goal state after:
case neg
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
h : ∀ (n : ℕ), (x, y) ∈ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

Tactic:
apply nndist_mul_mul_le

Goal state after:
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ ⇑(e ^ n) = (⇑e)^[n]

Tactic:
rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ (⇑(toPerm e))^[n] = (⇑e)^[n]
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
inst✝⁷ : SeminormedRing α
inst✝⁶ : SeminormedAddGroup β✝
inst✝⁵ : SMul α β✝
inst✝⁴ : NormSMulClass α β✝
ι : Type u_3
β : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddGroup (β i)
inst✝¹ : (i : ι) → SMul α (β i)
inst✝ : ∀ (i : ι), NormSMulClass α (β i)
r : α
x : (i : ι) → β i
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
by
    simp [nnnorm_def, ← coe_nnnorm, nnnorm_smul, ← NNReal.coe_mul, NNReal.mul_finset_sup]

Goal state after:
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
x y : β
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y

Tactic:
simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)

Tactic:
rcases eq_or_ne e 0 with (rfl | he)

Goal state after:
case inl
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 0)

case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = ⨆ i, (f i) s

Tactic:
iSup,

Goal state after:
α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (sSup (range fun i ↦ f i)) s = ⨆ i, (f i) s
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v ↦ v.elim hj

Tactic:
· simp only [TProd.elim_of_ne _ hji]
      rw [mem_cons] at hj
      exact (measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : Measurable p
⊢ MeasurableSet {a | p a}

Tactic:
by
    simpa using h (measurableSet_singleton True)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | p a ↔ q a}

Tactic:
by
    simp_rw [iff_iff_implies_and_implies]; exact hq.setOf.bihimp hp.setOf

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

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (-(x✝ * y✝)).abs = (-x✝).abs * y✝.abs

Tactic:
EReal.abs_neg,

Goal state after:
case neg_left
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (x✝ * y✝).abs = (-x✝).abs * y✝.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f r

Tactic:
rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]

Goal state after:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i
Module: Mathlib.Topology.Semicontinuity.Defs

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

Tactic:
rw [← upperHemicontinuousWithinAt_univ_iff, upperHemicontinuousWithinAt_iff_frequently]
  simp

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅

Tactic:
Set.eq_empty_iff_forall_notMem

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ ∀ (x : α), x ∉ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:

Tactic:
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, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n) ≤ (OuterMeasure.ofFunction m m_empty) (f '' s)

Tactic:
ofFunction_apply

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, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n) ≤ ⨅ t, ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)
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 β
⊢ (OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯) s ≤ ((comap f) (OuterMeasure.ofFunction m m_empty)) s

Tactic:
rw [comap_apply, ofFunction_apply, ofFunction_apply]

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, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n) ≤ ⨅ t, ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)
Module: Mathlib.Topology.Semicontinuity.Basic

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

Tactic:
exact hf.inf hg

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * m t = a * m (t ∩ s) + a * m (t \ s)

Tactic:
rw [(isCaratheodory_iff m).mp h t]

Goal state after:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * (m (t ∩ s) + m (t \ s)) = a * m (t ∩ s) + a * m (t \ s)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ (inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = (inducedOuterMeasure m P0 m0) A

Tactic:
rw [inducedOuterMeasure_eq_iInf _ msU m_mono, inducedOuterMeasure_eq_iInf _ msU m_mono]

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : ⇑f ⁻¹' A ⊆ t), m t ht = ⨅ t, ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
⊢ generateFrom {s} = MeasurableSpace.comap (fun x ↦ x ∈ s) ⊤

Tactic:
let : MeasurableSpace α := generateFrom {s}
  refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
  rintro _ ⟨u, -, rfl⟩
  exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ m₁.trim s ≤ m₂ s ↔ m₁ s ≤ m₂ s

Tactic:
rw [trim_eq _ hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')

Tactic:
refine measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_
  · rw [domRestrict_extend_range]
    simpa only [rangeSplitting] using! hg.comp hf.measurable_rangeSplitting
  · rw [domRestrict_extend_compl_range]
    exact hg'.comp measurable_subtype_coe

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)

Tactic:
rw [← hf.2.1]
        rintro _ ⟨s, hs, rfl⟩
        simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ μ ((fun i ↦ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)) i) = 0

Tactic:
simp only [measure_toMeasurable, inter_iUnion]
    exact (measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : map (⇑e.symm) (map (⇑e) μ₁) = map (⇑e.symm) (map (⇑e) μ₂)
⊢ μ₁ = μ₂

Tactic:
simpa [map_symm_map e] using hμ

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

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

Tactic:
by
  rw [EventuallyEq, ae_iff] at hst ⊢
  have h_eq_α : { a : α | ¬s a = t a } = s \ t ∪ t \ s := by
    ext1 x
    simp only [eq_iff_iff, mem_ofPred_eq, mem_union, Set.mem_sdiff]
    tauto
  have h_eq_β : { a : β | ¬(f '' s) a = (f '' t) a } = f '' s \ f '' t ∪ f '' t \ f '' s := by
    ext1 x
    simp only [eq_iff_iff, mem_ofPred_eq, mem_union, Set.mem_sdiff]
    tauto
  rw [← Set.image_sdiff hfi, ← Set.image_sdiff hfi, ← Set.image_union] at h_eq_β
  rw [h_eq_β]
  rw [h_eq_α] at hst
  exact measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst

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

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

Tactic:
rw [restrict, restrictₗ] at ht

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯) μ)
⊢ (μ.restrict s) t = μ (t ∩ s)
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) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
⊢ posmeas = ⋃ n, fairmeas n

Tactic:
have fairmeas_eq : ∀ n, fairmeas n = (fun i => μ (As i)) ⁻¹' Ici (as n) := fun n => by
      simp only [fairmeas]
      rfl

Goal state after:
α : 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) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
fairmeas_eq : ∀ (n : ℕ), fairmeas n = (fun i ↦ μ (As i)) ⁻¹' Ici (as n)
⊢ posmeas = ⋃ n, fairmeas n
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
⊢ μ = ν

Tactic:
refine ext_of_sUnion_eq_univ hc hU fun t ht => ?_

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
⊢ μ.restrict t = ν.restrict t
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : (ν.trim hm) s = 0
⊢ (μ.trim hm) s = 0

Tactic:
trim_measurableSet_eq hm hs

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : ν s = 0
⊢ μ s = 0
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
⊢ Disjoint u v

Tactic:
memPartition_succ

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
⊢ Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ memPartition f (n + 1) = univ

Tactic:
memPartition_succ

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} = univ
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
⊢ μ t ≤ μ s

Tactic:
have : μ t + ν t ≤ μ s + ν t :=
    calc
      μ t + ν t = μ s + ν s := h''.symm
      _ ≤ μ s + ν t := by gcongr

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ∞
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
this : μ t + ν t ≤ μ s + ν t
⊢ μ t ≤ μ s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
by
  have := ht.to_subtype
  rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']

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

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ (memPartition f (n + 1)).Finite

Tactic:
memPartition_succ

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite
Module: Mathlib.Data.Set.MemPartition

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

Tactic:
memPartition_succ

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈
    {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᵐ[μ] g / f
a : α
ha : 1 ≤ g a / f a
⊢ f a ≤ g a

Tactic:
one_le_div'

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᵐ[μ] g / f
a : α
ha : f a ≤ g a
⊢ f a ≤ g a
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ 1 ≤ g a / f a

Tactic:
one_le_div'

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ f a ≤ g a
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s \ t n ∈ memPartition t (n + 1)

Tactic:
memPartition_succ

Goal state after:
case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s \ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ memPartition t (n + 1)

Tactic:
memPartition_succ

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ memPartition t (n + 1)

Tactic:
memPartition_succ

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x ↦ b) μ
⊢ NullMeasurableSet s μ

Tactic:
convert! h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x ↦ b) μ
⊢ s = (s.indicator fun x ↦ b) ⁻¹' {0}ᶜ