mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal

Tactic:
{

Goal state after:
case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

Goal state after:
case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ + ↑a✝).toENNReal = ⊤.toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal

Tactic:
{

Goal state after:
case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

Tactic:
{

Goal state after:
case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal

Tactic:
{

Goal state after:
case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal

Tactic:
{

Goal state after:
case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal

Tactic:
{

Goal state after:
case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
{

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal

Tactic:
{

Goal state after:
case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal

Tactic:
{

Goal state after:
case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal

Tactic:
{

Goal state after:
case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal

Tactic:
{

Goal state after:
case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

Goal state after:
case bot.bot
hy : 0 ≤ ⊥
⊢ (⊥ - ⊥).toENNReal = ⊥.toENNReal - ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ - ↑a✝).toENNReal = ⊥.toENNReal - (↑a✝).toENNReal

Tactic:
{

Goal state after:
case bot.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ - ↑a✝).toENNReal = ⊥.toENNReal - (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal

Tactic:
{

Goal state after:
case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
hy : 0 ≤ ⊥
⊢ (↑a✝ - ⊥).toENNReal = (↑a✝).toENNReal - ⊥.toENNReal

Tactic:
{

Goal state after:
case coe.bot
a✝ : ℝ
hy : 0 ≤ ⊥
⊢ (↑a✝ - ⊥).toENNReal = (↑a✝).toENNReal - ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal

Tactic:
{

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

Goal state after:
case coe.top
a✝ : ℝ
hy : 0 ≤ ⊤
⊢ (↑a✝ - ⊤).toENNReal = (↑a✝).toENNReal - ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal

Tactic:
{

Goal state after:
case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

Goal state after:
case top.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ - ↑a✝).toENNReal = ⊤.toENNReal - (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal

Tactic:
{

Goal state after:
case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

Goal state after:
case bot.bot
h : ⊥ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊥ * ⊥ ≠ 0
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

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

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

Tactic:
{

Goal state after:
case bot.top
h : ⊥ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊥ * ⊤ ≠ 0
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

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

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

Tactic:
{

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ↑a✝¹ * ↑a✝ ≠ 0
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

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

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

Tactic:
{

Goal state after:
case top.bot
h : ⊤ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊤ * ⊥ ≠ 0
Module: Mathlib.Data.EReal.Operations

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

Tactic:
{

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

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

Tactic:
{

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
H : ∀ (j : Subtype p), j ∉ m
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
exact ⟨0, Or.inr H⟩

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

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

Tactic:
nth_rw 1 [← neg_zero]
  rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]

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

Goal state before:
pp: a b : EReal
⊢ a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
rw [ne_eq, mul_eq_bot]
  push +distrib Not
  rfl

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

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

Tactic:
{

Goal state after:
case bot.bot
hx : 0 ≤ ⊥
⊢ (⊥ * ⊥).toENNReal = ⊥.toENNReal * ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

Goal state after:
case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
⊢ (⊥ * ↑a✝).toENNReal = ⊥.toENNReal * (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

Goal state after:
case bot.top
hx : 0 ≤ ⊥
⊢ (⊥ * ⊤).toENNReal = ⊥.toENNReal * ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

Goal state after:
case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊥).toENNReal = (↑a✝).toENNReal * ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

Goal state after:
case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
⊢ (↑a✝¹ * ↑a✝).toENNReal = (↑a✝¹).toENNReal * (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

Goal state after:
case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

Goal state after:
case top.bot
hx : 0 ≤ ⊤
⊢ (⊤ * ⊥).toENNReal = ⊤.toENNReal * ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

Goal state after:
case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
⊢ (⊤ * ↑a✝).toENNReal = ⊤.toENNReal * (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

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

Tactic:
{

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

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

Tactic:
· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ b, a < b
⊢ limsup f (𝓝[>] a) = ⨅ r, ⨅ (_ : r > a), f r

Tactic:
by
  rw [(nhdsGT_basis_of_exists_gt hb).limsup_eq_iInf_iSup]
  refine le_antisymm
    (iInf₂_mono' fun r hr ↦ ⟨r, hr, iSup₂_le fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)
    (iInf₂_mono' fun r hr ↦ ?_)
  obtain ⟨b, hb⟩ := exists_between hr
  exact ⟨b, hb.1, le_iSup₂_of_le b hb le_rfl⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, b < a
⊢ limsup f (𝓝[<] a) = ⨅ r, ⨅ (_ : r < a), f r

Tactic:
rw [(nhdsLT_basis_of_exists_lt hb).limsup_eq_iInf_iSup]

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, b < a
⊢ ⨅ i, ⨅ (_ : i < a), ⨆ a_1 ∈ Set.Ioo i a, f a_1 = ⨅ r, ⨅ (_ : r < a), f r
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (CauchySeq fun s ↦ ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
by
  classical
  simp only [CauchySeq, cauchy_map_iff, prod_atTop_atTop_eq,
    uniformity_eq_comap_nhds_one α, tendsto_comap_iff, Function.comp_def, atTop_neBot, true_and]
  rw [tendsto_atTop']
  constructor
  · intro h e he
    obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he
    use s₁ ∪ s₂
    intro t ht
    specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩
    simpa only [Finset.prod_union ht.symm, mul_div_cancel_left] using h
  · rintro h e he
    rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩
    rcases h d hd with ⟨s, h⟩
    use (s, s)
    rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
    have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
      rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]
    simp only [this]
    exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

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

Goal state before:
pp: case neg
ι : 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
hL : ¬L.NeBot
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
· simpa [tprod_bot hL] using one_le_finprod' h

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
⊢ ∏' (b : ↑t), f ↑b ∈ o

Tactic:
refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)
      rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]
      apply hs
      simp_rw [Finset.mem_map]
      rintro _ ⟨b, -, rfl⟩
      exact hts b.prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∏ b ∈ t with g b = f b, g b = ∏ b ∈ t, g b

Tactic:
{

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∏ b ∈ t with g b = f b, g b = ∏ b ∈ t, g b
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i ≠ 1 ↔ ∃ x, f x ≠ 1

Tactic:
by
  rw [Ne, hf.tprod_eq_one_iff, not_forall]

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ f ⁻¹' e ∈ cofinite

Tactic:
rcases hf.vanishing he with ⟨s, hs⟩

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
⊢ f ⁻¹' e ∈ cofinite
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : Ring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : T2Space α
x : α
h : Summable fun x_1 ↦ x ^ x_1
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1

Tactic:
by
  refine tendsto_nhds_unique (h.hasSum.mul_left (1 - x)).tendsto_sum_nat ?_
  simpa [← Finset.mul_sum, mul_neg_geom_sum] using tendsto_const_nhds.sub h.tendsto_atTop_zero

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑(Kf * Kg) * edist ((g ∘ f) x) ((g ∘ f) y)

Tactic:
rw [ENNReal.coe_mul, mul_assoc]; rfl

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

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

Tactic:
← hf.comap_uniformity_le

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (pkg.extend f)

Tactic:
by
  rw [extend_def _ h.uniformContinuous]
  exact pkg.isDenseInducing.isUniformInducing_extend pkg.isUniformInducing h

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Tactic:
have uc' := pkg'.uniformContinuous_compare pkg

Goal state after:
α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ∞
hb✝ : b✝ ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), ↑n < a.1 * a.2

Tactic:
refine this.mono fun c hc => ?_

Goal state after:
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ∞
hb✝ : b✝ ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2
c : ℝ≥0∞ × ℝ≥0∞
hc : ↑n / ↑ε < c.1 ∧ ↑ε < c.2
⊢ ↑n < c.1 * c.2
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a

pp: case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion α
⊢ Completion.extension (lift' coe') (Completion.map SeparationQuotient.mk a) = a

Tactic:
· refine induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) ?_
    refine SeparationQuotient.surjective_mk.forall.2 fun a ↦ ?_
    rw [extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe α),
      map_coe uniformContinuous_mk]

Goal state after:
case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion α
⊢ Completion.extension (lift' coe') (Completion.map SeparationQuotient.mk a) = a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')

Tactic:
edist_comm y y'

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y' y)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl
a b : ℝ
h : a ≤ b
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
Real.ediam_eq (isBounded_Icc _ _),

Goal state after:
case inl
a b : ℝ
h : a ≤ b
⊢ ENNReal.ofReal (sSup (Icc a b) - sInf (Icc a b)) = ENNReal.ofReal (b - a)
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
⊢ IsClosed {x | 0 ≤ x}

Tactic:
have : {x : α | 0 ≤ x} = negPart ⁻¹' {0} := by ext; simp [negPart_eq_zero]
  rw [this]
  exact isClosed_singleton.preimage continuous_negPart

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x ↦ f x * g x) t

Tactic:
obtain ⟨Kf, t, ht, hKf⟩ := hf hx
  obtain ⟨Kg, u, hu, hKg⟩ := hg hx
  exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu,
    (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)

Tactic:
rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
⊢ z ∈ measurableAtom x → z ∉ measurableAtom y

Tactic:
intro hzx

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
⊢ z ∉ measurableAtom y