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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
g : C(X j, X i)
⊢ Continuous[inst✝¹ j, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑g)

Tactic:
Function.comp_assoc,

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
g : C(X j, X i)
⊢ Continuous[inst✝¹ j, _] (⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f ∘ ⇑g)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x ↦ x ∈ s) z, ⋯⟩ a = true
⊢ a ∈ s

Tactic:
aesop (add simp Proj)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x : ↑(π C fun x ↦ x ∈ s)
a : I
hx : ↑x a = false
z : I → Bool
hz : z ∈ C
ha : ↑⟨Proj (fun x ↦ x ∈ s) z, ⋯⟩ a = true
⊢ a ∈ s ∧ (if false = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) = 1 - e (π C fun x ↦ x ∈ s) a

Tactic:
aesop (add simp Proj)

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
⊢ Ultrafilter.lim ⁻¹' U ∈ FF

Tactic:
exact @c3 U (IsOpen.mem_nhds hU hx)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ x✝ : Products I
⊢ x✝¹ < x✝ ↔ List.Lex (fun x1 x2 ↦ x1 < x2) ↑x✝¹ ↑x✝

Tactic:
exact lt_iff_lex_lt _ _

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (((eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩).toFun ∘ ProjRestricts C ⋯) ∘ ProjRestrict C fun x ↦ ord I x < o₂) =
    ⇑((πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))

Tactic:
Function.comp_assoc,

Goal state after:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ ((eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩).toFun ∘ ProjRestricts C ⋯ ∘ ProjRestrict C fun x ↦ ord I x < o₂) =
    ⇑((πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x w✝ : I → Bool
left✝ : w✝ ∈ C
h : Proj (fun x ↦ ord I x < o) w✝ = x
j : I
hj : x j = true
⊢ ord I j < o

Tactic:
aesop (add simp Proj)

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case succ.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

Tactic:
· exact i.elim

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
⊢ t = ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace

Tactic:
by
  apply le_antisymm
  · rw [le_iInf_iff]
    exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)
  · intro u h
    rw [← generateFrom_iUnion_isOpen]
    apply isOpen_generateFrom_of_mem
    simp only [Set.mem_iUnion, Set.mem_ofPred_eq, isOpen_induced_iff]
    exact ⟨⟨u, h⟩, {True}, isOpen_singleton_true, by simp [Set.preimage]⟩

Goal state after:
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1

Tactic:
simp only [add_le_add_iff_right]

Goal state after:
θ : ↑I
⊢ ↑θ ≤ 1
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ ∀ (x : X × Y),
    (𝓝 x).HasBasis
      (fun x_1 ↦
        match x with
        | (x, y) =>
          match x_1 with
          | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
      fun x ↦
      match x with
      | (Ux, Uy) => Ux ×ˢ Uy

Tactic:
intro (x, y)

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ (𝓝 (x, y)).HasBasis
    (fun x_1 ↦
      match (x, y) with
      | (x, y) =>
        match x_1 with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
    fun x ↦
    match x with
    | (Ux, Uy) => Ux ×ˢ Uy
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ ∀ (x : X × Y) (i : Set X × Set Y),
    (match x with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
intro (x, y)

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ ∀ (i : Set X × Set Y),
    (match (x, y) with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
⊢ reorderRestrictProd S s p ∈ Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s

Tactic:
obtain ⟨y, hy_mem_s, hy_eq⟩ := p.1.2
  exact ⟨y, hy_mem_s, hy_eq.trans (restrict_compl_reorderRestrictProd p).symm⟩

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

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
h1 : ∀ n < n1, a n = b n
h2 : a n1 ≠ b n1
h3 : a n1 = 0
h4 : b n1 = 2
⊢ False

Tactic:
clear h2

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
⊢ False
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)

Tactic:
exact ⟨H.continuous, H.universally_closed _⟩

Goal state after:
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
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
simp only [finset_logSizeBallSeq_add_one, logSizeBallStruct.smallBall, Finset.mem_sdiff, hsV,
    Finset.mem_filter, true_and, not_le, not_lt] at h

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.List

Goal state before:
pp: case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)

Tactic:
simp_rw [tendsto_cons_iff, prod_cons]

Goal state after:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto (fun p ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ↑t ≤ 2⁻¹
⊢ Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default))) = fun x ↦
    Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t)

Tactic:
(ext i; rw [Unique.eq_default i]; simp)

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_2
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ¬↑t ≤ 2⁻¹
⊢ Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default) - 1)) = fun x ↦
    Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t - 1)

Tactic:
(ext i; rw [Unique.eq_default i]; simp)

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ dist (f (x, y)) (f (z, t)) ≤ ↑(2 * maxVar X Y) * dist (x, y) (z, t)

Tactic:
rw [Real.dist_eq, abs_sub_le_iff]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (x, y) - f (z, t) ≤ ↑(2 * maxVar X Y) * dist (x, y) (z, t) ∧
    f (z, t) - f (x, y) ≤ ↑(2 * maxVar X Y) * dist (x, y) (z, t)
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
⊢ nnHolderNorm r (Function.const X c) = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← ENNReal.coe_le_coe, ENNReal.coe_zero, ← eHolderNorm_const X r c]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ↑(nnHolderNorm r (Function.const X c)) ≤ eHolderNorm r (Function.const X c)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ ⋂₀ (compl '' S)
⊢ b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})

Tactic:
mem_Ici,

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ ⋂₀ (compl '' S)
⊢ sSup {a | (Ici a)ᶜ ∈ S} ≤ b
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ Continuous[inst✝⁴, inst✝²] f → ScottContinuousOn D f

Tactic:
refine fun hf t h₀ d₁ d₂ a d₃ ↦
      ⟨(monotone_of_continuous (D := D) hf).mem_upperBounds_image d₃.1,
      fun b hb ↦ ?_⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst✝⁴, inst✝²] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
⊢ f a ≤ b
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous fun x ↦ x ∈ t
⊢ ωScottContinuous fun x ↦ x ∈ ⋃₀ s

Tactic:
convert! CompleteLattice.ωScottContinuous.sSup hs

Goal state after:
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous fun x ↦ x ∈ t
x✝ : α
⊢ Membership.mem (⋃₀ s) = sSup s
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: case h
L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x | x (f t a)} = t
⊢ {x | x (⨆ t, ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S

Tactic:
map_iSup,

Goal state after:
case h
L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x | x (f t a)} = t
⊢ {x | ⨆ i, ⨆ (i_1 : i ∈ S), x (f i i_1)} = ⋃₀ S
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: α : 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
y : α
hy : x ⋖ y
x✝ : α
⊢ x✝ ∈ ⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩ ↔ x✝ ∈ Iio y

Tactic:
simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_left

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h : x ≠ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
by
  obtain h | h := h.not_le_or_not_ge
  · exact (exists_isClopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl
  · obtain ⟨U, hU, hU', hy, hx⟩ := exists_isClopen_lower_of_not_le h
    exact ⟨U, hU, Or.inr hU', hx, hy⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ unop V
⊢ ((if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then a else ⊤_ C)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then b else ⊤_ C)

Tactic:
have hU : p₀ ∈ U.unop := leOfHom i.unop hV
      simp only [skyscraperPresheaf_obj, hU, hV, ↓reduceDIte, eqToHom_trans_assoc, Category.assoc,
        eqToHom_trans]

Goal state after:
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
F : Sheaf C X
h : ∀ (x : ↑X), IsZero ((forget C X ⋙ stalkFunctor C x).obj F)
f : F ⟶ 0 := ⋯.from_ F
this : IsIso f
⊢ IsZero F

Tactic:
exact (isZero_zero _).of_iso (asIso f)

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
⊢ toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f

Tactic:
by
  apply NatTrans.ext
  ext U
  dsimp
  split_ifs with h
  · simp
  · exact ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext ..

Goal state after:
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⌋
⊢ (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋

Tactic:
simp only [F, (E q).symm_apply_apply]

Goal state after:
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:
congr; ring

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

Goal state before:

Tactic:
⨅ x, f (inl x, inr y) + C ≤ f (inl default, inr y) + C := ciInf_le (HD_below_aux2 C) default
    _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

Goal state after:
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 ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
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)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
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))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
⊢ ↑((F q).snd ((E q) (Ψ x)) ((E q) (Ψ y))) = min M ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊

Tactic:
simp only [F, (E q).symm_apply_apply]

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✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
E1 : ∀ (y : Y), (⨅ x, g (inl x, inr y)) + dist f g = ⨅ x, g (inl x, inr y) + dist f g
⊢ ⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g

Tactic:
have E2 : (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g = ⨆ y, (⨅ x, g (inl x, inr y)) + dist f g := by
    refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
    · intro x y hx
      simpa
    · simpa using HD_bound_aux2 _ 0

Goal state after:
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
E1 : ∀ (y : Y), (⨅ x, g (inl x, inr y)) + dist f g = ⨅ x, g (inl x, inr y) + dist f g
E2 : (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g = ⨆ y, (⨅ x, g (inl x, inr y)) + dist f g
⊢ ⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g