mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = -1 • (-x + y)
⊢ ‖-x + y‖ = ‖-1‖ * ‖-x + y‖

Tactic:
simp

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

Goal state before:
pp: case h₂.h₁
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ k ≠ 0 → MeasurableSet {x | p x k}

Tactic:
try intros

Goal state after:
case h₂.h₁
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : k ≠ 0
⊢ MeasurableSet {x | p x k}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a | p a b}ᶜ)

Tactic:
try intros

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ MeasurableSet (⋂ (_ : k < b✝), ⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n ≠ ∞ ↔ n ≠ ⊤

Tactic:
simp

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

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ k < b✝ → MeasurableSet (⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)

Tactic:
try intros

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ MeasurableSet (⋂ (_ : b✝¹ ≤ N), {a | p a b✝¹}ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ b✝¹ ≤ N → MeasurableSet {a | p a b✝¹}ᶜ

Tactic:
try intros

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝² : ℕ
b✝¹ : k < b✝²
b✝ : b✝² ≤ N
⊢ MeasurableSet {a | p a b✝²}ᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0
⊢ μ s = 0

Tactic:
choose! u hxu hu₀ using hs

Goal state after:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
x : β
⊢ {x} ⊆ measurableAtom x

Tactic:
simp

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

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖(↑n)⁻¹‖ * C = (↑n)⁻¹ * C

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m m₁ m₂ : OuterMeasure α
⊢ m₁ ∅ + m₂ ∅ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ c • 1 * 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = (⨆ i, ⇑(f i)) s

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
⊢ ∅.indicator (fun x ↦ 1) a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
⊢ ∑' (i : ι), (f i) ∅ = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ (measurableAtom y : Set β) := by
    ext1 ⟨x, y⟩
    simp only [mem_preimage, mem_iUnion, mem_prod]
    refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
    rintro ⟨y', hy's, hy'⟩
    rwa [h'f y' y x hy']
  rw [this]
  exact .iUnion (fun y ↦ (hf y hs).prod (.measurableAtom_of_countable y))

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
⊢ m (f '' ∅) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
t : β
ht : t ∈ Icc 0 1
⊢ 1 - t ∈ Icc 0 1

Tactic:
mem_Icc

Goal state after:
β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict univ) m) s = m s

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict ∅) m) s = 0 s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Nontrivial R
⊢ 0 ∈ Ico 0 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x ↦ g x a

Tactic:
simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
⊢ ∀ (a_1 : δ), Measurable fun x ↦ update x.1 a x.2 a_1

Tactic:
intro j

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x ↦ update x.1 a x.2 j
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S : Finset α
⊢ MeasurableSet {↑S}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S x✝ : Finset α
⊢ x✝ ∈ {s | ↑s ∈ {↑S}} ↔ x✝ ∈ {S}

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ zero = -1 ∨ zero = 0 ∨ zero = 1

Tactic:
simp

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

Goal state before:
pp: case neg
⊢ neg = -1 ∨ neg = 0 ∨ neg = 1

Tactic:
simp

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

Goal state before:
pp: case pos
⊢ pos = -1 ∨ pos = 0 ∨ pos = 1

Tactic:
simp

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

Goal state before:
pp: a : SignType
⊢ 0 < 3

Tactic:
simp

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

Goal state before:
pp: a : SignType
⊢ 1 < 3

Tactic:
simp

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

Goal state before:
pp: a : SignType
⊢ 2 < 3

Tactic:
simp

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

Goal state before:
pp: case zero
k : ℕ
⊢ (zero * zero) ^ k * zero = zero

Tactic:
simp

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

Goal state before:
pp: case neg
k : ℕ
⊢ (neg * neg) ^ k * neg = neg

Tactic:
simp

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

Goal state before:
pp: case pos
k : ℕ
⊢ (pos * pos) ^ k * pos = pos

Tactic:
simp

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

Goal state before:
pp: case inr.zero
k : ℤ
hs : zero ≠ 0
⊢ (zero * zero) ^ k * zero = zero

Tactic:
simp

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

Goal state before:
pp: case inr.neg
k : ℤ
hs : neg ≠ 0
⊢ (neg * neg) ^ k * neg = neg

Tactic:
simp

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

Goal state before:
pp: case inr.pos
k : ℤ
hs : pos ≠ 0
⊢ (pos * pos) ^ k * pos = pos

Tactic:
simp

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

Goal state before:
pp: a : Fin 3
isLt✝ : 0 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨0, isLt✝⟩) =
    ⟨0, isLt✝⟩

Tactic:
simp

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

Goal state before:
pp: a : Fin 3
isLt✝ : 1 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨1, isLt✝⟩) =
    ⟨1, isLt✝⟩

Tactic:
simp

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

Goal state before:
pp: a : Fin 3
isLt✝ : 2 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨2, isLt✝⟩) =
    ⟨2, isLt✝⟩

Tactic:
simp

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

Goal state before:
pp: case h₁
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 1 = 1

Tactic:
simp

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

Goal state before:
pp: case h₂
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 0 = 0

Tactic:
simp

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

Goal state before:
pp: case h₃
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f (-1) = -1

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ (toSpanSingleton R 1) 1 = (algebraMapCLM R A) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ (↑0)⁻¹ ≤ 1

Tactic:
simp

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

Goal state before:
pp: case bot
⊢ ⊥.abs = 0 ↔ ⊥ = 0

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
a : α
f : α → ℝ≥0∞
⊢ ⨆ (_ : a = a), f a = f a

Tactic:
simp

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

Goal state before:
pp: ⊢ ↑(sign ⊥) * ↑⊥.abs = ⊥

Tactic:
simp

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

Goal state before:
pp: ⊢ ↑(sign ⊤) * ↑⊤.abs = ⊤

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
s : Set ι
t : ι → Set α
⊢ ⋃ i ∈ s, t i = ⋃ i, t ↑i

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case top_top
⊢ (⊤ * ⊤)⁻¹ = ⊤⁻¹ * ⊤⁻¹

Tactic:
simp

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

Goal state before:
pp: case top_zero
⊢ (⊤ * 0)⁻¹ = ⊤⁻¹ * 0⁻¹

Tactic:
simp

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

Goal state before:
pp: case top_bot
⊢ (⊤ * ⊥)⁻¹ = ⊤⁻¹ * ⊥⁻¹

Tactic:
simp

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

Goal state before:
pp: case zero_bot
⊢ (0 * ⊥)⁻¹ = 0⁻¹ * ⊥⁻¹

Tactic:
simp

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

Goal state before:
pp: case bot_bot
⊢ (⊥ * ⊥)⁻¹ = ⊥⁻¹ * ⊥⁻¹

Tactic:
simp

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

Goal state before:
pp: case bot
⊢ ↑(sign ⊥) * (↑⊥.abs)⁻¹ = ⊥⁻¹

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ↑(sign ⊤) * (↑⊤.abs)⁻¹ = ⊤⁻¹

Tactic:
simp

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

Goal state before:
pp: case coe.inr.inl
⊢ ↑(sign ↑0) * (↑(↑0).abs)⁻¹ = (↑0)⁻¹

Tactic:
simp

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

Goal state before:
pp: case bot
⊢ ↑(sign ⊥) * ↑⊥.abs⁻¹ = ⊥⁻¹

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ↑(sign ⊤) * ↑⊤.abs⁻¹ = ⊤⁻¹

Tactic:
simp

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'

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
simp

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

Goal state before:
pp: case coe.inr.inl
⊢ ↑(sign ↑0) * ↑(↑0).abs⁻¹ = (↑0)⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ UpperHemicontinuousWithinAt f s x ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
UpperHemicontinuousWithinAt,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ SemicontinuousWithinAt (fun x t ↦ t ∈ 𝓝ˢ (f x)) s x ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case bot
h : 0 ≤ ⊥
⊢ 0 ≤ ⊥⁻¹

Tactic:
simp

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

Goal state before:
pp: case top
h : 0 ≤ ⊤
⊢ 0 ≤ ⊤⁻¹

Tactic:
simp

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

Goal state before:
pp: case bot
h : ⊥ ≤ 0
⊢ ⊥⁻¹ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case top
h : ⊤ ≤ 0
⊢ ⊤⁻¹ ≤ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
x✝ : α × β
⊢ x✝ ∈ {x | x.2 ∈ f x.1 ∩ g x.1} ↔ x✝ ∈ {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}

Tactic:
simp

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

Goal state before:
pp: case inl
a c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
· rcases eq_or_lt_of_le ha with rfl | ha
    · rw [zero_mul] at h
      exact (not_le_of_gt h hc).rec
    · obtain ⟨a', a0', aa'⟩ := exists_between ha
      use a', mem_Ioo.2 ⟨a0', aa'⟩
      rw [mul_top_of_pos ha] at h
      rwa [mul_top_of_pos a0']

Goal state after:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑(f a) < ↑x) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Iio i

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
x✝ : ℕ
⊢ (↑x✝)⁻¹ = (⇑(algebraMap ℚ≥0 𝕜) ∘ fun n ↦ (↑n)⁻¹) x✝

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
h₁ : 0 ≤ 0
h₂ : 0 ≠ ⊤
⊢ limsup (fun x ↦ 0 * u x) f = 0 * limsup u f

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ 1 + x * 0 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
i : ℕ
⊢ ∀ (i_1 : ℕ), f i i_1 ⊆ ⋃ i, ⋃ j, f i j

Tactic:
intro j

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
i j : ℕ
⊢ f i j ⊆ ⋃ i, ⋃ j, f i j
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
K : Type u_5
inst✝² : DivisionSemiring K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f g : α → K
l : Filter α
hg : Tendsto g l atTop
⊢ Set.Ioi 0 ⊆ {0}ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : ExistsAddOfLE 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 < r
this : Tendsto (fun n ↦ r⁻¹ ^ n) atTop atTop
n : ℕ
⊢ ((fun r ↦ r⁻¹) ∘ fun n ↦ r⁻¹ ^ n) n = r ^ n

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case zero
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
⊢ 0 ≠ 0 → m (f 0) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
simp

Goal state after: