mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ map (fun a ↦ a - k) atTop = atTop

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ map (fun a ↦ a + -k) atTop = atTop
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
⊢ m ≠ n → (fun m n ↦ 1 ≤ dist m n) m n

Tactic:
hne

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ g (blimsup u f p) ≤ blimsup (⇑g ∘ u) f p

Tactic:
by
  simp only [blimsup_eq_iInf_biSup, Function.comp]
  refine ((OrderHomClass.mono g).map_iInf₂_le _).trans ?_
  simp only [_root_.map_iSup, le_refl]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Tactic:
by
  refine le_antisymm ?_
    (sup_le (limsup_le_limsup_of_le le_sup_left) (limsup_le_limsup_of_le le_sup_right))
  simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_ofPred_eq, le_iInf₂_iff]
  intro a ha b hb
  exact sInf_le ⟨ha.mono fun _ h ↦ h.trans le_sup_left, hb.mono fun _ h ↦ h.trans le_sup_right⟩

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

Goal state before:
pp: a b c d : EReal
h1 : c ≠ ⊥ ∨ d ≠ ⊤
h2 : c ≠ ⊤ ∨ d ≠ ⊥
⊢ a + b + (-c - d) = a + -c + (b + -d)

Tactic:
sub_eq_add_neg

Goal state after:
a b c d : EReal
h1 : c ≠ ⊥ ∨ d ≠ ⊤
h2 : c ≠ ⊤ ∨ d ≠ ⊥
⊢ a + b + (-c + -d) = a + -c + (b + -d)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ 0
⊢ ⊤ * ↑x = ⊤

Tactic:
top_mul_coe_ennreal hx

Goal state after:
x : ℝ≥0∞
hx : x ≠ 0
⊢ ⊤ = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_neg
x✝ : ℝ
hx : x✝ < 0
⊢ ⊤ * ↑x✝ = ⊤ ↔ ⊤ = ⊥ ∧ ↑x✝ < 0 ∨ ⊤ < 0 ∧ ↑x✝ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ↑x✝ ∨ 0 < ⊤ ∧ ↑x✝ = ⊤

Tactic:
simp [hx.le, EReal.top_mul_coe_of_neg hx]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ sSup (⋃ j, ⋂ i, Iic (f ↑i)) = ⨆ j, ⨅ i, f ↑i

Tactic:
B,

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ sSup (⋃ j, Iic (⨅ i, f ↑i)) = ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe.inr.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a = 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

pp: case top.coe.inr.inr
hx : 0 ≤ ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
· simp [ha]

Goal state after:
case top.coe.inr.inr
hx : 0 ≤ ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg_coe
a b c : ℝ≥0∞
hc : 0 < c
⊢ -↑(a * c) - ↑(b * c) = -↑(a * c) + -↑(b * c)

Tactic:
sub_eq_add_neg

Goal state after:
case neg_coe
a b c : ℝ≥0∞
hc : 0 < c
⊢ -↑(a * c) + -↑(b * c) = -↑(a * c) + -↑(b * c)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ⊆ (t₁, t₂).1
ht₂ : (s, s).2 ⊆ (t₁, t₂).2
⊢ (∏ b ∈ (t₁, t₂).2, f b) / ∏ b ∈ (t₁, t₂).1, f b ∈ e

Tactic:
have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
      rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ⊆ (t₁, t₂).1
ht₂ : (s, s).2 ⊆ (t₁, t₂).2
this : (∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b
⊢ (∏ b ∈ (t₁, t₂).2, f b) / ∏ b ∈ (t₁, t₂).1, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : a = 0
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

Tactic:
· simp [ha]

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
· simp [ha]

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (if h : Multipliable (f ∘ g) then
      if True ∧ (mulSupport (f ∘ g)).Finite then finprod (Set.univ.mulIndicator (f ∘ g))
      else if HasProd (f ∘ g) 1 then 1 else Exists.choose ⋯
    else 1) =
    if h : Multipliable fun b ↦ f b then
      if True ∧ (mulSupport fun b ↦ f b).Finite then finprod (Set.univ.mulIndicator fun b ↦ f b)
      else if HasProd (fun b ↦ f b) 1 then 1 else Exists.choose ⋯
    else 1

Tactic:
true_and,

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (if h : Multipliable (f ∘ g) then
      if (mulSupport (f ∘ g)).Finite then finprod (Set.univ.mulIndicator (f ∘ g))
      else if HasProd (f ∘ g) 1 then 1 else Exists.choose ⋯
    else 1) =
    if h : Multipliable fun b ↦ f b then
      if (mulSupport fun b ↦ f b).Finite then finprod (Set.univ.mulIndicator fun b ↦ f b)
      else if HasProd (fun b ↦ f b) 1 then 1 else Exists.choose ⋯
    else 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑n)) g'
⊢ HasProd f (g * g' / f 0)

Tactic:
by
  refine mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_
  rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 - f j)
hprod : Multipliable fun x ↦ 1 - f x
⊢ ∏' (i : ι), (1 - f i) = 1 - ∑' (i : ι), f i * ∏ j < i, (1 - f j)

Tactic:
sub_eq_add_neg

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
⊢ ∏' (i : ι), (1 + -f i) = 1 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝¹ x✝ : α ⊕ β → γ
⊢ edist ((Equiv.sumArrowEquivProdArrow α β γ).toFun x✝¹) ((Equiv.sumArrowEquivProdArrow α β γ).toFun x✝) = edist x✝¹ x✝

Tactic:
simp [Prod.edist_eq, edist_pi_def, Finset.sup_univ_eq_iSup, iSup_sum]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
⊢ UniformContinuous fun p ↦ p.1 / p.2

Tactic:
uniformContinuous_dom₂

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
⊢ UniformContinuous fun p ↦ (mk p.1, mk p.2).1 / (mk p.1, mk p.2).2
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (((𝓤 α).lift' gen).lift' fun s ↦ s ○ s) = (𝓤 α).lift' fun s ↦ gen s ○ gen s

Tactic:
by
      rw [lift'_lift'_assoc]
      · exact monotone_gen
      · exact monotone_id.relComp monotone_id

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

Goal state before:
pp: ⊢ ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s

Tactic:
by
  obtain ⟨s, s_count, s_dense, hs⟩ :
    ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s :=
    exists_countable_dense_no_bot_top ℝ≥0∞
  exact ⟨s, s_count, s_dense, fun h => hs.1 0 (by simp) h, fun h => hs.2 ∞ (by simp) h⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val) x = f x

Tactic:
· simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]

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

Goal state before:
pp: s : Set ℝ
h : Bornology.IsBounded s
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Goal state after:
case inl
h : Bornology.IsBounded ∅
⊢ ediam ∅ = ENNReal.ofReal (sSup ∅ - sInf ∅)

case inr
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
⊢ liminf (fun i ↦ (u i).toReal) f = (liminf u f).toReal

Tactic:
have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) := by
    filter_upwards [le_b] with i i_le_b
    simp only [truncateToReal_eq_toReal b_ne_top i_le_b]

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ liminf (fun i ↦ (u i).toReal) f = (liminf u f).toReal
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ limsup (fun i ↦ (u i).toReal) f = (limsup u f).toReal

Tactic:
have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) := by
    filter_upwards [le_b] with i i_le_b
    simp only [truncateToReal_eq_toReal b_ne_top i_le_b]

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ limsup (fun i ↦ (u i).toReal) f = (limsup u f).toReal
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this : IsClosed[instTopologicalSpaceProd] {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}
⊢ s ×ˢ s ⊆ {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}

Tactic:
rintro ⟨x, y⟩ ⟨hx, hy⟩

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this : IsClosed[instTopologicalSpaceProd] {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
⊢ (x, y) ∈ {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: 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
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Tactic:
induction hne using Finset.Nonempty.cons_induction with
  | singleton => simpa using hs
  | cons a s ha hne ihs =>
    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: L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf f) x

Tactic:
simpa only [← Finset.inf_apply] using finset_inf_apply hs

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

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf f) t x

Tactic:
simpa only [← Finset.inf_apply] using finset_inf_apply hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : (n, y) ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < 1}
hGn : (n, y) ∈ (fun y ↦ (g y.2, G y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < 1}
hfg : (n, y) ∈ Prod.snd ⁻¹' {x | dist (f x) 0 ≤ C ∧ dist (g x) 0 ≤ C}
⊢ ((f (n, y).2, g (n, y).2), F (n, y).1 (n, y).2, G (n, y).1 (n, y).2) ∈ Metric.ball 0 (C + 1) ×ˢ Metric.ball 0 (C + 1)

Tactic:
simp only [mem_prod, Metric.mem_ball, Prod.dist_eq, Prod.fst_zero, Prod.snd_zero, sup_lt_iff,
    mem_preimage, mem_ofPred] at hFn hGn hfg ⊢

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ (dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1) ∧ dist (F n y) 0 < C + 1 ∧ dist (G n y) 0 < C + 1
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun i ↦ f i / a

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x✝¹ x✝ : ℝ
h₀ : 0 ≤ x✝¹
hr : x✝¹ < x✝
x : ℝ
h : x✝¹ < x ∧ x < x✝
⊢ x✝¹ < ‖x‖ ∧ ‖x‖ < x✝

Tactic:
by rwa [Real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : SeminormedGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : HasCompactMulSupport f
h'f : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa using (hf.isCompact_range h'f).isBounded.exists_norm_le'

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ dist (f x) (f y) = ↑(r * nndist x y)

Tactic:
hr.2,

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ ↑r * dist x y = ↑(r * nndist x y)
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
by_cases! hX : ∀ x y : X, edist x y = 0 ∨ edist x y = ∞

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (e.trans e') = ratio e * ratio e'
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

Tactic:
rcases s with ⟨⟨l⟩, hl⟩
  have : l.map f ≠ [] := by simpa using! hs
  simpa using! List.norm_prod_le' this

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

Goal state before:
pp: α : Type u_2
inst✝³ : NormedAddCommGroup α
inst✝² : MulOneClass α
inst✝¹ : NormMulClass α
inst✝ : Nontrivial α
⊢ ‖1‖ = 1

Tactic:
by
    obtain ⟨u, hu⟩ := exists_ne (0 : α)
    simpa [mul_eq_left₀ (norm_ne_zero_iff.mpr hu)] using (norm_mul u 1).symm

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ v (x - y) = v (x + -y)

Tactic:
sub_eq_add_neg

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ v (x + -y) = v (x + -y)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: R : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Finite ι
inst✝³ : Finite ι'
F : Type u_8
inst✝² : FunLike F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
⊢ ⨆ a, v (x a.1 * y a.2) = (⨆ i, v (x i)) * ⨆ j, v (y j)

Tactic:
Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),

Goal state after:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Finite ι
inst✝³ : Finite ι'
F : Type u_8
inst✝² : FunLike F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
⊢ ⨆ a, v (x a.1 * y a.2) = ⨆ i, v (x i) * ⨆ j, v (y j)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ generateFrom ({univ} ∪ S) = generateFrom S

Tactic:
← generateFrom_sup_generateFrom,

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ generateFrom {univ} ⊔ generateFrom S = generateFrom S
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ generateFrom ({∅} ∪ S) = generateFrom S

Tactic:
← generateFrom_sup_generateFrom,

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ generateFrom {∅} ⊔ generateFrom S = generateFrom S
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)

Tactic:
have : IsAddTorsionFree E := .of_module_rat E

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)