mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ sSup s * a = ⨆ b ∈ s, b * a

Tactic:
simp only [sSup_eq_iSup, iSup_mul]

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy : Subtype.val ⁻¹' u = Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r
⊢ Subtype.val ⁻¹' f ⁻¹' u = Metric.eball x ∞ ↓∩ Metric.eball x r

Tactic:
aesop (add simp [Set.ext_iff])

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ dist x y = (edist x y).toReal

Tactic:
by
  rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ sphere x ε ↔ dist x y = ε

Tactic:
by rw [dist_comm, mem_sphere]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
⊢ p y

Tactic:
obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z :=
    frequently_iff.1 H (Ioi_mem_atTop (dist y x))

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
R : ℝ
hR : R > dist y x
h : ∀ z ∈ ball x R, p z
⊢ p y
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddBelow s
⊢ sInf (a • s) = a • sInf s

Tactic:
Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h),

Goal state after:
case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddBelow s
⊢ 0 = a • sInf s
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: case pos
ι : Sort u_4
f : ι → ℕ
h : BddAbove (range f)
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
apply eq_of_forall_ge_iff

Goal state after:
case pos
ι : Sort u_4
f : ι → ℕ
h : BddAbove (range f)
⊢ ∀ (c : ℝ≥0), ↑(⨆ i, f i) ≤ c ↔ ⨆ i, ↑(f i) ≤ c
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
⊢ SeparableSpace X

Tactic:
choose U hUc hUu using fun n =>
    LindelofSpace.elim_nhds_subcover (fun x => ball x (V n))
      (fun x => ball_mem_nhds x (hVb.mem n))

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
⊢ SeparableSpace X
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : Bornology α
p : α → Prop
⊢ BoundedSpace (Subtype p) ↔ Bornology.IsBounded {x | p x}

Tactic:
boundedSpace_induced_iff,

Goal state after:
α : Type u_1
inst✝ : Bornology α
p : α → Prop
⊢ Bornology.IsBounded (range Subtype.val) ↔ Bornology.IsBounded {x | p x}
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : a ∈ closure[inst✝²] s
⊢ IsLUB s a

Tactic:
mem_closure_iff_clusterPt,

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : ClusterPt a (𝓟 s)
⊢ IsLUB s a
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
⊢ ∃ u, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
by
  rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
  exact ⟨u, hu.1, hu.2.2⟩

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ dist _r _y = ‖-_r + _y‖

Tactic:
by rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this✝ : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx✝ : b ≤ x
hbx : b < x
this : s ∩ Ioi b ∈ 𝓝[s] x
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c

Tactic:
filter_upwards [this] with y hy using hf hb hy.1 (le_of_lt hy.2)

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y⁻¹‖ = ‖y‖

Tactic:
norm_mul_eq_norm_right _ h,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y⁻¹‖ = ‖y‖
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ (factorization I) p.asIdeal = multiplicity p.asIdeal I

Tactic:
factorization_eq_count,

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedCancelAddMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedCancelAddMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x

Tactic:
have hU : {x : β | f x₀ < f x} ∈ Filter.cocompact β := by
    refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩
    simp only [Set.compl_ofPred, not_lt]
    exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
hU : {x | f x₀ < f x} ∈ cocompact β
⊢ ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: ι : Type u_3
α : Type u_4
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l)

Tactic:
classical
  exact if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
  else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H

Goal state after:
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
by
  apply le_antisymm
  · rw [limsup_eq]
    refine sInf_le_sInf fun x hx => ?_
    rcases (mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩
    filter_upwards [I_mem_F] with i hi
    exact hI ▸ le_sSup (mem_image_of_mem _ hi)
  · 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.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
rw [ne_eq, mul_eq_top]

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

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ g 1 = ∏'[L] (i : ι), g (f i)

Tactic:
tprod_eq_one_of_not_multipliable,

Goal state after:
case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ g 1 = 1

case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ ¬Multipliable (fun i ↦ g (f i)) L
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
disjoint_iff_inf_le

Goal state after:
case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Set.range Nat.cast ⊓ Set.range Int.negSucc ⊆ ⊥
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
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
⊢ ∃ u', u ⊆ u' ∧ (∏ x ∈ u', f x * if x = 0 then f 0 else 1) = ∏ b ∈ v', f ↑b * f (-↑b)

Tactic:
let u2 := v'.image fun x : ℕ ↦ -(x : ℤ)

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
⊢ ∃ u', u ⊆ u' ∧ (∏ x ∈ u', f x * if x = 0 then f 0 else 1) = ∏ b ∈ v', f ↑b * f (-↑b)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ HasProd (fun x ↦ 1 + f x) a

Tactic:
simp_rw [HasProd, prod_one_add]

Goal state after:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ Tendsto (fun s ↦ ∑ t ∈ s.powerset, ∏ i ∈ t, f i) (SummationFilter.unconditional ι).filter (nhds a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
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:
rcases isEmpty_or_nonempty ι with _ | _
  · simp
  obtain ⟨x, hx⟩ := hprod
  obtain ⟨a, ha⟩ := hsum
  convert! hx.tprod_eq
  unfold HasProd at hx
  conv at hx in fun _ ↦ _ => ext _; rw [prod_one_add_ordered] -- simp_rw would cause loop
  rw [ha.tsum_eq]
  refine (tendsto_nhds_unique (hx.comp tendsto_finset_Iic_atTop_atTop) ?_).symm
  apply Tendsto.const_add
  convert! ha.comp tendsto_finset_Iic_atTop_atTop using 2 with s
  refine sum_congr rfl (fun i hi ↦ ?_)
  congr
  grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.ediam (⇑h.symm '' s) = Metric.ediam s

Tactic:
ediam_image

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.ediam s = Metric.ediam s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (0 - ε) (0 + ε)

Tactic:
simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]
    exact nhds_bot_basis_Iic

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ Tendsto (fun n ↦ f n) l (𝓝 a)

Tactic:
ENNReal.tendsto_nhds ha

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (pkg.extend f)

Tactic:
extend_def _ h.uniformContinuous

Goal state after:
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (⋯.extend f)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x ↦ m x / b) f (𝓝 (a / b))

Tactic:
apply Tendsto.mul_const hm

Goal state after:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ a ≠ 0 ∨ b⁻¹ ≠ ∞
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hB : (𝓤 X).HasAntitoneBasis V
hV_symm : ∀ (n : ℕ), (V n).IsSymm
φ : ℕ → ℕ
hφ_comp : ∀ ⦃m n : ℕ⦄, m < n → (fun x ↦ V (φ n) ○ x)^[2] (V (φ n)) ⊆ V (φ m)
hφB : (𝓤 X).HasAntitoneBasis (V ∘ φ)
⊢ ∃ U, (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

Tactic:
exact ⟨V ∘ φ, fun n => hV_symm _, hφ_comp, hφB⟩

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

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

Tactic:
intro x y x_le_y
  simp only [truncateToReal]
  gcongr
  exact ne_top_of_le_ne_top t_ne_top (min_le_left _ _)

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

Goal state before:
pp: α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x ↦ f x i) g s

Tactic:
have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
    exact this.extend_real

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊔ c - c ⊔ d| ≤ |b - d|

Tactic:
sup_comm c

Goal state after:
case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|
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
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformly (F • G) (f • g) l

Tactic:
rw [← tendstoLocallyUniformlyOn_univ] at *

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
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformlyOn (F • G) (f • g) l univ
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖

Tactic:
by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
cases hj
    simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
    exact uniqueElim_default (α := fun j : ({i} : Finset ι) => π j) y

Goal state after:
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ p ∈ (fun x ↦ s • x) '' closedBall x ε ↔ p ∈ closedBall (s • x) (‖s‖ * ε)

Tactic:
simp_rw [Set.mem_image, mem_closedBall]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p) ↔ dist p (s • x) ≤ ‖s‖ * ε
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ TendstoLocallyUniformly F⁻¹ f⁻¹ l

Tactic:
rw [← tendstoLocallyUniformlyOn_univ] at *

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l Set.univ
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l Set.univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ b ∈ s, f b)

Tactic:
rw [biUnion_eq_iUnion]
  have := hs.to_subtype
  exact MeasurableSet.iUnion (by simpa using h)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋂ b, f b)ᶜ

Tactic:
compl_iInter

Goal state after:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ i, (f i)ᶜ)
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ μ (⋃₀ range s) = 0 ↔ ∀ (i : ι), μ (s i) = 0

Tactic:
measure_sUnion_null_iff (countable_range s),

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ (∀ s_1 ∈ range s, μ s_1 = 0) ↔ ∀ (i : ι), μ (s i) = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

Tactic:
simp +contextual [measurableAtom]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : Nontrivial α
inst✝ : DecidableLT α
n : ℤ
⊢ sign ↑n = sign n

Tactic:
simp only [sign_apply, Int.cast_pos, Int.cast_lt_zero]

Goal state after: