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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ NontrivialTopology E ↔ ∃ x, ‖x‖₊ ≠ 0

Tactic:
simp_rw [TopologicalSpace.nontrivial_iff_exists_not_inseparable, Metric.inseparable_iff_nndist,
    nndist_eq_nnnorm_inv_mul]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ (∃ x y, ¬‖x⁻¹ * y‖₊ = 0) ↔ ∃ x, ‖x‖₊ ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (algebraMap S R) p) =
    ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

Tactic:
finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset),

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ ∏ i ∈ {v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset, i.maxPowDividing (map (algebraMap S R) p) =
    ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

case h
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ (mulSupport fun v ↦ v.maxPowDividing (map (algebraMap S R) p)) ⊆ ↑{v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)

Tactic:
← comap_dist_right_atTop c,

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto f l (comap (fun x ↦ dist x c) atTop)
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1

Tactic:
by
    { rw [mul_one]
      exact le_max_left _ _ }

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

Goal state before:
pp: α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C x : α
⊢ x ∈ {x | |x| < C} ↔ x ∈ Ioo (-C) C

Tactic:
simp [abs_lt]

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: x : ℤ
r : ℝ
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_eq_Icc]
    exact (Set.finite_Icc _ _).isCompact

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: case inl
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Subsingleton G
⊢ Dense ↑S

pp: case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
⊢ Dense ↑S

Tactic:
· refine fun x => _root_.subset_closure ?_
    rw [Subsingleton.elim x 1]
    exact one_mem S

Goal state after:
case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
⊢ Dense ↑S
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: case some.none
α : Type u
β : Type v
γ : Type w
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, none)

Tactic:
exact tendsto_nhds_top_mono' continuousAt_snd fun p => le_add_left le_rfl

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_eq_Icc]
    exact (Set.finite_Icc _ _).isCompact

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

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

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih => ?_
  simp only [Finset.prod_cons, ← ih (hf.mono <| by simp)]
  refine ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
    (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)
  · exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀
  · exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀

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)
x : EReal
hx : ¬0 ≤ x
H₁ : 0 < -x
H₂ : x = -↑(-x).toENNReal
⊢ 0 < (-x).toENNReal

Tactic:
positivity

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

Goal state before:
pp: case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]

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

Goal state before:
pp: case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
rw [toENNReal_of_ne_top (ne_of_beq_false rfl).symm, ← coe_sub, toReal_coe,
      ofReal_sub x (EReal.coe_nonneg.mp hy)]
    simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Tendsto Finset.Iic atTop atTop

Tactic:
by
  rcases isEmpty_or_nonempty α with _ | _
  · exact tendsto_of_isEmpty
  by_cases h : IsDirectedOrder α
  · refine tendsto_atTop_atTop.mpr fun s ↦ ?_
    obtain ⟨a, ha⟩ := Finset.exists_le s
    exact ⟨a, fun b hb c hc ↦ by simpa using (ha c hc).trans hb⟩
  · obtain h := Filter.atTop_neBot_iff.not.mpr (fun h' ↦ h h'.2)
    simp [not_ne_iff.mp <| Filter.neBot_iff.not.mp h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ n ∈ {n | b'' < u n r}

Tactic:
simp [hn]

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

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

Tactic:
rw [← Tendsto]

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Tendsto (fun x ↦ Finset.range (x + 1)) atTop (Filter.map Finset.range atTop)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

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

Tactic:
rw [← Tendsto]

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Tendsto Finset.range atTop (Filter.map (fun x ↦ Finset.range (x + 1)) atTop)
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
⊢ extend e f 1 c ≤ g c

Tactic:
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)

Goal state after:
case inl
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ extend e f 1 (e i) ≤ g (e i)

case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ extend e f 1 c ≤ g c
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : HasProd f a L
n : ℕ
⊢ HasProd (fun x ↦ f x ^ n) (a ^ n) L

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn => simpa [pow_succ] using hn.mul hf

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

Goal state before:
pp: case refine_2
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hf : ∀ (i : ι), 1 ≤ 1 i
⊢ HasProd 1 1 L

Tactic:
exact hasProd_one

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

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℕ → G
⊢ Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
by
  rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tprod_vanishing]

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
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'
A : u ⊆ u1 ∪ u2
⊢ (∏ x ∈ u1 ∪ u2, f x * if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x

Tactic:
rw [prod_mul_distrib]

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'
A : u ⊆ u1 ∪ u2
⊢ ((∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x
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:
by
  simp_rw [HasProd, prod_one_add]
  exact h.comp tendsto_finset_powerset_atTop_atTop

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

Goal state before:
pp: case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
simp [hn]

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

Goal state before:
pp: case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
simp [hn]

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

Goal state before:
pp: case inl
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : IsEmpty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
simp [hn]

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

Goal state before:
pp: case inl
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

pp: case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
· obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top hf
    obtain ⟨q, hq⟩ := exists_rat_gt R
    refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩
    · refine fun hcon => hR ?_
      filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
    · simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
      refine fun hcon => hbdd ↑(q + 1) ?_
      filter_upwards [hcon] with x hx using not_lt.1 hx

Goal state after:
case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : NormedGroup E
⊢ comap norm (𝓝[>] 0) = 𝓝[≠] 1

Tactic:
by
  simp [nhdsWithin, comap_norm_nhds_one, Set.preimage, Set.compl_def]

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

Goal state before:
pp: case inr.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, ↑q < x i

Tactic:
· refine fun hcon => hR ?_
      filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a

Tactic:
simp [projIcc, Subtype.ext_iff, h.not_ge]

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

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

Tactic:
apply continuousOn_toReal.comp_continuous (by fun_prop)

Goal state after:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ ∀ (x : ℝ≥0∞), min t x ∈ {a | a ≠ ∞}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
i : ι
⊢ b ≤ (f + g) i → g i ≤ min (b - a) 1 → a ≤ f i

Tactic:
hfg

Goal state after:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
i : ι
hfg : b ≤ (f + g) i
⊢ g i ≤ min (b - a) 1 → a ≤ f i
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
⊢ limsup (f + g) u = limsup g u

Tactic:
rw [add_comm, limsup_add_of_right_tendsto_zero hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
⊢ ε / (2 * C) > 0

Tactic:
positivity

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

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

Tactic:
hfg

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : Type u_4
β : ι → Type u_5
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : Zero α
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul α (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul α (β i)
x : α
y₁ y₂ : (i : ι) → β i
⊢ 0 ≤ dist x 0 * dist y₁ y₂

Tactic:
positivity

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : Type u_4
β : ι → Type u_5
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : Zero α
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul α (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul α (β i)
x₁ x₂ : α
y : (i : ι) → β i
⊢ 0 ≤ dist x₁ x₂ * dist y 0

Tactic:
positivity

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : (i : ι) → PseudoMetricSpace (α i)
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul (α i) (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul (α i) (β i)
x : (i : ι) → α i
y₁ y₂ : (i : ι) → β i
⊢ 0 ≤ dist x 0 * dist y₁ y₂

Tactic:
positivity

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : (i : ι) → PseudoMetricSpace (α i)
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul (α i) (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul (α i) (β i)
x₁ x₂ : (i : ι) → α i
y : (i : ι) → β i
⊢ 0 ≤ dist x₁ x₂ * dist y 0

Tactic:
positivity

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ dist (f x) (f 1) = ‖x‖

Tactic:
hi.dist_eq,

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ dist x 1 = ‖x‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
⊢ (↑K + 1)⁻¹ > 0

Tactic:
positivity

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

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
⊢ 0 ≤ c⁻¹

Tactic:
positivity

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R₀ : ℝ
hR₀ : ∀ x ∈ s, ‖x‖ ≤ R₀
⊢ max R₀ 1 > 0

Tactic:
positivity

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R : ℝ
hR₀ : R > 0
hR : ∀ x ∈ s, ‖x‖ ≤ R
⊢ R + 1 > 0

Tactic:
positivity

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁵ : PseudoEMetricSpace α✝
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : FunLike F α✝ β
inst✝¹ : DilationClass F α✝ β
f : F
α : Type ?u.22
inst✝ : PseudoEMetricSpace α
x y : α
⊢ edist (id x) (id y) = ↑1 * edist x y

Tactic:
by simp only [id, ENNReal.coe_one, one_mul]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
⊢ 0 < S + 1

Tactic:
positivity

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖) ≤ max ‖x.1‖ ‖x.2‖ * max ‖y.2‖ ‖y.1‖

Tactic:
by
        apply max_mul_mul_le_max_mul_max <;> simp [norm_nonneg]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i j✝ : ι
l : List ι
inst✝ : DecidableEq ι
is : List ι
j : ι
v : TProd α (j :: is)
hj : j ∈ j :: is
⊢ α j

Tactic:
exact v.1

Goal state after: