mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ 0 = 0

pp: case h1
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n

pp: case hx
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n.succ, f n x⟩.fst ≤ n.succ

pp: case hy
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n.succ

Tactic:
]

Goal state after:
case h1
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n

case hx
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n.succ, f n x⟩.fst ≤ n.succ

case hy
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n.succ
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
]

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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
y : (n : ℕ) → E n
ys : y ∈ s
hy : cylinder x (Nat.find A - 1) = cylinder y (Nat.find A - 1)
⊢ cylinder y (Nat.find A - 1) = cylinder x (Nat.find A - 1)
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
]

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

Goal state before:
pp: case hfh
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ediam (D (PiNat.res x b)) ≤ u b

Tactic:
]

Goal state after:
case hfh
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ediam (D (PiNat.res x b)) ≤ u b
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
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ y ∈ cylinder x n

Tactic:
]

Goal state after:
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
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ y ∈ cylinder x n
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e) μa μb
⊢ μa = μa

Tactic:
]

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 : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : MeasurableSet s
⊢ map f (μa.restrict (f ⁻¹' s)) = map f (μa.restrict (f ⁻¹' s))

Tactic:
]

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 : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set β
⊢ map f (μa.restrict (f ⁻¹' s)) = map f (μa.restrict (f ⁻¹' s))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEMeasurable (g ∘ f) μa ↔ AEMeasurable (g ∘ f) μa

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : MeasurePreserving g μb μc
hf : MeasurePreserving f μa μb
⊢ μc = μc

Tactic:
]

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

Goal state before:
pp: case hfh
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
m : ℕ
hm : m ≠ 0
⊢ ediam (D (PiNat.res x m)) ≤ u m

Tactic:
]

Goal state after:
case hfh
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
m : ℕ
hm : m ≠ 0
⊢ ediam (D (PiNat.res x m)) ≤ u m
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
ga : α → α
gb : β → β
hfm : MeasurePreserving f μa μb
hga : MeasurePreserving ga μa μa
hf : Semiconj f ga gb
hgb : Measurable gb
this : MeasurePreserving gb μb μb
⊢ MeasurePreserving gb μb μb

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
ga : α → α
gb : β → β
hfm : MeasurePreserving f μa μb
hga : MeasurePreserving ga μa μa
hf : Semiconj f ga gb
hgb : Measurable gb
this : MeasurePreserving gb μb μb
⊢ MeasurePreserving gb μb μb
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
inst✝ : SigmaFinite μb
⊢ SigmaFinite μb

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst✝ : SigmaFinite μb
⊢ SigmaFinite μb
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
inst✝ : SFinite μa
⊢ SFinite (map f μa)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst✝ : SFinite μa
⊢ SFinite (map f μa)
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 : NullMeasurableSet s (map f μa)
⊢ μa (f ⁻¹' s) = (map f μa) s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s (map f μa)
⊢ μa (f ⁻¹' s) = (map f μa) s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff y x
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s

Tactic:
]

Goal state after:
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff y x
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
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 : NullMeasurableSet s (map f μa)
⊢ μa (f ⁻¹' s) = μa (f ⁻¹' s)

Tactic:
]

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 : α → β
hf : MeasurePreserving f μa μb
hfe : MeasurableEmbedding f
s : Set β
⊢ μa (f ⁻¹' s) = μa (f ⁻¹' s)

Tactic:
]

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 : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ μa (f ⁻¹' s) ≤ (map f μa) s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ μa (f ⁻¹' s) ≤ (map f μa) s
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 + μb' = μb + μb'

Tactic:
]

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

Goal state before:
pp: case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff y x
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
Z : Disjoint s (cylinder x (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s

Tactic:
]

Goal state after:
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff y x
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
Z : Disjoint s (cylinder x (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μa : Measure α
μb : Measure β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α → β
hf : MeasurePreserving f μa μb
c : R
⊢ c • μb = c • μb

Tactic:
]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n] ⁻¹' s)) + μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f^[n] ⁻¹' s)) + μ (s ∆ (f ⁻¹' s))

Tactic:
]

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n] ⁻¹' s)) + μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f^[n] ⁻¹' s)) + μ (s ∆ (f ⁻¹' s))
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
⊢ μ (s ∆ (f^[n] ⁻¹' s)) + μ (s ∆ (f ⁻¹' s)) ≤ μ (s ∆ (f^[n] ⁻¹' s)) + μ (s ∆ (f ⁻¹' s))

Tactic:
]

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

Goal state before:
pp: case e'_4
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
n : ℕ
hm : n.succ ≠ 0
⊢ n = n

Tactic:
]

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

Goal state before:
pp: case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix x s < longestPrefix y s
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty
Z : Disjoint s (cylinder y (longestPrefix x s).succ)
⊢ longestPrefix y s = longestPrefix x s

Tactic:
]

Goal state after:
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix x s < longestPrefix y s
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty
Z : Disjoint s (cylinder y (longestPrefix x s).succ)
⊢ longestPrefix y s = longestPrefix x s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
l_eq : longestPrefix y s = longestPrefix x s
⊢ x ∈ cylinder y (longestPrefix x s)

Tactic:
]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
l_eq : longestPrefix y s = longestPrefix x s
⊢ x ∈ cylinder y (longestPrefix x s)
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)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
⊢ f^[j] x ∈ s

Tactic:
]

Goal state after:
α : 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)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
⊢ f^[j] x ∈ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, (eapprox f n).lintegral (Measure.map g μ) = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, (eapprox f n).lintegral (Measure.map g μ) = ∫⁻ (a : α), f (g a) ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, (eapprox f n).lintegral (Measure.map g μ) = ⨆ n, (eapprox (f ∘ g) n).lintegral μ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, (eapprox f n).lintegral (Measure.map g μ) = ⨆ n, (eapprox (f ∘ g) n).lintegral μ