mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j✝ : Discrete ι
⊢ (𝟙 c.pt ≫ Pi.lift fun i ↦ c.π.app (op (single i))) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    ((Pi.lift fun i ↦ c.π.app (op (single i))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)) ≫
      limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝

Tactic:
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
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
x✝ x : X ⊕ Y
⊢ IsClosed {f | f (x✝, x) ≤ ↑(maxVar X Y)}

Tactic:
apply IsClosed.inter _ _

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
x✝ x : X ⊕ Y
⊢ IsClosed {f | f (x✝, x) ≤ ↑(maxVar X Y)}
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j✝ : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    ((Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.one)) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
j✝ : Discrete ι
⊢ (f.hom ≫ Pi.lift fun i ↦ c'.π.app (op (single i))) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    (Pi.lift fun i ↦ c.π.app (op (single i))) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
j✝ : Discrete (ι × ι)
⊢ (f.hom ≫ Pi.lift fun b ↦ c'.π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
y : (CategoryTheory.Pairwise ι)ᵒᵖ
x : CategoryTheory.Pairwise ι
f : op x ⟶ y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        y =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f

Tactic:
induction y with | op y => ?_

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op y) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.single.single.id_single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) ≫ 𝟙 (F.obj (op (U i)))

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    (Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫
      Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i)
⊢ (Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫
      Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op

Tactic:
simp

Goal state after:
case op.op.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    (Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫
      Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i)
⊢ Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map ((U j).infLERight (U i)).op =
    Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.pair.pair.id_pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (a✝¹, a✝) =
    (c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (a✝¹, a✝)) ≫
      𝟙 (F.obj (op (U a✝¹ ⊓ U a✝)))

Tactic:
simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ IsCompact univ

Tactic:
rw [← range_quotient_mk']

Goal state after:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ IsCompact (range Quotient.mk')
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete ι
⊢ (𝟙 c.pt ≫ Fork.ι c) ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    (Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))) ≫
      limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ c.π.app WalkingParallelPair.one) ≫ limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    (Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete ι
⊢ (𝟙 c.pt ≫ Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))) ≫
      limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝ =
    Fork.ι c ≫ limit.π (Discrete.functor fun i ↦ F.obj (op (U i))) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
j✝ : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    c.π.app WalkingParallelPair.one ≫ limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (cocone U).op).π.app (op (single a✝)) =
    ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (single a✝))

Tactic:
simp

Goal state after:
case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ F.map (coconeιApp U (single a✝)).op = F.map (leSupr U a✝).op
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 (Functor.mapCone F (cocone U).op).pt ≫
      ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (single a✝)) =
    (Functor.mapCone F (cocone U).op).π.app (op (single a✝))

Tactic:
simp

Goal state after:
case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ F.map (leSupr U a✝).op = F.map (coconeιApp U (single a✝)).op
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ 𝟙 ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).pt ≫
      (SheafConditionEqualizerProducts.fork F U).π.app WalkingParallelPair.zero =
    ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app WalkingParallelPair.zero

Tactic:
simp

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ SheafConditionEqualizerProducts.res F U = Pi.lift fun i ↦ F.map (coconeιApp U (single i)).op
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ 𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
      ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app WalkingParallelPair.zero =
    (SheafConditionEqualizerProducts.fork F U).π.app WalkingParallelPair.zero

Tactic:
simp

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ (Pi.lift fun i ↦ F.map (coconeιApp U (single i)).op) = SheafConditionEqualizerProducts.res F U
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∉ unop V
⊢ Epi ((skyscraperSheaf p₀ A).obj.map r)

Tactic:
simp

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∉ unop V
⊢ Epi (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C))
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: m : ℕ
IH :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {m_1 : ℕ},
    m_1 ≤ m → HasSmallInductiveDimensionLT X m_1 → HasSmallInductiveDimensionLT X m
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsEmpty X
hmn : 0 ≤ m + 1
⊢ ∀ U ∈ ∅, HasSmallInductiveDimensionLT (↑(frontier U)) m

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case succ
m✝ : ℕ
IH :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : ℕ},
    m ≤ m✝ → HasSmallInductiveDimensionLT X m → HasSmallInductiveDimensionLT X m✝
X : Type u_1
inst✝ : TopologicalSpace X
m : ℕ
hmn : m ≤ m✝ + 1
H : HasSmallInductiveDimensionLT X m
⊢ HasSmallInductiveDimensionLT X (m✝ + 1)

Tactic:
| succ m IH =>

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ ⊥ < ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
⊢ (⇑γ ∘ Icc.convexComb t₀ t₁) 0 = γ t₀

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
⊢ (⇑γ ∘ Icc.convexComb t₀ t₁) 1 = γ t₁

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case inl
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x✝ : ↑I
⊢ {
        toFun := fun x ↦
          ((γ.subpath t₀ (Icc.convexComb t₁ t₂ (x✝, x).1)).trans (γ.subpath (Icc.convexComb t₁ t₂ (x✝, x).1) t₂))
            (x✝, x).2,
        continuous_toFun := ⋯ }
      0 =
    ((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case inr
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x✝ : ↑I
⊢ {
        toFun := fun x ↦
          ((γ.subpath t₀ (Icc.convexComb t₁ t₂ (x✝, x).1)).trans (γ.subpath (Icc.convexComb t₁ t₂ (x✝, x).1) t₂))
            (x✝, x).2,
        continuous_toFun := ⋯ }
      1 =
    ((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap 1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
⊢ Subtype.val '' (J1 ∪ J2) ⊆ segment ℝ ↑y1 ↑y2

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
R : Type u_2
inst✝ : CommRing R
abv : AbsoluteValue R 𝕜
⊢ ∀ (x : R), abv (x - x) = 0

Tactic:
simp

Goal state after:
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
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly F f atTop

Tactic:
by
  refine (atTop : Filter ι).eq_or_neBot.elim (fun h ↦ ?eq_bot) (fun _ ↦ ?_)
  case eq_bot => simp [h, tendstoLocallyUniformly_iff_forall_tendsto]
  have F_le_f (x : α) (n : ι) : F n x ≤ f x := by
    refine _root_.ge_of_tendsto (h_tendsto x) ?_
    filter_upwards [Ici_mem_atTop n] with m hnm
    exact hF_mono hnm x
  simp_rw [Metric.tendstoLocallyUniformly_iff, dist_eq_norm']
  intro ε ε_pos x
  simp_rw +singlePass [tendsto_iff_norm_sub_tendsto_zero] at h_tendsto
  obtain ⟨n, hn⟩ := (h_tendsto x).eventually (eventually_lt_nhds ε_pos) |>.exists
  refine ⟨{y | ‖F n y - f y‖ < ε}, ⟨isOpen_lt (by fun_prop) continuous_const |>.mem_nhds hn, ?_⟩⟩
  filter_upwards [eventually_ge_atTop n] with m hnm z hz
  refine norm_le_norm_of_abs_le_abs ?_ |>.trans_lt hz
  simp only [abs_of_nonpos (sub_nonpos_of_le (F_le_f _ _)), neg_sub, sub_le_sub_iff_left]
  exact hF_mono hnm z

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : SeparationQuotient.mk c = SeparationQuotient.mk b
hbc : (b, c) ∈ U
⊢ SeparationQuotient.mk a = SeparationQuotient.mk a

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : SeparationQuotient.mk c = SeparationQuotient.mk b
hbc : (b, c) ∈ U
⊢ SeparationQuotient.mk d = SeparationQuotient.mk d

Tactic:
simp

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.mk x) (𝓝 i ×ˢ 𝓝 i)

Tactic:
comap_prod,

Goal state after:
γ : 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)
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = ⊤ ⊓ 𝓝 x ⊔ ⨆ i, ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
sup_inf : β
cY : Convex ℝ ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ ∅ fun y ↦ f x y
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
this : {t | ∃ x ∈ X, sup_y x = t} = {sup_inf}
⊢ IsGLB {sup_inf} sup_inf

Tactic:
simp

Goal state after: