mathlib-initiative/mathlib-tactics huggingface dataset:
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 → β
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
x : E
hx : x ∈ X
hx1 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y
hx2 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y'
⊢ max (f a ↑y) (f a ↑y') ≤ b

Tactic:
ha x hx

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
x : E
hx : x ∈ X
hx1 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y
hx2 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y'
⊢ max (f x ↑y) (f x ↑y') ≤ b
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
hmn : m ≤ n
H : HasSmallInductiveDimensionLE X m
⊢ HasSmallInductiveDimensionLE X n

Tactic:
by
  apply HasSmallInductiveDimensionLT.mono _ H
  rwa [add_le_add_iff_right]

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ smallInductiveDimension X = ⊥ ↔ smallInductiveDimension X < ↑0

Tactic:
WithBot.lt_coe_bot.symm,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ smallInductiveDimension X < ↑⊥ ↔ smallInductiveDimension X < ↑0