mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
y : EReal
hy : 0 ≤ y
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝).toENNReal = y.toENNReal ↔ ↑a✝ = y

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝).toENNReal = ⊥.toENNReal ↔ ↑a✝ = ⊥

case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹).toENNReal = (↑a✝).toENNReal ↔ ↑a✝¹ = ↑a✝

case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊤
⊢ (↑a✝).toENNReal = ⊤.toENNReal ↔ ↑a✝ = ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊤
⊢ ⊤.toENNReal = y.toENNReal ↔ ⊤ = y

Tactic:
induction y

Goal state after:
case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ ⊤.toENNReal = ⊥.toENNReal ↔ ⊤ = ⊥

case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ⊤.toENNReal = (↑a✝).toENNReal ↔ ⊤ = ↑a✝

case top.top
hx hy : 0 ≤ ⊤
⊢ ⊤.toENNReal = ⊤.toENNReal ↔ ⊤ = ⊤
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
⊢ a / (a / b) = b

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0
  · simp [h₀]
  obtain rfl | ha' := eq_or_ne a ∞
  · simp [h₁, top_div_of_lt_top]
  rw [ENNReal.div_eq_inv_mul, ENNReal.inv_div (Or.inr ha') (Or.inr ha),
    ENNReal.div_mul_cancel ha ha']

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

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

Tactic:
edist_comm z

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: case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z

Tactic:
rw [edist_comm] at h

Goal state after:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z
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:
· simp only [zpow_negSucc, ENNReal.inv_le_inv]
    apply pow_right_mono₀ hx
    simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.natCast_add, Int.ofNat_one] using! h

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

Goal state before:
pp: x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
⊢ x ^ a ≤ x ^ b

Tactic:
by
  obtain a | a := a <;> obtain b | b := b
  · simp only [Int.ofNat_eq_natCast, zpow_natCast]
    exact pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)
  · apply absurd h (not_le_of_gt _)
    exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.natCast_nonneg _)
  · simp only [zpow_negSucc, Int.ofNat_eq_natCast, zpow_natCast]
    refine (ENNReal.inv_le_one.2 ?_).trans ?_ <;> exact one_le_pow_of_one_le' hx _
  · simp only [zpow_negSucc, ENNReal.inv_le_inv]
    apply pow_right_mono₀ hx
    simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.natCast_add, Int.ofNat_one] using! h

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
⊢ (uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace ≤ e

Tactic:
let hα := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y))
      (fun x ↦ edist_self (f x)) (fun x y ↦ edist_comm (f x) (f y))
      (fun x y z ↦ edist_triangle (f x) (f y) (f z))

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
⊢ (uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace ≤ e
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
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_notMem : ¬v ∈ {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}
⊢ False

Tactic:
mem_union,

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
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_notMem : ¬(v ∈ {v | v.asIdeal ∣ J} ∨ v ∈ {v | v.asIdeal ∣ Ideal.span {a}})
⊢ False
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε

Tactic:
rw [mem_closedBall', mem_closedBall]

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

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∀ᶠ (y : α × ι) in 𝓝 x₀ ×ˢ f, p y.swap) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
Metric.eventually_nhds_prod_iff

Goal state after:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s

Tactic:
rw [zero_smul_set hs, zero_smul]

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sSup s

Tactic:
rw [zero_smul_set hs, zero_smul]

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup 0 = 0
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sSup s

Tactic:
rw [zero_smul_set hs, zero_smul]

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ closedEBall x ↑ε = closedBall x ↑ε

Tactic:
rw [← closedEBall_ofReal ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x✝¹ x✝ : X
⊢ edist x✝¹ x✝ = ENNReal.ofReal (dist x✝¹ x✝)

Tactic:
simp only [h]

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sInf s

Tactic:
rw [zero_smul_set hs, zero_smul]

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup 0 = 0
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure[inst✝¹] (Subtype.val '' t)
⊢ Dense t

Tactic:
rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]

Goal state after:
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ DiscreteTopology α ↔ OrderTopology α

Tactic:
refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩
  rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_preorderTopology]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ a * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c *
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den))

Tactic:
mul_comm a,

Goal state after:
case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) * a *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c *
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den))
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
⊢ MonotoneOn f (insert x s)

Tactic:
have : (𝓝[s] x).NeBot := hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
⊢ MonotoneOn f (insert x s)
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1
    obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2
    refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_ge h)) fun h ↦ hu x (le_of_not_ge h)

Goal state after:
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H' : ¬I'.divMod I J' = 0
⊢ spanSingleton R⁰ (I'.divMod I J') ≠ 0

Tactic:
by simpa [spanSingleton_eq_zero_iff] using H'

Goal state after:
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this :
  (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓
      (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * (spanSingleton R⁰ (I'.divMod I J') * I) =
    J
H' : ¬I'.divMod I J' = 0
⊢ spanSingleton R⁰ (I'.divMod I J') ≠ 0

Tactic:
by simpa [spanSingleton_eq_zero_iff] using H'

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α✝
α : Type u_3
β : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : ProperSpace α
inst✝ : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall x r ×ˢ closedBall y r)

Tactic:
exact (isCompact_closedBall x r).prod (isCompact_closedBall y r)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : ℝ
R0 : R > 0
H : ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
exact ⟨_, add_pos R0 R0, fun m n =>
      lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y⁻¹‖ = ‖y‖

Tactic:
norm_inv'

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ = ‖y‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y⁻¹‖ = 0

Tactic:
norm_inv'

Goal state after:
case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y‖ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖v‖

Tactic:
simpa [-tsub_le_iff_right, tsub_le_iff_left, two_mul, add_assoc]
    using norm_mul₃_le' (a := (u / v)) (b := v) (c := v)

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
rw [ENNReal.ofReal_le_ofReal_iff (norm_nonneg' _)] at h

Goal state after:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousAt f x
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' t)

Tactic:
simp_rw [← continuousWithinAt_univ] at hf
  simpa only [inter_univ] using
    exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk hf

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ⊢ Pairwise fun x y ↦ 1 ≤ dist ↑x ↑y

Tactic:
simpa using Int.pairwise_one_le_dist

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

Goal state before:
pp: case bot
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊥
⊢ (⊥ + y).toENNReal = ⊥.toENNReal + y.toENNReal

Tactic:
induction y

Goal state after:
case bot.bot
hx hy : 0 ≤ ⊥
⊢ (⊥ + ⊥).toENNReal = ⊥.toENNReal + ⊥.toENNReal

case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ + ↑a✝).toENNReal = ⊥.toENNReal + (↑a✝).toENNReal

case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ (⊥ + ⊤).toENNReal = ⊥.toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
hy : 0 ≤ y
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ + y).toENNReal = (↑a✝).toENNReal + y.toENNReal

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝ + ⊥).toENNReal = (↑a✝).toENNReal + ⊥.toENNReal

case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊤
⊢ (↑a✝ + ⊤).toENNReal = (↑a✝).toENNReal + ⊤.toENNReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
u_bdd_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
v_bdd_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)

Tactic:
obtain ⟨U, hU⟩ := u_bdd_le

Goal state after:
α : Type u_5
f : Filter α
R : Type u_6
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
v_bdd_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x U
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊤
⊢ (⊤ + y).toENNReal = ⊤.toENNReal + y.toENNReal

Tactic:
induction y

Goal state after:
case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal

case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ + ↑a✝).toENNReal = ⊤.toENNReal + (↑a✝).toENNReal

case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
R : Type u_6
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f u
hv : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)

Tactic:
obtain ⟨U, hU⟩ := hu.eventually_ge

Goal state after:
α : Type u_5
R : Type u_6
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f u
hv : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
⊢ (⊥ + y).toENNReal ≤ ⊥.toENNReal + y.toENNReal

Tactic:
induction y

Goal state after:
case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal

case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).toENNReal ≤ (↑a✝).toENNReal + y.toENNReal

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal

case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
⊢ (⊤ + y).toENNReal ≤ ⊤.toENNReal + y.toENNReal

Tactic:
induction y

Goal state after:
case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal

case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal

case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
by
  rcases eq_or_ne I ⊥ with rfl | hI
  · simp
  rcases eq_or_ne J ⊥ with rfl | hJ
  · simp
  have : I ⊔ J ≠ ⊥ := by grind
  have H {I' : Ideal R} (h : I' ≠ ⊥) : FiniteMultiplicity p.asIdeal I' :=
    FiniteMultiplicity.of_prime_left (prime p) h
  rw [(H this).emultiplicity_eq_multiplicity, (H hI).emultiplicity_eq_multiplicity,
    (H hJ).emultiplicity_eq_multiplicity, multiplicity_sup _ hI hJ]
  norm_cast

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

Goal state before:
pp: case bot
y : EReal
h1 : ⊥ ≠ ⊥ ∨ y ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(⊥ + y) = -⊥ - y

Tactic:
induction y

Goal state after:
case bot.bot
h1 : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊥ + ⊥) = -⊥ - ⊥

case bot.coe
a✝ : ℝ
h1 : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊥ + ↑a✝) = -⊥ - ↑a✝

case bot.top
h1 : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊥ + ⊤) = -⊥ - ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ y ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(↑a✝ + y) = -↑a✝ - y

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(↑a✝ + ⊥) = -↑a✝ - ⊥

case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝

case coe.top
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(↑a✝ + ⊤) = -↑a✝ - ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
h1 : ⊤ ≠ ⊥ ∨ y ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(⊤ + y) = -⊤ - y

Tactic:
induction y

Goal state after:
case top.bot
h1 : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊤ + ⊥) = -⊤ - ⊥

case top.coe
a✝ : ℝ
h1 : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊤ + ↑a✝) = -⊤ - ↑a✝

case top.top
h1 : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊤ + ⊤) = -⊤ - ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
hy : 0 ≤ y
⊢ (⊥ - y).toENNReal = ⊥.toENNReal - y.toENNReal

Tactic:
induction y

Goal state after:
case bot.bot
hy : 0 ≤ ⊥
⊢ (⊥ - ⊥).toENNReal = ⊥.toENNReal - ⊥.toENNReal

case bot.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ - ↑a✝).toENNReal = ⊥.toENNReal - (↑a✝).toENNReal

case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
hy : 0 ≤ y
a✝ : ℝ
⊢ (↑a✝ - y).toENNReal = (↑a✝).toENNReal - y.toENNReal

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
hy : 0 ≤ ⊥
⊢ (↑a✝ - ⊥).toENNReal = (↑a✝).toENNReal - ⊥.toENNReal

case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal

case coe.top
a✝ : ℝ
hy : 0 ≤ ⊤
⊢ (↑a✝ - ⊤).toENNReal = (↑a✝).toENNReal - ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
hy : 0 ≤ y
⊢ (⊤ - y).toENNReal = ⊤.toENNReal - y.toENNReal

Tactic:
induction y

Goal state after:
case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal

case top.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ - ↑a✝).toENNReal = ⊤.toENNReal - (↑a✝).toENNReal

case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : ¬y = ⊤
hxy : ¬x = y
⊢ x < y + (t - z)

Tactic:
· rw [← add_zero x]
    exact add_lt_add (by grind) (sub_pos.mpr h')

Goal state after: