mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z - ↑K * dist y z ≤ (fun x ↦ f ↑x + ↑K * dist y ↑x) t

Tactic:
dsimp

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z - ↑K * dist y z ≤ f ↑t + ↑K * dist y ↑t
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ limsup (f + g) u ≤ limsup f u

Tactic:
refine le_limsup_of_le (by isBoundedDefault) fun b hb ↦ ?_

Goal state after:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
⊢ limsup (f + g) u ≤ b
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzAdd.C ℝ) fun p ↦ p.1 + p.2

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
    exact lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : y = x
⊢ x = y

Tactic:
exact hxy.symm

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

Goal state before:
pp: case inr.refine_2
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ ∏ a, ⨆ i, f a i ≤ ⨆ i, ∏ a, f a (i a)

Tactic:
· rw [Classical.nonempty_pi] at h
    have H a : ∃ i : ι a, f a i = ⨆ i, f a i := exists_eq_ciSup_of_finite
    choose i hi using H
    simp only [← hi]
    exact Finite.le_ciSup_of_le i le_rfl

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
⊢ updateFinset x {i} y = update x i (y ⟨i, ⋯⟩)

Tactic:
congr with j
  by_cases hj : j = i
  · cases hj
    simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
  · simp [hj, updateFinset]

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

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x ↦ x) ⁻¹' Set.tprod l t = Set.tprod l t

Tactic:
dsimp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ x✝ ^ 0 = 1

Tactic:
ext; apply Nat.zero_mul

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Isometry ⇑(algebraMap 𝕜 𝕜')

Tactic:
refine Isometry.of_dist_eq fun x y => ?_
  rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']

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
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
⊢ ‖-x + y + (-y + z)‖ ≤ ‖-x + y‖ + ‖-y + z‖

Tactic:
exact core.norm_triangle _ _

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

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

Tactic:
dsimp

Goal state after:
case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x ↦ x.2
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case inr
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
simp [measurableSet_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
⊢ (fun a ↦ if 0 < a then 1 else if a < 0 then -1 else 0) a ≤ (fun a ↦ if 0 < a then 1 else if a < 0 then -1 else 0) b

Tactic:
dsimp

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
⊢ (if 0 < a then 1 else if a < 0 then -1 else 0) ≤ if 0 < b then 1 else if b < 0 then -1 else 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
⊢ sf < sg

Tactic:
have hg' : ∀ x, g x ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top (hg.tsum_eq.symm ▸ hsg)

Goal state after:
case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
⊢ sf < sg
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl.inr
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
use a', mem_Ioo.2 ⟨a0', aa'⟩

Goal state after:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl.inr
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
obtain ⟨a', a0', aa'⟩ := exists_between ha
      use a', mem_Ioo.2 ⟨a0', aa'⟩
      rw [mul_top_of_pos ha] at h
      rwa [mul_top_of_pos a0']

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

Goal state before:
pp: α : Type u_4
s : Set α
c : ℝ≥0∞
⊢ ∑' (x : ↑s), c = ↑s.encard * c

Tactic:
by
  simp [← tsum_set_one, ← ENNReal.tsum_mul_right]

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

Goal state before:
pp: case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
⊢ (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) h = (fun k ↦ (a + c * ↑k) / (b + d * ↑k)) h

Tactic:
dsimp

Goal state after:
case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
⊢ (a * (↑h)⁻¹ + c) / (b * (↑h)⁻¹ + d) = (a + c * ↑h) / (b + d * ↑h)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a r : ℝ
x✝ : EReal × EReal
h : ↑(r - (a - 1)) < x✝.1 ∧ ↑(a - 1) < x✝.2
⊢ ↑r < x✝.1 + x✝.2

Tactic:
simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

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

Goal state before:
pp: a r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑(r - (a + 1)) ∧ x✝.2 < ↑(a + 1)
⊢ x✝.1 + x✝.2 < ↑r

Tactic:
simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

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

Goal state before:
pp: r : ℝ≥0∞
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r ≠ ∞

Tactic:
refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))

Goal state after:
r : ℝ≥0∞
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
hr : r = ∞
⊢ (fun n ↦ ∞ ^ n) =ᶠ[atTop] fun x ↦ ∞
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : ↑(2 * max (x + 1) 0 / a) < p.1 ∧ ↑(a / 2) < p.2
⊢ ↑x < p.1 * p.2

Tactic:
rcases p_in_prod with ⟨p1_gt, p2_gt⟩

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ ↑x < p.1 * p.2
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ (n + m)

Tactic:
simp only [add_comm n, pow_add, ← div_div]

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
I : Set ι
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)

Tactic:
by
  simp only [← iInf_subtype'', iInf_apply' _ hs]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ∑' (i : ι), f i x') s x

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]
  refine lowerSemicontinuousWithinAt_iSup fun b => ?_
  exact lowerSemicontinuousWithinAt_sum fun i _hi => h i

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

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

Tactic:
refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_)

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.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case insert
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
i : ι
t : Finset ι
hi : i ∉ t
IH : (∀ i ∈ ↑t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ ↑t, s i)
h : ∀ i_1 ∈ ↑(insert i t), m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (⋃ i_1 ∈ ↑(insert i t), s i_1)

Tactic:
| insert i t hi IH =>

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
      · rw [Finset.coe_singleton]
      · rw [Finset.mem_singleton] at hx
        rwa [hx]
      · simp only [Finset.mem_singleton, iInter_iInter_eq_left]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
refine ⟨fun h => ?_, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩

Goal state after:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
h : ∃ 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: case neg
α : 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
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n

Tactic:
· exact absurd hn (by simp [hn1, h])

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] s

Tactic:
by
  convert! ae_eq_set_inter (ae_eq_refl s) h
  rw [inter_univ]

Goal state after:
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:
simp_rw +instances [MeasurableSpace.generateFrom_singleton]
  unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap
  simp_rw [MeasurableSpace.measurableSet_top, true_and]
  constructor
  · rintro ⟨x, rfl⟩
    by_cases hT : True ∈ x
    · by_cases hF : False ∈ x
      · suffices x = univ by grind
        grind [univ_eq_true_false]
      · grind
    · by_cases hF : False ∈ x
      · grind
      · suffices x ⊆ ∅ by grind
        intro p hp
        fin_cases p <;> contradiction
  · rintro (rfl | rfl | rfl | rfl)
    on_goal 1 => use ∅
    on_goal 2 => use {True}
    on_goal 3 => use {False}
    on_goal 4 => use Set.univ
    all_goals
      simp [compl_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a ↦ (Equiv.prodAssoc α β γ) a

Tactic:
dsimp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a ↦ (a.1.1, a.1.2, a.2)
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 γ
⊢ Measurable fun a ↦ (Equiv.prodAssoc α β γ).symm a

Tactic:
dsimp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a ↦ ((a.1, a.2.1), a.2.2)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s

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

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Measurable fun a ↦ (Equiv.sumPiEquivProdPi fun a ↦ α a) fun i ↦ a i

Tactic:
dsimp

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Measurable fun a ↦ (fun i ↦ a (Sum.inl i), fun i' ↦ a (Sum.inr i'))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ μ s + μ t ≤ μ u

Tactic:
calc
    μ s + μ t = μ (s ∪ t) := (measure_union h ht).symm
    _ ≤ μ u := measure_mono (union_subset h's h't)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ s = ⋃ n, s ∩ spanningSets μ n

Tactic:
← inter_iUnion,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ s = s ∩ ⋃ i, spanningSets μ i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, μ (s ∩ t) = 0
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : ⋃ n, t n = univ
⊢ s = ⋃ n, s ∩ t n

Tactic:
← inter_iUnion,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, μ (s ∩ t) = 0
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : ⋃ n, t n = univ
⊢ s = s ∩ ⋃ i, t i
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
← restrict_restrict_of_subset hs,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : s ⊆ t
h : μ.restrict t = ν.restrict t
⊢ (μ.restrict t).restrict s = ν.restrict s
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)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ ⋃ n, t ∩ disjointed w n

Tactic:
← inter_iUnion,

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)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ t ∩ ⋃ i, disjointed w i
Module: Mathlib.MeasureTheory.Measure.Trim

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

Tactic:
simp [trim_measurableSet_eq hm hs]

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 μ
⊢ (μ.trim hm) Set.univ < ∞

Tactic:
by
    rw [trim_measurableSet_eq hm (@MeasurableSet.univ _ m)]
    exact measure_lt_top _ _

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)

Tactic:
apply (measure_union_le _ _).trans

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ s) + μ (f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ iUnion t'

Tactic:
refine mem_iUnion.2 ⟨0, ?_⟩
        simp [hx, hxt]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < μ s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞

Tactic:
rw [← iSup_restrict_spanningSets,
    @lt_iSup_iff _ _ _ r fun i : ℕ => μ.restrict (spanningSets μ i) s] at h's

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : ∃ i, r < (μ.restrict (spanningSets μ i)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ (Measure.map f μ) (f '' spanningSets μ n ∪ (range f)ᶜ) < ∞

pp: case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ ⋃ i, f '' spanningSets μ i ∪ (range f)ᶜ = univ

Tactic:
· rw [hf.map_apply, Set.preimage_union]
    simp only [Set.preimage_compl, Set.preimage_range, Set.compl_univ, Set.union_empty,
      Set.preimage_image_eq _ hf.injective]
    exact measure_spanningSets_lt_top μ n

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ ⋃ i, f '' spanningSets μ i ∪ (range f)ᶜ = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.iUnion.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ⋃ i, f i = ⋃₀ ↑(⋃ n, ↑(S n)).toFinset

Tactic:
· simp only [coe_toFinset, sUnion_iUnion, hS_eq]

Goal state after: