mathlib-initiative/mathlib-tactics huggingface dataset:
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 f g : NonarchAddGroupNorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _, _⟩, _⟩ := f

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 g : 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
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) g
⊢ { 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'✝ } =
    g
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ∞
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

Tactic:
simpa only [← sSup_range, ← image_eq_range, Subtype.range_coe_subtype] using! (toNNReal_iSup hf)

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioi ⊥ = univ

Tactic:
by
  change ((WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (⊥ : WithBot (WithTop ℝ))) : Set ℝ) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ioi_bot, preimage_univ]

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

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ (x✝ ^ 0)⁻¹ = x✝⁻¹ ^ 0

Tactic:
by simp only [pow_zero, inv_one]

Goal state after:
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

Tactic:
have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by order
      rw [if_neg h_neg, hI, count_zero, mul_zero]

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

Goal state before:
pp: x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = x

Tactic:
toENNReal

Goal state after:
x : EReal
hx : 0 ≤ x
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ c * a * (c⁻¹ * b⁻¹) = a * b⁻¹

Tactic:
mul_mul_mul_comm,

Goal state after:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ c * c⁻¹ * (a * b⁻¹) = a * b⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * c * (b⁻¹ * c⁻¹) = a * b⁻¹

Tactic:
mul_mul_mul_comm,

Goal state after:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * b⁻¹ * (c * c⁻¹) = a * b⁻¹
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
· simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, ENNReal.inv_pos, false_and,
      not_false_eq_true]

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 β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
⊢ ∀ x ∈ f ⁻¹' s, ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s

Tactic:
intro x

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)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
⊢ x ∈ f ⁻¹' s → ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε \ ball x ε = sphere x ε

Tactic:
rw [← ball_union_sphere, Set.union_sdiff_cancel_left sphere_disjoint_ball.symm.le_bot]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
t : Set β
f : α → β
a : α
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, 0 < ia ∧ ∀ x ∈ ball a ia ∩ s, f x ∈ ball b ib ∩ t) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε

Tactic:
by
    simp only [inter_comm _ s, inter_comm _ t, mem_inter_iff, and_imp, gt_iff_lt, mem_ball]

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

Goal state before:
pp: α : Type u_3
d : α → α → ℝ≥0
⊢ (∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}) ∧
    ∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩

Goal state after:
case refine_1
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

case refine_2
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a

Tactic:
rw [mul_iSup]

Goal state after:
ι : Sort u_3
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ i, g * h i ≤ a
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : s.Countable
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
x : α
⊢ edist x (y x) ≤ ↑ε'

Tactic:
exact mod_cast hyx x

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

Goal state before:
pp: α : Type u_2
inst✝ : EMetricSpace α
⊢ (∃ x y, x ≠ y) ↔ ∃ x y, ¬edist x y = 0

Tactic:
edist_eq_zero

Goal state after:
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b x : α
⊢ Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
rw [← interior_Ico, mem_interior_iff_mem_nhds]

Goal state after:
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
Icc_sdiff_Ioo_same h.le

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ {a, b} = {a, b}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
h : a < b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
Icc_sdiff_Ioo_same h.le

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
h : a < b
⊢ {a, b} = {a, b}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
Icc_sdiff_Ioo_same h.le

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ {a, b} = {a, b}
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
⊢ upperBounds (f '' S) ⊆ upperBounds (closure[inst✝³] (f '' S))

Tactic:
intro x

Goal state after:
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
⊢ x ∈ upperBounds (f '' S) → x ∈ upperBounds (closure[inst✝³] (f '' S))
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (X b)
inst✝ : Nonempty β
x : (b : β) → X b
r : ℝ
hr : r < 0
⊢ closedBall x r = Set.univ.pi fun b ↦ closedBall (x b) r

Tactic:
simp [closedBall_eq_empty.2 hr]

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

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ Function.eval default ⁻¹' sphere (x default) 0

Tactic:
intro x

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x✝ : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → X x
⊢ x ∈ sphere x✝ 0 → x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
⊢ ‖r‖ₑ = ENNReal.ofReal |r|

Tactic:
by
  rw [← enorm_eq_ofReal (abs_nonneg _), enorm_abs]

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ r = ‖r‖

Tactic:
Real.norm_eq_abs r,

Goal state after:
r : ℝ
hr : 0 ≤ r
⊢ r = |r|
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]

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

Goal state before:
pp: case refine_1
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
⊢ ∀ x ∈ ↑I, ((Algebra.lsmul R R K) (I'.divMod I J')) x ∈ ↑I'

Tactic:
intro x

Goal state after:
case refine_1
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
x : K
⊢ x ∈ ↑I → ((Algebra.lsmul R R K) (I'.divMod I J')) x ∈ ↑I'
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
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
⊢ ↑J ≤ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'

Tactic:
intro x

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
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
x : K
⊢ x ∈ ↑J → x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
⊢ ∀ (x : γ), ContinuousAt (fun x ↦ sSup (f x '' K)) x

Tactic:
intro x

Goal state after:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
⊢ ContinuousAt (fun x ↦ sSup (f x '' K)) x
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 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' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J')

Tactic:
intro x

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 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' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
⊢ x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' → x ∈ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J')
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ ‖a‖

Tactic:
rw [← dist_one_right]
  exact dist_nonneg

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖b⁻¹ * a‖ = ‖a / b‖

Tactic:
div_eq_inv_mul

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖b⁻¹ * a‖ = ‖b⁻¹ * a‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖a⁻¹ * b‖ = ‖b / a‖

Tactic:
div_eq_inv_mul

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖a⁻¹ * b‖ = ‖a⁻¹ * b‖
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
⊢ StrictMono f

Tactic:
intro x

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x : α
⊢ ∀ ⦃b : α⦄, x < b → f x < f b
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
⊢ f x < f y

Tactic:
let t := max b y

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
⊢ f x < f y
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited ↑(Ioo a b)
g : ↑(Ioo a b) → δ := (Ioo a b).domRestrict f
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
have : StrictMono g ∨ StrictAnti g :=
    Continuous.strictMono_of_inj hf_c.domRestrict hf_i.injective

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this✝ : Inhabited ↑(Ioo a b)
g : ↑(Ioo a b) → δ := (Ioo a b).domRestrict f
this : StrictMono g ∨ StrictAnti g
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := ⋯
n N : ℕ
hn : n ≤ N
⊢ ⋂ n, ⋂ (_ : n ≤ N), s n ⊆ s n

Tactic:
intro x

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
hn : n ≤ N
x : α
⊢ x ∈ ⋂ n, ⋂ (_ : n ≤ N), s n → x ∈ s n
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Iio a)

Tactic:
· rw [e.preimage_Iio]
    apply isOpen_gt'

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

Goal state before:
pp: x y : ℕ
⊢ dist ↑x ↑y = dist x y

Tactic:
← Nat.dist_cast_real,

Goal state after:
x y : ℕ
⊢ dist ↑x ↑y = dist ↑x ↑y
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∀ x ∈ s, f x = ↑(f x).toNNReal

Tactic:
intro x

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
x : α
⊢ x ∈ s → f x = ↑(f x).toNNReal
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Tactic:
simp_rw [ENNReal.ofReal, ← ofNNReal_finsetSum, coe_inj]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ i ∈ s, f i).toNNReal = ∑ i ∈ s, (f i).toNNReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ ∀ (x : ι), v x ≤ V ∧ u x ≤ U ∧ 0 x ≤ u x ∧ 0 x ≤ v x → (u * v) x ≤ U * V

Tactic:
intro x

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
x : ι
⊢ v x ≤ V ∧ u x ≤ U ∧ 0 x ≤ u x ∧ 0 x ≤ v x → (u * v) x ≤ U * V
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) * (↑K)⁻¹ ≤ edist x y

Tactic:
← div_eq_mul_inv

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) / ↑K ≤ edist x y
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ e (blimsup u f p) = blimsup (⇑e ∘ u) f p

Tactic:
by
  simp only [blimsup_eq, map_sInf, Function.comp_apply, e.image_eq_preimage_symm,
    Set.preimage_ofPred_eq, e.le_symm_apply]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x ↦ (f x, g x)

Tactic:
intro x

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x : α
⊢ ∀ (y : α), edist ((fun x ↦ (f x, g x)) x) ((fun x ↦ (f x, g x)) y) ≤ ↑(max Kf Kg) * edist x y