mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-zero) = -↑zero

pp: case neg
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-neg) = -↑neg

pp: case pos
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-pos) = -↑pos

Tactic:
<;>

Goal state after:
case zero
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-zero) = -↑zero

case neg
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-neg) = -↑neg

case pos
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-pos) = -↑pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ 1 ≤ 1

pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ -1 ≤ 1

pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : b < 0
⊢ -1 ≤ -1

pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : ¬b < 0
⊢ -1 ≤ 0

pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ 0 ≤ 1

pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1

pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 0 ≤ 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ 1 ≤ 1

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ -1 ≤ 1

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : b < 0
⊢ -1 ≤ -1

case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : ¬b < 0
⊢ -1 ≤ 0

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ 0 ≤ 1

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1

case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 0 ≤ 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
⊢ sign a = sign b ∨ sign a = -sign b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top
⊢ ⊤.abs = 0 ↔ ⊤ = 0

Tactic:
· simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case ofNat.zero
⊢ (ofNat 0).sign = ↑(SignType.sign (ofNat 0))

pp: case ofNat.succ
n✝ : ℕ
⊢ (ofNat (n✝ + 1)).sign = ↑(SignType.sign (ofNat (n✝ + 1)))

pp: case negSucc
a✝ : ℕ
⊢ -[a✝+1].sign = ↑(SignType.sign -[a✝+1])

Tactic:
<;>

Goal state after:
case ofNat.zero
⊢ (ofNat 0).sign = ↑(SignType.sign (ofNat 0))

case ofNat.succ
n✝ : ℕ
⊢ (ofNat (n✝ + 1)).sign = ↑(SignType.sign (ofNat (n✝ + 1)))

case negSucc
a✝ : ℕ
⊢ -[a✝+1].sign = ↑(SignType.sign -[a✝+1])
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬↑x✝ = 0

Tactic:
coe_eq_zero

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case zero
⊢ ↑↑zero = ↑zero

pp: case neg
⊢ ↑↑neg = ↑neg

pp: case pos
⊢ ↑↑pos = ↑pos

Tactic:
<;>

Goal state after:
case zero
⊢ ↑↑zero = ↑zero

case neg
⊢ ↑↑neg = ↑neg

case pos
⊢ ↑↑pos = ↑pos
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.zero
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ sign x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ zero = zero ∨ sign x = pos ∧ zero = pos ∧ x.abs ≤ y.abs

pp: case mp.neg
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ sign x = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ neg = zero ∨ sign x = pos ∧ neg = pos ∧ x.abs ≤ y.abs

pp: case mp.pos
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ sign x = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ pos = zero ∨ sign x = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
<;>

Goal state after:
case mp.zero
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ sign x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ zero = zero ∨ sign x = pos ∧ zero = pos ∧ x.abs ≤ y.abs

case mp.neg
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ sign x = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ neg = zero ∨ sign x = pos ∧ neg = pos ∧ x.abs ≤ y.abs

case mp.pos
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ sign x = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ pos = zero ∨ sign x = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y z : EReal
⊢ (x * y * z).abs = (x * (y * z)).abs ∧ sign (x * y * z) = sign (x * (y * z))

Tactic:
simp only [mul_assoc, abs_mul, sign_mul, and_self_iff]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
s : Set α
⊢ LowerSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≤ y) → f x ≤ y

Tactic:
by
  simp [semicontinuousWithinAt_iff_frequently]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
s : Set α
⊢ UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≥ y) → f x ≥ y

Tactic:
by
  simp [semicontinuousWithinAt_iff_frequently]

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

Goal state before:
pp: case inl
x y : EReal
h : x ≤ y
⊢ min (-x) (-y) = -max x y

pp: case inr
x y : EReal
h : y ≤ x
⊢ min (-x) (-y) = -max x y

Tactic:
<;>

Goal state after:
case inl
x y : EReal
h : x ≤ y
⊢ min (-x) (-y) = -max x y

case inr
x y : EReal
h : y ≤ x
⊢ min (-x) (-y) = -max x y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
x y : EReal
h : x ≤ y
⊢ max (-x) (-y) = -min x y

pp: case inr
x y : EReal
h : y ≤ x
⊢ max (-x) (-y) = -min x y

Tactic:
<;>

Goal state after:
case inl
x y : EReal
h : x ≤ y
⊢ max (-x) (-y) = -min x y

case inr
x y : EReal
h : y ≤ x
⊢ max (-x) (-y) = -min x y
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case mpr
f : ℕ → ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f

Tactic:
rintro hnat ⟨r, hr⟩
    exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

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

Goal state before:
pp: case pos
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
h✝ : i' = i
⊢ 0 ≤ f i'

pp: case neg
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
h✝ : ¬i' = i
⊢ f i' ≤ f i'

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
h✝ : i' = i
⊢ 0 ≤ f i'

case neg
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
h✝ : ¬i' = i
⊢ f i' ≤ f i'
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
by
  cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s.Nonempty
⊢ BddBelow (f '' s)

Tactic:
obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_isMinOn h hs hf
      exact has.bddBelow

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∉ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∉ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∈ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∉ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∈ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∉ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∉ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∈ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
h : x ∉ s
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∈ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∉ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∈ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∉ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inl
a c : ℝ
ha : a ≠ 0
ha' : a < 0
⊢ Tendsto (fun x ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atBot_zero.comp
      (tendsto_atBot_add_const_right _ c (tendsto_id.const_mul_atTop_of_neg ha'))

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

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ↑a)

Tactic:
by
  simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
  refine fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
    (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_
  simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

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

Goal state before:
pp: case bot
y : EReal
h : (⊥, y).1 ≠ ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : (⊥, y).1 ≠ ⊥ ∨ (⊥, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, y)

pp: case coe
y : EReal
a✝ : ℝ
h : (↑a✝, y).1 ≠ ⊤ ∨ (↑a✝, y).2 ≠ ⊥
h' : (↑a✝, y).1 ≠ ⊥ ∨ (↑a✝, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, y)

pp: case top
y : EReal
h : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, y)

Tactic:
<;>

Goal state after:
case bot
y : EReal
h : (⊥, y).1 ≠ ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : (⊥, y).1 ≠ ⊥ ∨ (⊥, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, y)

case coe
y : EReal
a✝ : ℝ
h : (↑a✝, y).1 ≠ ⊤ ∨ (↑a✝, y).2 ≠ ⊥
h' : (↑a✝, y).1 ≠ ⊥ ∨ (↑a✝, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, y)

case top
y : EReal
h : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, y)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0

pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)

Tactic:
<;>

Goal state after:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0

u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u 0 ≤ c ^ 0 * u 0

pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0

Tactic:
<;>

Goal state after:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u 0 ≤ c ^ 0 * u 0

u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ HasSum (fun n ↦ (1 / 2) ^ n) 2

Tactic:
convert! hasSum_geometric_of_lt_one _ _

Goal state after:
case e'_6
⊢ 2 = (1 - 1 / 2)⁻¹

case convert_2
⊢ 0 ≤ 1 / 2

case convert_3
⊢ 1 / 2 < 1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case e'_6
⊢ 2 = (1 - 1 / 2)⁻¹

pp: case convert_2
⊢ 0 ≤ 1 / 2

pp: case convert_3
⊢ 1 / 2 < 1

Tactic:
<;>

Goal state after:
case e'_6
⊢ 2 = (1 - 1 / 2)⁻¹

case convert_2
⊢ 0 ≤ 1 / 2

case convert_3
⊢ 1 / 2 < 1
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f ⁻¹' s)

Tactic:
map_apply

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ (OuterMeasure.ofFunction m m_empty) (f ⁻¹' s) ≤ m (f ⁻¹' s)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case inl
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t = ∅
⊢ ⨆ (_ : t.Nonempty), m t = m t

pp: case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t = ∅
⊢ ⨆ (_ : t.Nonempty), m t = m t

case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case inl
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s

pp: case inr
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s

case inr
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case inl
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s

pp: case inr
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s

case inr
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case inl
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ (c • fun s ↦ ⨆ (_ : s.Nonempty), m s) ∅ = ⨆ (_ : ∅.Nonempty), (c • m) ∅

pp: case inr
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
hs : s.Nonempty
⊢ (c • fun s ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ (c • fun s ↦ ⨆ (_ : s.Nonempty), m s) ∅ = ⨆ (_ : ∅.Nonempty), (c • m) ∅

case inr
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
hs : s.Nonempty
⊢ (c • fun s ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ f a

pp: case refine_2
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ a

Tactic:
<;>

Goal state after:
case refine_1
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ f a

case refine_2
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ a
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
⊢ ↑x < p.1 * p.2

Tactic:
have lock := mul_le_mul_of_nonneg_right (le_of_lt p1_gt) (le_of_lt a2_pos)

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
lock : ↑(2 * max (x + 1) 0 / a) * ↑(a / 2) ≤ p.1 * ↑(a / 2)
⊢ ↑x < p.1 * p.2
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
⊢ (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) z y

Tactic:
have : (f x, g x) ∈ u ×ˢ v := ⟨xu, xv⟩

Goal state after:
case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
this : (f x, g x) ∈ u ×ˢ v
⊢ (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) z y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot
y : EReal
h₁ : (⊥, y).1 ≠ 0 ∨ (⊥, y).2 ≠ ⊥
h₂ : (⊥, y).1 ≠ 0 ∨ (⊥, y).2 ≠ ⊤
h₃ : (⊥, y).1 ≠ ⊥ ∨ (⊥, y).2 ≠ 0
h₄ : (⊥, y).1 ≠ ⊤ ∨ (⊥, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, y)

pp: case coe
y : EReal
a✝ : ℝ
h₁ : (↑a✝, y).1 ≠ 0 ∨ (↑a✝, y).2 ≠ ⊥
h₂ : (↑a✝, y).1 ≠ 0 ∨ (↑a✝, y).2 ≠ ⊤
h₃ : (↑a✝, y).1 ≠ ⊥ ∨ (↑a✝, y).2 ≠ 0
h₄ : (↑a✝, y).1 ≠ ⊤ ∨ (↑a✝, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, y)

pp: case top
y : EReal
h₁ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, y)

Tactic:
<;>

Goal state after:
case bot
y : EReal
h₁ : (⊥, y).1 ≠ 0 ∨ (⊥, y).2 ≠ ⊥
h₂ : (⊥, y).1 ≠ 0 ∨ (⊥, y).2 ≠ ⊤
h₃ : (⊥, y).1 ≠ ⊥ ∨ (⊥, y).2 ≠ 0
h₄ : (⊥, y).1 ≠ ⊤ ∨ (⊥, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, y)

case coe
y : EReal
a✝ : ℝ
h₁ : (↑a✝, y).1 ≠ 0 ∨ (↑a✝, y).2 ≠ ⊥
h₂ : (↑a✝, y).1 ≠ 0 ∨ (↑a✝, y).2 ≠ ⊤
h₃ : (↑a✝, y).1 ≠ ⊥ ∨ (↑a✝, y).2 ≠ 0
h₄ : (↑a✝, y).1 ≠ ⊤ ∨ (↑a✝, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, y)

case top
y : EReal
h₁ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, y)