mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible (Associates.mk J)
hJv : Associates.mk J = v
⊢ v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors

Tactic:
Associates.irreducible_mk

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = ENNReal.ofReal ↑r

Tactic:
by
  rw [ENNReal.ofReal, Real.toNNReal_coe]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ p x + q (x / x) ≤ p x

Tactic:
rw [div_self', map_one_eq_zero q, add_zero]

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

Tactic:
rw [← zpow_add₀ ((@coeIdeal_ne_zero R _ K _ _ _ _).mpr v.ne_bot), sub_eq_add_neg]

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
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 : ¬a = 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0

Tactic:
exact h_a_ne_zero

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
⊢ (s ∩ t).ordConnectedComponent x = s.ordConnectedComponent x ∩ t.ordConnectedComponent x

Tactic:
by
  simp [ordConnectedComponent, ofPred_and]

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 : 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)
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors) +
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)

Tactic:
← natCast_add,

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)
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors +
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)
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)
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors +
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)

Tactic:
← natCast_add,

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)
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors +
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors +
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)
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:
exact h_a_ne_zero

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

Goal state before:
pp: case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ ⨆ i, f i ≤ (⨆ i, a + f i) - a

Tactic:
exact iSup_le fun i ↦ ENNReal.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

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

Goal state before:
pp: x : ℝ≥0∞
⊢ ↑x = 0 ↔ x = 0

Tactic:
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]

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

Goal state before:
pp: ⊢ ↑2⁻¹ = 2⁻¹

Tactic:
rw [coe_inv _root_.two_ne_zero, coe_two]

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

Goal state before:
pp: case inl
a : ℝ≥0∞
ha : a ≠ ∞
hb₀ : ∞ ≠ 0
⊢ ∃ c, 0 < c ∧ c * a < ∞

pp: case inr
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ ∃ c, 0 < c ∧ c * a < b

Tactic:
· exact ⟨1, by simpa [lt_top_iff_ne_top]⟩

Goal state after:
case inr
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ ∃ c, 0 < c ∧ c * a < b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
| a * c = b * d

Tactic:
rw [eq_comm]

Goal state after:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
| b * d = a * c
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:
· exact (hI (FractionalIdeal.le_zero_iff.mp (h.trans hJ.le))).elim

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
⊢ count K v J ≤ count K v I
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
exact ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add hx₀ hx])

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

Goal state before:
pp: case mk.mk
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h :
  { toPseudoEMetricSpace := toPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ }.toEDist =
    { toPseudoEMetricSpace := toPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist
⊢ toPseudoEMetricSpace✝¹.toEDist = toPseudoEMetricSpace✝.toEDist

Tactic:
assumption

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

Goal state before:
pp: case mk.mk
α : Type u_2
inst✝ : TopologicalSpace α
toWeakPseudoEMetricSpace✝¹ : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toWeakPseudoEMetricSpace✝ : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h :
  { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ }.toEDist =
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }.toEDist
⊢ toWeakPseudoEMetricSpace✝¹.toEDist = toWeakPseudoEMetricSpace✝.toEDist

Tactic:
assumption

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

Goal state before:
pp: case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ toPseudoMetricSpace✝¹.toDist = toPseudoMetricSpace✝.toDist

Tactic:
assumption

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
a : α
⊢ a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Tactic:
by
  simpa only [hs.closure_eq] using @mem_closure_iff _ _ s a

Goal state after:
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)
⊢ SeparableSpace ↑s

Tactic:
refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩

Goal state after:
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
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hd : Disjoint u (Ioi x)
⊢ IsMax x

Tactic:
by_contra hx
  exact (mem_closure_iff_nhds.mp (closure_Ioi' (not_isMax_iff.mp hx) ▸ self_mem_Ici) u hu).ne_empty
    (disjoint_iff.mp hd)

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a✝ b✝ : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
y : α
hy : a < y ∧ y < b
xy : x ≠ y
⊢ s.Nonempty

Tactic:
exact ⟨y, us ⟨hab hy, xy.symm⟩⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N^[x✝ + 1] 0

Tactic:
· rw [iterate_succ_apply']; exact hN _

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

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

Tactic:
rw [Real.toNNReal_of_nonneg hr]

Goal state after:
r : ℝ
hr : 0 ≤ r
⊢ NNReal.mk r hr = ‖r‖₊
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
b : α
hb : b ∈ upperBounds sᶜ
c : α
hbc : b < c
x : α
hx : x ∈ {b | c ≤ b}
hx' : x ∉ s
⊢ False

Tactic:
exact hbc.not_ge <| hx.trans <| hb <| mem_compl hx'

Goal state after:
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 α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
hx : x ∈ {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}ᶜ
h'x : x ∈ {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x}ᶜ
⊢ x ∈ {x | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ

Tactic:
simp only [mem_compl_iff, mem_ofPred_eq, not_and, not_not] at hx h'x ⊢

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
hx : x ∈ s → ContinuousWithinAt f (s ∩ Ioi x) x
h'x : x ∈ s → ContinuousWithinAt f (s ∩ Iio x) x
⊢ x ∈ s → ContinuousWithinAt f s x
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : a ∈ ball b r
⊢ a ^ n ∈ ball (b ^ n) (n • r)

Tactic:
simp only [mem_ball, dist_eq_norm_inv_mul, ← inv_pow, ← mul_pow] at h ⊢

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a⁻¹ * b‖ < r
⊢ ‖(a⁻¹ * b) ^ n‖ < n • r
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: ⊢ cofinite = atBot ⊔ atTop

Tactic:
← cocompact_eq_cofinite,

Goal state after:
⊢ cocompact ℤ = atBot ⊔ atTop
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : MulAction ℚ R
inst✝² : MulAction ℚ≥0 R
inst✝¹ : IsScalarTower ℚ≥0 ℚ R
inst✝ : ContinuousSMul ℚ R
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 • p.2

Tactic:
by
    conv in _ • _ => rw [← NNRat.cast_smul_eq_nnqsmul ℚ]
    fun_prop

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 : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
⊢ LipschitzWith (Kα + Kβ) (uncurry f)

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
  simp only [Function.uncurry, ENNReal.coe_add, add_mul]
  apply le_trans (edist_triangle _ (f a₂ b₁) _)
  exact
    add_le_add (le_trans (hα _ _ _) <| mul_right_mono <| le_max_left _ _)
      (le_trans (hβ _ _ _) <| mul_right_mono <| le_max_right _ _)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f ^ n * f)

Tactic:
exact (h.pow_end n).mul_end h

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∀ᶠ (a : α) in f, b < u a

Tactic:
obtain ⟨c, hc, hbc⟩ : ∃ (c : β) (_ : c ∈ { c : β | ∀ᶠ n : α in f, c ≤ u n }), b < c := by
    simp_rw [exists_prop]
    exact exists_lt_of_lt_csSup hu h
  exact hc.mono fun x hx => lt_of_lt_of_le hbc hx

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

Goal state before:
pp: case h₁
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist (a, b).1 x' ≤ ↑δ + ↑δ

Tactic:
exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ᶠ (x : α) in f, u x ≤ b
⊢ limsup u f ≤ b

Tactic:
apply limsSup_le_of_le hu

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ᶠ (x : α) in f, u x ≤ b
⊢ ∀ᶠ (n : β) in map u f, n ≤ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
h : x < 0
⊢ ⊥ * x = ⊤

Tactic:
by
  rw [EReal.mul_comm]
  exact mul_bot_of_neg h

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

Goal state before:
pp: case zero_bot
⊢ (0 * ⊥).toReal = toReal 0 * ⊥.toReal

Tactic:
| zero_bot =>

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

Goal state before:
pp: case zero_bot
⊢ 0 < 0 * ⊥ ↔ 0 < 0 ∧ 0 < ⊥ ∨ 0 < 0 ∧ ⊥ < 0

Tactic:
| zero_bot =>

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
y : β
y_v : y < liminf u f
this : ∀ᶠ (a : α) in f, y < u a
⊢ ∃ᶠ (a : α) in f, y < v a

Tactic:
exact (h.and_eventually this).mono fun x ⟨ux_vx, y_ux⟩ ↦ y_ux.trans_le ux_vx

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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ Finite ↑{n | b'' < u n r}

Tactic:
simpa using! hb''

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

Goal state before:
pp: case zero_bot
⊢ -0 * ⊥ = -(0 * ⊥)

Tactic:
| zero_bot =>

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

Goal state before:
pp: case zero_bot
⊢ 0 * ⊥ = ⊤ ↔ 0 = ⊥ ∧ ⊥ < 0 ∨ 0 < 0 ∧ ⊥ = ⊥ ∨ 0 = ⊤ ∧ 0 < ⊥ ∨ 0 < 0 ∧ ⊥ = ⊤

Tactic:
| zero_bot =>

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ Tendsto (fun x ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ Tendsto (fun x ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ HasProd (fun b ↦ f b * (g b)⁻¹) (a₁ * a₂⁻¹) L

Tactic:
exact hf.mul hg.inv

Goal state after: