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

Goal state before:
pp: case refine_1
α : 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
n m N : ℕ
hNn : N ≤ n
hNm : N ≤ m
⊢ dist ↑(u n) ↑(u m) ≤ (1 / 2) ^ N

pp: case refine_2
α : 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
⊢ Tendsto (fun n ↦ (1 / 2) ^ n) atTop (𝓝 0)

Tactic:
· exact (dist_val_le_dist (u n) (u m)).trans (hu N n m hNn hNm).le

Goal state after:
case refine_2
α : 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
⊢ Tendsto (fun n ↦ (1 / 2) ^ n) atTop (𝓝 0)
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:
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.Gluing

Goal state before:
pp: case refine_2.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i ≠ j
⊢ dist x ⋯.some + 1 + dist y ⋯.some = dist y ⋯.some + 1 + dist x ⋯.some

Tactic:
abel

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
⊢ CompleteSpace s.CompleteCopy

Tactic:
by
  refine Metric.complete_of_convergent_controlled_sequences ((1 / 2) ^ ·) (by simp) fun u hu ↦ ?_
  have A : CauchySeq fun n => (u n).1 := by
    refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_
    · exact (dist_val_le_dist (u n) (u m)).trans (hu N n m hNn hNm).le
    · exact tendsto_pow_atTop_nhds_zero_of_lt_one (by simp) (by norm_num)
  obtain ⟨x, xlim⟩ : ∃ x, Tendsto (fun n => (u n).1) atTop (𝓝 x) := cauchySeq_tendsto_of_complete A
  by_cases xs : x ∈ s
  · exact ⟨⟨x, xs⟩, tendsto_subtype_rng.2 xlim⟩
  obtain ⟨C, hC⟩ : ∃ C, ∀ n, 1 / infDist (u n).1 sᶜ < C := by
    refine ⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩
    rw [← sub_lt_iff_lt_add]
    calc
      _ ≤ |1 / infDist (u n).1 sᶜ - 1 / infDist (u 0).1 sᶜ| := le_abs_self _
      _ = |1 / infDist (u 0).1 sᶜ - 1 / infDist (u n).1 sᶜ| := abs_sub_comm _ _
      _ ≤ dist (u 0) (u n) := le_add_of_nonneg_left dist_nonneg
      _ < (1 / 2) ^ 0 := hu 0 0 n le_rfl n.zero_le
  have Cpos : 0 < C := lt_of_le_of_lt (div_nonneg zero_le_one infDist_nonneg) (hC 0)
  have Hmem : ∀ {y}, y ∈ s ↔ 0 < infDist y sᶜ := fun {y} ↦ by
    rw [← s.isOpen.isClosed_compl.notMem_iff_infDist_pos ⟨x, xs⟩]; exact not_not.symm
  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
  have I' : 1 / C ≤ infDist x sᶜ :=
    have : Tendsto (fun n => infDist (u n).1 sᶜ) atTop (𝓝 (infDist x sᶜ)) :=
      ((continuous_infDist_pt (sᶜ : Set α)).tendsto x).comp xlim
    ge_of_tendsto' this I
  exact absurd (Hmem.2 <| lt_of_lt_of_le (div_pos one_pos Cpos) I') xs

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
by
  let := TopologicalSpace.upgradeIsCompletelyMetrizable α
  obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_isClosed_of_not_countable hC hunc
  obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty
  exact ⟨f, hfD.trans hDC, hf⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
n : ι
⊢ y ∈ s n

Tactic:
exact mem_iInter.1 hy n

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
⊢ map (fun x ↦ c) μ = μ univ • dirac c

Tactic:
ext s hs
  simp only [Measure.coe_smul, Pi.smul_apply,
    dirac_apply' _ hs, smul_eq_mul]
  classical
  rw [Measure.map_apply measurable_const hs, Set.preimage_const]
  by_cases hsc : c ∈ s
  · rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
  · rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
⊢ μ1 = μ2 ↔ ∀ (x : α), μ1.real {x} = μ2.real {x}

Tactic:
rw [Measure.ext_iff_singleton]

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
⊢ (∀ (a : α), μ1 {a} = μ2 {a}) ↔ ∀ (x : α), μ1.real {x} = μ2.real {x}
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ∃ s ∈ ae μ, ∃ t ∈ ae ν, Disjoint s t
⊢ Disjoint μ ν

Tactic:
mem_ae_iff

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ∃ s, μ sᶜ = 0 ∧ ∃ t, ν tᶜ = 0 ∧ Disjoint s t
⊢ Disjoint μ ν
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
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y)
this : cylinder Ax.some (firstDiff x y) = cylinder Ay.some (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
rw [← fx, ← fy, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at this

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
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y)
this : firstDiff x y ≤ firstDiff (f x) (f y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), ↑(a i) = ↑(∑' (i : α), a i)

Tactic:
ENNReal.tsum_coe_eq a_summable.hasSum

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ↑(∑' (b : α), a b) = ↑(∑' (i : α), a i)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}

Tactic:
by
  simp [lintegral_dirac' _ hf, mul_comm]

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

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

Tactic:
by
  simp [mul_comm]

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

Goal state before:
pp: case const.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
x : α
⊢ (piecewise t ht (const α c) (const α 0)) x ≤ (piecewise s hs (const α c) (const α 0)) x

Tactic:
refine indicator_le_indicator_of_subset ts (fun x => ?_) x

Goal state after:
case const.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
x✝ x : α
⊢ 0 x ≤ (const α c) x
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case e'_3
α : 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 : ℕ
⊢ cylinder x n = cylinder (↑(p n)).2.1 (↑(p n)).1

Tactic:
pn_fst,

Goal state after:
case e'_3
α : 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 : ℕ
⊢ cylinder x n = cylinder (↑(p n)).2.1 n
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 : ℕ
⊢ cylinder y n = cylinder (↑(p n)).2.2 (↑(p n)).1

Tactic:
pn_fst,

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 : ℕ
⊢ cylinder y n = cylinder (↑(p n)).2.2 n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.refine_2
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
⊢ distDenseSeq X n ⁻¹' ball 0 (ε / 2) ⊆ C

Tactic:
· intro y hy
    replace hy : dist y (denseSeq X n) < ε / 2 := by
      simpa [Subtype.dist_eq, abs_eq_self.mpr, coe_projIcc, not_lt_of_ge, ε, div_le_iff₀] using hy
    have : dist x y < infDist x (closure Cᶜ) :=
      ((dist_triangle_right x y (denseSeq X n)).trans_lt (add_lt_add hn hy)).trans_le (by simp [ε])
    simpa using notMem_of_notMem_closure (mt infDist_le_dist_of_mem this.not_ge)

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

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' sᶜ)

Tactic:
preimage_compl,

Goal state after:
case compl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)ᶜ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < ν v

Tactic:
· exact v_open.measure_pos ν ⟨y, yv⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
⊢ μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K

Tactic:
refine
    le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
r : ℝ≥0∞
hr : r < μ U
⊢ r < ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
h₀ : μ U = 0
⊢ 0 < ε

Tactic:
pos_iff_ne_zero

Goal state after:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
h₀ : μ U = 0
⊢ ε ≠ 0
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * ↑(hHT.equiv g₂).2 * g₁⁻¹ ∈ H

Tactic:
← hHT.equiv_fst_mul_equiv_snd g₁,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * ↑(hHT.equiv g₂).2 * (↑(hHT.equiv g₁).1 * ↑(hHT.equiv g₁).2)⁻¹ ∈ H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (hST.equiv g).2 = ⟨1, h1⟩

Tactic:
by
  ext
  rw [equiv_snd_eq_inv_mul, equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg, inv_mul_cancel]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
Ht : (μ.restrict (s n)) (A n) ≠ ∞
U : Set α
hAU : U ⊇ A n
hUo : IsOpen[inst✝¹] U
hU : μ (U ∩ s n) < μ (A n) + δ n
⊢ ∃ U ⊇ A n, IsOpen[inst✝¹] U ∧ μ U < μ (A n) + δ n

Tactic:
exact ⟨U ∩ s n, subset_inter hAU (hAs _), hUo.inter (h' n), hU⟩

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

Goal state before:
pp: case h₂
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝¹ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst✝³] v
w_open : IsOpen[inst✝³] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
⊢ False

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ > (0 : ℝ), ball z δ ⊆ f ⁻¹' v := by
      apply Metric.mem_nhds_iff.1
      exact f_cont.continuousAt.preimage_mem_nhds (v_open.mem_nhds fzv)

Goal state after:
case h₂
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝¹ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst✝³] v
w_open : IsOpen[inst✝³] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
⊢ False