mathlib-initiative/mathlib-tactics huggingface dataset:
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)))
this✝ : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {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)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
this : ∃ p, ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m q • Products.eval (C' C ho) q = m q • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑q)).prod

Tactic:
obtain ⟨p, hp⟩ := this

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
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {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)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
p : Products I
hp : ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m q • Products.eval (C' C ho) q = m q • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑q)).prod
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∈ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

Tactic:
· exact hmax hy

Goal state after:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ Equicontinuous fun x ↦ ⇑↑x

Tactic:
rw [isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff]

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ Equicontinuous ((fun x ↦ Subtype.val ∘ x) ∘ fun x ↦ ⇑↑x)
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 :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
z : α
hz : z ∈ Icc a c
h1 : ⟨z, hz⟩ ∈ K
h2 : b ≤ z
⊢ IccInclusionRight (projIccCM ↑⟨z, hz⟩) ∈ K

Tactic:
simpa [projIccCM, projIcc, h2, hz.2] using! h1

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_2
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ ⋃ i, {x (i + (k + 1))} ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}

Tactic:
exact iUnion_mono fun i => subset_closure

Goal state after:
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
⊢ Function.Injective ⇑(productOfMemOpens X)

Tactic:
intro x1 x2 h

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ x1 = x2
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l

Tactic:
Function.comp_def,

Goal state after:
α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ l.lift' fun x ↦ Iic (𝓟 x)} = Iic l
Module: Mathlib.Topology.EMetricSpace.Weak

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

Tactic:
by
  ext x
  constructor <;> intro h
  · obtain ⟨y, yh, yx⟩ := h
    rw [← yx]
    simpa
  match x with
  | none => simp at h
  | (y : α) =>
    exact ⟨y, h, rfl⟩

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n =
    ⋂ i, ((Set.image fun x ↦ x / 3) ∘ preCantorSet) i ∪ ((Set.image fun x ↦ (2 + x) / 3) ∘ preCantorSet) i

Tactic:
Function.comp_def,

Goal state after:
⊢ ⋂ n, preCantorSet n = ⋂ i, (fun x ↦ x / 3) '' preCantorSet i ∪ (fun x ↦ (2 + x) / 3) '' preCantorSet i
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : a ≠ b
⊢ False

Tactic:
rw [Function.ne_iff] at h

Goal state after:
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem :
  0 ≤ (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∧
    (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ≤ 1
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
rw [← mul_le_mul_iff_left₀ (show 0 < (3 : ℝ) ^ n by positivity), sub_mul, inv_pow,
    inv_mul_cancel₀ (by simp)]

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem :
  0 ≤ (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∧
    (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ≤ 1
⊢ x * 3 ^ n - 1 ≤ (∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i) * 3 ^ n
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
Y : Type u_3
f : Y → PseudoMetric X R
s : Finset Y
hs : s.Nonempty
x y : X
⊢ (s.sup f) x y = s.sup' hs fun i ↦ (f i) x y

Tactic:
induction hs using Finset.Nonempty.cons_induction with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ ∃ z' ∈ s (n + l + 1), edist (↑z) z' < B n / 2 ^ l

Tactic:
refine exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_
          simp only [ENNReal.inv_pow, div_eq_mul_inv]
          rw [← pow_add]
          apply hs <;> simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f < ∞
⊢ MemHolder r f

Tactic:
eHolderNorm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ⨅ C, ⨅ (_ : HolderWith C r f), ↑C < ∞
⊢ MemHolder r f
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ eHolderNorm r (Function.const X c) = 0

Tactic:
eHolderNorm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ⨅ C, ⨅ (_ : HolderWith C r (Function.const X c)), ↑C = 0
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ eHolderNorm r f = 0

Tactic:
eHolderNorm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C = 0
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ f x₁ = f x₂

Tactic:
eHolderNorm,

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ⨅ C, ⨅ (_ : HolderWith C r f), ↑C = 0
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ f x₁ = f x₂
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Fintype ↑s
⊢ s.einfsep = s.offDiag.toFinset.inf (uncurry edist)

Tactic:
by
  refine eq_of_forall_le_iff fun _ => ?_
  simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, mem_toFinset, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(eHolderNorm r f).toNNReal * edist x₁ x₂ ^ ↑r

Tactic:
eHolderNorm,

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(⨅ C, ⨅ (_ : HolderWith C r f), ↑C).toNNReal * edist x₁ x₂ ^ ↑r
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ eball x d = eball (toSnowflaking (ofSnowflaking x)) ((d ^ α⁻¹) ^ α)

Tactic:
toSnowflaking_ofSnowflaking,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ eball x d = eball x ((d ^ α⁻¹) ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ closedEBall x d = closedEBall (toSnowflaking (ofSnowflaking x)) ((d ^ α⁻¹) ^ α)

Tactic:
toSnowflaking_ofSnowflaking,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ closedEBall x d = closedEBall x ((d ^ α⁻¹) ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ ball x r = ball (toSnowflaking (ofSnowflaking x)) ((r ^ α⁻¹) ^ α)

Tactic:
toSnowflaking_ofSnowflaking,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ ball x r = ball x ((r ^ α⁻¹) ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = closedBall (toSnowflaking (ofSnowflaking x)) ((r ^ α⁻¹) ^ α)

Tactic:
toSnowflaking_ofSnowflaking,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = closedBall x ((r ^ α⁻¹) ^ α)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
⊢ (∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S) → ∃ a, (Ici a)ᶜ = U

Tactic:
intro ⟨S, hS1, hS2⟩
    have hUS : univ ∉ S := by
      by_contra hUS'
      apply hU
      rw [hS2]
      exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)
    use sSup {a | (Ici a)ᶜ ∈ S}
    rw [hS2, sUnion_eq_compl_sInter_compl, compl_inj_iff]
    apply le_antisymm
    · intro b hb
      simp only [sInter_image, mem_iInter, mem_compl_iff]
      intro s hs
      obtain ⟨a, ha⟩ := (subset_insert_iff_of_notMem hUS).mp hS1 hs
      subst hS2 ha
      simp_all only [compl_Ici, mem_Ici, sSup_le_iff, mem_ofPred_eq, mem_Iio, not_lt]
    · intro b hb
      rw [mem_Ici, sSup_le_iff]
      intro c hc
      simp only [sInter_image, mem_iInter] at hb
      rw [← not_lt, ← mem_Iio, ← compl_Ici]
      exact hb _ hc

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a : α) (b : ℚ) (b_1 : (IsSuccPrelimit a → 0 ≤ b) ∧ (IsPredPrelimit a → b ≤ 0)) (a_1 : α) (b_2 : ℚ)
    (b_3 : (IsSuccPrelimit a_1 → 0 ≤ b_2) ∧ (IsPredPrelimit a_1 → b_2 ≤ 0)),
    a < a_1 ∨ a = a_1 ∧ b < b_2 → ∃ a_3, ⟨toLex (a, b), b_1⟩ < a_3 ∧ a_3 < ⟨toLex (a_1, b_2), b_3⟩

Tactic:
rintro x q ⟨hx₁, hx₂⟩ y r ⟨hy₁, hy₂⟩ (h | ⟨rfl, h⟩)

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩

case inr
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (x, r), ⋯⟩
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
obtain hq | hq := le_or_gt q 0

Goal state after:
case refine_2.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

case refine_2.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 < q
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
V : Opens ↑X
i : α
hV : V ≤ Us i
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op V)).obj left✝ ⟶ (principals ↑X).obj x
e : principalOpen x ≤ V
VV : OpensLeCover Us := { obj := V, property := ⋯ }
xx : OpensLeCover Us := { obj := principalOpen x, property := ⋯ }
⊢ S.π.app (Opposite.op { obj := principalOpen x, property := ⋯ }) ≫
      limit.π (generator (principalOpen x) ⋙ F)
        { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) } =
    S.π.app (Opposite.op { obj := V, property := ⋯ }) ≫
      limit.π (StructuredArrow.proj (Opposite.op V) (principals ↑X) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
let ee : xx ⟶ VV := ObjectProperty.homMk e.hom

Goal state after:
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
V : Opens ↑X
i : α
hV : V ≤ Us i
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op V)).obj left✝ ⟶ (principals ↑X).obj x
e : principalOpen x ≤ V
VV : OpensLeCover Us := { obj := V, property := ⋯ }
xx : OpensLeCover Us := { obj := principalOpen x, property := ⋯ }
ee : xx ⟶ VV := ObjectProperty.homMk e.hom
⊢ S.π.app (Opposite.op { obj := principalOpen x, property := ⋯ }) ≫
      limit.π (generator (principalOpen x) ⋙ F)
        { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) } =
    S.π.app (Opposite.op { obj := V, property := ⋯ }) ≫
      limit.π (StructuredArrow.proj (Opposite.op V) (principals ↑X) ⋙ F) { left := left✝, right := x, hom := f }
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))|

Tactic:
abs_mul,

Goal state after:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)|
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
scard : N ≤ K n
hN : #↑s = ↑N
⊢ #↑s = #(Fin N)

Tactic:
rw [hN, Cardinal.mk_fin]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
⊢ BddBelow (range fun x ↦ (candidatesBDist X Y) (inl x, inr y))

Tactic:
simpa using HD_below_aux2 0

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
⊢ CompactSpace (WithConstructibleTopology X)

Tactic:
suffices h : @CompactSpace X (constructibleTopology X) from
    @Function.Surjective.compactSpace _ _ (constructibleTopology X) _ _
      (WithTopology.continuous_toTopology _) _ (WithTopology.toTopology_surjective _)

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
⊢ CompactSpace X
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case right
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
ht : ↑t ∈ uIcc ↑t₀ ↑t₁
⊢ ∃ a, Icc.convexComb t₀ t₁ a = t

Tactic:
← segment_eq_uIcc,

Goal state after:
case right
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
ht : ↑t ∈ segment ℝ ↑t₀ ↑t₁
⊢ ∃ a, Icc.convexComb t₀ t₁ a = t
Module: Mathlib.Topology.UniformSpace.Dini

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone fun x_1 ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly (fun i x ↦ F i ↑x) (f ∘ Subtype.val) atTop

Tactic:
exact tendstoLocallyUniformly_of_forall_tendsto (hF_cont · |>.domRestrict)
    (fun _ _ h x ↦ hF_mono _ x.2 h) hf.domRestrict (fun x ↦ h_tendsto x x.2)

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = ⨆ i, comap (Prod.fst ∘ Prod.mk x) (𝓝 i) ⊓ comap (Prod.snd ∘ Prod.mk x) (𝓝 i)

Tactic:
Function.comp_def,

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = ⨆ i, comap (fun x_1 ↦ x) (𝓝 i) ⊓ comap (fun x ↦ x) (𝓝 i)