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

Goal state before:
pp: case mk
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 : NonarchAddGroupNorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
eq_zero_of_map_eq_zero'✝¹ :
  ∀ (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }.toFun x = 0 → x = 0
toNonarchAddGroupSeminorm✝ : NonarchAddGroupSeminorm E
eq_zero_of_map_eq_zero'✝ : ∀ (x : E), toNonarchAddGroupSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun)
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }

Tactic:
;

Goal state after:
case mk
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 : NonarchAddGroupNorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
eq_zero_of_map_eq_zero'✝¹ :
  ∀ (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }.toFun x = 0 → x = 0
toNonarchAddGroupSeminorm✝ : NonarchAddGroupSeminorm E
eq_zero_of_map_eq_zero'✝ : ∀ (x : E), toNonarchAddGroupSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun)
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
y : α
hy : y ∈ s.ordConnectedSection
x : ↑s
h : [[s.ordConnectedProj x, y]] ⊆ s
⊢ s.ordConnectedProj x = y

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
y : α
hy : y ∈ s.ordConnectedSection
x : ↑s
h : [[s.ordConnectedProj x, y]] ⊆ s
⊢ s.ordConnectedProj x = y
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
      disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset

Goal state after:
case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a : ℝ≥0
⊢ ∞ - ↑a = ∞

Tactic:
;

Goal state after:
a : ℝ≥0
⊢ ∞ - ↑a = ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

pp: case inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
⊢ (a - b) * c = a * c - b * c

Tactic:
;

Goal state after:
case inl
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

case inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
⊢ (a - b) * c = a * c - b * c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr.inl
a c : ℝ≥0∞
h : 0 < 0 → 0 < a → c ≠ ∞
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c

pp: case inr.inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c

Tactic:
;

Goal state after:
case inr.inl
a c : ℝ≥0∞
h : 0 < 0 → 0 < a → c ≠ ∞
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c

case inr.inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a : ℝ≥0∞
b : ℝ≥0
⊢ (a - ↑b).toNNReal = a.toNNReal - (↑b).toNNReal

Tactic:
;

Goal state after:
a : ℝ≥0∞
b : ℝ≥0
⊢ (a - ↑b).toNNReal = a.toNNReal - (↑b).toNNReal
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₁ * Ideal.span {a}) = ↑(J * Ideal.span {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)
⊢ ¬J = 0

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
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₁ * Ideal.span {a}) = ↑(J * Ideal.span {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)
⊢ ¬J = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ ⨅ i, f i + a = ⨅ b, a + f b

Tactic:
;

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ ⨅ i, f i + a = ⨅ b, a + f b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: p : EReal → Prop
r : EReal
hr : p r
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
;

Goal state after:
p : EReal → Prop
r : EReal
hr : p r
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r
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 ≤ ⨅ i, ⨅ b, f i + g b

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 ≤ ⨅ i, ⨅ b, f i + g b
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₁ * Ideal.span {a}) = ↑(J * Ideal.span {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)
⊢ ¬choose ⋯ = 0

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
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₁ * Ideal.span {a}) = ↑(J * Ideal.span {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)
⊢ ¬choose ⋯ = 0
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₁ * Ideal.span {a}) = ↑(J * Ideal.span {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)
⊢ ¬Ideal.span {a} = 0

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
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₁ * Ideal.span {a}) = ↑(J * Ideal.span {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)
⊢ ¬Ideal.span {a} = 0
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ¬a = 0

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
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ¬a = 0
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
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ 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
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ ¬a' = 0

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
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ ¬a' = 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: ⊢ range Real.toEReal = {⊥, ⊤}ᶜ

Tactic:
ext x
  induction x <;> simp

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

Goal state before:
pp: ⊢ range Real.toEReal = Ioo ⊥ ⊤

Tactic:
ext x
  induction x <;> simp

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

Goal state before:
pp: a : ℝ≥0
h0 : ¬a = 0
⊢ ↑a * (↑a)⁻¹ = 1

Tactic:
;

Goal state after:
a : ℝ≥0
h0 : ¬a = 0
⊢ ↑a * (↑a)⁻¹ = 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ a * (a⁻¹ * b) = b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0
  · simp_all
  obtain rfl | ha := eq_or_ne a ⊤
  · simp_all
  · simp [← mul_assoc, ENNReal.mul_inv_cancel, *]

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

Goal state before:
pp: case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
⊢ a * b * b⁻¹ = a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Goal state after:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞ * ∞⁻¹ = a

case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b * b⁻¹ = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
⊢ a * b⁻¹ * b = a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Goal state after:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞⁻¹ * ∞ = a

case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b⁻¹ * b = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case top
a : ℝ≥0
h : ↑a < ∞
⊢ ∞⁻¹ < (↑a)⁻¹

pp: case coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
;

Goal state after:
case top
a : ℝ≥0
h : ↑a < ∞
⊢ ∞⁻¹ < (↑a)⁻¹

case coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inl
x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹

pp: case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
;

Goal state after:
case coe.inl
x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹

case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ∞
⊢ a / c ≤ b

pp: case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ∞
⊢ a / c ≤ b

Tactic:
;

Goal state after:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ∞
⊢ a / c ≤ b

case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ∞
⊢ a / c ≤ b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a c a' : ℝ≥0∞
ha' : a' < a
hc✝ : c < a * 0
hc : c / 0 < a'
⊢ False

Tactic:
;

Goal state after:
a c a' : ℝ≥0∞
ha' : a' < a
hc✝ : c < a * 0
hc : c / 0 < a'
⊢ False
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b a' : ℝ≥0∞
ha' : a' < a
hc✝ : ∞ < a * b
hc : ∞ / b < a'
⊢ False

Tactic:
;

Goal state after:
a b a' : ℝ≥0∞
ha' : a' < a
hc✝ : ∞ < a * b
hc : ∞ / b < a'
⊢ False
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
;

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

Goal state before:
pp: α : Type u_2
m' : PseudoEMetricSpace α
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    m'.toEDist
⊢ { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U, uniformity_edist := hU } =
    m'

Tactic:
;

Goal state after:
α : Type u_2
m' : PseudoEMetricSpace α
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    m'.toEDist
⊢ { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U, uniformity_edist := hU } =
    m'
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u_2
ed : EDist α
edist_self✝¹ : ∀ (x : α), edist x x = 0
edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := ed, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U', uniformity_edist := hU' }.toEDist
⊢ { toEDist := ed, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
      toUniformSpace := U, uniformity_edist := hU } =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U', uniformity_edist := hU' }

Tactic:
;

Goal state after:
α : Type u_2
ed : EDist α
edist_self✝¹ : ∀ (x : α), edist x x = 0
edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := ed, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U', uniformity_edist := hU' }.toEDist
⊢ { toEDist := ed, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
      toUniformSpace := U, uniformity_edist := hU } =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U', uniformity_edist := hU' }
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ 0 ≤ ε

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ 0 ≤ ε
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ 0 < ∞

Tactic:
;

Goal state after:
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ 0 < ∞
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
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 t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
Cs : ℝ
hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs
⊢ ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
;

Goal state after:
α✝ : 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 t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
Cs : ℝ
hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs
⊢ ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' eball a r = eball (↑a) r ∩ {a | p a}

Tactic:
rw [← preimage_eball, image_preimage_eq_inter_range, range_val_subtype]

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

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
x x✝ : γ
⊢ x✝ ∈ closedEBall x 0 ↔ x✝ ∈ {x}

Tactic:
;

Goal state after:
γ : Type w
inst✝ : EMetricSpace γ
x x✝ : γ
⊢ x✝ ∈ closedEBall x 0 ↔ x✝ ∈ {x}