mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q✝ p q : NonarchAddGroupSeminorm E
⊢ q 0 ≤ 0

Tactic:
map_zero q

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q✝ p q : NonarchAddGroupSeminorm E
⊢ 0 ≤ 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g

Tactic:
by simp_rw [iInf_add, add_iInf]

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

Goal state before:
pp: x y z : ℝ≥0∞
h : y + z < x
⊢ ∃ y' > y, ∃ z' > z, y' + z' < x

Tactic:
contrapose! h
  simpa using le_iInf₂_add_iInf₂ h

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

Goal state before:
pp: case mp
⊢ ∀ (y : ℝ), ⊥ < ↑y

Tactic:
exact bot_lt_coe

Goal state after:
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
h1 : 1 = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑1
⊢ count K v 1 = 0

Tactic:
rw [count_well_defined K v one_ne_zero h1, Ideal.span_singleton_one, Ideal.one_eq_top, sub_self]

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

Goal state before:
pp: x : ℝ≥0∞
⊢ ↑x = 1 ↔ ↑x = ↑1

Tactic:
coe_ennreal_one

Goal state after:
x : ℝ≥0∞
⊢ ↑x = 1 ↔ ↑x = 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0 ∨ ∞ ≠ ∞
hb : a ≠ ∞ ∨ ∞ ≠ 0
⊢ (a * ∞)⁻¹ = a⁻¹ * ∞⁻¹

Tactic:
case =>

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

Goal state before:
pp: x✝ : ℝ≥0
ha : ∞ ≠ 0 ∨ ↑x✝ ≠ ∞
hb : ∞ ≠ ∞ ∨ ↑x✝ ≠ 0
⊢ (∞ * ↑x✝)⁻¹ = ∞⁻¹ * (↑x✝)⁻¹

Tactic:
case =>

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b * c
⊢ a < b / c⁻¹

Tactic:
by rwa [div_eq_mul_inv, inv_inv]

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

Goal state before:
pp: a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ r * a ≤ r * r⁻¹ * b

Tactic:
ENNReal.mul_inv_cancel hr₀ hr₁,

Goal state after:
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ r * a ≤ 1 * b
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' closedEBall a r = closedEBall (↑a) r ∩ {a | p a}

Tactic:
← preimage_closedEBall,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' val ⁻¹' closedEBall (↑a) r = closedEBall (↑a) r ∩ {a | p a}
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds]

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case pos
α : 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 : BddAbove s
⊢ sSup (a • s) = a • sSup s

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 : ¬BddAbove s
⊢ sSup (a • s) = a • sSup s

Tactic:
· exact ((OrderIso.smulRight ha').map_csSup' hs h).symm

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 : ¬BddAbove s
⊢ sSup (a • s) = a • sSup s
Module: Mathlib.Topology.Order.DenselyOrdered

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

Tactic:
by
  apply Subset.antisymm
  · exact closure_minimal Ioi_subset_Ici_self isClosed_Ici
  · rw [← sdiff_subset_closure_iff, Ici_sdiff_Ioi_same, singleton_subset_iff]
    exact isGLB_Ioi.mem_closure h

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
this : Ioo a b = Icc a b
⊢ False

Tactic:
grind => have : b ∈ Ioo a b; finish

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t

Tactic:
by
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
  refine ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩
  · exact sdiff_subset.trans hts
  · exact htc.mono sdiff_subset
  · exact htd.sdiff_finite ((subsingleton_isBot α).finite.union (subsingleton_isTop α).finite)
  · simp [hx]
  · simp [hx]

Goal state after:
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
    [inst_3 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K},
    a ≤ c → a ≠ 0 → b ≠ 0 → b = 1 → ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
⊢ b⁻¹ * a ≠ 0

Tactic:
simp [ha, hb]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
G : ι → Type u_4
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x y : E × F
⊢ dist x y = ‖x⁻¹ * y‖

Tactic:
simp [Prod.norm_def, Prod.dist_eq, dist_eq_norm_inv_mul]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : PreconnectedSpace α
x y : α
hxy : x < y
this : (Iio y ∩ Ioi x).Nonempty
⊢ ∃ a, x < a ∧ a < y

Tactic:
grind [Set.inter_nonempty_iff_exists_left]

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

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

Tactic:
← dist_one,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ dist 1 (a / b) = dist 1 (b / a)
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (univ.pi fun b ↦ closedBall (x b) r)

Tactic:
exact isCompact_univ_pi fun _ => isCompact_closedBall _ _

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u⁻¹ * v‖ + ‖v‖

Tactic:
← norm_inv' v,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖
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
⊢ Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.comap (↑I').subtype (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I).range) =
    ⊤

Tactic:
LinearMap.range_domRestrict,

Goal state after:
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
⊢ Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.comap (↑I').subtype (Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I)) =
    ⊤
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ a = 1 ∨ 0 < ‖a‖

Tactic:
by
  simpa [eq_comm] using (norm_nonneg' a).eq_or_lt

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

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

Tactic:
case =>

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (f '' ?m.75 ∪ f '' ?m.75ᶜ)

pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Set β

Tactic:
refine (hsf.image f).isBounded.union (isBounded_image_iff.2 ⟨1, fun x hx y hy ↦ ?_⟩)

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
x : β
hx : x ∈ sᶜ
y : β
hy : y ∈ sᶜ
⊢ dist (f x) (f y) ≤ 1
Module: Mathlib.Analysis.Normed.Group.Int

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

Tactic:
rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa [Int.norm_natCast] using norm_pow_le_mul_norm

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

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞
⊢ ∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i

Tactic:
by
  simp only [div_eq_mul_inv, prod_inv_distrib hg, ← Finset.prod_mul_distrib]

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

Goal state before:
pp: x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x + y).toReal = x.toReal + y.toReal

Tactic:
by
  lift x to ℝ using ⟨hx, h'x⟩
  lift y to ℝ using ⟨hy, h'y⟩
  rfl

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ ∅, u k)

Tactic:
case =>

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : ∀ k ∈ Finset.cons k₀ s k₀_notin_s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Tactic:
case =>

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : IsLUB s f
⊢ Tendsto Subtype.val atTop (𝓝 f)

Tactic:
simp only [isLUB_pi, ← range_domRestrict] at h

Goal state after:
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : ∀ (a : ι), IsLUB (range (s.domRestrict (eval a))) (f a)
⊢ Tendsto Subtype.val atTop (𝓝 f)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
⊢ 0 ≤ -a ↔ a ≤ 0

Tactic:
EReal.le_neg,

Goal state after:
a : EReal
⊢ a ≤ -0 ↔ a ≤ 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x ↦ False) = ⊤

Tactic:
by
  simp [bliminf_eq]

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
y : EReal
H₁ : 0 ≤ y
hy : ↑y.toENNReal = y
⊢ recENNReal coe neg_coe y ≍ coe y.toENNReal

Tactic:
simp [recENNReal, H₁]

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

Goal state before:
pp: x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x - y).toReal = x.toReal - y.toReal

Tactic:
by
  lift x to ℝ using ⟨hx, h'x⟩
  lift y to ℝ using ⟨hy, h'y⟩
  rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : Preorder β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : BoundedLENhdsClass α
inst✝⁴ : BoundedLENhdsClass β
f✝ : Filter ι
u : ι → α
a : α
inst✝³ : Finite ι
inst✝² : (i : ι) → Preorder (π i)
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), BoundedLENhdsClass (π i)
x f : (i : ι) → π i
hf : ∀ (i : ι), ∀ᶠ (x : π i) in 𝓝 (x i), (fun x1 x2 ↦ x1 ≤ x2) x (f i)
⊢ IsBounded (fun x1 x2 ↦ x1 ≤ x2) (pi fun i ↦ 𝓝 (x i))

Tactic:
exact ⟨f, eventually_pi hf⟩

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

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

Tactic:
EReal.le_neg,

Goal state after:
a b : EReal
⊢ 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Data.EReal.Operations

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

Tactic:
EReal.le_neg,

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

Goal state before:
pp: case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Tendsto (fun x ↦ Finset.range (x + 1)) atTop (Filter.map Finset.range atTop)

Tactic:
simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage]

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ ∀ (s : Set (Finset ℕ)),
    (∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s) → ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Tendsto Finset.range atTop (Filter.map (fun x ↦ Finset.range (x + 1)) atTop)

Tactic:
simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage]

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ ∀ (s : Set (Finset ℕ)),
    (∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s) → ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
Module: Mathlib.Data.EReal.Operations

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

Tactic:
rename_i a
    rcases lt_trichotomy a 0 with (ha | ha | ha)
    · simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]
    · simp [ha]
    · simp_all [top_mul_of_pos (EReal.coe_pos.mpr ha)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ map (Embedding.subtype fun x ↦ x ∈ ↑s) L.support.toFinset, f b) L

Tactic:
by
  simpa [prod_attach] using hasProd_fintype_support (f ∘ Subtype.val) L

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
⊢ ∀ᶠ (a : α) in f, max (u a) (v a) < b

Tactic:
have hu := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_left _ _) hb) h₃

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
⊢ ∀ᶠ (a : α) in f, max (u a) (v a) < b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
a✝ : ℕ
hx : Int.ofNat a✝ ∈ u
⊢ a✝ ∈ u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯

Tactic:
by simpa using Or.inl hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (𝓝 (f x)) ≤ 𝓝 x

Tactic:
simp only [nhds_eq_comap_uniformity]
  grw [← hf.comap_uniformity_le]
  simp [comap_comap, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
b : E
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (fun e ↦ ‖(f e)⁻¹ * b‖ₑ) a (𝓝 0)

Tactic:
simp only [← edist_eq_enorm_inv_mul, ← tendsto_iff_edist_tendsto_0]

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:
rw [uniformContinuous_dom₂]
    exact uniformContinuous_mk.comp uniformContinuous_div

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

Goal state before:
pp: case refine_2
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ ∀ (n : ℕ), v n ∈ s

Tactic:
rintro ⟨⟩

Goal state after:
case refine_2.zero
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ v 0 ∈ s

case refine_2.succ
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n✝ : ℕ
⊢ v (n✝ + 1) ∈ s
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_2
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
⊢ d (x :: l)[M] (l ++ [y])[M] ≤ L.sum

pp: case refine_3
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
⊢ d (l ++ [y])[M] y ≤ L.sum

Tactic:
· exact single_le_sum (fun x _ => zero_le) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, getElem_zipWith⟩)

Goal state after:
case refine_3
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
⊢ d (l ++ [y])[M] y ≤ L.sum