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

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
obtain h | _ := isTop_or_exists_gt d

Goal state after:
case inl.inl
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
h✝ : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h : IsTop d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

case inl.inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
⊢ f (sSup s) = sSup (f '' s)

Tactic:
rcases s.eq_empty_or_nonempty with h | h
  · simp [h, fbot]
  · exact Mf.map_csSup_of_continuousWithinAt Cf h

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
have := FractionalIdeal.sup_mul_inf J' (spanSingleton R⁰ (I'.divMod I J') * I)
    rwa [FractionalIdeal.sup_eq_add, divMod_spec h' hJ' hI, mul_left_comm, mul_comm J' I, H,
      mul_comm I' J, ← mul_assoc, (mul_left_injective₀ _).eq_iff] at this
    rintro rfl
    exact hJ' (by simpa using h')

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
⊢ s ∈ atBot

Tactic:
obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ s ∈ atBot
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous[inst✝³, inst✝⁴] f
h : HasCompactMulSupport f
x : β
hx : f x ∈ lowerBounds (range f)
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
mem_lowerBounds,

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous[inst✝³, inst✝⁴] f
h : HasCompactMulSupport f
x : β
hx : ∀ x_1 ∈ range f, f x ≤ x_1
⊢ ∃ x, ∀ (y : β), f x ≤ f y
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
⊢ sSup (f '' K) < y

Tactic:
refine (csSup_le (h0K.image f) ?_).trans_lt (h x hx)

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
⊢ ∀ b ∈ f '' K, b ≤ f x
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : SeminormedGroup E
inst✝ : Subsingleton E
a : E
⊢ ‖a‖ = 0

Tactic:
by
  rw [Subsingleton.elim a 1, norm_one']

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x * r) l atTop

Tactic:
simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)

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

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] ↑x
hft : LipschitzOnWith K f t
⊢ ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
exact ⟨_, ⟨t, ht, Subset.rfl⟩, hft.mono <| inter_subset_right.trans <| image_preimage_subset ..⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_
    rintro _ ⟨_, h, rfl⟩
    exact h

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

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Tactic:
· rintro ⟨t, ⟨u, hu, hut⟩, hft⟩
    exact ⟨s ∩ u, Filter.inter_mem self_mem_nhdsWithin hu,
      hft.mono fun x hx ↦ ⟨hx.1, ⟨x, hx.1⟩, hut hx.2, rfl⟩⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ ⨅ s ∈ l, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i

Tactic:
simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ i ∈ l, ∃ i_2, (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: case h₁
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist (f (a, b)) (f (x', b)) ≤ ↑K * (↑δ + ↑δ)

Tactic:
refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
        exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ -a < 0 ∧ b = ⊥ ∨ -a = ⊤ ∧ 0 < b ∨ 0 < -a ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
neg_eq_top_iff,

Goal state after:
a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ -a < 0 ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ 0 < -a ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a : α
h : HasProd f a L
⊢ HasProd (fun b ↦ (f b)⁻¹) a⁻¹ L

Tactic:
by
  simpa only using! h.map (MonoidHom.id α)⁻¹ continuous_inv

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : IsCompl s t
ha : HasProd (f ∘ Subtype.val) a
hb : HasProd (f ∘ Subtype.val) b
⊢ HasProd f (a * b)

Tactic:
simpa [← hs.compl_eq] using
    (hasProd_subtype_iff_mulIndicator.1 ha).mul (hasProd_subtype_iff_mulIndicator.1 hb)

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
a✝ : α
⊢ f a✝ ≠ ∞ → g a✝ ≠ ∞ → (f a✝).toReal = (g a✝).toReal → f a✝ = g a✝

Tactic:
hfx

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
a✝ : α
hfx : f a✝ ≠ ∞
⊢ g a✝ ≠ ∞ → (f a✝).toReal = (g a✝).toReal → f a✝ = g a✝
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : CommMonoid γ
inst✝ : TopologicalSpace γ
f : β → α
g : β → γ
a : α
b : γ
hf : HasProd f a L
hg : HasProd g b L
⊢ HasProd (fun x ↦ (f x, g x)) (a, b) L

Tactic:
simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prodMk_nhds hf hg]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : m ∈ s
hLm : L.length ≤ m
⊢ False

Tactic:
rw [mem_ofPred_eq, take_of_length_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
          sum_eq_zero_iff, ← forall_iff_forall_mem, forall_zipWith,
          ← isChain_cons_append_singleton_iff_forall₂]
          at hm <;>
        [skip; simp]

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : List.IsChain (fun x y ↦ d x y = 0) (x :: l ++ [y])
hLm : L.length ≤ m
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
L : Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ t0, f p) atTop (𝓝 (∏ b ∈ t0, g b))
this : ∃ t, ∏ p ∈ t with p.fst ∈ t0, f p ∈ v ∧ s ⊆ t
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
obtain ⟨t, tv, st⟩ := this

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
L : Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ t0, f p) atTop (𝓝 (∏ b ∈ t0, g b))
t : Finset ((b : β) × γ b)
tv : ∏ p ∈ t with p.fst ∈ t0, f p ∈ v
st : s ⊆ t
⊢ ∃ b, s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Module: Mathlib.Topology.Algebra.UniformMulAction

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
⊢ m • n • x = n • m • x

Tactic:
have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl

Goal state after:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
⊢ m • n • x = n • m • x
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
⊢ (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n

Tactic:
dsimp only [d]

Goal state after:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
⊢ ((1 / 2) ^ n ≤ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0) ↔ (x, y) ∉ U n
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
by
  simpa only [div_eq_mul_inv, dist_inv_inv] using dist_mul_mul_le a₁ a₂⁻¹ b₁ b₂⁻¹

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mp
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 → x ≠ 0

Tactic:
intro hx

Goal state after:
case mp
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : ‖x‖ = 1
⊢ x ≠ 0
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ x ≠ 0 → ‖x‖ = 1

Tactic:
intro hx

Goal state after:
case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ = 1
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
h : ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
rcases h with ⟨x, hx, hx1⟩

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
⊢ ∃ x, 1 < ‖x‖
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : ↥t) → π ↑i
⊢ s.restrict (updateFinset x t y) = restrict₂ hst y

Tactic:
by
  ext i
  simp [updateFinset, dif_pos (hst i.2)]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ Measurable f ↔ Measurable (f ∘ g)

Tactic:
measurable_iff_le_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ mγ ≤ MeasurableSpace.map f mβ ↔ Measurable (f ∘ g)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ mγ ≤ MeasurableSpace.map f mβ ↔ Measurable (f ∘ g)

Tactic:
measurable_iff_le_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ mγ ≤ MeasurableSpace.map f mβ ↔ mγ ≤ MeasurableSpace.map (f ∘ g) (MeasurableSpace.comap g mβ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)

Tactic:
by
  rw [preimage_iUnionLift]
  exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
i j : ι
x : α
hxi : x ∈ t i
⊢ ∀ (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩

Tactic:
hxj

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
i j : ι
x : α
hxi : x ∈ t i
hxj : x ∈ t j
⊢ g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
by
  rcases lt_trichotomy 0 a with (h | h | h)
  · simp [h, h.le]
  · simp [← h]
  · simp [h, h.not_ge]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : EReal
⊢ x.abs = 0 ↔ x = 0

Tactic:
induction x
  · simp
  · simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]
  · simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
mul_comm b⁻¹ a⁻¹

Goal state after:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : EReal
⊢ ⊥ < x⁻¹

Tactic:
by
  cases x with
  | bot => exact inv_bot ▸ bot_lt_zero
  | top => exact EReal.inv_top ▸ bot_lt_zero
  | coe x => exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
hf : Summable fun i ↦ ↑(f i)
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i ↦ ↑(g i)) b ≤ (fun i ↦ ↑(f i)) b
⊢ Summable fun i ↦ ↑(g i)

Tactic:
rw [NNReal.summable_coe] at hf ⊢

Goal state after:
β : Type u_2
f : β → ℝ≥0
hf : Summable f
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i ↦ ↑(g i)) b ≤ (fun i ↦ ↑(f i)) b
⊢ Summable g
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
⊢ False

Tactic:
let _ : (𝓝 a ⊓ ℱ).NeBot := h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝² : Nonempty α
x✝¹ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
⊢ False
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
⊢ ∀ i < ⊤, ∃ i', True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ

Tactic:
simp only [EReal.image_coe_Ici, true_and]
    intro x hx
    by_cases hx_bot : x = ⊥
    · simp [hx_bot]
    lift x to ℝ using ⟨hx.ne_top, hx_bot⟩
    refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
    simp [h1, h2.ne_top]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)

Tactic:
simp [tendsto_inv_atTop_nhds_zero_nat]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ s ≤ ⊤ s

Tactic:
top_apply hs

Goal state after:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ∞ ≤ ⊤ s
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
      filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
      rcases le_or_gt (f a) (f x) with h | h
      · exact hl ⟨lfa, h⟩
      · exact hu ⟨le_of_lt h, fau⟩

Goal state after: