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

Goal state before:
pp: n : ℕ
r : ℝ
⊢ r.toNNReal < ↑n ↔ r < ↑n ∧ n ≠ 0

Tactic:
simpa using

Goal state after:
n : ℕ
r : ℝ
⊢ r.toNNReal < ↑n ↔ r < ↑n ∧ ¬n = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a

Tactic:
simpa using

Goal state after:
a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
⊢ x⁻¹ < 1 ↔ 1 < x

Tactic:
← one_div,

Goal state after:
x : ℝ≥0
hx : x ≠ 0
⊢ 1 / x < 1 ↔ 1 < x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: x✝ : ℝ
⊢ x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x ↦ ↑x) → a ≤ x} ↔ x✝ ∈ ∅

Tactic:
simpa using

Goal state after:
x✝ : ℝ
⊢ ∃ x, x✝ < ↑x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: x✝ : ℝ
⊢ x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x ↦ ↑x) → x ≤ a} ↔ x✝ ∈ ∅

Tactic:
simpa using

Goal state after:
x✝ : ℝ
⊢ ∃ x, ↑x < x✝
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ 0 ≤ r ∨ 0 ≤ -r

Tactic:
simpa using

Goal state after:
r : ℝ
⊢ 0 ≤ r ∨ r ≤ 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove (range ((fun x_1 ↦ x_1 x) ∘ Subtype.val))

Tactic:
simpa using

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove (range ((fun x ↦ x y) ∘ Subtype.val))

Tactic:
simpa using

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove ((fun x ↦ x y) '' s)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ (↑a).toReal ≤ ↑b

Tactic:
simpa using

Goal state after:
b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ a ≤ b
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: b a : ℝ≥0
h : ↑a = ∞ → ↑b = ∞
h_nnreal : ↑a ≠ ∞ → ↑b ≠ ∞ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b

Tactic:
simpa using

Goal state after:
b a : ℝ≥0
h : ↑a = ∞ → ↑b = ∞
h_nnreal : ↑a ≠ ∞ → ↑b ≠ ∞ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ a ≤ b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ p 1 + q (x / 1) ≤ q x

Tactic:
simpa using

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ q x ≤ q x
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b = ∑ x ∈ f.support, φ ↑(f x)

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b = ∑ x ∈ f.support, φ ↑(f x)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : AddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa using

Goal state after:
R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : AddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ (↑b).toReal

Tactic:
simpa using

Goal state after:
a : ℝ
b : ℝ≥0
⊢ a.toNNReal ≤ b ↔ a ≤ ↑b
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
b : ℝ≥0
⊢ ENNReal.ofReal a < ↑b ↔ a < (↑b).toReal

Tactic:
simpa using

Goal state after:
a : ℝ
ha : 0 ≤ a
b : ℝ≥0
⊢ a.toNNReal < b ↔ a < ↑b
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: b : ℝ
hb : 0 ≤ b
a : ℝ≥0
⊢ ↑a ≤ ENNReal.ofReal b ↔ (↑a).toReal ≤ b

Tactic:
simpa using

Goal state after:
b : ℝ
hb : 0 ≤ b
a : ℝ≥0
⊢ a ≤ b.toNNReal ↔ ↑a ≤ b
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: b : ℝ
a : ℝ≥0
⊢ ↑a < ENNReal.ofReal b ↔ (↑a).toReal < b

Tactic:
simpa using

Goal state after:
b : ℝ
a : ℝ≥0
⊢ a < b.toNNReal ↔ ↑a < b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove (range ((fun x_1 ↦ x_1 x) ∘ Subtype.val))

Tactic:
simpa using

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove (range ((fun x ↦ x y) ∘ Subtype.val))

Tactic:
simpa using

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ BddAbove ((fun x ↦ x y) '' s)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p : ℝ≥0∞
⊢ p = 0 ∨ p = ∞ ∨ 0 < p.toReal

Tactic:
simpa using

Goal state after:
p : ℝ≥0∞
⊢ ¬p = 0 → ¬p = ∞ → 0 < p.toReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ∞ ∨
      0 = 0 ∧ 0 < q.toReal ∨
        0 = ∞ ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal

Tactic:
simpa using

Goal state after:
case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ q = 0 ∨ q = ∞ ∨ 0 < q.toReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ∞
⊢ p = 0 ∧ ∞ = 0 ∨
    p = 0 ∧ ∞ = ∞ ∨
      p = 0 ∧ 0 < ∞.toReal ∨ p = ∞ ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ 0 < ∞.toReal ∧ p.toReal ≤ ∞.toReal

Tactic:
simpa using

Goal state after:
case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ∞
⊢ p = 0 ∨ p = ∞ ∨ 0 < p.toReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ p = ∞ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal

Tactic:
simpa using

Goal state after:
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ p = ∞ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
have h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁ :=
    (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : GroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa using

Goal state after:
R : Type u_1
E : Type u_3
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : GroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : NonarchAddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa using

Goal state after:
R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : NonarchAddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑J₁ / spanSingleton R⁰ ((algebraMap R K) a₁) = ↑J / spanSingleton R⁰ ((algebraMap R K) a)
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
div_eq_div_iff h_a₁' h_a',

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑J₁ * spanSingleton R⁰ ((algebraMap R K) a) = ↑J * spanSingleton R⁰ ((algebraMap R K) a₁)
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * b = a ↔ b = 1

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * b = a ↔ b = 1
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b = b ↔ a = 1

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b = b ↔ a = 1
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a : ℝ≥0∞
⊢ a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0

Tactic:
simpa using

Goal state after:
a : ℝ≥0∞
⊢ a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ∞ → a = ∞
hc : c = ∞ → a = ∞
⊢ b + c = ∞ → a = ∞

Tactic:
simpa using

Goal state after:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ∞ → a = ∞
hc : c = ∞ → a = ∞
⊢ (b = ∞ → a = ∞) ∧ (c = ∞ → a = ∞)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
⊢ a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
⊢ a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y : ℝ≥0
⊢ ofNNReal '' uIoc x y = uIoc ↑x ↑y

Tactic:
by simp [uIoc]

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

Goal state before:
pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
f : ι → ℝ≥0
⊢ (⨅ i, ↑(f i)).toNNReal = ⨅ i, ((fun i ↦ ↑(f i)) i).toNNReal

Tactic:
simp_rw [← coe_iInf, toNNReal_coe]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup G
inst✝² : PartialOrder G
inst✝¹ : MulAction 𝕜 G
inst✝ : PosSMulMono 𝕜 G
_a : 𝕜
ha : 0 < _a
b₁ b₂ : G
h : _a • b₁ ≤ _a • b₂
⊢ b₁ ≤ b₂

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
G : Type u_2
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup G
inst✝² : PartialOrder G
inst✝¹ : MulAction 𝕜 G
inst✝ : PosSMulMono 𝕜 G
_a : 𝕜
ha : 0 < _a
b₁ b₂ : G
h : _a • b₁ ≤ _a • b₂
⊢ b₁ ≤ b₂
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup G
inst✝² : PartialOrder G
inst✝¹ : MulActionWithZero 𝕜 G
inst✝ : PosSMulStrictMono 𝕜 G
a : 𝕜
ha : 0 < a
b₁ b₂ : G
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
G : Type u_2
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup G
inst✝² : PartialOrder G
inst✝¹ : MulActionWithZero 𝕜 G
inst✝ : PosSMulStrictMono 𝕜 G
a : 𝕜
ha : 0 < a
b₁ b₂ : G
h : a • b₁ < a • b₂
⊢ b₁ < b₂
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y z : ℝ≥0∞
h : ∀ y' > y, ∀ z' > z, x ≤ y' + z'
⊢ x ≤ y + z

Tactic:
simpa using

Goal state after:
x y z : ℝ≥0∞
h : ∀ y' > y, ∀ z' > z, x ≤ y' + z'
⊢ x ≤ y + z
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ y + z ≤ x

Tactic:
simpa using

Goal state after:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ y + z ≤ x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
hx : 0 < ↑x
h'x : ↑x ≠ ⊤
⊢ 0 < (↑x).toReal

Tactic:
simpa using

Goal state after:
x : ℝ
hx : 0 < ↑x
h'x : ↑x ≠ ⊤
⊢ 0 < x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
hx : ↑x < 0
h'x : ↑x ≠ ⊥
⊢ (↑x).toReal < 0

Tactic:
simpa using

Goal state after:
x : ℝ
hx : ↑x < 0
h'x : ↑x ≠ ⊥
⊢ x < 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
y : ℝ
hy0 : 0 < ↑y
right✝ : ↑y < ⊤
⊢ (↑y).toReal ∈ Ioi 0

Tactic:
simpa using

Goal state after:
case mp
y : ℝ
hy0 : 0 < ↑y
right✝ : ↑y < ⊤
⊢ 0 < y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case h
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑x ∈ Ioo 0 ⊤ ∧ (↑x).toReal = x

Tactic:
simpa using

Goal state after:
case h
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
y : ℝ
left✝ : ⊥ < ↑y
hy0 : ↑y < 0
⊢ (↑y).toReal ∈ Iio 0

Tactic:
simpa using

Goal state after:
case mp
y : ℝ
left✝ : ⊥ < ↑y
hy0 : ↑y < 0
⊢ y < 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case h
x : ℝ
hx : x ∈ Iio 0
⊢ ↑x ∈ Ioo ⊥ 0 ∧ (↑x).toReal = x

Tactic:
simpa using

Goal state after:
case h
x : ℝ
hx : x ∈ Iio 0
⊢ x < 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ (↑x).toReal ≤ (↑y).toReal

Tactic:
simpa using

Goal state after:
x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ x ≤ y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: r p : ℝ≥0
⊢ ↑(p / r) ≤ ↑p / ↑r

Tactic:
simpa using

Goal state after:
r p : ℝ≥0
⊢ ↑p * ↑r⁻¹ ≤ ↑p * (↑r)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1⁻¹ = 1

Tactic:
simpa using

Goal state after:
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1⁻¹ = 1
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: a : ℝ
x✝ : ↑a < ⊤
b : ℚ
hab : a < ↑b
⊢ ↑a < ↑↑b

Tactic:
simpa using

Goal state after:
a : ℝ
x✝ : ↑a < ⊤
b : ℚ
hab : a < ↑b
⊢ a < ↑b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: a : ℝ
x✝ : ⊥ < ↑a
b : ℚ
hab : ↑b < a
⊢ ↑↑b < ↑a

Tactic:
simpa using

Goal state after:
a : ℝ
x✝ : ⊥ < ↑a
b : ℚ
hab : ↑b < a
⊢ ↑b < a
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
simpa using

Goal state after:
x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ ¬x = ⊥ ∧ ¬x = ⊤
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ∞

Tactic:
simpa using

Goal state after:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → ¬c = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
⊢ a⁻¹ < b ↔ b⁻¹ < a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
⊢ a < b⁻¹ ↔ b < a⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a = 0

Tactic:
simpa using

Goal state after:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
⊢ ∃ c, 0 < c ∧ c * a < b

Tactic:
by
  obtain rfl | hb := eq_or_ne b ∞
  · exact ⟨1, by simpa [lt_top_iff_ne_top]⟩
  refine ⟨b / (a + 1), ENNReal.div_pos hb₀ (by finiteness), ENNReal.mul_lt_of_lt_div ?_⟩
  gcongr
  exact ENNReal.lt_add_right ha one_ne_zero

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

Goal state before:
pp: a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
← one_div,

Goal state after:
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ 1 / a ≤ b ↔ 1 ≤ a * b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1

Tactic:
← one_div,

Goal state after:
a b : ℝ≥0∞
⊢ a ≤ 1 / b ↔ a * b ≤ 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
h : a * b = 1
⊢ a = b⁻¹

Tactic:
← mul_one a,

Goal state after:
a b : ℝ≥0∞
h : a * b = 1
⊢ a * 1 = b⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ 1 - 2⁻¹ = 2⁻¹

Tactic:
← one_div,

Goal state after:
⊢ 1 - 1 / 2 = 1 / 2
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) x < (fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) y

pp: case refine_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
⊢ ↑((fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) ((fun x ↦ ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x

Tactic:
· simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]

Goal state after:
case refine_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
⊢ ↑((fun x ↦ ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) ((fun x ↦ ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝

Tactic:
simpa using

Goal state after:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ a✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ∞

Tactic:
simpa using

Goal state after:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a < ∞ ∨ a✝ = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ y ≠ 0

Tactic:
simpa using

Goal state after:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ¬y = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0

Tactic:
simpa using

Goal state after:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ¬x = 0
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ 0 < ε - edist y x

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ edist y x < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inr.inr
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
⊢ dist a x + dist x b ≤ C + C

Tactic:
simpa using

Goal state after:
case inr.inr
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
⊢ dist x a + dist x b ≤ C + C
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ x ≠ 0

Tactic:
simpa using

Goal state after:
m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ¬x = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
⊢ 0 ≤ m

Tactic:
simpa using

Goal state after:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
⊢ 0 ≤ m
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case neg.inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ∞ ≠ 0
i : ι
hi : ¬f i = 0
⊢ ∞ * ⨆ i, f i = ⨆ i, ∞ * f i

Tactic:
simpa using

Goal state after:
case neg.inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ∞ ≠ 0
i : ι
hi : ¬f i = 0
⊢ ⨆ i, ∞ * f i = ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
simpa using

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≠ 0 ↔ x ≠ y

Tactic:
simpa using

Goal state after:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y = 0 ↔ x = y
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≤ 0 ↔ x = y

Tactic:
simpa using

Goal state after:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≤ 0 ↔ x = y