mathlib-initiative/mathlib-tactics huggingface dataset:
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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))⁻¹

Tactic:
[

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))⁻¹
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
p : GroupSeminorm E
f : F →* E
⊢ p (f 1) = 0

Tactic:
[

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
p : GroupSeminorm E
f : F →* E
⊢ p (f 1) = 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
p : GroupSeminorm E
f : F →* E
x : F
⊢ p (f x⁻¹) = p (f x)

Tactic:
[

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
p : GroupSeminorm E
f : F →* E
x : F
⊢ p (f x⁻¹) = p (f x)
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
⊢ ⨅ x_1, p x_1⁻¹ + q (x⁻¹ / x_1⁻¹) = ⨅ y, p y + q (x / y)

Tactic:
[

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
⊢ ⨅ x_1, p x_1⁻¹ + q (x⁻¹ / x_1⁻¹) = ⨅ y, p y + q (x / y)
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
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x : E
⊢ (if -x = 0 then 0 else 1) = if x = 0 then 0 else 1

Tactic:
[

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
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x : E
⊢ (if -x = 0 then 0 else 1) = if x = 0 then 0 else 1
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
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x : E
⊢ r • p (-x) = r • p x

Tactic:
[

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
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x : E
⊢ r • p (-x) = r • p x
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✝ p q : NonarchAddGroupSeminorm E
x : E
⊢ (⇑p ⊔ ⇑q) (-x) = (⇑p ⊔ ⇑q) x

Tactic:
[

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✝ p q : NonarchAddGroupSeminorm E
x : E
⊢ (⇑p ⊔ ⇑q) (-x) = (⇑p ⊔ ⇑q) x
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✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x : E
⊢ (if x⁻¹ = 1 then 0 else 1) = if x = 1 then 0 else 1

Tactic:
[

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✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x : E
⊢ (if x⁻¹ = 1 then 0 else 1) = if x = 1 then 0 else 1
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✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x : E
⊢ r • p x⁻¹ = r • p x

Tactic:
[

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✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x : E
⊢ r • p x⁻¹ = r • p x
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
[

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
[

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
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
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
⊢ r • p (x + y) ≤ max (r • p x) (r • p y)

Tactic:
by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ←
          mul_max_of_nonneg _ _ NNReal.zero_le_coe]
        gcongr
        apply map_add_le_max

Goal state after:
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
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x : E
⊢ r • p (-x) = r • p x

Tactic:
[

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
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x : E
⊢ r • p (-x) = r • p x
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ c + a - (c + b) = a - b

Tactic:
[

Goal state after:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ c + a - (c + b) = a - b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
ofReal_of_nonpos (sub_nonpos_of_le h),

Goal state after:
case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ 0 = ENNReal.ofReal p - ENNReal.ofReal q
Module: Mathlib.Data.ENNReal.Operations

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

Tactic:
[

Goal state after:
case inr
ι : Sort u_1
h✝ : Nonempty ι
f : ι → ℝ≥0
⊢ (⨅ i, ↑(f i)).toNNReal = ⨅ i, (↑(f i)).toNNReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g

Tactic:
[

Goal state after:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g

Tactic:
[

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
[

Goal state after:
ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, (↑(f i)).toNNReal

Tactic:
[

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, (↑(f i)).toNNReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
[

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
[

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
hx : ⊥ ≠ ⊤ ∧ ⊥ ≠ ⊥
⊢ ∃ y, ↑y = ⊥

Tactic:
simp at hx

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

Goal state before:
pp: case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤

Tactic:
simp at hx

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

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
[

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mpr
x : ℝ
⊢ x ∈ Ioi 0 → x ∈ toReal '' Ioo 0 ⊤

Tactic:
intro hx
    use (x : EReal)
    simpa using hx

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

Goal state before:
pp: case mpr
x : ℝ
⊢ x ∈ Iio 0 → x ∈ toReal '' Ioo ⊥ 0

Tactic:
intro hx
    use (x : EReal)
    simpa using hx

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

Goal state before:
pp: x y : ℝ
⊢ WithBot.some '' WithTop.some '' Icc x y = Icc ↑x ↑y

Tactic:
rw [WithTop.image_coe_Icc, WithBot.image_coe_Icc]

Goal state after:
x y : ℝ
⊢ Icc ↑↑x ↑↑y = Icc ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Icc ↑x ↑y = Icc x y

Tactic:
[

Goal state after:
x y : ℝ
⊢ Real.toEReal ⁻¹' Icc ↑x ↑y = Icc x y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ico ↑x ↑y = Ico x y

Tactic:
[

Goal state after:
x y : ℝ
⊢ Real.toEReal ⁻¹' Ico ↑x ↑y = Ico x y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ↑x ↑y = Ioc x y

Tactic:
[

Goal state after:
x y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ↑x ↑y = Ioc x y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y

Tactic:
[

Goal state after:
x y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
hx : 0 ≤ x
h : ¬x = ⊤
⊢ x.toENNReal.toReal = x.toReal

Tactic:
· simp [h, toReal_nonneg hx]

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

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c

Tactic:
[

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

Goal state before:
pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
rw [← ENNReal.mul_le_mul_iff_left hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]

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

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

Tactic:
rw [← inv_inv c]

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

Goal state before:
pp: a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ b' < b, c < a * b'

Tactic:
[

Goal state after:
a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ b' < b, c < a * b'
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s

Tactic:
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩

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

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

Tactic:
simpa only [not_le] using not_congr dist_le_zero

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

Goal state before:
pp: R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
[

Goal state after:
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
← smul_one_mul c (sSup s),

Goal state after:
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • 1 * sSup s = ⨆ a ∈ s, c • a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal (x / y) ≤ ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
[

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal (x / y) ≤ ENNReal.ofReal x / ENNReal.ofReal y
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ i, a * f i = ⨆ i, f i * a

Tactic:
[

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ i, a * f i = ⨆ i, f i * a
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ

Tactic:
[

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded s

Tactic:
rw [hs]
    exact totallyBounded_empty

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
hq : p' ∈ s
⊢ a p' = ∑ p ∈ s, a p - ∑ q ∈ s \ {p'}, a q

Tactic:
rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem hp's, add_sub_cancel_right]

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

Goal state before:
pp: α : Type u_2
inst✝ : EMetricSpace α
⊢ Nontrivial α ↔ NontrivialTopology α

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : EMetricSpace α
⊢ Nontrivial α ↔ NontrivialTopology α
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inl.mk
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
fst✝ : α
snd✝ : β
⊢ sphere (fst✝, snd✝) 0 = sphere fst✝ 0 ×ˢ closedBall snd✝ 0 ∪ closedBall fst✝ 0 ×ˢ sphere snd✝ 0

Tactic:
[

Goal state after:
case inr.inl.mk
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
fst✝ : α
snd✝ : β
⊢ sphere (fst✝, snd✝) 0 = sphere fst✝ 0 ×ˢ closedBall snd✝ 0 ∪ closedBall fst✝ 0 ×ˢ sphere snd✝ 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ (x', y') ∈ sphere x r ↔ (x', y') ∈ sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
[

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ (x', y') ∈ sphere x r ↔ (x', y') ∈ sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {x} ⊔ Ideal.span {y} = Ideal.span {x, y_1}

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {x} ⊔ Ideal.span {y} = Ideal.span {x, y_1}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ Ioi a ∩ interior (Iio b) = Ioo a b

Tactic:
interior_Iio,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ Ioi a ∩ Iio b = Ioo a b
Module: Mathlib.Topology.EMetricSpace.Pi

Goal state before:
pp: β : Type v
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → EDist (X b)
f g : (b : β) → X b
d : ℝ≥0∞
⊢ (∀ b ∈ Finset.univ, edist (f b) (g b) ≤ d) ↔ ∀ (b : β), edist (f b) (g b) ≤ d

Tactic:
by simp only [Finset.mem_univ, forall_const]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ ((∃ x, ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
[

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ ((∃ x, ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g = ↑r ↔ (∃ i, dist (f i) (g i) = ↑r) ∧ ∀ (b : β), dist (f b) (g b) ≤ ↑r

Tactic:
[

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g = ↑r ↔ (∃ i, dist (f i) (g i) = ↑r) ∧ ∀ (b : β), dist (f b) (g b) ≤ ↑r
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
⊢ (edist (mk x') (mk y)).toReal = (edist (mk x') (mk y')).toReal

Tactic:
mk_eq_mk.2 hy

Goal state after:
α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
⊢ (edist (mk x') (mk y')).toReal = (edist (mk x') (mk y')).toReal
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
hy : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)

Tactic:
simpa using! exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
rw [← ofReal_norm, norm_of_nonneg hr]

Goal state after: