mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: case refine_1
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ‖x‖ ≤ ‖f x‖

pp: case refine_2
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
x : E
⊢ ‖x‖ ≤ ↑(NNReal.mk c⁻¹ ⋯) * ‖f x‖

Tactic:
· grw [hK.le_mul_norm' (map_one f), ← mul_assoc]
    exact mul_le_of_le_one_left (norm_nonneg' (f x)) (by simp [field])

Goal state after:
case refine_2
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
x : E
⊢ ‖x‖ ≤ ↑(NNReal.mk c⁻¹ ⋯) * ‖f x‖
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
⊢ ∀ (e g : X ≃ᵈ Y), ⇑e.toEquiv = ⇑g.toEquiv → ⇑e.symm = ⇑g.symm → e = g

Tactic:
rintro ⟨⟩ ⟨⟩ h -

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } = { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = ↑(r • 1) • ↑s

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = ↑(r • 1) * ↑s
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: r : ℝ≥0
s : ℝ≥0∞
⊢ (↑r • s).toReal = r • s.toReal

Tactic:
smul_eq_mul,

Goal state after:
r : ℝ≥0
s : ℝ≥0∞
⊢ (↑r * s).toReal = r • s.toReal
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMul α β
inst✝ : NormSMulClass α β
r : α
x : β
⊢ ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

Tactic:
by simp [enorm, nnnorm_smul]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
inst✝ : DecidableEq ι
i : ι
is : List ι
v : TProd α (i :: is)
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ α j

Tactic:
by
      subst hji
      exact v.1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *
  intro x hx
  rcases basis_sets _ |>.map _ |>.disjoint_iff nhds_basis_ball
    |>.mp (hf x hx) with ⟨U, hUx, r, hr₀, hr⟩
  refine Tendsto.comp (uniformContinuousOn_inv₀ (s := (closedBall (0 : α) (r / 2))ᶜ)
    (by simp [closedBall_mem_nhds, hr₀])) <| tendsto_inf.mpr ⟨hF x hx, tendsto_principal.mpr ?_⟩
  filter_upwards [hF x hx (dist_mem_uniformity (half_pos hr₀)), tendsto_snd hUx] with y hy₁ hy₂
  have : r ≤ ‖f y.2‖ := by simp_all [Set.disjoint_left]
  have : r / 2 < ‖F y.1 y.2‖ := by
    simp [dist_eq_norm_sub] at hy₁
    linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]
  simp_all [(half_lt_self hr₀).trans_le]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ generateFrom (insert ∅ S) = generateFrom S

Tactic:
by
  rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
⊢ Disjoint (measurableAtom x) (measurableAtom y)

Tactic:
Set.disjoint_iff_inter_eq_empty

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
⊢ measurableAtom x ∩ measurableAtom y = ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
j : δ
h : j = a
⊢ Measurable fun x ↦ ⋯ ▸ x.2

Tactic:
subst h
    dsimp
    exact measurable_snd

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

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∀ (b : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)),
    Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) b ∉ s → Sum.elim sgn 0 b = 0

Tactic:
rintro (b | b) hb

Goal state after:
case inl
α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
b : β
hb : Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) (Sum.inl b) ∉ s
⊢ Sum.elim sgn 0 (Sum.inl b) = 0

case inr
α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
b : Fin (n - ∑ i ∈ s, (f i).natAbs)
hb : Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) (Sum.inr b) ∉ s
⊢ Sum.elim sgn 0 (Sum.inr b) = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ a * (b / c) = a * b / c

Tactic:
change a * (b * c⁻¹) = (a * b) * c⁻¹
  rw [mul_assoc]

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

Goal state before:
pp: b : EReal
h : b ≤ 0
⊢ Antitone fun a ↦ a / b

Tactic:
by
  intro a a' h'
  change a' * b⁻¹ ≤ a * b⁻¹
  rw [← neg_neg (a * b⁻¹), ← neg_neg (a' * b⁻¹), neg_le_neg_iff, mul_comm a b⁻¹, mul_comm a' b⁻¹,
    ← neg_mul b⁻¹ a, ← neg_mul b⁻¹ a', mul_comm (-b⁻¹) a, mul_comm (-b⁻¹) a', ← inv_neg b]
  have : 0 ≤ -b := by apply EReal.le_neg_of_le_neg; simp [h]
  exact div_le_div_right_of_nonneg this h'

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

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c

Tactic:
mul_div b c b,

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * c / b ↔ a ≤ b * c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]

Goal state after:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 + a.2
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
hr' hr : r < 1
⊢ (↑(1 - r))⁻¹ = (↑(1 - r))⁻¹

Tactic:
coe_sub,

Goal state after:
r : ℝ≥0
hr' hr : r < 1
⊢ (↑1 - ↑r)⁻¹ = (↑1 - ↑r)⁻¹
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: x : EReal × EReal
y : EReal
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
by_cases hx₁ : x.1 = ⊥

Goal state after:
case pos
x : EReal × EReal
y : EReal
hx₁ : x.1 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y

case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : m.Nonempty
⊢ (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)

Tactic:
sInf_eq_boundedBy_sInfGen,

Goal state after:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : m.Nonempty
⊢ (boundedBy (sInfGen m)) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
ι : 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 : ι
⊢ 0 < (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) i

pp: case refine_2
ι : 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 ≤ ε
⊢ HasSum (fun i ↦ (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) ↑i) c

Tactic:
· conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]

Goal state after:
case refine_2
ι : 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 ≤ ε
⊢ HasSum (fun i ↦ (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) ↑i) c
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

Tactic:
by rintro rfl s; rfl

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

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ (∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ) → AEMeasurable g μ

Tactic:
intro h
    use fun x a ↦ (h a).mk _ x, measurable_pi_lambda _ fun a ↦ (h a).measurable_mk
    exact (eventually_countable_forall.mpr fun a ↦ (h a).ae_eq_mk).mono fun _ h ↦ funext h

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

Goal state before:
pp: case refine_1
α✝ : 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 γ
⊢ Measurable ((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inl) univ).symm)

Tactic:
refine (prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 ?_

Goal state after:
case refine_1
α✝ : 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 γ
⊢ Measurable
    (((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inl) univ).symm) ∘
      ⇑(Set.rangeInl.prodCongr (Set.univ γ)).symm)
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : IsMax k
⊢ m ≤ φ m

pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
⊢ m ≤ φ m

Tactic:
· rw [succ_eq_iff_isMax.2 hk] at hm
    exact ih (hφ.mono <| Iic_subset_Iic.2 (le_succ _)) _ hm

Goal state after:
case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
⊢ m ≤ φ m
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((OuterMeasure.map (AEMeasurable.mk f hf)) μ.toOuterMeasure) s = μ (f ⁻¹' s)

Tactic:
measure_congr (hf.ae_eq_mk.preimage s)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((OuterMeasure.map (AEMeasurable.mk f hf)) μ.toOuterMeasure) s = μ (AEMeasurable.mk f hf ⁻¹' 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
s : Set α
hνs : (c • 1) • ν s = 0
⊢ (c • 1) • μ s = 0

Tactic:
smul_eq_mul,

Goal state after:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : c • 1 * ν s = 0
⊢ c • 1 * μ s = 0
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : QuasiMeasurePreserving f μa μb
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μa] f'
⊢ QuasiMeasurePreserving f' μa μb

Tactic:
by
  refine ⟨hf', ?_⟩
  rw [Measure.map_congr h.symm]
  exact hf.absolutelyContinuous

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

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

Tactic:
by
    simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
⊢ comap f (comap g μ) = comap (g ∘ f) μ

Tactic:
by_cases hf : Injective f

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ (s \ t) = 0
⊢ μ (s ∩ t) = μ s

Tactic:
← sdiff_compl,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ (s \ t) = 0
⊢ μ (s \ tᶜ) = μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ tᶜ = 0
⊢ μ (s ∩ t) = μ s

Tactic:
← sdiff_compl,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ tᶜ = 0
⊢ μ (s \ tᶜ) = μ 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 α
⊢ (μ univ)⁻¹ • μ univ < ∞

Tactic:
smul_eq_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.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 α
R : Type u_5
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsFiniteMeasure μ
r : R
⊢ IsFiniteMeasure (r • μ)

Tactic:
by
  rw [← smul_one_smul ℝ≥0 r μ]
  infer_instance

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))

Tactic:
by_cases ha : Order.IsPredPrelimit a
  · have : (atBot : Filter (Ioi a)).IsCountablyGenerated := by
      rw [← comap_coe_Ioi_nhdsGT a ha]
      infer_instance
    simp_rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]
    apply tendsto_measure_iInter_atBot
    · rwa [Subtype.forall]
    · exact fun i j h ↦ hm i j i.2 h
    · simpa only [Subtype.exists, exists_prop]
  · rw [Order.not_isPredPrelimit_iff] at ha
    rcases ha with ⟨b, hab⟩
    simp [hab.nhdsGT]

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

Goal state before:
pp: case iUnion
α : 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
u : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), μ (f i ∩ t) = ν (f i ∩ t)
⊢ μ ((⋃ i, f i) ∩ t) = ν ((⋃ i, f i) ∩ t)

Tactic:
simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢

Goal state after:
case iUnion
α : 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
u : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), (μ.restrict t) (f i) = (ν.restrict t) (f i)
⊢ (μ.restrict t) (⋃ i, f i) = (ν.restrict t) (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
⊢ x ∈ ⋃ i, f i

Tactic:
obtain ⟨t, tT, xt⟩ : ∃ t : Set α, t ∈ range f ∧ x ∈ t := by
    have : x ∈ ⋃₀ T := by simp only [hT, mem_univ]
    simpa only [mem_sUnion, exists_prop, ← hf]

Goal state after:
case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
t : Set α
tT : t ∈ range f
xt : x ∈ t
⊢ x ∈ ⋃ i, f i
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
refine ext_of_generateFrom_of_cover h_gen hc h_inter hU htop ?_ fun t ht => h_eq t (h_sub ht)
  intro t ht s hs; rcases (s ∩ t).eq_empty_or_nonempty with H | H
  · simp only [H, measure_empty]
  · exact h_eq _ (h_inter _ hs _ (h_sub ht) H)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
⊢ μ Set.univ < ∞

Tactic:
exact measure_lt_top _ _

Goal state after:
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 a ≤ (g / f) a

Tactic:
· rwa [Pi.one_apply, Pi.div_apply, one_le_div']

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ μ (s ∩ t) = μ (t ∩ s)

Tactic:
inter_comm t

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ μ (s ∩ t) = μ (s ∩ t)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case hC
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht' : t' ∈ {t | ∃ s_1, MeasurableSet s_1 ∧ Subtype.val ⁻¹' s_1 = t}
ht✝ : MeasurableSet t'
⊢ NullMeasurableSet (Subtype.val '' t') μ

Tactic:
obtain ⟨s', hs', rfl⟩ := ht'

Goal state after:
case hC
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht✝ : MeasurableSet (Subtype.val ⁻¹' s')
⊢ NullMeasurableSet (Subtype.val '' Subtype.val ⁻¹' s') μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ (ν₁.restrict (spanningSets μ i)) s = (ν₂.restrict (spanningSets μ i)) s

Tactic:
rw [← ENNReal.add_right_inj (measure_mono s.inter_subset_right |>.trans_lt <|
    measure_spanningSets_lt_top μ i).ne]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s =
    μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
⊢ ∀ (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
let := generateFrom S

Goal state after:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
⊢ ∀ (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
x y : α
h : True → y = x
⊢ x = y

Tactic:
forall_true_left

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
x y : α
h : y = x
⊢ x = y