mathlib-initiative/mathlib-tactics huggingface dataset:
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'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ count K v (I * I') =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).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 {a'})).factors))

Tactic:
count_well_defined K v (mul_ne_zero hI hI') h_prod,

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'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (J * J')).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a * a'})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).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 {a'})).factors))
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' Iio ↑x = Ioo ⊥ ↑x

Tactic:
WithBot.image_coe_Iio

Goal state after:
x : ℝ
⊢ Ioo ⊥ ↑↑x = Ioo ⊥ ↑x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' Ici ↑x = Ici x

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Ici (WithBot.some (WithTop.some x))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ici, WithTop.preimage_coe_Ici]

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

Goal state before:
pp: r b : ℝ≥0
hb : 1 ≤ ↑(r * b)
⊢ 1 ≤ r * b

Tactic:
← coe_one,

Goal state after:
r b : ℝ≥0
hb : ↑1 ≤ ↑(r * b)
⊢ 1 ≤ r * b
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case negSucc
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 : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I

Tactic:
rw [negSucc_eq, count_neg_zpow, ← Int.natCast_succ, zpow_natCast, count_pow]

Goal state after:
case negSucc
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 : ℕ
⊢ -(↑n.succ * count K v I) = -↑n.succ * count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a + 1 ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
simp [pos_iff_ne_zero, not_or]

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

Goal state before:
pp: case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z

Tactic:
rw [← zero_add (edist y z), ← h]
    apply edist_triangle

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

Goal state before:
pp: r : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
rcases n with n | n
  · simp only [Int.ofNat_eq_natCast, coe_pow, zpow_natCast]
  · have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
    simp only [zpow_negSucc, coe_inv this, coe_pow]

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

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

Tactic:
exact fun _ _ ↦ ⟨i, by simpa [hi]⟩

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

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

Tactic:
exact fun _ _ ↦ ⟨i, by simpa [hi]⟩

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

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f i) * ⨅ j, g j

Tactic:
rw [← iInf_ne_top_subtype]

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = (↑(nndist x y)).toNNReal

Tactic:
Real.toNNReal_coe

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = nndist x y
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ sphere x ε
hε : ε ≠ 0
⊢ x ∉ sphere x ε

Tactic:
by simpa using hε.symm

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
_ε : ℝ
ε0 : 0 < _ε
n : ℕ
hn : 1 / (↑n + 1) < _ε
⊢ 1 / ↑(n + 1) ≤ _ε

Tactic:
simpa using hn.le

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 : ℝ), |x - x| = 0

Tactic:
simp [abs_zero]

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

Goal state before:
pp: α : Type u_2
inst✝ : EMetricSpace α
⊢ Subsingleton α ↔ IndiscreteTopology α

Tactic:
simpa [not_nontrivial_iff_subsingleton] using nontrivial_iff_nontrivialTopology (α := α).not

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ioc a b)

Tactic:
apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self)

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span ({x} ∪ {y}) = Ideal.span {x, y_1}

Tactic:
Set.union_singleton,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {y, x} = Ideal.span {x, y_1}
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case refine_2
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist a 0 ≤ nndist (Pi.single i a) (Pi.single j b)

pp: case refine_3
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist b 0 ≤ nndist (Pi.single i a) (Pi.single j b)

Tactic:
· simpa [h] using nndist_le_pi_nndist (Pi.single i a : β → Y) (Pi.single j b) i

Goal state after:
case refine_3
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist b 0 ≤ nndist (Pi.single i a) (Pi.single j b)
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
⊢ dist x y = dist x' y'

Tactic:
rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Tactic:
refine h.image_uIcc_eq_Icc.trans (uIcc_of_le ?_).symm

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
⊢ b ∈ s

Tactic:
by
  let S := s ∩ Icc a b
  replace ha : a ∈ S := ⟨ha, left_mem_Icc.2 hab⟩
  have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩
  let c := sSup (s ∩ Icc a b)
  have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd
  have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2
  rcases eq_or_lt_of_le c_le with hc | hc
  · exact hc ▸ c_mem.1
  exfalso
  rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩
  exact not_lt_of_ge (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ ∀ (a c : α), 0 ≤ c → (a + k ≤ c ↔ a ≤ c - k)

Tactic:
by simp [le_sub_iff_add_le]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atBot

Tactic:
by
  simpa only [tendsto_neg_atTop_iff, mul_neg] using hf.atTop_mul_const' (neg_pos.mpr hr)

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

Goal state before:
pp: ⊢ Pairwise fun m n ↦ 1 ≤ dist m n

Tactic:
intro m n hne

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
· rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
    _ < ⌈↑x - r⌉₊ := by
      rw [floor_natCast, Nat.lt_ceil]
      linarith

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l v

Tactic:
apply hu.imp

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ ∀ (a : β), (∀ᶠ (x : β) in map u l, (fun x1 x2 ↦ x1 ≤ x2) x a) → ∀ᶠ (x : β) in map v l, (fun x1 x2 ↦ x1 ≤ x2) x a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case mpr.coe
r : ℝ
h : ↑r ≠ ⊥
⊢ ⊤ + ↑r = ⊤

Tactic:
| coe r =>

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

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

Tactic:
x_U

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
⊢ v x ≤ V → 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 : α → β
hf : LipschitzWith K f
x y : α
h : edist x y ≠ ∞
⊢ ↑K * edist x y < ∞

Tactic:
finiteness

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

Goal state after:
α : 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
c : β
hc : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toRight atTop atTop

Tactic:
intro s hs
  simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢
  obtain ⟨t, H⟩ := hs
  exact ⟨.disjSum ∅ t, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h b ↦ .filter_mono h ?_⟩

Goal state after:
case refine_1
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ L.filter

case refine_2
β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
⊢ ∀ᶠ (x : Finset β) in atTop, b ∈ x
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
simp only [h, update_of_ne, if_false, Ne, one_mul, not_false_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : CommMonoid α
inst✝⁶ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst✝⁶, inst✝⁴] ⇑g
hg' : Continuous[inst✝⁴, inst✝⁶] ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f) L
⊢ Multipliable f L

Tactic:
have := h.map _ hg'
    rwa [← Function.comp_assoc, hinv.id] at this

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', ↑a = x) ∧ ∃ a ∈ v', -↑a = x
this : x = 0
⊢ f x = if x = 0 then f 0 else 1

Tactic:
simp only [this, if_true]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (𝓝 a)

Tactic:
refine Tendsto.mono_right ?_ (biInf_le_nhds _)

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (⨅ ε, ⨅ (_ : ε > 0), 𝓟 (Icc (a - ε) (a + ε)))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ 2 ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: case neg
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (pkg.extend f)

Tactic:
· unfold AbstractCompletion.extend
    rw [if_neg hf]
    exact uniformContinuous_of_const fun a b => by congr 1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ dist (a • b) (a • y) + dist a x * dist y 0 ≤ ε

Tactic:
dist_smul_pair,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ dist a 0 * dist b y + dist a x * dist y 0 ≤ ε
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|

Tactic:
gcongr ?_ + ?_
      · exact abs_inf_sub_inf_le_abs _ _ _
      · rw [inf_comm c, inf_comm c]
        exact abs_inf_sub_inf_le_abs _ _ _

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x✝¹ x✝ : ℝ
h₀ : 0 ≤ x✝¹
hr : x✝¹ < x✝
x : ℝ
h : x✝¹ < x ∧ x < x✝
⊢ x✝¹ < ‖x‖ ∧ ‖x‖ < x✝

Tactic:
rwa [Real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝² : SeminormedAddCommGroup α
inst✝¹ : One α
inst✝ : NormOneClass α
⊢ ‖1‖ = 1

Tactic:
simp [ULift.norm_def]

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π ↑i
⊢ s.restrict (updateFinset x s y) = y

Tactic:
restrict_updateFinset_of_subset subset_rfl

Goal state after:
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π ↑i
⊢ restrict₂ ⋯ y = y
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case mpr.inl
K : Type u_4
inst✝ : NormedField K
h : IsComplete (closedBall 0 1)
h✝ : DiscreteTopology K
⊢ CompleteSpace K

Tactic:
completeSpace_iff_isComplete_univ,

Goal state after:
case mpr.inl
K : Type u_4
inst✝ : NormedField K
h : IsComplete (closedBall 0 1)
h✝ : DiscreteTopology K
⊢ IsComplete Set.univ
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)

Tactic:
rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
    refine ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, ?_⟩
    ext ⟨x, hx⟩
    obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
    rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff,
      AddSubgroup.coe_mk, AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat,
      Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _,
      ← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
⊢ Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})

Tactic:
refine ⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩

Goal state after:
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
n : ℕ∞
⊢ MeasurableSet (f ⁻¹' {n})
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : Set α
hs : s.Countable
⊢ μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0

Tactic:
by
  rw [← measure_biUnion_null_iff hs, biUnion_of_singleton]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
by
  rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.mp h]
  · simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : (map f) ma ≤ mb
s : Set β
⊢ ((map f) ma) s ≤ ((restrict (range f)) mb) s

Tactic:
by simpa using h (s ∩ range f)

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x ↦ (Equiv.piEquivPiSubtypeProd p X).symm x j

Tactic:
· simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]
    have : Measurable fun (f : ∀ i : { x // ¬p x }, X i.1) => f ⟨j, hj⟩ :=
      measurable_pi_apply (X := fun i : {x // ¬p x} => X i.1) ⟨j, hj⟩
    exact Measurable.comp this measurable_snd

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

Goal state before:
pp: α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
← Fintype.coe_image_univ,

Goal state after:
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f Finset.univ) = {f zero, f neg, f pos}