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

Goal state before:
pp: case neg
α : 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
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : b ≤ ↑x
⊢ ((F i).concat (G i)) x ∈ U

Tactic:
concat_right hfg hxb

Goal state after:
case neg
α : 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
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : b ≤ ↑x
⊢ (G i) ⟨↑x, ⋯⟩ ∈ U
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ IsOpen[inst✝²] V

Tactic:
rw [IsGeneratedBy.isOpen_iff X]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝³ i] (⇑f ⁻¹' V)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
· exact edist_ne_top _ _

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

Goal state before:
pp: θ : ↑I
⊢ 1 * (1 + ↑(1, θ).2) ≤ 2 * ↑(1, θ).1

Tactic:
by
      dsimp only
      rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]
      simp only [add_le_add_iff_right]
      exact le_one _

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

Goal state before:
pp: p : ℚ
s : Set ℚ
⊢ (cocompact ℚ ⊓ 𝓝 p).NeBot

Tactic:
refine (hasBasis_cocompact.inf (nhds_basis_opens _)).neBot_iff.2 ?_

Goal state after:
p : ℚ
s : Set ℚ
⊢ ∀ {i : Set ℚ × Set ℚ}, IsCompact i.1 ∧ p ∈ i.2 ∧ IsOpen i.2 → (i.1ᶜ ∩ i.2).Nonempty
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 : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
this : #(logSizeBallSeq J hJ a c i).finset = 0
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - (i + 1)

Tactic:
by simp [this]

Goal state after:
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
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this✝ :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a →
      ↑(#J) ≤ a ^ n →
        ∀ {s t : T},
          (s, t) ∈ pairSet J a c → ∀ i < #J, (s, t) ∈ pairSetSeq J a c i → J.Nonempty → 1 ≤ n → edist s t ≤ ↑n * c
hn : n < 1
this : s = t
⊢ edist s t ≤ ↑n * c

Tactic:
by simp [this]

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ toLoop i (fromLoop i p) = p

Tactic:
by
  simp_rw [toLoop, fromLoop, ContinuousMap.comp_assoc,
    toContinuousMap_comp_symm, ContinuousMap.comp_id]
  ext; rfl

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p ↦ p.1 :: p.2.eraseIdx n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l.eraseIdx n))

Tactic:
exact tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)

Goal state after:
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]
    have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
    rw [ContinuousAt, nhds_prod_eq] at this
    exact this.comp (tendsto_id.prodMap ih)

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ⟨(↑⟨l, hl⟩).insertIdx (↑i) a, ⋯⟩)

Tactic:
tendsto_subtype_rng

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x ↦ ↑(insertIdx x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨(↑⟨l, hl⟩).insertIdx (↑i) a, ⋯⟩)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (eraseIdx i) (𝓝 ⟨l, hl⟩) (𝓝 ⟨l.eraseIdx ↑i, ⋯⟩)

Tactic:
tendsto_subtype_rng

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x ↦ ↑(eraseIdx i x)) (𝓝 ⟨l, hl⟩) (𝓝 ↑⟨l.eraseIdx ↑i, ⋯⟩)
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r (c • f) / ‖c‖₊) * edist x₁ x₂ ^ ↑r

Tactic:
rw [coe_div hc, ← ENNReal.mul_div_right_comm,
        ENNReal.le_div_iff_mul_le (Or.inl <| coe_ne_zero.2 hc) <| Or.inl coe_ne_top,
        mul_comm, ← smul_eq_mul, ← ENNReal.smul_def, ← edist_smul₀, ← Pi.smul_apply,
        ← Pi.smul_apply]

Goal state after:
case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist ((c • f) x₁) ((c • f) x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r
Module: Mathlib.Topology.MetricSpace.Infsep

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

pp: case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0

Tactic:
· classical simp_rw [(H.mpr hs).infsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h.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 ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
s : Set α
hs : s ∈ S
⊢ b ∉ s

Tactic:
obtain ⟨a, ha⟩ := (subset_insert_iff_of_notMem hUS).mp hS1 hs

Goal state after:
case h.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 ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
s : Set α
hs : s ∈ S
a : α
ha : (Ici a)ᶜ = s
⊢ b ∉ s
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set ↑T
hR : R ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
⊢ hull T (kernel S) ⊆ R

Tactic:
← (hull_kernel_of_isClosed hT hG hR.1),

Goal state after:
case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set ↑T
hR : R ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
⊢ hull T (kernel S) ⊆ hull T (kernel R)
Module: Mathlib.Topology.Order.PartialSups

Goal state before:
pp: L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto (fun a ↦ (partialSups fun x ↦ f x a) n) l (𝓝 ((partialSups g) n))

Tactic:
by
  simpa only [← Pi.partialSups_apply] using Tendsto.partialSups hf

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

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

Tactic:
· 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.Separation.LinearUpperLowerSetTopology

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
a : α
hsct : Disjoint {a} (closure t)
hcst : Disjoint (closure {a}) t
ha : a ∈ s
b : α
hb : b ∈ t
⊢ False

Tactic:
← singleton_subset_iff.mpr hb

Goal state after:
case inr.inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint {a} (closure {b})
hcst : Disjoint (closure {a}) {b}
hb : b ∈ t
⊢ False
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
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:
· apply ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext

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
A : C
inst✝ : HasTerminal C
⊢ (skyscraperPresheaf p₀ A).IsSheaf

Tactic:
classical exact
    (Presheaf.isSheaf_iso_iff (eqToIso <| skyscraperPresheaf_eq_pushforward p₀ A)).mpr <|
      (Sheaf.pushforward_sheaf_of_sheaf _
        (Presheaf.isSheaf_on_punit_of_isTerminal _ (by
          dsimp [skyscraperPresheaf]
          rw [if_neg]
          · exact terminalIsTerminal
          · #adaptation_note /-- 2024-03-24
            Previously the universe annotation was not needed here. -/
            exact Set.notMem_empty PUnit.unit.{u + 1})))

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
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ 𝓕.map ((OpenNhds.inclusion p₀).op.map inc) ≫ f.app (op ((OpenNhds.inclusion p₀).obj (unop V))) ≫ eqToHom ⋯ =
    (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯) ≫ 𝟙 c

Tactic:
rw [Category.comp_id, ← Category.assoc, comp_eqToHom_iff, Category.assoc,
            eqToHom_trans, f.naturality, skyscraperPresheaf_map]

Goal state after:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫
      if h : p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop V))) then eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop U))) then c else ⊤_ C)) =
    f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
⊢ ∃! s_1, IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) s_1

Tactic:
refine Sheaf.existsUnique_gluing F _ _ (fun i j ↦ ?_)

Goal state after:
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : Cb X Y
C : ℝ
⊢ BddAbove (range fun x ↦ ⨅ y, f (inl x, inr y) + C)

Tactic:
obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove
  refine ⟨Cf + C, forall_mem_range.2 fun x => ?_⟩
  calc
    ⨅ y, f (inl x, inr y) + C ≤ f (inl x, inr default) + C := ciInf_le (HD_below_aux1 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))
⊢ min M ⌊ε⁻¹ * dist x y⌋₊ = ⌊ε⁻¹ * dist x y⌋₊

Tactic:
refine min_eq_right (Nat.floor_mono ?_)

Goal state after:
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))
⊢ ε⁻¹ * dist x y ≤ ε⁻¹ * max C 0
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⌋₊
⊢ min M ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊

Tactic:
refine min_eq_right (Nat.floor_mono ?_)

Goal state after:
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⌋₊
⊢ ε⁻¹ * dist (Ψ x) (Ψ y) ≤ ε⁻¹ * max C 0
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ ⊥ ∈ {n | ∀ (i : ℕ), n < ↑i → HasSmallInductiveDimensionLT X i}

Tactic:
exact fun _ _ ↦ h.mono zero_le

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : Fin 1 → X
F : (k : Fin 0) → Path (p k.castSucc) (p k.succ)
⊢ concat p F = refl (p 0)

Tactic:
by
  rw [concat, dfoldl_zero]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ (concat (fun x_1 ↦ x) fun x_1 ↦ refl x) = refl x

Tactic:
rw [concat_zero]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      ((k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ ((concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))).Homotopy
    ((concat (p ∘ castSucc) fun k ↦ G k.castSucc).trans (G (last n)))

Tactic:
exact hcomp (ih _ _ _ (fun k ↦ H k.castSucc)) (H (last n))

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
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e ↦ ‖F e x - f x‖) atTop (𝓝 0)
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Tactic:
obtain ⟨n, hn⟩ := (h_tendsto x).eventually (eventually_lt_nhds ε_pos) |>.exists

Goal state after:
ι : 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
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e ↦ ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε