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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ¬Ideal.span {a} = 0

Tactic:
Ideal.zero_eq_bot,

Goal state after:
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ¬Ideal.span {a} = ⊥
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ ¬Ideal.span {a'} = 0

Tactic:
Ideal.zero_eq_bot,

Goal state after:
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ ¬Ideal.span {a'} = ⊥
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(ENNReal.ofReal x.toReal) = x

Tactic:
simp only [coe_ennreal_ofReal, hx, toReal_nonneg, max_eq_left]

Goal state after:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑x.toReal = x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
· rw [← coe_ne_zero] at hb
    rw [← ENNReal.mul_le_mul_iff_left hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a * (2⁻¹ + 2⁻¹) = a

Tactic:
inv_two_add_inv_two,

Goal state after:
a : ℝ≥0∞
⊢ a * 1 = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
hc : c ≠ 0 ∨ d ≠ ∞
hd : c ≠ ∞ ∨ d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
by
  simp only [div_eq_mul_inv, ENNReal.mul_inv hc hd]
  ring

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ Bornology.IsBounded univ ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C

Tactic:
Metric.isBounded_iff_nndist

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ univ → ∀ ⦃y : α⦄, y ∈ univ → nndist x y ≤ C) ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]

Goal state after:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ 0 < J * ∏ x ∈ s \ {p}, x.asIdeal

Tactic:
Ideal.zero_eq_bot,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ ⊥ < J * ∏ x ∈ s \ {p}, x.asIdeal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ J ∣ Ideal.span {∑ p ∈ s, a p}

Tactic:
rw [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ ∑ p ∈ s, a p ∈ J
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ x✝ ∈ sphere x r ↔ x✝ ∈ {x - r, x + r}

Tactic:
simp [dist_eq]

Goal state after:
x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ |x✝ - x| = r ↔ x✝ = x - r ∨ x✝ = x + r
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
e : β → α
a : α
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range e) ↔ ∀ ε > 0, ∃ k, dist a (e k) < ε

Tactic:
by
  simp only [mem_closure_iff, exists_range_iff]

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure[inst✝³] (Ioi a)

Tactic:
rw [← sdiff_subset_closure_iff, Ici_sdiff_Ioi_same, singleton_subset_iff]
    exact isGLB_Ioi.mem_closure h

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
simp [hd, dist_comm]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
simp [hd, dist_comm]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LinearOrder α
inst✝⁴ : OrderTopology α
β : Type u_3
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
have hux (n : ℕ) : u n ∈ Iio x := (huxf n).1

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LinearOrder α
inst✝⁴ : OrderTopology α
β : Type u_3
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case inl.inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ (n : ℕ), ∀ᶠ (x : γ) in l, f x < u n
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
rw [← eventually_countable_forall] at h

Goal state after:
case inl.inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ ∃ x, IsLeast s x

Tactic:
suffices (s ∩ ⋂ x ∈ s, Iic x).Nonempty from
    ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x ∈ s, Iic x).Nonempty
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ = ‖b / a‖ₑ

Tactic:
rw [← enorm_inv', inv_div]

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 ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty

Tactic:
rw [union_comm s t] at hab

Goal state after:
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
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:

Tactic:
b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr

Goal state after:
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 '' Icc a b = Icc (f a) (f b)

Tactic:
rcases le_or_gt a b with hab | hab
  · exact hf_c.continuousOn.image_Icc_of_monotoneOn hab (hf.monotone.monotoneOn _)
  · simp [not_le.mpr hab, not_le.mpr (hf hab)]

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

Goal state before:
pp: case inr
α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
x : α
⊢ IsCompact s

Tactic:
rcases hb.subset_closedBall x with ⟨r, hr⟩

Goal state after:
case inr
α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s
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 atBot
⊢ Tendsto (fun x ↦ f x • r) l atBot

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢

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 (fun x ↦ -f x) l atTop
⊢ Tendsto (fun x ↦ -f x • r) l atTop
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
h : ediam s ≠ ∞
hx : x ∈ s
hy : y ∈ s
⊢ dist x y ≤ (ediam s).toReal

Tactic:
dist_edist

Goal state after:
α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
h : ediam s ≠ ∞
hx : x ∈ s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (ediam s).toReal
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
⊢ {a} ⊆ ↑H

Tactic:
simp [a_in]

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

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ ∑ a ∈ Finset.cons a s ha, ⨆ i, f a i = ⨆ i, ∑ a ∈ Finset.cons a s ha, f a i

Tactic:
Finset.sum_cons,

Goal state after:
case cons
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ (⨆ i, f a i) + ∑ a ∈ s, ⨆ i, f a i = ⨆ i, f a i + ∑ a ∈ s, f a i
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 (fst '' s) (a, b).1 ∧ IsLUB (snd '' s) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))

Tactic:
← range_domRestrict,

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 (snd '' s) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))
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]
    exact neg_nonneg.2 h

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

Goal state before:
pp: x : EReal
h : x < 0
⊢ ⊤ * x = ⊥

Tactic:
by
  rw [EReal.mul_comm]
  exact mul_top_of_neg h

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

Goal state before:
pp: case refine_1
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ L.filter

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

Goal state after:
case refine_1
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b ∈ s
⊢ s ∈ L.filter
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd f a

Tactic:
simpa using hasProd_subtype_comap_iff_of_mulSupport_subset hf (L := unconditional _)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
b : β
hb : b > s.sup' hs fun i ↦ limsup (F i) f
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i ↦ F i a) < b

Tactic:
simp only [gt_iff_lt, sup'_lt_iff, eventually_all_finset] at hb ⊢

Goal state after:
case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
b : β
hb : ∀ i ∈ s, limsup (F i) f < b
⊢ ∀ i ∈ s, ∀ᶠ (x : α) in f, F i x < b
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
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

Tactic:
simp only [this]

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₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ (CauchySeq fun s ↦ ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
cauchySeq_finset_iff_prod_vanishing

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ (∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

pp: case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
· have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by
      ext1 i
      rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
    have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds
    simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat

Goal state after:
case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i = ∏ i ∈ t, g i

Tactic:
by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

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

Goal state before:
pp: case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
x✝ : A
| ∑ kl ∈ antidiagonal x✝, f kl.1 * g kl.2

pp: case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A

Tactic:
← Finset.sum_finset_coe,

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
x✝ : A
| ∑ i, f (↑i).1 * g (↑i).2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
x✝ : A
| ∑ kl ∈ antidiagonal x✝, f kl.1 * g kl.2

pp: case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| SummationFilter.unconditional A

Tactic:
← Finset.sum_finset_coe,

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
x✝ : A
| ∑ i, f (↑i).1 * g (↑i).2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| SummationFilter.unconditional A
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)

Tactic:
simp only [AntilipschitzWith, edist_nndist]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)