mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
⊢ FinStronglyMeasurable f μ

Tactic:
have h_fs_t_compl : ∀ n, ∀ x, x ∉ t → fs n x = 0 := by
    intro n x hxt
    rw [SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)]
    refine Set.indicator_of_notMem ?_ _
    simp [hxt]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
⊢ FinStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ n, aeSeq hf p n) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [iSup_apply]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), ⨆ i, aeSeq hf p i a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
Measure.restrict_univ

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case neg.e_a.e_6
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
x : α
H : ¬g x = 0
⊢ x ∈ s

Tactic:
contrapose H

Goal state after:
case neg.e_a.e_6
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
x : α
H : x ∉ s
⊢ g x = 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite μ
⊢ SigmaFinite (μ.restrict univ)

Tactic:
Measure.restrict_univ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite μ
⊢ SigmaFinite μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ ‖f x‖

Tactic:
Real.norm_eq_abs

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ |f x|
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a ↦ f ↑a
hd : StronglyMeasurable fun a ↦ f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∉ s
⊢ Function.extend Subtype.val (fun x ↦ f ↑x) (Function.extend Subtype.val (fun x ↦ f ↑x) fun x ↦ default) x = f x

Tactic:
lift x to t using (h trivial).resolve_left hxs

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a ↦ f ↑a
hd : StronglyMeasurable fun a ↦ f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : { x // x ∈ t }
hxs : ↑x ∉ s
⊢ Function.extend Subtype.val (fun x ↦ f ↑x) (Function.extend Subtype.val (fun x ↦ f ↑x) fun x ↦ default) ↑x = f ↑x
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 (U ∩ C)).NeBot

Tactic:
← inf_principal,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ (𝓟 U ⊓ 𝓟 C)).NeBot
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ {a | ClusterPt a (𝓟 C)}
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Tactic:
exact hx

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ False

Tactic:
have hU_cnt : (U ∩ C).Countable := by
        apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)
        · rintro y ⟨yU, yC⟩
          by_cases h : y ∈ V
          · exact mem_union_right _ (mem_inter h yC)
          · exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)
        exact Countable.union h Vct

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : (U ∩ C).Countable
⊢ False
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]
    by_contra h
    rw [h, union_empty] at VD
    rw [VD] at hunc
    contradiction

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ K ↑z ⋯ + 2 * K' ↑z ⋯ ≤ K ↑z ⋯ + 2 * K' ↑z ⋯

Tactic:
by rfl

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

Goal state before:
pp: case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder y n = cylinder x n
⊢ y ∈ cylinder y n

Tactic:
exact self_mem_cylinder _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ 0 < ε / 2

Tactic:
ENNReal.div_pos_iff

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ∞
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) = inductiveLimitDist f y x

Tactic:
inductiveLimitDist_eq_dist I y x m hy hx,

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 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)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ range g

Tactic:
exact mem_range_self

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ μ.restrict s ⟂ₘ ν

Tactic:
refine ⟨h.nullSet, h.measurableSet_nullSet, ?_, h.measure_compl_nullSet⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ (μ.restrict s) h.nullSet = 0
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ Disjoint (ae μ) (ae ν)

Tactic:
by
  rw [disjoint_iff_inf_le]
  intro s _
  refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩
  · rw [mem_ae_iff, compl_union, compl_compl]
    exact measure_inter_null_of_null_right _ h.measure_nullSet
  · rw [mem_ae_iff, compl_union]
    exact measure_inter_null_of_null_right _ h.measure_compl_nullSet
  · rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
      ← compl_union, compl_compl, inter_union_compl, compl_compl]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Subsingleton α
i : α
⊢ count.restrict univ = count.restrict {i}

Tactic:
by congr; ext j; simp [Subsingleton.elim j i]

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

Goal state before:
pp: α : 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 := ⋯
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 := ⋯
p : ℕ → A := ⋯
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
⊢ m < (↑(p n)).1

Tactic:
pn_fst

Goal state after:
α : 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
⊢ m < n
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in univ, f x ∂μ

Tactic:
Measure.restrict_univ

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : 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 := ⋯
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 := ⋯
p : ℕ → A := ⋯
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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
⊢ m < (↑(p n)).1

Tactic:
pn_fst

Goal state after:
α : 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
⊢ m < n
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

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

Tactic:
set y : ℕ → ℕ := fun n => (p (n + 1)).1.2.2 n with hy

Goal state after:
α : 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
⊢ False
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case left
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
⊢ ∀ (i : ℝ≥0∞), 0 < i → {p | edist p.1 p.2 < i} ∈ ⨅ i, ⨅ i_2, ⨅ (_ : 0 < i_2), 𝓟 {a | edist (a.1 i) (a.2 i) < i_2}

pp: case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
⊢ ∀ (i : ι) (i_1 : ℝ≥0∞), 0 < i_1 → {a | edist (a.1 i) (a.2 i) < i_1} ∈ ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
· intro ε hε
      obtain ⟨K, hK⟩ : ∃ K : Finset ι, ∑' i : {j // j ∉ K}, 2⁻¹ ^ encode (i : ι) < ε / 2 :=
        ((tendsto_order.1 <| ENNReal.tendsto_tsum_compl_atTop_zero
          (tsum_geometric_encode_lt_top ENNReal.one_half_lt_one).ne).2 _
            <| by simpa using hε.ne').exists
      obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ δ * K.card < ε / 2 :=
        ENNReal.exists_pos_mul_lt (by simp) (by simpa using hε.ne')
      apply @mem_iInf_of_iInter _ _ _ _ _ K.finite_toSet fun i =>
          {p : (∀ i : ι, F i) × ∀ i : ι, F i | edist (p.fst i) (p.snd i) < δ}
      · rintro ⟨i, hi⟩
        refine mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)
        simp only [mem_principal, Subset.rfl]
      · rintro ⟨x, y⟩ hxy
        simp only [mem_iInter, mem_ofPred_eq, SetCoe.forall, Finset.mem_coe] at hxy
        calc
          edist x y = ∑' i : ι, min (2⁻¹ ^ encode i) (edist (x i) (y i)) := rfl
          _ = ∑ i ∈ K, min (2⁻¹ ^ encode i) (edist (x i) (y i)) +
                ∑' i : ↑(K : Set ι)ᶜ, min (2⁻¹ ^ encode (i : ι)) (edist (x i) (y i)) :=
            (ENNReal.sum_add_tsum_compl ..).symm
          _ ≤ ∑ i ∈ K, edist (x i) (y i) + ∑' i : ↑(K : Set ι)ᶜ, 2⁻¹ ^ encode (i : ι) := by
            gcongr
            · apply min_le_right
            · apply min_le_left
          _ < ∑ _i ∈ K, δ + ε / 2 := by
            refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK
            gcongr with i hi
            exact (hxy i hi).le
          _ ≤ ε / 2 + ε / 2 := by gcongr; simpa [mul_comm] using hδ.le
          _ = ε := ENNReal.add_halves _

Goal state after:
case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
⊢ ∀ (i : ι) (i_1 : ℝ≥0∞), 0 < i_1 → {a | edist (a.1 i) (a.2 i) < i_1} ∈ ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | edist p.1 p.2 < ε}
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
n : ℕ
hn : K < 2 ^ n
ε : ℝ
hε₀ : ε ∈ Ioi 0
hε : ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (t * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)

Tactic:
rw [mem_Ioi] at hε₀

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
n : ℕ
hn : K < 2 ^ n
ε : ℝ
hε₀ : 0 < ε
hε : ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (t * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ

Tactic:
refine lintegral_congr fun x ↦ ?_

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (x_1 : M), ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ ∂ν

Tactic:
refine lintegral_congr fun x ↦ ?_

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x✝ x : M
⊢ ∫⁻ (y : M), f (x✝ * x * y) ∂ρ = ∫⁻ (y : M), f (x✝ * (x * y)) ∂ρ
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x✝ x : M
⊢ ∫⁻ (y : M), f (x✝ * x * y) ∂ρ = ∫⁻ (y : M), f (x✝ * (x * y)) ∂ρ

Tactic:
refine lintegral_congr fun x ↦ ?_

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x✝¹ x✝ x : M
⊢ f (x✝¹ * x✝ * x) = f (x✝¹ * (x✝ * x))
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x✝¹ x✝ x : M
⊢ f (x✝¹ * x✝ * x) = f (x✝¹ * (x✝ * x))

Tactic:
refine lintegral_congr fun x ↦ ?_

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x✝¹ x✝ x : M
⊢ f (x✝¹ * x✝ * x) = f (x✝¹ * (x✝ * x))
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : ↑univ × ↑S
h✝ : (fun x ↦ ↑x.1 * ↑x.2) a = 1
⊢ S.Nonempty

Tactic:
exact ⟨a.2.1, a.2.2⟩

Goal state after: