mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑(n + 1))) (g' / f (-0))
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)

Tactic:
neg_zero

Goal state after:
G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑(n + 1))) (g' / f 0)
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case he
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k) * f (2 * k)

Tactic:
simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul]

Goal state after:
case he
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ f (2 * k)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist x (f (g y)) = edist x y

Tactic:
hg _

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist x y = edist x y
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
⊢ ↑(⨅ l, (zipWith d (x :: l) (l ++ [z])).sum) ≤
    ↑(⨅ l, (zipWith d (x :: l) (l ++ [y])).sum) + ↑(⨅ l, (zipWith d (y :: l) (l ++ [z])).sum)

Tactic:
by
    rw [← NNReal.coe_add, NNReal.coe_le_coe]
    refine NNReal.le_iInf_add_iInf fun lxy lyz ↦ ?_
    calc
      ⨅ l, (zipWith d (x::l) (l ++ [z])).sum ≤
          (zipWith d (x::lxy ++ y::lyz) ((lxy ++ y::lyz) ++ [z])).sum :=
        ciInf_le (OrderBot.bddBelow _) (lxy ++ y::lyz)
      _ = (zipWith d (x::lxy) (lxy ++ [y])).sum + (zipWith d (y::lyz) (lyz ++ [z])).sum := by
        rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc,
          append_assoc, append_assoc]
        rw [length_cons, length_append, length_singleton]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_1
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ Monotone fun t ↦ range pureCauchy ∩ UniformSpace.ball f t

pp: case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Tactic:
· exact monotone_const.inter monotone_preimage

Goal state after:
case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = ⟨b, ⋯⟩ ↔ b ≤ x

Tactic:
by
  simp [projIcc, Subtype.ext_iff, max_min_distrib_left, h.le, h.not_ge]

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x y : α
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
have h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_inf_sub_inf_le_add_norm x y 0 0
  simpa only [inf_idem, sub_zero] using h

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:

Tactic:
↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :=
      sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)
    _ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 - x.1) * x.2‖

Tactic:
sub_mul,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 * x.2 - x.1 * x.2)‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by
  simpa [smul_zero] using dist_smul_pair r 0 x

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
⊢ ((comap f) m) (f ⁻¹' s) = m s

Tactic:
comap_apply,

Goal state after:
α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
⊢ m (f '' f ⁻¹' s) = m s
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
⊢ ((comap f) ((map f) m)) s = m s

Tactic:
comap_apply,

Goal state after:
α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
⊢ ((map f) m) (f '' s) = m s
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ ((comap f) ⊤) s = ⊤ s

Tactic:
comap_apply,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ ⊤ (f '' s) = ⊤ s
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable f ↔ ¬Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]

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

Goal state before:
pp: case zero.neg
⊢ Decidable (zero ≤ neg)

Tactic:
exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case pos.zero
⊢ Decidable (pos ≤ zero)

Tactic:
exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case pos.neg
⊢ Decidable (pos ≤ neg)

Tactic:
exact isFalse (by rintro ⟨_⟩)

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

Goal state before:
pp: case neg.refl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0

Tactic:
exact (le_of_not_gt h_1).eq_of_not_lt h_2

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

Goal state before:
pp: case mp
x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y → x = y

Tactic:
rintro ⟨habs, hsign⟩

Goal state after:
case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ x = y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case bot
⊢ 0 = -0

Tactic:
neg_zero

Goal state after:
case bot
⊢ 0 = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top
⊢ 0 = -0

Tactic:
neg_zero

Goal state after:
case top
⊢ 0 = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : a ≠ 0
⊢ a / a = 1

Tactic:
by
  rw [← coe_toReal h₂ h₁] at h₃ ⊢
  rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]

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

Goal state before:
pp: case inr
α : Type u_4
s : Set α
hinf : s.Infinite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
have : Infinite s := infinite_coe_iff.mpr hinf
    rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

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

Goal state before:
pp: α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Iio ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x

Tactic:
by simp only [true_implies, mem_Iio]

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

Goal state before:
pp: case h'
x✝¹ : ℝ
x : EReal
x✝ : x ∈ Iic ↑x✝¹ ∩ {⊥}ᶜ
h1 : x ≤ ↑x✝¹
h2 : x ∈ {⊥}ᶜ
⊢ x ∈ Ioc ⊥ ↑x✝¹

Tactic:
simp [h1, Ne.bot_lt' fun a ↦ h2 a.symm]

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 β
⊢ (OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯) s ≤ ((comap f) (OuterMeasure.ofFunction m m_empty)) s

Tactic:
comap_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 β
⊢ (OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯) s ≤ (OuterMeasure.ofFunction m m_empty) (f '' s)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

Tactic:
· intro y hy
    rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩
    filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
h₃ : ¬a✝ = 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ↑a✝)

Tactic:
exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)

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

Tactic:
Finset.mem_range

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
Finset.mem_range

Goal state after:
case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f a ≤ f x
⊢ a ∈ f ⁻¹' v

Tactic:
exact hl ⟨lfa, h⟩

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ {s_1 | ∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s_1 = ⋂ x ∈ t, f x} ↔
    s' ∈ {s' | ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i}

Tactic:
Set.mem_ofPred_eq

Goal state after:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔ ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
⊢ t1 ∩ t2 ∈ {s | ∃ t, ∃ (_ : ↑t ⊆ S), ∃ f, ∃ (_ : ∀ x ∈ t, f x ∈ π x), s = ⋂ x ∈ t, f x}

Tactic:
Set.mem_ofPred_eq

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
⊢ ∃ t, ∃ (_ : ↑t ⊆ S), ∃ f, ∃ (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ μ (toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ) = 0

Tactic:
measure_toMeasurable

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
MeasurableSpace.generateFrom_singleton

Goal state after:
α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Module: Mathlib.MeasureTheory.Measure.Map

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

Tactic:
rw [mem_ae_map_iff h hf]

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

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

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ μ (f ⁻¹' s) = μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
⊢ c • μ ≪ c • ν

Tactic:
by
  intro s hνs
  rw [smul_apply, ← smul_one_smul ℝ≥0∞, smul_eq_mul, mul_eq_zero] at hνs ⊢
  exact hνs.imp_right fun hs ↦ h hs

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, {i | x ∈ s i}.Finite

Tactic:
by
  rw [ae_iff, ← measure_limsup_cofinite_eq_zero h]
  congr 1 with x
  simp [mem_limsup_iff_frequently_mem, Filter.Frequently]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
k : ℕ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
by
  induction k with
  | zero => rfl
  | succ k ih =>
    rw [iterate_succ, preimage_comp]
    exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs

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

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ (comap (fun x ↦ x) μ) s = μ s

Tactic:
comap_apply,

Goal state after:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ μ ((fun x ↦ x) '' s) = μ s

case hfi
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective fun x ↦ x

case hf
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet ((fun x ↦ x) '' s)

case hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
measure_toMeasurable

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (𝓝[<] a) l

Tactic:
← map_coe_Iio_atTop a ha,

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (map Subtype.val atTop) l
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
rw [inter_comm]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (t ∩ s).Nonempty
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
μ : Measure α
h : SigmaFinite μ
n : ℕ
⊢ μ (toMeasurable μ (⋯.some.set n)) < ∞

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
μ : Measure α
h : SigmaFinite μ
n : ℕ
⊢ μ (⋯.some.set n) < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ (μ.restrict t) (toMeasurable (μ.restrict t) s) = (μ.restrict t) s

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ (μ.restrict t) s = (μ.restrict t) s
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
| insert i s _ hs =>

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

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

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
n : ℕ
⊢ μ (t ∩ v n) < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
p : β → Prop
hp : MeasurableSet {x | p x}
⊢ (∀ᵐ (y : β) ∂Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)

Tactic:
by
  rw [← map_trim_comap hf, ae_map_iff (Measurable.of_comap_le le_rfl).aemeasurable hp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
a✝ : MeasurableSet s
⊢ 0 = ν s

Tactic:
apply_eq_zero_of_isEmpty

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
a✝ : MeasurableSet s
⊢ 0 = 0
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case mp
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn α p t

Tactic:
exact h.of_subtype <| fun s ↦ id

Goal state after: