mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∈ s → s.piecewise u v a = u a

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∉ s → s.piecewise u v a = v a

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∈ s → s.piecewise u v a = u a

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∉ s → s.piecewise u v a = v a
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
exact tendsto_of_liminf_eq_limsup (le_antisymm (le_trans (liminf_le_limsup h h') hsup) hinf)
      (le_antisymm hsup (le_trans hinf (liminf_le_limsup h h'))) h h'

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

Goal state before:
pp: case bot
b : ℝ
⊢ ⊥ + ↑b - ↑b = ⊥

pp: case coe
b a✝ : ℝ
⊢ ↑a✝ + ↑b - ↑b = ↑a✝

pp: case top
b : ℝ
⊢ ⊤ + ↑b - ↑b = ⊤

Tactic:
<;>

Goal state after:
case bot
b : ℝ
⊢ ⊥ + ↑b - ↑b = ⊥

case coe
b a✝ : ℝ
⊢ ↑a✝ + ↑b - ↑b = ↑a✝

case top
b : ℝ
⊢ ⊤ + ↑b - ↑b = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
b : ℝ
⊢ ↑b - (⊥ + ↑b) = -⊥

pp: case coe
b a✝ : ℝ
⊢ ↑b - (↑a✝ + ↑b) = -↑a✝

pp: case top
b : ℝ
⊢ ↑b - (⊤ + ↑b) = -⊤

Tactic:
<;>

Goal state after:
case bot
b : ℝ
⊢ ↑b - (⊥ + ↑b) = -⊥

case coe
b a✝ : ℝ
⊢ ↑b - (↑a✝ + ↑b) = -↑a✝

case top
b : ℝ
⊢ ↑b - (⊤ + ↑b) = -⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case refine_1
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊥ ∨ c ≠ ⊥

pp: case refine_2
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊤ ∨ c ≠ ⊤

Tactic:
<;>

Goal state after:
case refine_1
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊥ ∨ c ≠ ⊥

case refine_2
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊤ ∨ c ≠ ⊤
Module: Mathlib.Order.LiminfLimsup

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

pp: case refine_2
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
t : Set α
h : t ∈ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}
⊢ x ∈ t

Tactic:
<;>

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

case refine_2
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
t : Set α
h : t ∈ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}
⊢ x ∈ t
Module: Mathlib.Data.EReal.Operations

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

Tactic:
by
  refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩
  rw [WithTop.forall]
  aesop

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

Goal state before:
pp: case bot
b : EReal
h : ⊥ ≠ 0 ∧ b ≠ 0
⊢ ⊥ * b ≠ 0

pp: case coe
b : EReal
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ b ≠ 0
⊢ ↑a✝ * b ≠ 0

pp: case top
b : EReal
h : ⊤ ≠ 0 ∧ b ≠ 0
⊢ ⊤ * b ≠ 0

Tactic:
<;>

Goal state after:
case bot
b : EReal
h : ⊥ ≠ 0 ∧ b ≠ 0
⊢ ⊥ * b ≠ 0

case coe
b : EReal
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ b ≠ 0
⊢ ↑a✝ * b ≠ 0

case top
b : EReal
h : ⊤ ≠ 0 ∧ b ≠ 0
⊢ ⊤ * b ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
h : ⊥ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊥ * ⊥ ≠ 0

pp: case bot.coe
a✝ : ℝ
h : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊥ * ↑a✝ ≠ 0

pp: case bot.top
h : ⊥ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊥ * ⊤ ≠ 0

pp: case coe.bot
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
⊢ ↑a✝ * ⊥ ≠ 0

pp: case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ↑a✝¹ * ↑a✝ ≠ 0

pp: case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0

pp: case top.bot
h : ⊤ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊤ * ⊥ ≠ 0

pp: case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

pp: case top.top
h : ⊤ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊤ * ⊤ ≠ 0

Tactic:
<;>

Goal state after:
case bot.bot
h : ⊥ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊥ * ⊥ ≠ 0

case bot.coe
a✝ : ℝ
h : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊥ * ↑a✝ ≠ 0

case bot.top
h : ⊥ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊥ * ⊤ ≠ 0

case coe.bot
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
⊢ ↑a✝ * ⊥ ≠ 0

case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ↑a✝¹ * ↑a✝ ≠ 0

case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0

case top.bot
h : ⊤ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊤ * ⊥ ≠ 0

case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

case top.top
h : ⊤ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊤ * ⊤ ≠ 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
⊢ x ≤ limsup u f

Tactic:
← forall_lt_iff_le

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
⊢ ∀ ⦃c : β⦄, c < x → c < limsup u f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe.inl
a✝ : ℝ
h✝ : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
h : ↑a✝ < 0
⊢ ⊥ * ↑a✝ ≠ 0

pp: case bot.coe.inr
a✝ : ℝ
h✝ : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
h : 0 < ↑a✝
⊢ ⊥ * ↑a✝ ≠ 0

Tactic:
<;>

Goal state after:
case bot.coe.inl
a✝ : ℝ
h✝ : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
h : ↑a✝ < 0
⊢ ⊥ * ↑a✝ ≠ 0

case bot.coe.inr
a✝ : ℝ
h✝ : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
h : 0 < ↑a✝
⊢ ⊥ * ↑a✝ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot.inl
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
h : ↑a✝ < 0
⊢ ↑a✝ * ⊥ ≠ 0

pp: case coe.bot.inr
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
h : 0 < ↑a✝
⊢ ↑a✝ * ⊥ ≠ 0

Tactic:
<;>

Goal state after:
case coe.bot.inl
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
h : ↑a✝ < 0
⊢ ↑a✝ * ⊥ ≠ 0

case coe.bot.inr
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
h : 0 < ↑a✝
⊢ ↑a✝ * ⊥ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top.inl
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
h : ↑a✝ < 0
⊢ ↑a✝ * ⊤ ≠ 0

pp: case coe.top.inr
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
h : 0 < ↑a✝
⊢ ↑a✝ * ⊤ ≠ 0

Tactic:
<;>

Goal state after:
case coe.top.inl
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
h : ↑a✝ < 0
⊢ ↑a✝ * ⊤ ≠ 0

case coe.top.inr
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
h : 0 < ↑a✝
⊢ ↑a✝ * ⊤ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe.inl
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : ↑a✝ < 0
⊢ ⊤ * ↑a✝ ≠ 0

pp: case top.coe.inr
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : 0 < ↑a✝
⊢ ⊤ * ↑a✝ ≠ 0

Tactic:
<;>

Goal state after:
case top.coe.inl
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : ↑a✝ < 0
⊢ ⊤ * ↑a✝ ≠ 0

case top.coe.inr
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : 0 < ↑a✝
⊢ ⊤ * ↑a✝ ≠ 0
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
⊢ (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → x ≤ limsup u f

Tactic:
← forall_lt_iff_le

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, y ≤ u a) → ∀ ⦃c : β⦄, c < x → c < limsup u f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl
a b : EReal
h : a < 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)

pp: case inr.inl
a b : EReal
h : a = 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)

pp: case inr.inr
a b : EReal
h : 0 < a
⊢ (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:
<;>

Goal state after:
case inl
a b : EReal
h : a < 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)

case inr.inl
a b : EReal
h : a = 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)

case inr.inr
a b : EReal
h : 0 < a
⊢ (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)
Module: Mathlib.Data.EReal.Operations

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

pp: 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

Tactic:
<;>

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

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: x y : EReal
⊢ -x * y = -(x * y)

Tactic:
by
  induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]

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

Goal state before:
pp: case mp
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ (∃ a, ∀ (b : Finset β), a ⊆ b → b.preimage ⇑f ⋯ ∈ s) → ∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s

pp: case mpr
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ (∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s) → ∃ a, ∀ (b : Finset β), a ⊆ b → b.preimage ⇑f ⋯ ∈ s

Tactic:
<;>

Goal state after:
case mp
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ (∃ a, ∀ (b : Finset β), a ⊆ b → b.preimage ⇑f ⋯ ∈ s) → ∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s

case mpr
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ (∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s) → ∃ a, ∀ (b : Finset β), a ⊆ b → b.preimage ⇑f ⋯ ∈ s
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
hx : 0 ≤ ⊥
⊢ (⊥ * y).toENNReal = ⊥.toENNReal * y.toENNReal

pp: case coe
y : EReal
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * y).toENNReal = (↑a✝).toENNReal * y.toENNReal

pp: case top
y : EReal
hx : 0 ≤ ⊤
⊢ (⊤ * y).toENNReal = ⊤.toENNReal * y.toENNReal

Tactic:
<;>

Goal state after:
case bot
y : EReal
hx : 0 ≤ ⊥
⊢ (⊥ * y).toENNReal = ⊥.toENNReal * y.toENNReal

case coe
y : EReal
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * y).toENNReal = (↑a✝).toENNReal * y.toENNReal

case top
y : EReal
hx : 0 ≤ ⊤
⊢ (⊤ * y).toENNReal = ⊤.toENNReal * y.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
hx : 0 ≤ ⊥
⊢ (⊥ * ⊥).toENNReal = ⊥.toENNReal * ⊥.toENNReal

pp: case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
⊢ (⊥ * ↑a✝).toENNReal = ⊥.toENNReal * (↑a✝).toENNReal

pp: case bot.top
hx : 0 ≤ ⊥
⊢ (⊥ * ⊤).toENNReal = ⊥.toENNReal * ⊤.toENNReal

pp: case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊥).toENNReal = (↑a✝).toENNReal * ⊥.toENNReal

pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
⊢ (↑a✝¹ * ↑a✝).toENNReal = (↑a✝¹).toENNReal * (↑a✝).toENNReal

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

pp: case top.bot
hx : 0 ≤ ⊤
⊢ (⊤ * ⊥).toENNReal = ⊤.toENNReal * ⊥.toENNReal

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

pp: case top.top
hx : 0 ≤ ⊤
⊢ (⊤ * ⊤).toENNReal = ⊤.toENNReal * ⊤.toENNReal

Tactic:
<;>

Goal state after:
case bot.bot
hx : 0 ≤ ⊥
⊢ (⊥ * ⊥).toENNReal = ⊥.toENNReal * ⊥.toENNReal

case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
⊢ (⊥ * ↑a✝).toENNReal = ⊥.toENNReal * (↑a✝).toENNReal

case bot.top
hx : 0 ≤ ⊥
⊢ (⊥ * ⊤).toENNReal = ⊥.toENNReal * ⊤.toENNReal

case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊥).toENNReal = (↑a✝).toENNReal * ⊥.toENNReal

case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
⊢ (↑a✝¹ * ↑a✝).toENNReal = (↑a✝¹).toENNReal * (↑a✝).toENNReal

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

case top.bot
hx : 0 ≤ ⊤
⊢ (⊤ * ⊥).toENNReal = ⊤.toENNReal * ⊥.toENNReal

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

case top.top
hx : 0 ≤ ⊤
⊢ (⊤ * ⊤).toENNReal = ⊤.toENNReal * ⊤.toENNReal
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

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:
<;>

Goal state after:
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

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
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)

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:
<;>

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)

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.SummationFilter

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

pp: 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

Tactic:
<;>

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

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.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = ∅

Tactic:
simp_rw [← not_nonempty_iff_eq_empty, nonempty_iInter_Iic_iff]

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.bot
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + z) = ↑x * ⊥ + ↑x * z

pp: case inr.coe
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + z) = ↑x * ↑a✝ + ↑x * z

pp: case inr.top
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + z) = ↑x * ⊤ + ↑x * z

Tactic:
<;>

Goal state after:
case inr.bot
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + z) = ↑x * ⊥ + ↑x * z

case inr.coe
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + z) = ↑x * ↑a✝ + ↑x * z

case inr.top
z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + z) = ↑x * ⊤ + ↑x * z
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.bot.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊥) = ↑x * ⊥ + ↑x * ⊥

pp: case inr.bot.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊥ + ↑a✝) = ↑x * ⊥ + ↑x * ↑a✝

pp: case inr.bot.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊤) = ↑x * ⊥ + ↑x * ⊤

pp: case inr.coe.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊥) = ↑x * ↑a✝ + ↑x * ⊥

pp: case inr.coe.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝¹ a✝ : ℝ
⊢ ↑x * (↑a✝¹ + ↑a✝) = ↑x * ↑a✝¹ + ↑x * ↑a✝

pp: case inr.coe.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊤) = ↑x * ↑a✝ + ↑x * ⊤

pp: case inr.top.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊥) = ↑x * ⊤ + ↑x * ⊥

pp: case inr.top.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊤ + ↑a✝) = ↑x * ⊤ + ↑x * ↑a✝

pp: case inr.top.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊤) = ↑x * ⊤ + ↑x * ⊤

Tactic:
<;>

Goal state after:
case inr.bot.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊥) = ↑x * ⊥ + ↑x * ⊥

case inr.bot.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊥ + ↑a✝) = ↑x * ⊥ + ↑x * ↑a✝

case inr.bot.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊤) = ↑x * ⊥ + ↑x * ⊤

case inr.coe.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊥) = ↑x * ↑a✝ + ↑x * ⊥

case inr.coe.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝¹ a✝ : ℝ
⊢ ↑x * (↑a✝¹ + ↑a✝) = ↑x * ↑a✝¹ + ↑x * ↑a✝

case inr.coe.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊤) = ↑x * ↑a✝ + ↑x * ⊤

case inr.top.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊥) = ↑x * ⊤ + ↑x * ⊥

case inr.top.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊤ + ↑a✝) = ↑x * ⊤ + ↑x * ↑a✝

case inr.top.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊤) = ↑x * ⊤ + ↑x * ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case e'_2.e'_6
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ x = 1 * x

pp: case succ.convert_4
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ ↑n

pp: case succ.convert_5
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ 1

Tactic:
<;>

Goal state after:
case e'_2.e'_6
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ x = 1 * x

case succ.convert_4
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ ↑n

case succ.convert_5
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ 1
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop ≤ Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop

pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop ≤ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop

Tactic:
<;>

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop ≤ Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop

case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop ≤ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ t, a ∉ (↑s ∩ L.support).toFinset → f a = 1

pp: case h₂
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ (↑s ∩ L.support).toFinset, a ∉ t → f a = 1

pp: case h
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ t, a ∈ (↑s ∩ L.support).toFinset → f a = f a

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ t, a ∉ (↑s ∩ L.support).toFinset → f a = 1

case h₂
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ (↑s ∩ L.support).toFinset, a ∉ t → f a = 1

case h
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ t, a ∈ (↑s ∩ L.support).toFinset → f a = f a
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
by_cases hL : L.NeBot
    · exact hg.hasProd.one_le h
    · simpa [tprod_bot hL] using one_le_finprod' h

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

Goal state before:
pp: case neg
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
x✝ : Finset α
⊢ ¬Multipliable fun a ↦ f ↑a

Tactic:
rwa [Finset.multipliable_compl_iff]

Goal state after: