mathlib-initiative/mathlib-tactics huggingface dataset:
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 : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ toUniformSpace = toUniformSpace

Tactic:
by
  dsimp +instances [replaceEDist]

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

Goal state before:
pp: r : ℝ
⊢ ENNReal.ofReal r ≤ ‖r‖ₑ

Tactic:
enorm_eq_ofReal_abs

Goal state after:
r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
⊢ ENNReal.ofReal r ≤ ‖r‖ₑ

Tactic:
rw [enorm_eq_ofReal_abs]

Goal state after:
r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
⊢ cocompact α ≤ atBot ⊔ atTop

Tactic:
refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro

Goal state after:
case refine_1
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : IsEmpty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s
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 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
⊢ Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I

Tactic:
ext x

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 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
x : K
⊢ x ∈ Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I ↔ x ∈ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst✝²] (s ∩ Icc y b)
⊢ y ∈ s

Tactic:
exact IsClosed.mem_of_ge_of_forall_exists_lt this hb hy.2 fun x hx ↦
    hgt x ⟨hx.1, Ioc_subset_Ioc_left hy.1 hx.2⟩ y hx.2.1

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

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := ⋯
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := ⋯
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
this : closure[inst✝³] A ⊆ s ∩ Icc a b
⊢ t₁ ∈ closure[inst✝³] A

Tactic:
exact csSup_mem_closure ⟨a, a_mem⟩ bdd_A

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ ball 1 r} = ball a r

Tactic:
ext x

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ ball 1 r} ↔ x ∈ ball a r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ closedBall 1 r} = closedBall a r

Tactic:
ext x

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ closedBall 1 r} ↔ x ∈ closedBall a r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ sphere 1 r} = sphere a r

Tactic:
ext x

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ sphere 1 r} ↔ x ∈ sphere a r
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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

Tactic:
· intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv

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

Goal state before:
pp: x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Tactic:
by
  rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
by
  have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs
  refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
  · filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)
  · rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
    have : a < c := not_le.1 fun h => hac.not_ge <| h_mono hcs has h
    filter_upwards [hs, Ico_mem_nhdsGE this]
    rintro x hx ⟨_, hxc⟩
    exact (h_mono hx hcs hxc.le).trans_lt hcb

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

Goal state before:
pp: ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Tactic:
by
  induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

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

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

Tactic:
contrapose! Hle
  apply ENNReal.sum_lt_sum_of_nonempty hs Hle

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
⊢ ∀ (a : β), (∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a

Tactic:
intro c hc

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ b ≤ c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
⊢ ∀ (a : β), (∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a

Tactic:
intro c hc

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ b ≤ c
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} = ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
x : α
⊢ x ∈ {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} ↔ x ∈ ⋃ j, ⋂ i, Iic (f ↑i)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ a

Tactic:
refine liminf_le_of_le hu_le fun b hb ↦ ?_
  obtain ⟨n, hna, hbn⟩ := (hu.and_eventually hb).exists
  exact hbn.trans hna

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -↑(a✝¹ + a✝) = -↑a✝¹ - ↑a✝

Tactic:
← coe_neg,

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ ↑(-(a✝¹ + a✝)) = -↑a✝¹ - ↑a✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ ↑(-(a✝¹ + a✝)) = -↑a✝¹ - ↑a✝

Tactic:
← coe_neg,

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ ↑(-(a✝¹ + a✝)) = ↑(-a✝¹) - ↑a✝
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 : α
⊢ BoundedLENhdsClass (α × β)

Tactic:
refine ⟨fun x ↦ ?_⟩

Goal state after:
ι : 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 : α
x : α × β
⊢ IsBounded (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x)
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)
⊢ BoundedLENhdsClass ((i : ι) → π i)

Tactic:
refine ⟨fun x ↦ ?_⟩

Goal state after:
ι : 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 : (i : ι) → π i
⊢ IsBounded (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} = {x | {n | p n ∧ x ∈ s n}.Infinite}

Tactic:
ext x

Goal state after:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} ↔ x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
h : a ≤ b + c
⊢ a - c ≤ b

Tactic:
induction c with
  | bot => rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]
  | coe c => exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h
  | top => simp only [sub_top, bot_le]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}

Tactic:
rw [← compl_inj_iff]
  simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup,
    cofinite.blimsup_set_eq]
  rfl

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

Goal state before:
pp: case inr.refine_2
ι : 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'
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ i, u i b_1 < b

Tactic:
obtain ⟨r, hr⟩ : ∃ r, ∀ s ≥ r, limsup (u · s) cofinite ≤ b' := by simpa using! this

Goal state after:
case inr.refine_2
ι : 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_1 : α) in atTop, ⨆ i, u i b_1 < b
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
by_cases h : L.filter = ⊥
  · exact .inr h
  · exact .inl ⟨⟨h⟩⟩

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ L.support = univ ↔ L.filter ≤ atTop

Tactic:
simp only [support, Set.eq_univ_iff_forall, Set.mem_ofPred]

Goal state after:
β : Type u_2
L : SummationFilter β
⊢ (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)

Tactic:
rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]

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

Goal state before:
pp: case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊤ = ⊥

Tactic:
← coe_neg,

Goal state after:
case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ ↑(-x✝) * ⊤ = ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = ⊤

Tactic:
← coe_neg,

Goal state after:
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ ↑(-x✝) * ⊥ = ⊤
Module: Mathlib.Topology.Order.LiminfLimsup

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

Tactic:
intro c hc

Goal state after:
case a
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < liminf f F
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: n : ℕ
⊢ Finset.Iic n = Finset.range (n + 1)

Tactic:
ext x

Goal state after:
n x : ℕ
⊢ x ∈ Finset.Iic n ↔ x ∈ Finset.range (n + 1)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ (n + 1) • x = ↑(n + 1) * x

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ]
    convert! (EReal.right_distrib_of_nonneg _ _).symm <;> simp

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

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

Tactic:
← Set.mulIndicator_range_comp,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
⊢ HasProd ((Set.range Subtype.val).mulIndicator f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
g : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏'[L] (x : ι), 1 < ∏'[L] (i : ι), g i

Tactic:
exact multipliable_one.tprod_lt_tprod hg hi hsum

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

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

Tactic:
by rw [h]

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

Goal state before:
pp: case codisjoint
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
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
rw [codisjoint_iff_le_sup]

Goal state after:
case codisjoint
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.Basic

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

Tactic:
tprod_congr

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∏' (b : ↑s), ?m.37 b = ∏' (x : ↑s), s.mulIndicator f ↑x

α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : ↑s), f ↑b = ?m.37 b

α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ↑s → α
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x

Tactic:
by
  have : mulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _
  simp_rw [← hg.tprod_eq this, hg.extend_apply]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
⊢ f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}

Tactic:
by
  simp [hf.dist_eq]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
⊢ IsSeqCompact (f '' K)

Tactic:
intro ys ys_in_fK

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
ys_in_fK : ∀ (n : ℕ), ys n ∈ f '' K
⊢ ∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
⊢ IccExtend h (f ∘ Subtype.val) = f

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
⊢ IccExtend h (f ∘ Subtype.val) x = f x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_1
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s

pp: case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ ediam s

Tactic:
· exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)

Goal state after:
case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ ediam s
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: case singleton
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a✝ : ι
hs : ∀ i ∈ {a✝}, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ({a✝}.sup' ⋯ f) l (𝓝 ({a✝}.sup' ⋯ g))

Tactic:
simpa using hs

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

Goal state before:
pp: case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Tactic:
exact finset_sup'_nhds hne hs

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x✝¹ x✝ : ℝ
h₀ : 0 ≤ x✝¹
hr : x✝¹ < x✝
x : ℝ
h : x✝¹ < x ∧ x < x✝
⊢ x✝¹ < |x| ∧ |x| < x✝

Tactic:
abs_of_nonneg (h₀.trans h.1.le)

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x✝¹ x✝ : ℝ
h₀ : 0 ≤ x✝¹
hr : x✝¹ < x✝
x : ℝ
h : x✝¹ < x ∧ x < x✝
⊢ x✝¹ < x ∧ x < x✝
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ v (y + -x) = v (x + -y)

Tactic:
← sub_eq_add_neg,

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ v (y - x) = v (x + -y)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : v (y + -x) = 0
⊢ x = y

Tactic:
← sub_eq_add_neg,

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : v (y - x) = 0
⊢ x = y
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist (s⁻¹ • p) x < ε

Tactic:
refine lt_of_mul_lt_mul_of_nonneg_left ?_ (norm_nonneg s)

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ ‖s‖ * dist (s⁻¹ • p) x < ‖s‖ * ε