mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
rw [tendsto_iff_seq_tendsto]
  intro x xl
  have hxl := by
    rw [tendsto_atTop'] at xl
    exact xl
  have h := inter_mem hF_meas h_bound
  replace h := hxl _ h
  rcases h with ⟨k, h⟩
  rw [← tendsto_add_atTop_iff_nat k]
  refine tendsto_lintegral_of_dominated_convergence' ?_ ?_ ?_ ?_ ?_
  · exact bound
  · intro
    refine (h _ ?_).1
    exact Nat.le_add_left _ _
  · intro
    refine (h _ ?_).2
    exact Nat.le_add_left _ _
  · assumption
  · refine h_lim.mono fun a h_lim => ?_
    apply @Tendsto.comp _ _ _ (fun n => x (n + k)) fun n => F n a
    · assumption
    rw [tendsto_add_atTop_iff_nat]
    assumption

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⨆ i, μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0

Tactic:
ENNReal.iSup_eq_zero

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ∀ (i : ℕ), μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
n : ℕ
⊢ μ ((tᶜ ∪ T n) ∩ ⋃ b, T b) < ∞

Tactic:
Set.union_inter_distrib_right,

Goal state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
n : ℕ
⊢ μ ((tᶜ ∩ ⋃ b, T b) ∪ T n ∩ ⋃ b, T b) < ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MulZeroClass β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑((fun n ↦ hf.approx n * hg.approx n) n)) < ∞

Tactic:
exact (measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n)

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : ({x} ∩ closure[inst✝¹] (U \ {x})).Nonempty
⊢ AccPt x (𝓟 U)

Tactic:
rw [Set.singleton_inter_nonempty, mem_closure_iff_clusterPt,
      ← accPt_principal_iff_clusterPt] at h

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (n : ι), f n x - ∑ n ∈ n, f n x‖ < ε

Tactic:
← A.of_norm.sum_add_tsum_subtype_compl n,

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑ x_1 ∈ n, f x_1 x + ∑' (x_1 : { x // x ∉ n }), f (↑x_1) x - ∑ n ∈ n, f n x‖ < ε
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case left
α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a✝ b✝ c d : α
h : a✝ ≤ b✝
δ : α
a b : ℝ
x y : ↑(Icc a b)
t : ↑unitInterval
⊢ a ≤ (1 - ↑t) * ↑x + ↑t * ↑y

pp: case right
α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a✝ b✝ c d : α
h : a✝ ≤ b✝
δ : α
a b : ℝ
x y : ↑(Icc a b)
t : ↑unitInterval
⊢ (1 - ↑t) * ↑x + ↑t * ↑y ≤ b

Tactic:
· nlinarith [x.2.1, y.2.1, t.2.1, t.2.2]

Goal state after:
case right
α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a✝ b✝ c d : α
h : a✝ ≤ b✝
δ : α
a b : ℝ
x y : ↑(Icc a b)
t : ↑unitInterval
⊢ (1 - ↑t) * ↑x + ↑t * ↑y ≤ b
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h_open
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ u ∈ {s | ∃ x n, s = cylinder x n}, IsOpen[Pi.topologicalSpace] u

Tactic:
rintro u ⟨x, n, rfl⟩
    apply isOpen_cylinder

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)

Tactic:
have := x.property.some_mem
  rw [mem_iInter] at this
  exact this n

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
hA : VanishingDiam A
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
⊢ ∃ n, ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε

Tactic:
specialize hA x

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : Tendsto (fun n ↦ Metric.ediam (A (res x n))) atTop (𝓝 0)
⊢ ∃ n, ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
⊢ ∃ x, Tendsto u atTop (𝓝 x)

Tactic:
have I : ∀ n, 1 / C ≤ infDist (u n).1 sᶜ := fun n ↦ by
    have : 0 < infDist (u n).1 sᶜ := Hmem.1 (u n).2
    rw [div_le_iff₀' Cpos]
    exact (div_le_iff₀ this).1 (hC n).le

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
I : ∀ (n : ℕ), 1 / C ≤ infDist (↑(u n)) (↑s)ᶜ
⊢ ∃ x, Tendsto u atTop (𝓝 x)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
n : ℕ
⊢ {a | a.1 n = a.2 n} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}

Tactic:
refine mem_iInf_of_mem ((1 / 2) ^ n : ℝ) ?_

Goal state after:
case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
n : ℕ
⊢ {a | a.1 n = a.2 n} ∈ ⨅ (_ : (1 / 2) ^ n > 0), 𝓟 {p | dist p.1 p.2 < (1 / 2) ^ n}
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
⊢ (inducedMap A).fst = univ

Tactic:
by
  rw [eq_univ_iff_forall]
  intro x
  choose u hu using fun n => hnonempty (res x n)
  have umem : ∀ n m : ℕ, n ≤ m → u m ∈ A (res x n) := by
    have : Antitone fun n : ℕ => A (res x n) := by
      refine antitone_nat_of_succ_le ?_
      intro n
      apply hanti.antitone
    intro n m hnm
    exact this hnm (hu _)
  have : CauchySeq u := by
    rw [Metric.cauchySeq_iff]
    intro ε ε_pos
    obtain ⟨n, hn⟩ := hdiam.dist_lt _ ε_pos x
    use n
    intro m₀ hm₀ m₁ hm₁
    apply hn <;> apply umem <;> assumption
  obtain ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this
  use y
  rw [mem_iInter]
  intro n
  apply hanti _ (x n)
  apply mem_closure_of_tendsto hy
  rw [eventually_atTop]
  exact ⟨n.succ, umem _⟩

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

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
⊢ dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd) =
    dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hx (fun {k} ↦ f k) x.snd)

Tactic:
dist_comm

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
⊢ dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hx (fun {k} ↦ f k) x.snd) =
    dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hx (fun {k} ↦ f k) x.snd)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
y : (n : ℕ) → E n
ys : y ∈ s
hy : cylinder x (Nat.find A - 1) = cylinder y (Nat.find A - 1)
⊢ cylinder y (Nat.find A - 1) = cylinder x (Nat.find A - 1)

Tactic:
rw [hy]

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

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
⊢ TopologicalSpace.SeparableSpace (InductiveLimit I)

Tactic:
let s := ⋃ (i : ℕ), (toInductiveLimit I i '' (hsX i))

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit I) := ⋃ i, toInductiveLimit I i '' hsX i
⊢ TopologicalSpace.SeparableSpace (InductiveLimit I)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∉ s
⊢ firstDiff x y ≤ firstDiff x (f y)

Tactic:
have A : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
        inter_cylinder_longestPrefix_nonempty hs hne y

Goal state after:
case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∉ s
A : (s ∩ cylinder y (longestPrefix y s)).Nonempty
⊢ firstDiff x y ≤ firstDiff x (f y)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this : PolishSpace ↑s
⊢ AnalyticSet s

Tactic:
rw [← @Subtype.range_val α s]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this : PolishSpace ↑s
⊢ AnalyticSet (range Subtype.val)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ (t \ (↑s)ᶜ) = (∑ a ∈ s, μ {a} • dirac a) t

Tactic:
rw [Set.sdiff_compl, ← (s : Set α).biUnion_of_singleton]

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ ⋃ x ∈ ↑s, {x}) = (∑ a ∈ s, μ {a} • dirac a) t
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}

Tactic:
disjoint_singleton_right

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ a ∉ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ f (⋃ i, spanningSets (μ.trim hm) i) ≤ C

Tactic:
refine (h_F_lim S hS_meas hS_mono).trans ?_

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ ⨆ n, f (S n) ≤ C
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < 2⁻¹ ^ encode i
x y : (i : ι) → F i
hn : edist x y < 2⁻¹ ^ encode i
⊢ edist x y < ε → edist (x i) (y i) < ε

Tactic:
exact (edist_le_edist_pi_of_edist_lt hn).trans_lt

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
n i : ℕ
hi : i < n
⊢ y i = (↑(p n)).2.2 i

Tactic:
rw [hy]

Goal state after:
case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
n i : ℕ
hi : i < n
⊢ (fun n ↦ (↑(p (n + 1))).2.2 n) i = (↑(p n)).2.2 i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
firststep : X ≃ₜ PiNatEmbed X (fun i ↦ ↑I) (distDenseSeq X) :=
  { toFun := toPiNat, invFun := ofPiNat, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
secondstep : PiNatEmbed X (fun i ↦ ↑I) (distDenseSeq X) → ℕ → ↑I := embed X (fun i ↦ ↑I) (distDenseSeq X)
⊢ ∃ F, IsEmbedding F

Tactic:
let isEmbedding_secondstep : IsEmbedding secondstep :=
      (isUniformEmbedding_embed injective_distDenseSeq).isEmbedding

Goal state after:
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
firststep : X ≃ₜ PiNatEmbed X (fun i ↦ ↑I) (distDenseSeq X) :=
  { toFun := toPiNat, invFun := ofPiNat, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
secondstep : PiNatEmbed X (fun i ↦ ↑I) (distDenseSeq X) → ℕ → ↑I := embed X (fun i ↦ ↑I) (distDenseSeq X)
isEmbedding_secondstep : IsEmbedding secondstep :=
  IsUniformEmbedding.isEmbedding (isUniformEmbedding_embed injective_distDenseSeq)
⊢ ∃ F, IsEmbedding F
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
lintegral_eq_nnreal,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ ↑(f x)), (SimpleFunc.map ofNNReal φ).lintegral μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous[_, inst✝³] f
h : Disjoint (range f) ∅
⊢ MeasurablySeparable (range f) ∅

Tactic:
exact ⟨univ, subset_univ _, by simp, MeasurableSet.univ⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' S * ↑(map H.subtype H'') = ↑H

Tactic:
rw [← this, cmem.mul_eq]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' univ = ↑H
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
⊢ μ s = ν s

Tactic:
let C₂ := image2 (· ×ˢ ·) { t : Set β | MeasurableSet t } { u : Set γ | MeasurableSet u }

Goal state after:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
⊢ μ s = ν s
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : ⇑H.subtype '' (↑H'' * S) = ↑(map H.subtype H'') * ⇑H.subtype '' S
⊢ ↑(map H.subtype H'') * ⇑H.subtype '' S = ↑H

Tactic:
rw [← this, cmem.mul_eq]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : ⇑H.subtype '' (↑H'' * S) = ↑(map H.subtype H'') * ⇑H.subtype '' S
⊢ ⇑H.subtype '' univ = ↑H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ LeftCosetEquivalence (↑K) g₁ g₂

Tactic:
rw [LeftCosetEquivalence, leftCoset_eq_iff]
  constructor
  · intro h
    rw [← hSK.equiv_fst_mul_equiv_snd g₂, ← hSK.equiv_fst_mul_equiv_snd g₁, ← h,
      mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul]
    exact Subtype.property _
  · intro h
    apply (isComplement_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique
    · -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
      rw [equiv_fst_eq_mul_inv]; simp
    · rw [SetLike.mem_coe, ← mul_mem_cancel_right h]
      -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
      rw [equiv_fst_eq_mul_inv]; simp [← mul_assoc]

Goal state after: