mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ count p.asIdeal (normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod) =
    min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)

pp: case h
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥

Tactic:
← count_normalizedFactors_eq_multiplicity hI,

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ count p.asIdeal (normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod) =
    min (count p.asIdeal (normalizedFactors I)) (multiplicity p.asIdeal J)

case h
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
⊢ f '' Ioc a b = Ioc (f a) (f b)

Tactic:
rcases le_or_gt a b with hab | hab
  · exact hf_c.continuousOn.image_Ioc_of_strictMonoOn hab (hf.strictMonoOn _)
  · simp [lt_asymm hab, lt_asymm (hf hab)]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
hn : n ≤ N
x : α
hx : x ∈ ⋂ n, ⋂ (_ : n ≤ N), s n
⊢ x ∈ s n

Tactic:
simp only [mem_iInter] at hx

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
hn : n ≤ N
x : α
hx : ∀ i ≤ N, x ∈ s i
⊢ x ∈ s n
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u ∨ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
rcases h with (h' | h')

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊥ + y ≠ ⊤ ↔ ⊥ ≠ ⊤

Tactic:
simp [add_ne_top_iff_ne_top₂, hy, hy']

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

Goal state before:
pp: case coe
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
a✝ : ℝ
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤

Tactic:
simp [add_ne_top_iff_ne_top₂, hy, hy']

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

Goal state before:
pp: case top
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤

Tactic:
simp [add_ne_top_iff_ne_top₂, hy, hy']

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
⊢ ↑Kf * ↑Kg * edist x y = ↑(Kf * Kg) * edist x y

Tactic:
ENNReal.coe_mul

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
⊢ ↑Kf * ↑Kg * edist x y = ↑Kf * ↑Kg * edist x y
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
b : ℝ
⊢ a + ↑b - ↑b = a

Tactic:
cases a <;> norm_cast
  exact _root_.add_sub_cancel_right _ _

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)

Tactic:
exact ⟨sInf ∅, tendsto_bot⟩

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

Goal state before:
pp: a b : EReal
h : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0

Tactic:
cases a <;> cases b

Goal state after:
case bot.bot
h : ⊥ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊥ * ⊥ ≠ 0

case bot.coe
a✝ : ℝ
h : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊥ * ↑a✝ ≠ 0

case bot.top
h : ⊥ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊥ * ⊤ ≠ 0

case coe.bot
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
⊢ ↑a✝ * ⊥ ≠ 0

case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ↑a✝¹ * ↑a✝ ≠ 0

case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0

case top.bot
h : ⊤ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊤ * ⊥ ≠ 0

case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

case top.top
h : ⊤ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊤ * ⊤ ≠ 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
⊢ x ≤ limsup u f

Tactic:
rw [← forall_lt_iff_le]
    intro y y_x
    obtain ⟨z, y_z, z_x⟩ := h' y y_x
    exact y_z.trans_le (le_limsup_of_frequently_le ((h z z_x).mono (fun _ ↦ le_of_lt)) h₂)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
u v : α → β
h : ∃ᶠ (x : α) in ⊥, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ v
⊢ liminf u ⊥ ≤ limsup v ⊥

Tactic:
exact (frequently_bot h).rec

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ u n v ≤ b''

Tactic:
refine hrs n v ?_
    calc rs n
    _ = rs (⟨n, by simp [hn]⟩ : {n | b'' < u n r}) := rfl
    _ ≤ ⨆ n : {n | b'' < u n r}, rs n := by
      refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})
      have : Finite {n | b'' < u n r} := by simpa using! hb''
      exact Finite.bddAbove_range _
    _ ≤ r ⊔ ⨆ n : {n | b'' < u n r}, rs n := le_sup_right
    _ ≤ v := hv

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

Goal state before:
pp: a b : EReal
⊢ 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
mul_nonneg_iff,

Goal state after:
a b : EReal
⊢ 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hAtTop : True
hL : F ≤ pure Finset.univ
s : Set (Finset β)
hs : s ∈ F
hs' : Finset.univ ∉ s
⊢ ∅ ∈ F

Tactic:
simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a ↔ HasProd f a

Tactic:
← hg.hasProd_comap_iff hf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a ((unconditional β).comap { toFun := g, inj' := hg })
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ (b + -c) * a = b * a - c * a

Tactic:
right_distrib_of_nonneg_of_ne_top ha ha'

Goal state after:
a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ b * a + -c * a = b * a - c * a
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
⊢ Multipliable (f ∘ Subtype.val)

Tactic:
by
  have := hs.toFinset.multipliable f
  rwa [hs.coe_toFinset] at this

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

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable fun b ↦ f ↑b

Tactic:
apply hf.subtype

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : ¬(mulSupport f).Finite
⊢ ∏ᶠ (b : ι), f b ≤ a₂

Tactic:
finprod_of_infinite_mulSupport hf

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : ¬(mulSupport f).Finite
⊢ 1 ≤ a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective Nat.cast

pp: case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective fun n ↦ -(↑n + 1)

Tactic:
exacts [Nat.cast_injective, @Int.negSucc.inj]

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

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]

Goal state after:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
cases isEmpty_or_nonempty ι
  · simp [hn]
  · exact iSup_pow hf _

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 : 2 * L.sum ≤ L.sum
hLm : L.length ≤ m
⊢ False

Tactic:
two_mul,

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 : L.sum + L.sum ≤ L.sum
hLm : L.length ≤ m
⊢ False
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s : Set (CauchyFilter α × CauchyFilter α)
t : Set (α × α)
_h : t ∈ 𝓤 α
⊢ gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s

Tactic:
exact ⟨fun h _f _g ht => h ht, fun h _p hp => h _ _ hp⟩

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

Goal state before:
pp: case refine_3.inr
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 : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs' : (take (M + 1) L).sum + (drop (M + 1) L).sum ≤ 2 * (take (M + 1) L).sum
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
two_mul,

Goal state after:
case refine_3.inr
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 : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs' : (take (M + 1) L).sum + (drop (M + 1) L).sum ≤ (take (M + 1) L).sum + (take (M + 1) L).sum
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i ↦ x i < ↑q) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n ↦ x n < R) x_1

Tactic:
filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le

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

Goal state before:
pp: ι : Type u_4
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ∞
f : ι → ℝ≥0
⊢ Tendsto (fun n ↦ ((fun i ↦ ↑(f i)) n).toReal) fi (𝓝 x.toReal) ↔ Tendsto (fun i ↦ ↑(f i)) fi (𝓝 x)

Tactic:
lift x to ℝ≥0 using hx

Goal state after:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0
x : ℝ≥0
⊢ Tendsto (fun n ↦ ((fun i ↦ ↑(f i)) n).toReal) fi (𝓝 (↑x).toReal) ↔ Tendsto (fun i ↦ ↑(f i)) fi (𝓝 ↑x)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ Continuous t.truncateToReal

Tactic:
by
  apply continuousOn_toReal.comp_continuous (by fun_prop)
  simp [t_ne_top]

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

Goal state before:
pp: case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Tactic:
rw [forall_mem_cons] at hs
    simp only [sup'_cons, hne]
    exact hs.1.sup_nhds (ihs hs.2)

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

Goal state before:
pp: case inl
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ ∅, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (∅.sup f) l (𝓝 (∅.sup g))

pp: case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
· simpa using! tendsto_const_nhds

Goal state after:
case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f : α → E
s : Set α
⊢ LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f

Tactic:
by
  simp [LocallyLipschitzOn]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
Kg : ℝ≥0
u : Set α
hu : u ∈ 𝓝[s] x
hKg : LipschitzOnWith Kg g u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x ↦ f x * g x) t

Tactic:
exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu,
    (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ ↑(r * nndist x y) = ↑r * ↑(nndist x y)

Tactic:
ENNReal.coe_mul

Goal state after:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ ↑r * ↑(nndist x y) = ↑r * ↑(nndist x y)
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
⊢ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε

Tactic:
intro ε ε₀

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
⊢ ↑(ratio (g.comp f)) = ↑(ratio g * ratio f)

Tactic:
ENNReal.coe_mul

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
⊢ ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 ↦ x_1 / x) ∘ u) n ∈ closedBall 0 1
a : K
ha' : Tendsto ((fun x_1 ↦ x_1 / x) ∘ u) atTop (𝓝 a)
⊢ ∀ (x_1 : ℕ), ((fun x_2 ↦ x_2 * x) ∘ (fun x_2 ↦ x_2 / x) ∘ u) x_1 = u x_1

Tactic:
have hx' : x ≠ 0 := by
    contrapose! hx
    simp [hx, kpos]

Goal state after:
case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 ↦ x_1 / x) ∘ u) n ∈ closedBall 0 1
a : K
ha' : Tendsto ((fun x_1 ↦ x_1 / x) ∘ u) atTop (𝓝 a)
hx' : x ≠ 0
⊢ ∀ (x_1 : ℕ), ((fun x_2 ↦ x_2 * x) ∘ (fun x_2 ↦ x_2 / x) ∘ u) x_1 = u x_1
Module: Mathlib.MeasureTheory.MeasurableSpace.Instances

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Subsingleton α
⊢ MeasurableSingletonClass α

Tactic:
refine ⟨fun i => ?_⟩
  convert! MeasurableSet.univ
  simp [Set.eq_univ_iff_forall, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x = measurableAtom y

Tactic:
refine subset_antisymm (measurableAtom_subset_of_mem hx) ?_

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom y ⊆ measurableAtom x
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d

Tactic:
by
  simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a b : SignType
⊢ Decidable (a ≤ b)

Tactic:
cases a <;> cases b

Goal state after:
case zero.zero
⊢ Decidable (zero ≤ zero)

case zero.neg
⊢ Decidable (zero ≤ neg)

case zero.pos
⊢ Decidable (zero ≤ pos)

case neg.zero
⊢ Decidable (neg ≤ zero)

case neg.neg
⊢ Decidable (neg ≤ neg)

case neg.pos
⊢ Decidable (neg ≤ pos)

case pos.zero
⊢ Decidable (pos ≤ zero)

case pos.neg
⊢ Decidable (pos ≤ neg)

case pos.pos
⊢ Decidable (pos ≤ pos)