mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a₁ a₂ : Fill α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simp only [ofLex_toLex, Subtype.forall, Prod.Lex.lt_iff, Subtype.mk_lt_mk,
      Lex.forall, Prod.forall]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a : α) (b : ℚ) (b_1 : (IsSuccPrelimit a → 0 ≤ b) ∧ (IsPredPrelimit a → b ≤ 0)) (a_1 : α) (b_2 : ℚ)
    (b_3 : (IsSuccPrelimit a_1 → 0 ≤ b_2) ∧ (IsPredPrelimit a_1 → b_2 ≤ 0)),
    a < a_1 ∨ a = a_1 ∧ b < b_2 → ∃ a_3, ⟨toLex (a, b), b_1⟩ < a_3 ∧ a_3 < ⟨toLex (a_1, b_2), b_3⟩
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type ?u.3
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set ↑T
⊢ kernel S ≤ OrderDual.toDual (kernel (hull T (OrderDual.ofDual (kernel S))))

Tactic:
OrderDual.le_toDual,

Goal state after:
α : Type ?u.3
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set ↑T
⊢ kernel (hull T (OrderDual.ofDual (kernel S))) ≤ OrderDual.ofDual (kernel 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:
rw [← (hull_kernel_of_isClosed hT hG hR.1), ← gc_closureOperator]

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}
⊢ ⋯.closureOperator S ⊆ hull T (kernel R)
Module: Mathlib.Topology.Separation.AlexandrovDiscrete

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x✝ : X
⊢ x✝ ∈ nhdsKer s ↔ x✝ ∈ s

Tactic:
simp [mem_nhdsKer_iff_specializes]

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
L : ↑K.compactNhds
⊢ ∃ j₂, K.openRcNhdsToCompactNhds j₂ ≤ L

Tactic:
obtain ⟨U, h1, h2⟩ := exists_open_set_nhds_of_compactsNhds L

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
L : ↑K.compactNhds
U : Opens α
h1 : ↑K ⊆ ↑U
h2 : ↑U ⊆ ↑↑L
⊢ ∃ j₂, K.openRcNhdsToCompactNhds j₂ ≤ L
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 : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
⊢ ↑((E q).symm (Fin.cast Npq ((E p) z))) = y

Tactic:
rw [C1, C2, C3]

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

Goal state before:
pp: case mp
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
S : ShortComplex (Sheaf C X)
⊢ S.Exact → ∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact

pp: case mpr
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
S : ShortComplex (Sheaf C X)
⊢ (∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact) → S.Exact

Tactic:
· intro h x
    have := (forget C X ⋙ stalkFunctor C x).exact_tfae.out 2 1
    exact this.mp inferInstance S h

Goal state after:
case mpr
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
S : ShortComplex (Sheaf C X)
⊢ (∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact) → S.Exact
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 : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y (u n)
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < N q := ((E q) ⟨y, ys⟩).isLt
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
⊢ ↑((E q).symm (Fin.cast Npq ((E p) z))) = y

Tactic:
rw [C1, C2, C3]

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✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ HD (candidatesBDist X Y) ≤ diam univ + 1 + diam univ

Tactic:
by
  refine max_le (ciSup_le fun x => ?_) (ciSup_le fun y => ?_)
  · have A : ⨅ y, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl x, inr default) :=
      ciInf_le (by simpa using HD_below_aux1 0) default
    have B : dist (inl x) (inr default) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) :=
      calc
        dist (inl x) (inr (default : Y)) = dist x (default : X) + 1 + dist default default := rfl
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
    exact le_trans A B
  · have A : ⨅ x, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl default, inr y) :=
      ciInf_le (by simpa using HD_below_aux2 0) default
    have B : dist (inl default) (inr y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) :=
      calc
        dist (inl (default : X)) (inr y) = dist default default + 1 + dist default y := rfl
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
    exact le_trans A B

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✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hfx' : ↑z ∈ {x_1 | x_1 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_1}
hx : x ∈ sublevelLeft X f b ↑z
⊢ min (f ↑x ↑y) (f ↑x ↑y') ≤ b

Tactic:
exact le_trans hfx'.2 hx

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : HasSmallInductiveDimensionLT X (n + 1)
⊢ smallInductiveDimension X < ↑(n + 1)

Tactic:
apply (smallInductiveDimension_le_iff.2 h).trans_lt

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : HasSmallInductiveDimensionLT X (n + 1)
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := ⋯
F : Filter (γ × γ) := ⋯
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ (y, y) ∈ interior V

Tactic:
rw [mem_interior_iff_mem_nhds]

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ V ∈ 𝓝 (y, y)