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
⊢ -y + x = x + -y

Tactic:
;

Goal state after:
𝕜✝ : 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
⊢ -y + x = x + -y
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
i : ℕ
⊢ disjointed t i ⊆ t i

Tactic:
;

Goal state after:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
i : ℕ
⊢ disjointed t i ⊆ t i
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case h
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ s ∩ t ⊆ t

Tactic:
;

Goal state after:
case h
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ s ∩ t ⊆ t
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case h
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ S ∩ s k ⊆ s k

Tactic:
;

Goal state after:
case h
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ S ∩ s k ⊆ s k
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case h₁
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ μ (s k) ≤ M

Tactic:
;

Goal state after:
case h₁
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋯
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⋯
k : ι
⊢ μ (s k) ≤ M
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✝⁴ : Module 𝕜✝ E✝
inst✝³ : Norm E✝
𝕜 : Type u_8
E : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
core : Core 𝕜 E
r : 𝕜
x : E
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
rw [core.norm_smul r x]

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
hn : C / ε < ↑0
hnpos : 0 < ↑0
⊢ False

Tactic:
;

Goal state after:
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
hn : C / ε < ↑0
hnpos : 0 < ↑0
⊢ False
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 • 0 = 0

Tactic:
;

Goal state after:
α : 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 • 0 = 0
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:
;

Goal state after:
α : 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
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this : (⨆ i, bif i then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)

Tactic:
;

Goal state after:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this : (⨆ i, bif i then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∑' (i : ι), (f i) (⋃ i, s i) ≤ ∑' (b : ι) (a : ℕ), (f b) (s a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∑' (i : ι), (f i) (⋃ i, s i) ≤ ∑' (b : ι) (a : ℕ), (f b) (s a)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable fun x ↦ x

Tactic:
;

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable fun x ↦ x
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
by
  refine le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)
  refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_
  rw [sum_Ico_eq_sum_range]
  refine Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_
  exact hd.comp_injective (add_right_injective n)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | (p a → q a) ∧ (q a → p a)}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | (p a → q a) ∧ (q a → p a)}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋂ i, {x | p i x})

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋂ i, {x | p i x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋃ i, {x | p i x})

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋃ i, {x | p i x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
| a = f x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
| a = f x
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace β
g : β → Finset α
⊢ (∀ (a : α), Measurable fun x ↦ a ∈ ↑(g x)) ↔ ∀ (a : α), Measurable fun x ↦ a ∈ g x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace β
g : β → Finset α
⊢ (∀ (a : α), Measurable fun x ↦ a ∈ ↑(g x)) ↔ ∀ (a : α), Measurable fun x ↦ a ∈ g x
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:
;

Goal state after:
α : 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}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst✝ : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Measurable Sigma.uncurry

Tactic:
by
  refine measurable_pi_lambda _ fun _ ↦ ?_
  simp only [Sigma.uncurry]
  fun_prop

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ #(univ.sigma fun a ↦ range (f ↑a).natAbs) = ∑ a ∈ s, (f a).natAbs

pp: case refine_2
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ a ∈ s,
    (∑ b ∈ univ.sigma fun a ↦ range (f ↑a).natAbs,
        if (fun a ↦ ↑a.fst) b = a then ↑((fun a ↦ sign (f ↑a.fst)) b) else 0) =
      f a

Tactic:
· simp [sum_attach (f := fun a => (f a).natAbs)]

Goal state after:
case refine_2
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ a ∈ s,
    (∑ b ∈ univ.sigma fun a ↦ range (f ↑a).natAbs,
        if (fun a ↦ ↑a.fst) b = a then ↑((fun a ↦ sign (f ↑a.fst)) b) else 0) =
      f a
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:
;

Goal state after:
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
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
h : (fun f ↦ ⇑f.toAlgHom) { toAlgHom := toAlgHom✝, cont := cont✝ } = (fun f ↦ ⇑f.toAlgHom) g
⊢ { toAlgHom := toAlgHom✝, cont := cont✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
h : (fun f ↦ ⇑f.toAlgHom) { toAlgHom := toAlgHom✝, cont := cont✝ } = (fun f ↦ ⇑f.toAlgHom) g
⊢ { toAlgHom := toAlgHom✝, cont := cont✝ } = g
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
⊢ ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g ↔ { toAlgHom := toAlgHom✝, cont := cont✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
⊢ ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g ↔ { toAlgHom := toAlgHom✝, cont := cont✝ } = g
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
⊢ ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔
    { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
⊢ ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔
    { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ (↑n)⁻¹ ≤ 1

Tactic:
exact cast_inv_le_one n

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

Goal state before:
pp: x : ℝ
⊢ ↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)

Tactic:
;

Goal state after:
x : ℝ
⊢ ↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ sign ↑(-x) = -sign ↑x

Tactic:
sign_coe,

Goal state after:
x : ℝ
⊢ sign (-x) = -sign ↑x
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ sign (-x) = -sign ↑x

Tactic:
sign_coe,

Goal state after:
x : ℝ
⊢ sign (-x) = -sign x
Module: Mathlib.Data.EReal.Inv

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

Tactic:
sign_coe,

Goal state after:
x : ℝ
⊢ ↑(sign x) * ↑(↑x).abs = ↑x
Module: Mathlib.Data.EReal.Inv

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

Tactic:
;

Goal state after:
case mp.neg
x y : EReal
h : ↑neg * ↑x.abs ≤ ↑neg * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs
Module: Mathlib.Data.EReal.Inv

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
case mp.pos
x y : EReal
h : ↑pos * ↑x.abs ≤ ↑pos * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
;

Goal state after:
case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
;

Goal state after:
case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
;

Goal state after:
case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (b * a)⁻¹ = b⁻¹ * a⁻¹

Tactic:
rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]

Goal state after:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
;

Goal state after:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case neg_bot
x : ℝ
x_neg : x < 0
⊢ (↑x * ⊥)⁻¹ = (↑x)⁻¹ * ⊥⁻¹

Tactic:
rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]

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

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

Tactic:
sign_coe,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

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

Tactic:
sign_coe,

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

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

Tactic:
sign_coe,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

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

Tactic:
sign_coe,

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ a

Tactic:
;

Goal state after:
case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0

Tactic:
;

Goal state after:
case coe
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : ℝ
h : 0 < ↑a
h' : ↑a ≠ ⊤
⊢ 0 < ↑a⁻¹

Tactic:
;

Goal state after:
a : ℝ
h : 0 < ↑a
h' : ↑a ≠ ⊤
⊢ 0 < ↑a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : ℝ
h' : ¬↑a = ⊤
h : 0 < a
⊢ 0 < a⁻¹

Tactic:
;

Goal state after:
a : ℝ
h' : ¬↑a = ⊤
h : 0 < a
⊢ 0 < a⁻¹
Module: Mathlib.Topology.Semicontinuity.Defs

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

Tactic:
by
  simp_rw [upperHemicontinuous_iff, upperHemicontinuousAt_iff_frequently]

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

Goal state before:
pp: a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ ↑a⁻¹ < 0

Tactic:
;

Goal state after:
a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ ↑a⁻¹ < 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : ℝ
h' : ¬↑a = ⊥
h : a < 0
⊢ a⁻¹ < 0

Tactic:
;

Goal state after:
a : ℝ
h' : ¬↑a = ⊥
h : a < 0
⊢ a⁻¹ < 0
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:
;

Goal state after:
α : 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}
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
⊢ HasOpenCGraph fun x ↦ f x ∩ g x

Tactic:
have : {x : α × β | x.2 ∈ f x.1 ∩ g x.1} =
      {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1} := by ext; simp
  rw [HasOpenCGraph, this]
  exact IsOpen.inter hf hg

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun n ↦ (f n).toNNReal

Tactic:
apply NNReal.summable_coe.1
  refine .of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => ?_) hf.abs
  simp only [le_abs_self, Real.coe_toNNReal', max_le_iff, abs_nonneg, and_self_iff]

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

Goal state before:
pp: case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ b * a / b = a

Tactic:
← mul_div b a b,

Goal state after:
case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ b * (a / b) = a
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)

Tactic:
ENNReal.ofReal,

Goal state after:
α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ↑(∑' (n : α), f n).toNNReal = ∑' (n : α), ↑(f n).toNNReal
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ b ≤ -0

Tactic:
;

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ b ≤ -0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c

Tactic:
;

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c

Tactic:
;

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ (Ioo ⊥ ⊤).OrdConnected

Tactic:
;

Goal state after:
⊢ (Ioo ⊥ ⊤).OrdConnected
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ (Ici 0).OrdConnected

Tactic:
;

Goal state after:
⊢ (Ici 0).OrdConnected
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ IsClosed (Ici 0)

Tactic:
;

Goal state after:
⊢ IsClosed (Ici 0)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
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' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]

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

Goal state before:
pp: α : Type u_4
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)

Tactic:
;

Goal state after:
α : Type u_4
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c

Tactic:
;

Goal state after:
α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c