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

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

Tactic:
← Subtype.coe_inj

Goal state after:
ι : Sort u_1
c : ι → Set ↑I
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t, ↑(t 0) = ↑0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
h : x ≠ y
⊢ x = y

Tactic:
simp [dist_eq_of_ne h] at hxy

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

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
by
  rcases eq_or_ne y x with (rfl | hne)
  · simp [PiNat.dist_self]
  suffices (∀ i : ℕ, i < n → y i = x i) ↔ n ≤ firstDiff y x by simpa [dist_eq_of_ne hne]
  constructor
  · intro hy
    by_contra! H
    exact apply_firstDiff_ne hne (hy _ H)
  · intro h i hi
    exact apply_eq_of_lt_firstDiff (hi.trans_le h)

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

Goal state before:
pp: case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
⊢ x i = y i

Tactic:
have : n < firstDiff x y := by
    simpa [dist_eq_of_ne hne, inv_lt_inv₀, pow_lt_pow_iff_right₀, one_lt_two] using h

Goal state after:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
this : n < firstDiff x y
⊢ x i = y i
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)
⊢ ∀ (a : (n : ℕ) → E n) (u : Set ((n : ℕ) → E n)),
    a ∈ u → IsOpen[Pi.topologicalSpace] u → ∃ v ∈ {s | ∃ x n, s = cylinder x n}, a ∈ v ∧ v ⊆ u

Tactic:
intro x

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)),
    x ∈ u → IsOpen[Pi.topologicalSpace] u → ∃ v ∈ {s | ∃ x n, s = cylinder x n}, x ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
⊢ ∀ (x : ℕ → β), x ∈ (inducedMap A).fst

Tactic:
intro x

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
⊢ x ∈ (inducedMap A).fst
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ IsClopenable s

Tactic:
classical
  have : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  have : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]

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

Goal state before:
pp: case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
n : ℕ
⊢ ∀ (a b : (n : ℕ) → E n), dist a b < (1 / 2) ^ n → a n = b n

Tactic:
intro x

Goal state after:
case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
n : ℕ
x : (n : ℕ) → E n
⊢ ∀ (b : (n : ℕ) → E n), dist x b < (1 / 2) ^ n → x n = b n
Module: Mathlib.Topology.MetricSpace.Perfect

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

Tactic:
intro x

Goal state after:
α : 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
⊢ Tendsto (fun n ↦ ediam (D (PiNat.res x n))) atTop (nhds 0)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case refine_1.h₂
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 := ⋯
fs : ∀ x ∈ s, f x = x
⊢ s ⊆ range f

Tactic:
intro x

Goal state after:
case refine_1.h₂
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 : (n : ℕ) → E n
⊢ x ∈ s → x ∈ range f
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
h✝ : Nonempty β
⊢ range f = ∅ ∨ ∃ f_1, Continuous[_, inst✝²] f_1 ∧ range f_1 = range f

Tactic:
obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g :=
      exists_nat_nat_continuous_surjective β

Goal state after:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous[_, inst✝¹] g
hg : Surjective g
⊢ range f = ∅ ∨ ∃ f_1, Continuous[_, inst✝²] f_1 ∧ range f_1 = range f
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
⊢ μ ≪ ν₁

Tactic:
refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
  let t := h_ms.nullSet
  have ht : MeasurableSet t := h_ms.measurableSet_nullSet
  have htμ : μ t = 0 := h_ms.measure_nullSet
  have htν₂ : ν₂ tᶜ = 0 := h_ms.measure_compl_nullSet
  have : μ s = μ (s ∩ tᶜ) := by
    conv_lhs => rw [← inter_union_compl s t]
    rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add]
    · exact (disjoint_compl_right.inter_right' _).inter_left' _
    · exact hs.inter ht.compl
  rw [this]
  refine h ?_
  simp only [Measure.coe_add, Pi.add_apply, add_eq_zero]
  exact ⟨measure_inter_null_of_null_left _ hs_zero, measure_inter_null_of_null_right _ htν₂⟩

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

Goal state before:
pp: case refine_3
α : 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
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
⊢ Injective fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩

Tactic:
intro x

Goal state after:
case refine_3
α : 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
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
x : ℕ → Bool
⊢ ∀ ⦃a₂ : ℕ → Bool⦄, (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) x = (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) a₂ → x = a₂
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
α : 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 x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
let n := firstDiff x.1 y.1 - 1

Goal state after:
case inr
α : 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 x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
⊢ dist (g x) (g y) ≤ 4 * dist x y
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: case refine_2
α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ b.2 s

Tactic:
exact (Measure.measurable_coe hs).comp measurable_snd

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

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
this :
  ∀ {f : α → ℝ≥0∞},
    AEMeasurable f m.join → Measurable f → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
· rcases hf with ⟨g, hgm, hfg⟩
    rw [lintegral_congr_ae hfg, this hgm.aemeasurable hgm]
    exact lintegral_congr_ae <| (ae_ae_of_ae_join hfg).mono fun μ hμ ↦
      .symm <| lintegral_congr_ae hμ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
intro ε hε

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

Goal state before:
pp: case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < 2⁻¹ ^ encode i
⊢ ∀ (a b : (i : ι) → F i), edist a b < 2⁻¹ ^ encode i → edist a b < ε → edist (a i) (b i) < ε

Tactic:
intro x

Goal state after:
case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < 2⁻¹ ^ encode i
x : (i : ι) → F i
⊢ ∀ (b : (i : ι) → F i), edist x b < 2⁻¹ ^ encode i → edist x b < ε → edist (x i) (b i) < ε
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:
by
    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]
    constructor
    · intro ε hε
      obtain ⟨K, hK⟩ : ∃ K : Finset ι, ∑' i : {j // j ∉ K}, 2⁻¹ ^ encode (i : ι) < ε / 2 :=
        ((tendsto_order.1 <| ENNReal.tendsto_tsum_compl_atTop_zero
          (tsum_geometric_encode_lt_top ENNReal.one_half_lt_one).ne).2 _
            <| by simpa using hε.ne').exists
      obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ δ * K.card < ε / 2 :=
        ENNReal.exists_pos_mul_lt (by simp) (by simpa using hε.ne')
      apply @mem_iInf_of_iInter _ _ _ _ _ K.finite_toSet fun i =>
          {p : (∀ i : ι, F i) × ∀ i : ι, F i | edist (p.fst i) (p.snd i) < δ}
      · rintro ⟨i, hi⟩
        refine mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)
        simp only [mem_principal, Subset.rfl]
      · rintro ⟨x, y⟩ hxy
        simp only [mem_iInter, mem_ofPred_eq, SetCoe.forall, Finset.mem_coe] at hxy
        calc
          edist x y = ∑' i : ι, min (2⁻¹ ^ encode i) (edist (x i) (y i)) := rfl
          _ = ∑ i ∈ K, min (2⁻¹ ^ encode i) (edist (x i) (y i)) +
                ∑' i : ↑(K : Set ι)ᶜ, min (2⁻¹ ^ encode (i : ι)) (edist (x i) (y i)) :=
            (ENNReal.sum_add_tsum_compl ..).symm
          _ ≤ ∑ i ∈ K, edist (x i) (y i) + ∑' i : ↑(K : Set ι)ᶜ, 2⁻¹ ^ encode (i : ι) := by
            gcongr
            · apply min_le_right
            · apply min_le_left
          _ < ∑ _i ∈ K, δ + ε / 2 := by
            refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK
            gcongr with i hi
            exact (hxy i hi).le
          _ ≤ ε / 2 + ε / 2 := by gcongr; simpa [mul_comm] using hδ.le
          _ = ε := ENNReal.add_halves _
    · intro i ε hε₀
      have : (0 : ℝ≥0∞) < 2⁻¹ ^ encode i := ENNReal.pow_pos (by norm_num) _
      refine mem_iInf_of_mem (min (2⁻¹ ^ encode i) ε) <| mem_iInf_of_mem (by positivity) ?_
      simp only [and_imp, Prod.forall, ofPred_subset_ofPred, lt_min_iff, mem_principal]
      intro x y hn
      exact (edist_le_edist_pi_of_edist_lt hn).trans_lt

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

Goal state before:
pp: ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝² : Encodable ι
inst✝¹ : (i : ι) → PseudoMetricSpace (Y i)
inst✝ : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toPiNat

Tactic:
rw [continuous_iff_continuous_dist]
  simp only [dist_def]
  apply continuous_tsum (by fun_prop) summable_geometric_two_encode <| by simp [abs_of_nonneg]

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x✝ : ℝ
a✝ : α
⊢ x✝ = K⁻¹ * (K * x✝)

Tactic:
simp [inv_mul_cancel_left₀ hK.ne']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (s ×ˢ t)ᶜ = 0

Tactic:
Set.compl_prod_eq_union,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ) = 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous[_, inst✝³] f
g : (ℕ → ℕ) → α
g_cont : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
⊢ MeasurablySeparable (range f) (range g)

Tactic:
exact measurablySeparable_range_of_disjoint f_cont g_cont h

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 γ := ⋯
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := ⋯
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 β := ⋯
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := ⋯
⊢ ⋂ n, F n ⊆ range f

Tactic:
intro x

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 : β
⊢ x ∈ ⋂ n, F n → x ∈ range f
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1

Tactic:
apply (isComplement_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique

Goal state after:
case mpr.py₁
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (↑(hSK.equiv g₁).1)⁻¹ * g₁ ∈ ↑K

case mpr.py₂
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (↑(hSK.equiv g₂).1)⁻¹ * g₁ ∈ ↑K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s ↦ (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
t' : G
ht' : t' ∈ ↑T
h : (↑⟨(fun x ↦ f • x) t', ⋯⟩)⁻¹ * g ∈ ↑H
⊢ ⟨(fun x ↦ f • x) t', ⋯⟩ = ⟨f • ↑t, ⋯⟩

Tactic:
replace h := QuotientAction.inv_mul_mem f⁻¹ h

Goal state after:
case refine_2
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s ↦ (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
t' : G
ht' : t' ∈ ↑T
h : (f⁻¹ • ↑⟨(fun x ↦ f • x) t', ⋯⟩)⁻¹ * f⁻¹ • g ∈ H
⊢ ⟨(fun x ↦ f • x) t', ⋯⟩ = ⟨f • ↑t, ⋯⟩