mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
⊢ isGood (π C fun x ↦ ord I x < o) l ↔ ∃ o' < o, isGood (π C fun x ↦ ord I x < o') l

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨o', ⟨ho', hl⟩⟩ ↦ isGood_mono C (le_of_lt ho') hl⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
⊢ ∃ o' < o, isGood (π C fun x ↦ ord I x < o') l
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
⊢ Function.Injective (ι S)

Tactic:
intro a b h

Goal state after:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
⊢ a = b
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
⊢ List.IsChain (fun x x_1 ↦ x > x_1) (term I ho :: ↑q)

Tactic:
have : Inhabited I := ⟨term I ho⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.IsChain (fun x x_1 ↦ x > x_1) (term I ho :: ↑q)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

Tactic:
have : Inhabited I := ⟨term I ho⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ Products.isGood (C' C ho) (↑l).Tail

Tactic:
have : Inhabited I := ⟨term I ho⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
⊢ Products.isGood (C' C ho) (↑l).Tail
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : ↑t ≤ b
⊢ (f.concat g) t = f ⟨↑t, ⋯⟩

Tactic:
nth_rewrite 2 [← concat_comp_IccInclusionLeft hb]

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : ↑t ≤ b
⊢ (f.concat g) t = ((f.concat g).comp IccInclusionLeft) ⟨↑t, ⋯⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ Products.eval C ↑q ∈ Products.eval C '' {m | m < ↑l}

Tactic:
refine ⟨q.val, ⟨?_, rfl⟩⟩

Goal state after:
case h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ ↑q ∈ {m | m < ↑l}
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf : Tendsto F p (𝓝 f)
hg : Tendsto G p (𝓝 g)
⊢ Tendsto (fun i ↦ (F i).concat (G i)) p (𝓝 (f.concat g))

Tactic:
rw [tendsto_nhds_compactOpen] at hf hg ⊢
  rintro K hK U hU hfgU
  have h : b ∈ Icc a c := ⟨Fact.out, Fact.out⟩
  let K₁ : Set (Icc a b) := projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
  let K₂ : Set (Icc b c) := projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
  have hK₁ : IsCompact K₁ :=
    hK.inter_right isClosed_Iic |>.image continuous_subtype_val |>.image projIccCM.continuous
  have hK₂ : IsCompact K₂ :=
    hK.inter_right isClosed_Ici |>.image continuous_subtype_val |>.image projIccCM.continuous
  have hfU : MapsTo f K₁ U := by
    rw [← concat_comp_IccInclusionLeft hfg']
    apply hfgU.comp
    rintro x ⟨y, ⟨⟨z, hz⟩, ⟨h1, (h2 : z ≤ b)⟩, rfl⟩, rfl⟩
    simpa [projIccCM, projIcc, h2, hz.1] using! h1
  have hgU : MapsTo g K₂ U := by
    rw [← concat_comp_IccInclusionRight hfg']
    apply hfgU.comp
    rintro x ⟨y, ⟨⟨z, hz⟩, ⟨h1, (h2 : b ≤ z)⟩, rfl⟩, rfl⟩
    simpa [projIccCM, projIcc, h2, hz.2] using! h1
  filter_upwards [hf K₁ hK₁ U hU hfU, hg K₂ hK₂ U hU hgU, hfg] with i hf hg hfg x hx
  by_cases! hxb : x ≤ b
  · rw [concat_left hfg hxb]
    refine hf ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
    simp [projIccCM, projIcc, hxb, x.2.1]
  · replace hxb : b ≤ x := hxb.le
    rw [concat_right hfg hxb]
    refine hg ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
    simp [projIccCM, projIcc, hxb, x.2.2]

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
⊢ ContinuousGeneratedBy X g ↔
    ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
      Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)

Tactic:
refine ⟨fun h i₁ f₁ i₂ f₂ ↦ ?_, fun h ↦ ?_⟩
  · rw [IsGeneratedBy.continuous_iff X]
    intro j p
    let φ : X i₁ × X i₂ → Y × Z := fun (x₁, x₂) ↦ (f₂ x₂, f₁ x₁)
    replace h := h.comp (show Continuous φ by fun_prop).continuousGeneratedBy
    rw [continuousGeneratedBy_def] at h
    exact h p
  · rw [continuousGeneratedBy_def]
    intro i f
    exact (h i (ContinuousMap.snd.comp f) i (ContinuousMap.fst.comp f)).comp
      (Continuous.prodMk continuous_id continuous_id)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : none ∈ Metric.eball (some a) r
⊢ none ∈ some '' Metric.eball a r

Tactic:
| =>

Goal state after:
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : none ∈ Metric.eball (some a) r
⊢ none ∈ some '' Metric.eball a r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
y : α
h : some y ∈ Metric.eball (some a) r
⊢ some y ∈ some '' Metric.eball a r

Tactic:
| =>

Goal state after:
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
y : α
h : some y ∈ Metric.eball (some a) r
⊢ some y ∈ some '' Metric.eball a r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
r : ℝ≥0∞
hr : 0 < r
x : Option α
val✝ : α
⊢ some val✝ ∈ Metric.eball none r → some val✝ = none

Tactic:
| =>

Goal state after:
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
r : ℝ≥0∞
hr : 0 < r
x : Option α
val✝ : α
⊢ some val✝ ∈ Metric.eball none r → some val✝ = none
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
r : ℝ≥0∞
hr : 0 < r
x : Option α
⊢ none ∈ Metric.eball none r → none = none

Tactic:
| =>

Goal state after:
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
r : ℝ≥0∞
hr : 0 < r
x : Option α
⊢ none ∈ Metric.eball none r → none = none
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : none ∈ s
⊢ ∃ ε > 0, Metric.eball none ε ⊆ s

Tactic:
| =>

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : none ∈ s
⊢ ∃ ε > 0, Metric.eball none ε ⊆ s
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x✝ : Option α
x : α
xs : some x ∈ s
⊢ ∃ ε > 0, Metric.eball (some x) ε ⊆ s

Tactic:
| =>

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x✝ : Option α
x : α
xs : some x ∈ s
⊢ ∃ ε > 0, Metric.eball (some x) ε ⊆ s
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball (some x) r)

Tactic:
| =>

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball (some x) r)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
y : Option α
yh : none ∈ Metric.eball (some x) ∞
⊢ ⟨none, yh⟩ ∈ Subtype.val ⁻¹' some '' s' ↔ ⟨none, yh⟩ ∈ Subtype.val ⁻¹' Metric.eball (some x) r

Tactic:
| =>

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
y : Option α
yh : none ∈ Metric.eball (some x) ∞
⊢ ⟨none, yh⟩ ∈ Subtype.val ⁻¹' some '' s' ↔ ⟨none, yh⟩ ∈ Subtype.val ⁻¹' Metric.eball (some x) r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
y : Option α
z : α
yh : some z ∈ Metric.eball (some x) ∞
⊢ ⟨some z, yh⟩ ∈ Subtype.val ⁻¹' some '' s' ↔ ⟨some z, yh⟩ ∈ Subtype.val ⁻¹' Metric.eball (some x) r

Tactic:
| =>

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
y : Option α
z : α
yh : some z ∈ Metric.eball (some x) ∞
⊢ ⟨some z, yh⟩ ∈ Subtype.val ⁻¹' some '' s' ↔ ⟨some z, yh⟩ ∈ Subtype.val ⁻¹' Metric.eball (some x) r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x : Option α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball none r)

Tactic:
| =>

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x : Option α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball none r)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
| y

Tactic:
← γ.target

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
| γ 1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ (logSizeBallSeq J hJ a c 0).radius ≤ n

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ (logSizeBallSeq J hJ a c 0).radius ≤ n
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i✝ i : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).radius ≤ n

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i✝ i : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).radius ≤ n
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c 0).radius

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c 0).radius
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i✝ i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c (i + 1)).radius

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i✝ i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c (i + 1)).radius
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c 0).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c 0).point ∈ (logSizeBallSeq J hJ a c 0).finset

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c 0).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c 0).point ∈ (logSizeBallSeq J hJ a c 0).finset
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ (logSizeBallSeq J hJ a c (i + 1)).finset
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ha : 1 < a
⊢ (if (logSizeBallSeq J hJ a c 0).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c 0).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c 0).smallBall c))

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ha : 1 < a
⊢ (if (logSizeBallSeq J hJ a c 0).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c 0).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c 0).smallBall c))
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))

Tactic:
| =>

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
rw [Finset.coe_infsep, dif_pos hs]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Pi

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → PseudoMetricSpace (X i)
inst✝ : ∀ (i : ι), IsUltrametricDist (X i)
f : (i : ι) → X i
⊢ ∀ (y z : (i : ι) → X i), dist f z ≤ max (dist f y) (dist y z)

Tactic:
g

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → PseudoMetricSpace (X i)
inst✝ : ∀ (i : ι), IsUltrametricDist (X i)
f g : (i : ι) → X i
⊢ ∀ (z : (i : ι) → X i), dist f z ≤ max (dist f g) (dist g z)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s u v : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} u
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)

Tactic:
| inter u v _ _ hu2 hv2 =>

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ ↑(LowerSet.Iic a) = Iic a

Tactic:
LowerSet.coe_Iic

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ Iic a = Iic a
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsLowerSet α
inst✝ : Topology.IsLowerSet β
f : α → β
⊢ Monotone f ↔ Continuous[inst✝³, inst✝²] f

Tactic:
rw [← monotone_dual_iff]
  exact IsUpperSet.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ)
    (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: h : Set Prop
hs : h ∈ {∅, {True}}
⊢ h ∈ {s | ∃ a, (Iic a)ᶜ = s}

Tactic:
simp only [compl_Iic, mem_ofPred_eq]

Goal state after:
h : Set Prop
hs : h ∈ {∅, {True}}
⊢ ∃ a, Ioi a = h