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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0

Tactic:
refine ⟨fun n => (hf.approx n).restrict s, ?_, ?_⟩
  · intro x
    by_cases hx : x ∈ s
    · simpa [SimpleFunc.coe_restrict, hs, hx] using hf.tendsto_approx x
    · simpa [SimpleFunc.coe_restrict, hs, hx, hf_zero x hx] using tendsto_const_nhds
  · intro x hx n
    simp [SimpleFunc.coe_restrict, hs, hx]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
h_sub : MeasurableSpace.comap Subtype.val m ≤ MeasurableSpace.comap Subtype.val m₂
x y : ↑sᶜ
⊢ sᶜ.domRestrict f x = sᶜ.domRestrict f y

Tactic:
by simp [hf_zero _ x.2, hf_zero _ y.2]

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ (CauchySeq fun s ↦ ∑ i ∈ s, f i) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]
  · simp only [ball_zero_eq, Set.mem_ofPred_eq]
  · rintro s t hst ⟨s', hs'⟩
    exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case neg
α : 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
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∉ V
⊢ y ∈ E ∩ D ∪ V ∩ C

Tactic:
exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)

Goal state after:
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 β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε

Tactic:
have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos

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 β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
this : ∀ᶠ (b : Finset ι) in atTop, ∑' (a : { x // x ∉ b }), u ↑a < ε
⊢ ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable (U n)

Tactic:
simp_rw [U, this]

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable ((fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ StronglyMeasurable (U n)

Tactic:
simp_rw [U, this]

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Subtype.val ⁻¹' Iio ↑x = Ico 0 x

Tactic:
preimage_subtype_val_Iio

Goal state after:
x : ↑I
⊢ Iio x = Ico 0 x
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z

Tactic:
by_cases ht : (t : ℝ) = 1
    · simp [ht]
    · have : (1 - s * t : ℝ) ≠ 0 := by
        intro h
        have : 1 ≤ (t : ℝ) := by nlinarith [s.2.2, t.2.1]
        grind
      field_simp
      ring_nf

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
⊢ Injective (inducedMap A).snd

Tactic:
by
  rintro x y hxy
  ext1
  apply res_injective
  ext n : 1
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [res_succ, cons.injEq]
    refine ⟨?_, ih⟩
    contrapose hA
    simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne, not_forall, exists_prop]
    refine ⟨res x n, _, _, hA, ?_⟩
    rw [not_disjoint_iff]
    refine ⟨(inducedMap A).2 x, ?_, ?_⟩
    · rw [← res_succ]
      apply map_mem
    rw [hxy, ih, ← res_succ]
    apply map_mem

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

Goal state before:
pp: case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F).pi U
Uu : (↑F).pi U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
⊢ ∃ v ∈ {s | ∃ x n, s = cylinder x n}, x ∈ v ∧ v ⊆ u

Tactic:
refine ⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans ?_ Uu⟩

Goal state after:
case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F).pi U
Uu : (↑F).pi U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
⊢ cylinder x (n + 1) ⊆ (↑F).pi U
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : MeasurableSet s
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
rw [← hf.map_eq, restrict_map hf.measurable hs]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
μa' : Measure α
μb' : Measure β
hf : MeasurePreserving f μa μb
hf' : MeasurePreserving f μa' μb'
⊢ μb + map f μa' = μb + μb'

Tactic:
hf'.map_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
μa' : Measure α
μb' : Measure β
hf : MeasurePreserving f μa μb
hf' : MeasurePreserving f μa' μb'
⊢ μb + μb' = μb + μb'
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol : μ univ < ↑n * μ s
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s
this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)
⊢ ∃ i < n, ∃ j < n, i ≠ j ∧ (f^[i] ⁻¹' s ∩ f^[j] ⁻¹' s).Nonempty

Tactic:
by
    simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ ↦ A m) this

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ μ ⟂ₘ μ

Tactic:
(rw [h]; exact zero_left)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ (map f μ) univ = 1

Tactic:
by simp [map_apply_of_aemeasurable, hf]

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

Goal state before:

Tactic:
dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
    _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ ∈ measurableAtom x

Tactic:
convert! h_points_mem _
      simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
this : ⊥ = 0
u : Set α
hu : MeasurableSet u
x✝ : u.Nonempty
⊢ sInf {m | ∃ t, m = μ (t ∩ u) + ν (tᶜ ∩ u)} = 0

Tactic:
refine csInf_eq_bot_of_bot_mem ⟨t, ?_⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
this : ⊥ = 0
u : Set α
hu : MeasurableSet u
x✝ : u.Nonempty
⊢ ⊥ = μ (t ∩ u) + ν (tᶜ ∩ u)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
x y : α
s : Set α
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left✝ : z ∈ univ
hz : measurableAtom z = s
h_points_mem : points ⟨s, ⋯⟩ ∈ s
hsy : points ⟨s, ⋯⟩ = y
⊢ measurableAtom (points ⟨s, ⋯⟩) = measurableAtom z

Tactic:
refine measurableAtom_eq_of_mem ?_

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
x y : α
s : Set α
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left✝ : z ∈ univ
hz : measurableAtom z = s
h_points_mem : points ⟨s, ⋯⟩ ∈ s
hsy : points ⟨s, ⋯⟩ = y
⊢ points ⟨s, ⋯⟩ ∈ measurableAtom z
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
obtain ⟨b, b_count, -, hb⟩ :
      ∃ b : Set (Set (range f)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b :=
    exists_countable_basis (range f)
  have : Countable b := b_count.to_subtype
  have : ∀ s : b, IsClopenable (rangeFactorization f ⁻¹' s) := fun s ↦ by
    apply MeasurableSet.isClopenable
    exact hf.subtype_mk (hb.isOpen s.2).measurableSet
  choose T Tt Tpolish _ Topen using this
  obtain ⟨t', t'T, t't, t'_polish⟩ :
      ∃ t' : TopologicalSpace α, (∀ i, t' ≤ T i) ∧ t' ≤ t ∧ @PolishSpace α t' :=
    exists_polishSpace_forall_le (t := t) T Tt Tpolish
  refine ⟨t', t't, ?_, t'_polish⟩
  have : Continuous[t', _] (rangeFactorization f) :=
    hb.continuous_iff.2 fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
  exact continuous_subtype_val.comp this

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:
rw [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.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
⊢ x ∈ s

Tactic:
refine nonempty_iInter_of_nonempty_biInter (fun n => isClosed_closedBall)
      (fun n => isBounded_closedBall) (fun N ↦ ?_) L

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
⊢ (⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty
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:
rw [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.Topology.MetricSpace.PiNat

Goal state before:
pp: case h
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
x y z : (i : ι) → F i
n : ι
⊢ min (2⁻¹ ^ encode n) (min (2⁻¹ ^ encode n) (edist (x n) (y n)) + min (2⁻¹ ^ encode n) (edist (y n) (z n))) ≤
    min (2⁻¹ ^ encode n) (edist (x n) (y n)) + min (2⁻¹ ^ encode n) (edist (y n) (z n))

Tactic:
min_le_right

Goal state after:
case h
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
x y z : (i : ι) → F i
n : ι
⊢ min (2⁻¹ ^ encode n) (edist (x n) (y n)) + min (2⁻¹ ^ encode n) (edist (y n) (z n)) ≤
    min (2⁻¹ ^ encode n) (edist (x n) (y n)) + min (2⁻¹ ^ encode n) (edist (y n) (z n))
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (g a) s) (m.bind f)

Tactic:
exact (measurable_coe hs).comp_aemeasurable hg

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

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
a : ι
⊢ min (2⁻¹ ^ encode a) (edist (x a) (y a)) = ENNReal.ofReal (min (2⁻¹ ^ encode a) (dist (x a) (y a)))

Tactic:
simp [edist, ENNReal.inv_pow, PseudoMetricSpace.edist_dist (x a) (y a)]

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

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
by
  cases isEmpty_or_nonempty X
  · exact continuous_of_discreteTopology
  refine continuous_projIcc.comp <| Continuous.dist continuous_id' ?_
  convert! continuous_const (y := denseSeq X n)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
⊢ (x • μ).OuterRegular

Tactic:
· refine ⟨fun A _ r hr => ?_⟩
    rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr
    simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using! hr

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : ↑(hST.equiv g).1 = g
⊢ ↑(hST.equiv g).1 ∈ S

Tactic:
exact Subtype.prop _

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : ↑(hST.equiv g).2 = g
⊢ ↑(hST.equiv g).2 ∈ T

Tactic:
exact Subtype.prop _

Goal state after:
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 μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ ν (⇑MeasurableEquiv.prodAssoc ⁻¹' s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

Tactic:
congr 1 with x

Goal state after:
case e_6
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν✝ : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
x : (α × β) × γ
⊢ x ∈ ⇑MeasurableEquiv.prodAssoc ⁻¹' s ×ˢ t ×ˢ u ↔ x ∈ (s ×ˢ t) ×ˢ u