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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

Tactic:
by
    have : Set.InjOn x t := by
      intro c hc d hd hcd
      have : f (x c) = f (x d) := by simp [hcd]
      rwa [hfx _ hc, hfx _ hd] at this
    exact countable_of_injective_of_countable_image this H

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
⊢ ∀ ⦃a : α⦄, x c < a → a < y (f (x c)) → ∀ ⦃b : α⦄, x d < b → b < y (f (x d)) → ¬a = b

Tactic:
rintro a xca ayc b xda ayd rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y (f (x c))
xda : x d < a
ayd : a < y (f (x d))
⊢ False
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : α → β
inst✝ : SecondCountableTopology α
hf : Monotone f
⊢ {c | ∃ x y, x < y ∧ f x = c ∧ f y = c}.Countable

Tactic:
← monotoneOn_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f univ
⊢ {c | ∃ x y, x < y ∧ f x = c ∧ f y = c}.Countable
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
x : β
hx : x ∈ s
hx' : IsMinOn f s x
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
exact ⟨f x, hf' x hx, hx'⟩

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
⊢ BddBelow s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Goal state after:
case inl
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
hs : IsCompact ∅
⊢ BddBelow ∅

case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∪ t
b : X
hb : b ∈ s ∪ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
mem_union

Goal state after:
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∨ a ∈ t
b : X
hb : b ∈ s ∨ b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x ↦ b * x) ⁻¹' sphere a r ↔ c ∈ sphere (a / b) r

Tactic:
simp only [Set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm]

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

Goal state before:
pp: case refine_4
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
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑J' ≤ ↑I'

Tactic:
· exact h'

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

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ t ∪ s
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty

Tactic:
exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))

Tactic:
rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hlt : ∀ i ∈ s, f i < g i
⊢ ∑ i ∈ s, f i < ∑ i ∈ s, g i

Tactic:
induction hs using Finset.Nonempty.cons_induction with

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∀ i ∈ s, g i < f i
⊢ ∑ i ∈ s, g i < ∑ i ∈ s, f i

Tactic:
apply ENNReal.sum_lt_sum_of_nonempty hs Hle

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderInf α
inst✝ : InfConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ i, f i))

Tactic:
convert! tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB s (a, b)
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))

Tactic:
rw [isLUB_prod, ← range_domRestrict, ← range_domRestrict] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (range (s.domRestrict snd)) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ blimsup u atTop p = ⨅ i, ⨆ j, ⨆ (_ : p j ∧ i ≤ j), u j

Tactic:
simp only [atTop_basis.blimsup_eq_iInf_iSup, @and_comm (p _), iSup_and, mem_Ici, iInf_true]

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

Goal state before:
pp: x : EReal
⊢ x - x ≤ 0

Tactic:
by
  cases x <;> simp

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

Goal state before:
pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real,
      Real.coe_toNNReal, zero_sub, coe_neg, neg_neg]

Goal state after:
case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x
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 : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i

Tactic:
refine ⟨fun i : { i | q i } => g (b i) (hl.mem_of_mem i.2), fun i => ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
α : 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 : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ x ∈ u ((fun i ↦ g (b ↑i) ⋯) i)

case refine_2
α : 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 : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ p ((fun i ↦ g (b ↑i) ⋯) i) ∧ (fun i ↦ g (b ↑i) ⋯) i ∈ b ↑i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
a : β
ha : ∀ᶠ (x : α) in f, v x ≤ a
⊢ ∃ᶠ (x : α) in f, u x ≤ a

Tactic:
exact (h.and_eventually ha).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ d ∈ {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Tactic:
· rcases hd with ⟨e, ⟨he, fe_eq_d⟩⟩
      filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
⊢ (if L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite then finprod (L.support.mulIndicator fun b ↦ f b)
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
rw [L.support_eq_univ, Set.inter_univ, Set.mulIndicator_univ]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
⊢ (if L.HasSupport ∧ (mulSupport fun b ↦ f b).Finite then ∏ᶠ (b : β), f b
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b
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
H : ∃ j, BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

Tactic:
classical
  rcases H with ⟨j0, hj0⟩
  let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))}
  have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs j)
  have A : ⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i) =
         ⋃ (j : Subtype p), ⋂ (i : s (liminfReparam f s p j)), Iic (f i) := by
    apply Subset.antisymm
    · apply iUnion_subset (fun j ↦ ?_)
      by_cases hj : j ∈ m
      · have : j = liminfReparam f s p j := by simp only [m, liminfReparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j
      · simp only [m, mem_ofPred_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj
        simp only [hj, empty_subset]
    · apply iUnion_subset (fun j ↦ ?_)
      exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminfReparam f s p j)
  have B : ∀ (j : Subtype p), ⋂ (i : s (liminfReparam f s p j)), Iic (f i) =
                                Iic (⨅ (i : s (liminfReparam f s p j)), f i) := by
    intro j
    apply (Iic_ciInf _).symm
    change liminfReparam f s p j ∈ m
    by_cases Hj : j ∈ m
    · simpa only [m, liminfReparam, if_pos Hj] using Hj
    · simp only [m, liminfReparam, if_neg Hj]
      have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by
        rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
        exact ⟨n, Or.inl hj0⟩
      rcases Nat.find_spec Z with hZ | hZ
      · exact hZ
      · exact (hZ j0 hj0).elim
  simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : HasProd (fun b ↦ f b) 1 L
⊢ HasProd f 1 L

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L

Tactic:
· exact h'

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd (extend g f 1) a ↔ HasProd f a

Tactic:
rw [← hg.hasProd_iff, extend_comp hg]
  exact extend_apply' _ _

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℕ → M
h : HasProd (fun n ↦ f (n + 1)) m
⊢ HasProd f (f 0 * m)

Tactic:
simpa only [prod_range_one] using h.prod_range_mul

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) g ↔ HasProd ((fun x ↦ f ↑x) ∘ ⇑(notMemRangeEquiv k).symm) g

Tactic:
Function.comp_def,

Goal state after:
G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) g ↔ HasProd (fun x ↦ f ↑((notMemRangeEquiv k).symm x)) g
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
⊢ Finite ι

Tactic:
have : ∀ s : Finset ι, #s ≤ n := fun s ↦ by
    simpa [nsmul_le_nsmul_iff_left hb] using (H s).trans hn

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this : ∀ (s : Finset ι), #s ≤ n
⊢ Finite ι
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : Bool → α
⊢ ∏' (i : Bool), f i = f false * f true

Tactic:
rw [tprod_fintype, Fintype.prod_bool, mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↑↑s), f ↑x = ∏ x ∈ s, f x

Tactic:
by
  simp [prod_attach]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)

Tactic:
by
  rw [← summable_coe] at hf ⊢
  exact hf.comp_injective hi

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

Goal state before:
pp: case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr

Tactic:
· ext (_ | _) <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.ediam (f '' univ) = Metric.ediam univ

Tactic:
exact hf.ediam_image univ

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) s

Tactic:
tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,

Goal state after:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOn f l s ↔ TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b ↦ f b c
⊢ ∏' (p : γ × β), uncurry (fun b c ↦ f c b) p = ∏' (p : β × γ), uncurry f p

Tactic:
← (Equiv.prodComm γ β).tprod_eq (uncurry f)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b ↦ f b c
⊢ ∏' (p : γ × β), uncurry (fun b c ↦ f c b) p = ∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β) c)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_1
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

pp: case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
· obtain ⟨n, hn⟩ := h ε hε
    exact ⟨n, hn n le_rfl⟩

Goal state after:
case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)

Tactic:
Function.comp_def,

Goal state after:
α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (fun x ↦ pkg'.coe (f x)) (pkg.coe a) = g (pkg.coe a)
Module: Mathlib.Topology.Algebra.UniformMulAction

Goal state before:
pp: M : Type v
X : Type x
Y : Type y
inst✝⁴ : UniformSpace X
inst✝³ : UniformSpace Y
inst✝² : SMul M X
inst✝¹ : SMul M Y
inst✝ : UniformContinuousConstSMul M Y
f : X → Y
hf : IsUniformInducing f
hsmul : ∀ (c : M) (x : X), f (c • x) = c • f x
c : M
⊢ UniformContinuous fun x ↦ c • x

Tactic:
by
    simpa only [hf.uniformContinuous_iff, Function.comp_def, hsmul]
      using! hf.uniformContinuous.const_smul c

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

Goal state before:
pp: α : Type u_4
inst✝ : PseudoMetricSpace α
s : Set α
⊢ diam (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = diam s

Tactic:
by simp only [Metric.diam, Metric.ediam_closure]

Goal state after:
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✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Goal state after:
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))

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.Field.Basic

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
⊢ Metric.closedBall 0 1 = Set.univ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
h₀ : edist x y ≠ 0
htop : edist x y ≠ ∞
hr : edist (f x) (f y) = ↑r * edist x y
⊢ r = ratio f

Tactic:
by
  simpa only [hr, ENNReal.mul_left_inj h₀ htop, ENNReal.coe_inj] using edist_eq f x y

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ ratio e.toDilationEquiv = 1

Tactic:
← ratio_toDilation,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ ratio e.toDilationEquiv.toDilation = 1