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

Goal state before:
pp: case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
j : ι
p : C(X j, X i₁ × X i₂)
⊢ Continuous[inst✝⁴ j, inst✝¹]
    ((fun x ↦
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
      ⇑p)

Tactic:
let φ : X i₁ × X i₂ → Y × Z := fun (x₁, x₂) ↦ (f₂ x₂, f₁ x₁)

Goal state after:
case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun x ↦
    match x with
    | (x₁, x₂) => (f₂ x₂, f₁ x₁)
⊢ Continuous[inst✝⁴ j, inst✝¹]
    ((fun x ↦
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
      ⇑p)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ∃ x, x ∈ preCantorSet i ∧ x / 3 = ofDigits a ∨ x ∈ preCantorSet i ∧ (2 + x) / 3 = ofDigits a

Tactic:
use ofDigits (fun i ↦ a (i + 1))

Goal state after:
case h
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i ∧ (ofDigits fun i ↦ a (i + 1)) / 3 = ofDigits a ∨
    (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i ∧ (2 + ofDigits fun i ↦ a (i + 1)) / 3 = ofDigits a
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
· apply H.apply_zero

Goal state after:
case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ coveringNumber ε A ≤ coveringNumber ε (f '' A)

Tactic:
simp only [coveringNumber, le_iInf_iff]
    intro C hC_subset hC_cover
    obtain ⟨C', hC'_subset, rfl⟩ : ∃ C', C' ⊆ A ∧ C = C'.image f := by
      have (x : C) : ∃ y ∈ A, f y = x := by simpa using hC_subset x.2
      choose g hg_mem hg using this
      refine ⟨Set.range g, ?_, ?_⟩
      · rwa [Set.range_subset_iff]
      · ext
        simp
        grind
    refine (iInf_le _ C').trans <| (iInf_le _ hC'_subset).trans ?_
    simp only [hf.isCover_image_iff] at hC_cover
    refine (iInf_le _ hC_cover).trans ?_
    rw [InjOn.encard_image]
    exact hf_inj.mono hC'_subset

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : 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
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
· rw [← eHolderNorm_eq_top] at hf
    rw [hf, mul_top <| coe_ne_zero.2 hc, eHolderNorm_eq_top, MemHolder.smul_iff hc]
    rw [nnnorm_eq_zero] at hc
    intro h
    exact h.eHolderNorm_lt_top.ne hf

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
⊢ toGHSpace X = toGHSpace Y → Nonempty (X ≃ᵢ Y)

Tactic:
by
    simp only [toGHSpace]
    rw [Quotient.eq]
    rintro ⟨e⟩
    have I :
      (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) =
        (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rfl
    have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange
    have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange.symm
    exact ⟨f.trans <| (cast I e).trans g⟩

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

Goal state before:
pp: α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
hα : ∀ (a : α), 𝓝 a = 𝓟 (Ici a)
⊢ inst✝¹ = upperSet α

Tactic:
simp [TopologicalSpace.ext_iff_nhds, hα, nhds_eq_principal_Ici]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ ↑(lowerClosure {a}) = Iic a

Tactic:
lowerClosure_singleton,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ ↑(LowerSet.Iic a) = Iic a
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ {a, b} ∈ range fun c ↦ range ⇑c

Tactic:
by
    use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace] ↑(lowerClosure {a})

Tactic:
lowerClosure_singleton,

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace] ↑(LowerSet.Iic a)
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Tactic:
refine ⟨W, hWU, ⟨ℱ.map hWV.op s, ?_⟩, hxW⟩

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
⊢ (ConcreteCategory.hom (T.app (op W))) ((ConcreteCategory.hom (ℱ.map hWV.op)) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
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⌋₊
⊢ ∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ

Tactic:
let F : GHSpace → Σ k : Fin (K n).succ, Fin k → Fin k → Fin M.succ := fun p =>
    ⟨⟨N p, lt_of_le_of_lt (hN p) (Nat.lt_succ_self _)⟩, fun a b =>
      ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊,
        (min_le_left _ _).trans_lt (Nat.lt_succ_self _)⟩⟩

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)⌋₊, ⋯⟩⟩
⊢ ∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
⊢ IsOpen[inst✝⁴] i

Tactic:
by grind [hB.prop, constructibleTopologySubbasis]

Goal state after: