mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inr.inl
α✝ : 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}
x : α
hx : x ∈ s
ht : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ s ∪ ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

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
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

Tactic:
·

Goal state after:
case inr.inl
α✝ : 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}
x : α
hx : x ∈ s
ht : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ s ∪ ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inr.inl
α✝ : 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}
x : α
hx : x ∈ s
ht : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ s ∪ ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

Tactic:
union_empty

Goal state after:
case inr.inl
α✝ : 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}
x : α
hx : x ∈ s
ht : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hI
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0

pp: case h_aJ
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J

Tactic:
·

Goal state after:
case hI
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)

Tactic:
·

Goal state after:
case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h_aJ
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J

Tactic:
·

Goal state after:
case h_aJ
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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
J : Ideal R
hJ : J = 0
⊢ 0 ≤ count K v ↑J

pp: case neg
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
J : Ideal R
hJ : ¬J = 0
⊢ 0 ≤ count K v ↑J

Tactic:
·

Goal state after:
case pos
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
J : Ideal R
hJ : J = 0
⊢ 0 ≤ count K v ↑J
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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
J : Ideal R
hJ : ¬J = 0
⊢ 0 ≤ count K v ↑J

Tactic:
·

Goal state after:
case neg
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
J : Ideal R
hJ : ¬J = 0
⊢ 0 ≤ count K v ↑J
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case mp
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ 0 < x ∧ x < ∞ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

pp: case mpr
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ∞

Tactic:
·

Goal state after:
case mp
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ 0 < x ∧ x < ∞ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
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
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

pp: α✝ : 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, ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
·

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
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case mpr
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ∞

Tactic:
·

Goal state after:
case mpr
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case mpr.left
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x

pp: case mpr.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ∞

Tactic:
·

Goal state after:
case mpr.left
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : J = 0
⊢ count K v J ≤ count K v I

pp: case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
⊢ count K v J ≤ count K v I

Tactic:
·

Goal state after:
case pos
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : J = 0
⊢ count K v J ≤ count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case mpr.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ∞

Tactic:
·

Goal state after:
case mpr.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b

pp: case ofNat.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

pp: case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

pp: case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b

Tactic:
·

Goal state after:
case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

pp: case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

pp: case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b

Tactic:
·

Goal state after:
case ofNat.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

pp: case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b

Tactic:
·

Goal state after:
case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b

Tactic:
·

Goal state after:
case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ 0 ≤ count K v ↑J'

pp: case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ ↑J' ≠ 0

Tactic:
·

Goal state after:
case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ 0 ≤ count K v ↑J'
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ ↑J' ≠ 0

Tactic:
·

Goal state after:
case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ ↑J' ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

pp: case inr
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
·

Goal state after:
case inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
⊢ x ^ (-m) = (x ^ m)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
⊢ x ^ (-m) = (x ^ m)⁻¹

pp: case inr.inr
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x ≠ ∞
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
·

Goal state after:
case inr.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
⊢ x ^ (-m) = (x ^ m)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case pos
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

pp: case neg
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
·

Goal state after:
case pos
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i
Module: Mathlib.Data.ENNReal.Inv

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

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

Tactic:
·

Goal state after:
case neg.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ 0 * ⨆ i, f i = ⨆ i, 0 * f i
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, f i = ⨆ i, ∞ * f i

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

Tactic:
·

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

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

Tactic:
·

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

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

pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : 0 = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : 0 = 0 → Nonempty ι
⊢ 0 * ⨅ i, f i = ⨅ i, 0 * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i

pp: case inr.inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
·

Goal state after:
case inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i

pp: case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i

Tactic:
·

Goal state after:
case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i

Tactic:
·

Goal state after:
case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case e_toBornology
α : Type u_3
toDist✝ : Dist α
dist_self✝¹ : ∀ (x : α), dist x x = 0
dist_comm✝¹ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝¹ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝¹ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝¹ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝¹ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝¹ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB }.toDist
edist✝ : α → α → ℝ≥0∞
toUniformSpace✝ : UniformSpace α
toBornology✝ : Bornology α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α :=
  { toDist := d, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝, edist := edist✝,
      edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU', toBornology := toBornology✝,
      cobounded_sets := hB' }.toDist
⊢ toBornology✝¹ = toBornology✝

Tactic:
·

Goal state after:
case e_toBornology
α : Type u_3
toDist✝ : Dist α
dist_self✝¹ : ∀ (x : α), dist x x = 0
dist_comm✝¹ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝¹ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝¹ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝¹ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝¹ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝¹ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB }.toDist
edist✝ : α → α → ℝ≥0∞
toUniformSpace✝ : UniformSpace α
toBornology✝ : Bornology α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α :=
  { toDist := d, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝, edist := edist✝,
      edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU', toBornology := toBornology✝,
      cobounded_sets := hB' }.toDist
⊢ toBornology✝¹ = toBornology✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
·

Goal state after:
case inr.inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨅ i, f i = ⨅ i, a * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
· exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iInf _

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

Goal state before:
pp: case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ (closedBall x r).Subsingleton

pp: case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ (closedBall x 0).Subsingleton

Tactic:
·

Goal state after:
case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ (closedBall x r).Subsingleton
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ (closedBall x 0).Subsingleton

Tactic:
·

Goal state after:
case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ (closedBall x 0).Subsingleton
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: case a
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y ≤ dist 1 (x⁻¹ * y)

pp: case a
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist 1 (x⁻¹ * y) ≤ dist x y

Tactic:
·

Goal state after:
case a
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y ≤ dist 1 (x⁻¹ * y)
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: case a
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist 1 (x⁻¹ * y) ≤ dist x y

Tactic:
·

Goal state after:
case a
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist 1 (x⁻¹ * y) ≤ dist x y
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

pp: case neg
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
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
·

Goal state after:
case pos
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
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0