mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ Metric.ball 0 1
y : EuclideanSpace ℝ (Fin n)
hy : y ∈ Metric.ball 0 1
h :
  (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (ballInclusion n)) { down := ⟨y, hy⟩ }
⊢ x = y

Tactic:
simpa [ballInclusion, disk] using h

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
⊢ CompactSpace ↑(𝔻 n)

Tactic:
convert! Homeomorph.compactSpace Homeomorph.ulift.symm

Goal state after:
case convert_1
n : ℕ
⊢ CompactSpace ↑(Metric.closedBall 0 1)
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
⊢ CompactSpace ↑(∂𝔻 n)

Tactic:
convert! Homeomorph.compactSpace Homeomorph.ulift.symm

Goal state after:
case convert_1
n : ℕ
⊢ CompactSpace ↑(Metric.sphere 0 1)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : RelCWComplex C ∅
⊢ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C

Tactic:
by simpa using union' (C := C)

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (spanFinBasis C s))

Tactic:
by
  intro f _
  rw [Finsupp.mem_span_range_iff_exists_finsupp]
  use Finsupp.onFinset (Finset.univ) f.toFun (fun _ _ ↦ Finset.mem_univ _)
  ext x
  change LocallyConstant.evalₗ ℤ x _ = _
  simp only [zsmul_eq_mul, map_finsuppSum, LocallyConstant.evalₗ_apply,
    LocallyConstant.coe_mul, Pi.mul_apply, spanFinBasis, LocallyConstant.coe_mk, mul_ite, mul_one,
    mul_zero, Finsupp.sum_ite_eq, Finsupp.mem_support_iff, ne_eq, ite_not]
  split_ifs with h <;> [exact h.symm; rfl]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ D ∪ ⋃ n, ⋃ j, closedCell n j

Tactic:
exact subset_union_of_subset_right (subset_iUnion₂ _ _) _

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
x : ↑(π C J)
⊢ (fun i ↦ ↑x ↑i) ∈ IndexFunctor.obj C J

Tactic:
by
    rcases x with ⟨x, y, hy, rfl⟩
    refine ⟨y, hy, ?_⟩
    ext ⟨i, hi⟩
    simp [precomp, Proj, hi]

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ ∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = 0

Tactic:
push Not at h

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
⊢ ∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = 0
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Epi g
⊢ ∃ f', f' ≫ g = f

Tactic:
rw [epi_iff_surjective] at hg

Goal state after:
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
⊢ ∃ f', f' ≫ g = f
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 ↦ Subtype.val ∘ x) ∘ fun x ↦ ⇑↑x)

Tactic:
exact H.comp (A.restrictPreimage F)

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ ∀ x ∈ S,
    ∀ y ∈ {t | t.Finite ∧ t ⊆ T},
      {f | MapsTo (⇑f) x (⋃₀ y)} ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {U | IsOpen[inst✝] U}

Tactic:
intro K hK t ht

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
K : Set X
hK : K ∈ S
t : Set (Set Y)
ht : t ∈ {t | t.Finite ∧ t ⊆ T}
⊢ {f | MapsTo (⇑f) K (⋃₀ t)} ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {U | IsOpen[inst✝] U}
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case refine_2
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.fst (𝓝[S] fg) (𝓝 fg.1)

pp: case refine_3
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)

Tactic:
· exact tendsto_nhdsWithin_of_tendsto_nhds continuousAt_fst

Goal state after:
case refine_3
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
hX :
  ∃ S,
    S.Countable ∧
      (∀ K ∈ S, IsCompact K) ∧
        ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ ∃ b, b.Countable ∧ compactOpen = generateFrom b

Tactic:
by
    rcases hX with ⟨S, hScount, hScomp, hS⟩
    refine ⟨_, ?_, compactOpen_eq_generateFrom (S := S) hScomp (isBasis_countableBasis _) ?_⟩
    · exact .image2 hScount (countable_ofPred_finite_subset (countable_countableBasis Y)) _
    · intro f x V hV hx
      apply hS
      exacts [isOpen_of_mem_countableBasis hV, hx]

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ (morphismPropertyWithGeneratedByTopologyEquiv X).IsInvertedBy (toContinuousGeneratedByCat X)

Tactic:
by rintro _ _ _ ⟨Z⟩; infer_instance

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ (morphismPropertyWithGeneratedByTopologyEquiv X).IsInvertedBy toGeneratedByTopCat

Tactic:
by rintro _ _ _ ⟨Z⟩; infer_instance

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

Goal state before:
pp: case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG }.toFun (0, x, y) =
    ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
      (x, y)

Tactic:
exact Prod.ext (HSpace.hmulE.1.2 x) (HSpace.hmulE.1.2 y)

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

Goal state before:
pp: case a
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i✝ i : ℕ
⊢ {x ∈ (logSizeBallSeq J hJ a c (i + 1)).finset | edist (logSizeBallSeq J hJ a c (i + 1)).point x ≤ ↑n * c} ⊆ J

Tactic:
exact (Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)

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

Goal state before:
pp: n : ℕ+
r : ℝ
⊢ IsCompact (closedBall n r)

Tactic:
by
    change IsCompact (((↑) : ℕ+ → ℕ) ⁻¹' closedBall (↑n : ℕ) r)
    rw [Nat.closedBall_eq_Icc]
    exact ((Set.finite_Icc _ _).preimage PNat.coe_injective.injOn).isCompact

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
⊢ (Finset.range #J).biUnion (pairSetSeq J a c) ⊆ J ×ˢ J

Tactic:
Finset.biUnion_subset_iff_forall_subset

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
⊢ ∀ x ∈ Finset.range #J, pairSetSeq J a c x ⊆ J ×ˢ J
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos.ht
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ (logSizeBallSeq J ⋯ a c i).ball c ⊆ J

Tactic:
exact (Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)

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

Goal state before:
pp: case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ((Finset.range #J).biUnion fun x ↦
      {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤ (↑(logSizeBallSeq J hJ a c x).radius - 1) * c}) ⊆
    J

Tactic:
Finset.biUnion_subset_iff_forall_subset

Goal state after:
case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∀ x ∈ Finset.range #J,
    {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤ (↑(logSizeBallSeq J hJ a c x).radius - 1) * c} ⊆
      J
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝¹ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
i : ℕ
a✝ : i ∈ Finset.range #J
⊢ {x ∈ (logSizeBallSeq J hJ a c i).finset |
      edist (logSizeBallSeq J hJ a c i).point x ≤ (↑(logSizeBallSeq J hJ a c i).radius - 1) * c} ⊆
    J

Tactic:
exact (Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)

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

Goal state before:
pp: n : ℕ
⊢ preCantorSet n ⊆ Set.Icc 0 1

Tactic:
rw [← preCantorSet_zero]
  exact preCantorSet_antitone (by simp)

Goal state after:
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
⊢ a = b

Tactic:
by
  by_contra! h
  rw [Function.ne_iff] at h
  let n0 := Nat.find h
  have h1 (n) (hn : n < n0) : a n = b n := by simpa using Nat.find_min h hn
  have h2 : a n0 ≠ b n0 := by simpa using Nat.find_spec h
  generalize n0 = n1 at h1 h2
  clear h n0
  wlog h3 : a n1 = 0 ∧ b n1 = 2 generalizing a b
  · exact this hb ha h.symm (fun n hn ↦ (h1 n hn).symm) h2.symm (by grind)
  obtain ⟨h3, h4⟩ := h3
  clear h2
  have : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x := by
    apply Finset.sum_congr rfl
    grind [ofDigitsTerm]
  rw [ofDigits_eq_sum_add_ofDigits a (n1 + 1),
    ofDigits_eq_sum_add_ofDigits b (n1 + 1), Finset.sum_range_succ,
    Finset.sum_range_succ, this] at h
  replace h : ofDigitsTerm a n1 + (3⁻¹ ^ n1 * ofDigits fun i ↦ a (1 + n1 + i)) * (1 / 3) =
      (3⁻¹ ^ n1 * ofDigits fun i ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 := by
    ring_nf at h
    linarith
  simp only [ofDigitsTerm, h3, Fin.isValue, Fin.coe_ofNat_eq_mod, Nat.zero_mod, CharP.cast_eq_zero,
    Nat.cast_ofNat, pow_succ, mul_inv_rev, zero_mul, inv_pow, one_div, zero_add, h4,
    Nat.mod_succ] at h
  replace h : (ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹ =
      (ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * 3⁻¹ := by
    rw [← mul_right_inj' (show ((3 : ℝ) ^ n1)⁻¹ ≠ 0 by positivity)]
    linarith
  linarith [ofDigits_nonneg (fun i ↦ b (1 + n1 + i)), ofDigits_le_one (fun i ↦ a (1 + n1 + i))]

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✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
f : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ ((fun y ↦ ⟨ContinuousMap.const (N → ↑I) y, ⋯⟩) ((fun f ↦ f 0) f)) y✝ = f y✝

Tactic:
exact congr_arg f (Subsingleton.elim _ _)

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

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ ∃ x₀, J = {x₀}

Tactic:
rw [← Finset.card_eq_one]

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ #J = 1
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
⊢ CompleteSpace (Closeds α)

Tactic:
have B_ne_top : ∀ n, B n ≠ ⊤ := by finiteness

Goal state after:
α : 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 ≠ ∞
⊢ CompleteSpace (Closeds α)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ ↑ε
a : X
ha : a ∈ A
⊢ coveringNumber ε A ≤ 1

Tactic:
calc coveringNumber ε A
      _ ≤ ({a} : Set X).encard :=
        (IsCover.singleton_of_ediam_le hA ha).coveringNumber_le_encard (by simp [ha])
      _ ≤ 1 := by simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
exact hs.infsep_zero

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
classical rw [Set.infsep_of_fintype, dif_pos hs]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
exact hs.infsep_zero

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
dy : dist (Φ xX) y < diam univ + 1 + diam univ
z : Y
hzy : Ψ z = y
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
← hzy

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ inst✝¹ = generateFrom {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
topology_eq α,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ lower α = generateFrom {s | ∃ a, (Ici a)ᶜ = s}
Module: Mathlib.Topology.Order.UpperLowerSetTopology

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

Tactic:
constructor
  · intro hf
    simp_rw [continuous_def, isOpen_iff_isUpperSet]
    exact fun _ hs ↦ IsUpperSet.preimage hs hf
  · intro hf a b hab
    rw [← mem_Iic, ← closure_singleton] at hab ⊢
    apply Continuous.closure_preimage_subset hf {f b}
    apply mem_of_mem_of_subset hab
    apply closure_mono
    rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]

Goal state after:
Module: Mathlib.Topology.Order.Category.AlexDisc

Goal state before:
pp: X : AlexDisc
⊢ ↑((𝟭 AlexDisc).obj X).toTopCat ≃ₜ
    ↑(((forget₂ AlexDisc TopCat ⋙ topToPreord) ⋙
              { obj := fun X ↦ AlexDisc.of (WithUpperSet ↑X),
                map := fun {X Y} f ↦ ConcreteCategory.ofHom (WithUpperSet.map (Preord.Hom.hom f)),
                map_id := alexDiscEquivPreord._proof_1, map_comp := @alexDiscEquivPreord._proof_2 }).obj
          X).toTopCat

Tactic:
by
    dsimp; exact homeoWithUpperSetTopologyorderIso X

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

Goal state before:
pp: case inl
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : X
⊢ f (inl val✝) ∈ range Φ ∪ range Ψ

Tactic:
apply mem_union_left; apply mem_range_self

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
⊢ dist x z ≤ dist x y + dist y z

Tactic:
have Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z :=
      toGlue_commute hΦ hΨ

Goal state after:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist x z ≤ dist x y + dist y z
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed t

Tactic:
← inter_eq_self_of_subset_right ht,

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed (s ∩ t)
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = {x | f x = 0} ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝] {x | f x = 0}
ht : IsClosed[inst✝] {x | g x = 0}
hst : Disjoint {x | f x = 0} {x | g x = 0}
hf : s = {x | f x = 0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
hg : t = {x | g x = 0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfx : f x = 0
⊢ f x + g x ≠ 0

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = {x | f x = 0} ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝] {x | f x = 0}
ht : IsClosed[inst✝] {x | g x = 0}
hst : Disjoint {x | f x = 0} {x | g x = 0}
hf : s = {x | f x = 0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
hg : t = {x | g x = 0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfx : f x ≠ 0
⊢ f x + g x ≠ 0

Tactic:
· simpa [hfx] using hst.notMem_of_mem_left hfx

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = {x | f x = 0} ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝] {x | f x = 0}
ht : IsClosed[inst✝] {x | g x = 0}
hst : Disjoint {x | f x = 0} {x | g x = 0}
hf : s = {x | f x = 0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
hg : t = {x | g x = 0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfx : f x ≠ 0
⊢ f x + g x ≠ 0
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2.refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ Tendsto (fun t ↦ 2 * ↑(maxVar X Y) * t) (𝓝 0) (𝓝 0)

Tactic:
have : Tendsto (fun t : ℝ => 2 * (maxVar X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * maxVar X Y * 0)) :=
        tendsto_const_nhds.mul tendsto_id
      simpa using this

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

Goal state before:
pp: case h.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ (y : ↥↑⟨U, m⟩) → F.stalk ↑y

Tactic:
exact fun y => F.germ _ _ y.2 s

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
⊢ ∀ (fU : (y : ↥↑U) → F.stalk ↑y),
    (Sheafify.isLocallyGerm F).pred fU →
      ∀ (fV : (y : ↥↑V) → F.stalk ↑y),
        (Sheafify.isLocallyGerm F).pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
fU

Goal state after:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
⊢ (Sheafify.isLocallyGerm F).pred fU →
    ∀ (fV : (y : ↥↑V) → F.stalk ↑y),
      (Sheafify.isLocallyGerm F).pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)