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

Goal state before:
pp: case e'_2
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ exps v =
    { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.prod fun x1 x2 ↦ ↑x1.asIdeal ^ x2

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset (s := h_exps.toFinset), Finsupp.prod]

Goal state after:
case e'_2
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ i ∈ Finite.toFinset h_exps, ↑i.asIdeal ^ exps i =
    ∏ a ∈ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.support,
      ↑a.asIdeal ^ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ } a

case e'_2.h
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s

pp: case inr.inr
α : 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
⊢ sInf (a • s) = a • sInf s

Tactic:
· rw [zero_smul_set hs, zero_smul]
    exact csInf_singleton 0

Goal state after:
case inr.inr
α : 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
⊢ sInf (a • s) = a • sInf s
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sSup s

pp: case inr.inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
⊢ sInf (a • s) = a • sSup s

Tactic:
· rw [zero_smul_set hs, zero_smul]
    exact csInf_singleton 0

Goal state after:
case inr.inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
⊢ sInf (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 α
inst✝ : DiscreteTopology α
a b : α
⊢ b ≤ a

Tactic:
by_contra! contra

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ False
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
by_cases hki : k = i

Goal state after:
case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (nhds a).IsCountablyGenerated

Tactic:
by rw [nhds_discrete]; exact isCountablyGenerated_pure

Goal state after:
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
⊢ ∃ x, IsLeast s x

Tactic:
have : Nonempty s := ne_s.to_subtype
  suffices (s ∩ ⋂ x ∈ s, Iic x).Nonempty from
    ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩
  rw [biInter_eq_iInter]
  by_contra H
  rw [not_nonempty_iff_eq_empty] at H
  rcases hs.elim_directed_family_closed (fun x : s => Iic ↑x) (fun x => isClosed_Iic) H
      (Monotone.directed_ge fun _ _ h => Iic_subset_Iic.mpr h) with ⟨x, hx⟩
  exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
rw [h.image_Icc (hc.1.trans hc.2)] at this

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
rw [h.image_Icc (hc.1.trans hc.2)] at this

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
this : closedBall x 1 ∈ f
y : α
hy : f ≤ nhds y
⊢ ∃ x, f ≤ nhds x

Tactic:
exact ⟨y, hy⟩

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

Goal state before:
pp: case neg
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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
hx : x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'
⊢ x ∈ ↑(spanSingleton R⁰ (I'.divMod I J')⁻¹ * J')

Tactic:
convert! mul_mem_mul (mem_spanSingleton_self _ _) hx

Goal state after:
case e'_1
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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
hx : x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'
⊢ x = (I'.divMod I J')⁻¹ * ((Algebra.lsmul R R K) (I'.divMod I J')) x
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
o : Option ι
s : ι → Set X
⊢ ediam (⋃ i ∈ o, s i) = ⨆ i ∈ o, ediam (s i)

Tactic:
cases o <;> simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖₊ = 0

Tactic:
exact nnnorm_one'

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
y : E
ε : ℝ
⊢ ball y ε = {x | ‖x / y‖ < ε}

Tactic:
ball_eq_norm_inv_mul_lt,

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
y : E
ε : ℝ
⊢ {x | ‖x⁻¹ * y‖ < ε} = {x | ‖x / y‖ < ε}
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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
⊢ StrictMono f ∨ StrictAnti f

Tactic:
by
  have H {c d : α} (hcd : c < d) : StrictMono f ∨ StrictAnti f :=
    (hf_c.continuousOn.strictMonoOn_of_injOn_Icc' hcd.le hf_i.injOn).imp
      (hf_c.strictMonoOn_of_inj_rigidity hf_i hcd)
      (hf_c.strictMonoOn_of_inj_rigidity (δ := δᵒᵈ) hf_i hcd)
  cases subsingleton_or_nontrivial α with
  | inl h => exact Or.inl <| Subsingleton.strictMono f
  | inr h =>
    obtain ⟨a, b, hab⟩ := exists_pair_lt α
    exact H hab

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto (fun x ↦ -f x) l atTop
⊢ Tendsto (fun x ↦ -f x * r) l atTop

Tactic:
exact hf.atTop_mul_const' hr

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : MetricSpace α
hs1 : s.Nontrivial
hs2 : Bornology.IsBounded s
⊢ 0 < diam s

Tactic:
rcases hs1 with ⟨x, hx, y, hy, hxy⟩
  exact (dist_pos.mpr hxy).trans_le <| Metric.dist_le_diam_of_mem hs2 hx hy

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: case refine_1
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
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ g / a ^ k ∈ H

pp: case refine_2
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
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ 1 < g / a ^ k

Tactic:
· exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)

Goal state after:
case refine_2
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
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ 1 < g / a ^ k
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 β
inst✝ : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure[inst✝²] (f '' univ) ∈ 𝓝 (f a)

Tactic:
by simp only [image_univ, h_dense.closure_eq, univ_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (range f)

Tactic:
← image_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' univ)
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_add,

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: x : EReal
h : x ≠ ⊥
⊢ x - ⊥ = ⊤

Tactic:
cases x <;> tauto

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

Goal state before:
pp: x : EReal
hx : x ≠ ⊤
⊢ ⊤ - x = ⊤

Tactic:
cases x <;> tauto

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

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

Tactic:
induction c with

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

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

Tactic:
exact sub_le_of_le_add h

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

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

Tactic:
exact sub_le_of_le_add h

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

Goal state before:
pp: x y : EReal
h : ∀ (z : ℝ), x < ↑z → y ≤ ↑z
⊢ ∀ (z : WithTop ℝ), x < ↑z → y ≤ ↑z

Tactic:
WithTop.forall

Goal state after:
x y : EReal
h : ∀ (z : ℝ), x < ↑z → y ≤ ↑z
⊢ (x < ↑⊤ → y ≤ ↑⊤) ∧ ∀ (x_1 : ℝ), x < ↑↑x_1 → y ≤ ↑↑x_1
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x
⊢ ∀ (z : WithTop ℝ), ↑z < y → ↑z ≤ x

Tactic:
WithTop.forall

Goal state after:
x y : EReal
h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x
⊢ (↑⊤ < y → ↑⊤ ≤ x) ∧ ∀ (x_1 : ℝ), ↑↑x_1 < y → ↑↑x_1 ≤ x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y

Tactic:
refine ⟨fun h _ h' ↦ (eventually_lt_of_limsup_lt (h.trans_lt h') h₂).mono fun _ ↦ le_of_lt, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → limsup u f ≤ x
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝ : Fintype α
⊢ map Finset.card atTop = pure (Fintype.card α)

Tactic:
simp [OrderTop.atTop_eq]

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

Goal state before:
pp: case inl.inl
a b : EReal
h : a < 0
h' : b < 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

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

Goal state before:
pp: case inl.inr.inl
a b : EReal
h : a < 0
h' : b = 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
y : β
y_v : y < liminf u f
⊢ ∃ᶠ (a : α) in f, y < v a

Tactic:
have := (le_liminf_iff h₃ h₁).1 (le_refl (liminf u f)) y y_v

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
y : β
y_v : y < liminf u f
this : ∀ᶠ (a : α) in f, y < u a
⊢ ∃ᶠ (a : α) in f, y < v a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl.inr.inr
a b : EReal
h : a < 0
h' : 0 < b
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

Goal state after:
case inl.inr.inr
a b : EReal
h : a < 0
h' : 0 < b
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.inl.inl
a b : EReal
h : a = 0
h' : b < 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

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

Goal state before:
pp: case inr.inl.inr.inl
a b : EReal
h : a = 0
h' : b = 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

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

Goal state before:
pp: case inr.inl.inr.inr
a b : EReal
h : a = 0
h' : 0 < b
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

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

Goal state before:
pp: case inr.inr.inl
a b : EReal
h : 0 < a
h' : b < 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

Goal state after:
case inr.inr.inl
a b : EReal
h : 0 < a
h' : b < 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.inr.inr.inl
a b : EReal
h : 0 < a
h' : b = 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

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

Goal state before:
pp: case inr.inr.inr.inr
a b : EReal
h : 0 < a
h' : 0 < b
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

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

Goal state before:
pp: case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s

Tactic:
exact ⟨a + 1, fun b hb ↦ ha (b + 1) (by lia)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a : α
s : Finset β
⊢ HasProd f ((∏ b ∈ s, f b) * a) ↔ HasProd f (a * ∏ i ∈ s, f i)

Tactic:
rw [mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous[inst✝⁴, inst✝²] ⇑g
⊢ HasProd (⇑g ∘ f) (g a) L

Tactic:
by
  have : (g ∘ fun s : Finset β ↦ ∏ b ∈ s, f b) = fun s : Finset β ↦ ∏ b ∈ s, (g ∘ f) b :=
    funext <| map_prod g _
  unfold HasProd
  rw [← this]
  exact (hg.tendsto a).comp hf

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Tactic:
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
hf : HasFiniteMulSupport f
⊢ ∏'[L] (b : β), f b = ∏ᶠ (b : β), f b

Tactic:
by
  simp [tprod_def, multipliable_of_hasFiniteMulSupport hf, show Set.Finite _ from hf,
    show L.HasSupport by infer_instance]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ ∏ x ∈ Finset.map g hfg_fin.toFinset, f x = ∏ x ∈ hf_fin.toFinset, f x

Tactic:
refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ ↑(Finset.map g hfg_fin.toFinset) = ↑hf_fin.toFinset
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun i ↦ f i / a₂) (a₁ / a₂) L ↔ HasSum f a₁ L

Tactic:
simpa only [div_eq_mul_inv] using hasSum_mul_right_iff (inv_ne_zero h)

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

Goal state before:
pp: case he
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k) * f (2 * k)

pp: case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k + 1) * f (2 * k + 1)

Tactic:
· simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul]
    exact hf.comp_injective (mul_right_injective₀ (two_ne_zero' ℕ))

Goal state after:
case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k + 1) * f (2 * k + 1)