mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
⊢ Measurable fun x ↦ liminf (fun x_1 ↦ f x_1 x) v

Tactic:
by
  classical
  /- We would like to write the liminf as `⨆ (j : Subtype p), ⨅ (i : s j), f i x`, as the
  measurability would follow from the measurability of infs and sups. Unfortunately, this is not
  true in general conditionally complete linear orders because of issues with empty sets or sets
  which are not bounded above or below. A slightly more complicated expression for the liminf,
  valid in general, is given in `Filter.HasBasis.liminf_eq_ite`. This expression, built from
  `if ... then ... else` and infs and sups, can be readily checked to be measurable. -/
  have : Countable (Subtype p) := hv.countable
  rcases isEmpty_or_nonempty (Subtype p) with hp | hp
  · simp [hv.liminf_eq_sSup_iUnion_iInter]
  by_cases H : ∃ (j : Subtype p), s j = ∅
  · simp_rw [hv.liminf_eq_ite, if_pos H, measurable_const]
  simp_rw [hv.liminf_eq_ite, if_neg H]
  have : ∀ i, Countable (s i) := fun i ↦ countable_coe_iff.2 (hs i)
  let m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range (fun (i : s j) ↦ f i x))}
  have m_meas : ∀ j, MeasurableSet (m j) :=
    fun j ↦ measurableSet_bddBelow_range (fun (i : s j) ↦ hf i)
  have mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j} := by
    rw [ofPred_forall]
    exact MeasurableSet.iInter (fun j ↦ (m_meas j).compl)
  refine measurable_const.piecewise mc_meas <| .iSup fun j ↦ ?_
  let reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
  let F0 : Subtype p → δ → α := fun j x ↦ ⨅ (i : s j), f i x
  have F0_meas : ∀ j, Measurable (F0 j) := fun j ↦ .iInf (fun (i : s j) ↦ hf i)
  set F1 : δ → α := fun x ↦ F0 (reparam x j) x with hF1
  change Measurable F1
  let g : ℕ → Subtype p := Classical.choose (exists_surjective_nat (Subtype p))
  have Z : ∀ x, ∃ n, x ∈ m (g n) ∨ ∀ k, x ∉ m k := by
    intro x
    by_cases! H : ∃ k, x ∈ m k
    · rcases H with ⟨k, hk⟩
      rcases Classical.choose_spec (exists_surjective_nat (Subtype p)) k with ⟨n, rfl⟩
      exact ⟨n, Or.inl hk⟩
    · exact ⟨0, Or.inr H⟩
  have : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find (Z x))) x := by
    ext x
    have A : reparam x j = if x ∈ m j then j else g (Nat.find (Z x)) := rfl
    split_ifs with hjx
    · have : reparam x j = j := by rw [A, if_pos hjx]
      simp only [hF1, this]
    · have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
      simp only [hF1, this]
  rw [this]
  apply Measurable.piecewise (m_meas j) (F0_meas j)
  apply Measurable.find (fun n ↦ F0_meas (g n)) (fun n ↦ ?_)
  exact (m_meas (g n)).union mc_meas

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ = ν ↔ ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν

Tactic:
by
  refine ⟨fun h _ _ ↦ by rw [h], ?_⟩
  intro h
  ext s hs
  simp only [← lintegral_indicator_one hs]
  exact h (s.indicator 1) ((measurable_indicator_const_iff 1).mpr hs)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
h : ¬f x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))

Tactic:
simp_all only [ne_eq, measurableSet_setOfPred, SimpleFunc.coe_inv, SimpleFunc.coe_restrict,
      Pi.inv_apply, mem_ofPred_eq, not_false_eq_true, indicator_of_mem]
    apply (hf.tendsto_approx x).inv₀ h

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
a : α
⊢ (eapprox f i) a + (eapprox g i) a ≤ (eapprox f j) a + (eapprox g j) a

Tactic:
gcongr <;> exact monotone_eapprox _ h _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ ∫⁻ (a : α), (const α r * eapprox f n) a ∂μ = r * (eapprox f n).lintegral μ

Tactic:
rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]

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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ μ ∅ < ∞ ∧
    (μ.restrict (μ.sigmaFiniteSetWRT' ν))
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair n).1) <
      ∞

Tactic:
Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT'

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ μ ∅ < ∞ ∧
    μ
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
            μ.sigmaFiniteSetGE ν (Nat.unpair n).1 ∩
          μ.sigmaFiniteSetWRT' ν) <
      ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case 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
⊢ ∀ x ∈ tᶜ, f x = 0

Tactic:
have h_fs_zero : ∀ n, ∀ x ∈ tᶜ, fs n x = 0 := by
      intro n x hxt
      rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt
      simpa [T] using hxt n
    refine fun x hxt => tendsto_nhds_unique (h_approx x) ?_
    rw [funext fun n => h_fs_zero n x hxt]
    exact tendsto_const_nhds

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h : IsPreconnected U
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)

Tactic:
isPreconnected_closed_iff

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝¹] t →
      IsClosed[inst✝¹] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)
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)
this : ∀ (x : α) (hx : x ∈ s), ∃ K', ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑K' * edist x y
⊢ ∃ K, LipschitzOnWith K f s

Tactic:
choose K' hK' using this

Goal state after:
α : 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
⊢ ∃ K, LipschitzOnWith K f s
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
⊢ convexComb x (convexComb y z t) s =
    convexComb (convexComb x y (convexComb_assoc_coeff₁ s t)) z (convexComb_assoc_coeff₂ s t)

Tactic:
by
  simp only [convexComb, coe_mul, Subtype.mk.injEq]
  by_cases hs : (s : ℝ) = 1
  · simp only [hs]
    by_cases ht : (t : ℝ) = 1
    · simp [ht]
    · have : (1 - t : ℝ) ≠ 0 := by grind
      field_simp
      simp
  · 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.UnitInterval

Goal state before:
pp: ι : Sort u_1
c : ι → Set (↑I × ↑I)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t,
    t 0 = 0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
by
  obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
  have hδ := half_pos δ_pos
  simp_rw [Subtype.ext_iff]
  have h : (0 : ℝ) ≤ 1 := zero_le_one
  refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩
  obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) trivial
  exact ⟨i, fun t ht ↦ hsub (Metric.mem_ball.mpr <| (max_le (abs_sub_addNSMul_le h hδ.le n ht.1) <|
    abs_sub_addNSMul_le h hδ.le m ht.2).trans_lt <| half_lt_self δ_pos)⟩

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

Goal state before:
pp: case pos
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 : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : max x.fst y.fst = m + 1
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd)

Tactic:
generalize m + 1 = m' at *
      subst m'
      rfl

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

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
by
      rw [mem_cylinder_comm] at hy
      exact mem_cylinder_iff_dist_le.1 hy

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)
n : ℕ
x y : X n
⊢ dist ⟨n, x⟩.snd (leRecOn ⋯ (fun {k} ↦ f k) ⟨n, y⟩.snd) = dist x y

Tactic:
leRecOn_self

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ dist ⟨n, x⟩.snd ⟨n, y⟩.snd = dist x y
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
by
  rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h
  · apply Or.inl (measure_univ_eq_zero.mp h)
  · exact Or.inr ⟨h⟩

Goal state after:
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 : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
have Ay : (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 : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
⊢ ξ ≤ ⊥

Tactic:
rw [h_bot_iff]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
⊢ ξ = 0
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
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g

Tactic:
refine continuous_iff_continuousAt.2 fun y => ?_

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
y : ↑s
⊢ ContinuousAt g y
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) }
n : ℕ
x y : ℕ → ℕ
hp : ¬MeasurablySeparable (f '' cylinder (n, x, y).2.1 (n, x, y).1) (g '' cylinder (n, x, y).2.2 (n, x, y).1)
⊢ ∃ q,
    (↑q).1 = (↑⟨(n, x, y), hp⟩).1 + 1 ∧
      (↑q).2.1 ∈ cylinder (↑⟨(n, x, y), hp⟩).2.1 (↑⟨(n, x, y), hp⟩).1 ∧
        (↑q).2.2 ∈ cylinder (↑⟨(n, x, y), hp⟩).2.2 (↑⟨(n, x, y), hp⟩).1

Tactic:
rcases I n x y hp with ⟨x', y', hx', hy', h'⟩

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) }
n : ℕ
x y : ℕ → ℕ
hp : ¬MeasurablySeparable (f '' cylinder (n, x, y).2.1 (n, x, y).1) (g '' cylinder (n, x, y).2.2 (n, x, y).1)
x' y' : ℕ → ℕ
hx' : x' ∈ cylinder x n
hy' : y' ∈ cylinder y n
h' : ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
⊢ ∃ q,
    (↑q).1 = (↑⟨(n, x, y), hp⟩).1 + 1 ∧
      (↑q).2.1 ∈ cylinder (↑⟨(n, x, y), hp⟩).2.1 (↑⟨(n, x, y), hp⟩).1 ∧
        (↑q).2.2 ∈ cylinder (↑⟨(n, x, y), hp⟩).2.2 (↑⟨(n, x, y), hp⟩).1
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c * (μ.restrict s) univ < ∞

Tactic:
exact ENNReal.mul_lt_top hc.lt_top (measure_lt_top (μ.restrict s) univ)

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 := { 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)
n : ℕ
⊢ (↑(p n)).1 = n

Tactic:
by
    induction n with
    | zero => rfl
    | succ n IH => simp only [prec, hFn, IH]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a

Tactic:
by
  rw [count, lintegral_sum_measure]
  congr
  exact funext fun a => lintegral_dirac a f

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 : ι) → PseudoEMetricSpace (F i)
⊢ uniformity ((i : ι) → F i) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
simp only [Pi.uniformity, comap_iInf, gt_iff_lt, preimage_ofPred_eq, comap_principal,
      PseudoEMetricSpace.uniformity_edist, le_antisymm_iff, le_iInf_iff, le_principal_iff]

Goal state after:
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}) ∧
    ∀ (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.OpenPos

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst✝³] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : μ {a | a ∈ U ∧ ¬f a = g a} = 0
this : IsOpen[inst✝³] (U ∩ {a | f a ≠ g a})
⊢ EqOn f g U

Tactic:
replace := (this.eq_empty_of_measure_zero h).le

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst✝³] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : μ {a | a ∈ U ∧ ¬f a = g a} = 0
this : U ∩ {a | f a ≠ g a} ⊆ ∅
⊢ EqOn f g U
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x ↦ ν (Prod.mk x ⁻¹' f i)
this : ∀ (a : α), ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), ν (Prod.mk a ⁻¹' f i)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' ⋃ i, f i)

Tactic:
simpa only [this] using Measurable.tsum ihf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s

Tactic:
map_apply measurable_prodMk_right hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ μ ((fun x ↦ (x, b)) ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ μ S * ν T = μ s * ν t

Tactic:
measure_toMeasurable,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ μ s * ν T = μ s * ν t
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
⊢ S.Nonempty

pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

pp: case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement univ S

Tactic:
· obtain ⟨a, _⟩ := h.2 1
    exact ⟨a.2.1, a.2.2⟩

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement univ S
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

Tactic:
have : (⟨⟨_, mem_top a⁻¹⟩, ⟨a, ha⟩⟩ : (⊤ : Set G) × S) = ⟨⟨_, mem_top b⁻¹⟩, ⟨b, hb⟩⟩ :=
      h.1 ((inv_mul_cancel a).trans (inv_mul_cancel b).symm)
    exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).2

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
⊢ S.Nonempty

Tactic:
obtain ⟨a, _⟩ := h.2 1
    exact ⟨a.1.1, a.1.2⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ T, IsComplement (↑H) T ∧ g ∈ T

Tactic:
by
  classical
  refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_right fun q ↦ ?_,
    Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩
  by_cases hq : q = Quotient.mk'' g
  · exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
  · simp [Function.update, dif_neg hq, q.out_eq']

Goal state after: