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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if 0 + y = 0 then 0 else 1) ≤ 0 + if y = 0 then 0 else 1

Tactic:
zero_add,

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ 0 + if y = 0 then 0 else 1
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective ⇑φ
⊢ Surjective ⇑(map P.asIdeal φ)

Tactic:
by
  classical
  rintro ⟨y, hy⟩
  obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y
  obtain ⟨f, hf⟩ : ∃ f : Π₀ i : HeightOneSpectrum A, primaryComponent M₁ i.asIdeal,
      (DFinsupp.lsum ℕ fun i : HeightOneSpectrum A ↦
      (primaryComponent M₁ i.asIdeal).subtype) f = b := by
    simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]
  refine ⟨f P, Subtype.ext ?_⟩
  simp only [map_apply_coe]
  rw [eq_comm, ← sub_eq_zero]
  refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_
  · exact Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)
  · have hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q) := by
      rw [sub_eq_iff_eq_add',
        ← Finset.sum_eq_add_sum_sdiff_singleton P (fun P ↦ φ (f P)) (by aesop)]
      simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm
    rw [hdiff]
    exact Submodule.sum_mem _ fun Q hQ ↦ Submodule.mem_iSup_of_mem Q <|
        Submodule.mem_iSup_of_mem (by grind) (primaryComponent_map_mem _ _ _)

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

Goal state before:
pp: case inr.inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
hq' : 0 < q
hp' : p < ∞
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
simp [ENNReal.toReal_mono hq.ne hpq, ENNReal.toReal_pos_iff, hp, hp', hq', hq]

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

Tactic:
count,

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)
⊢ (if x : I = 0 then 0
    else
      have a := choose ⋯;
      have J := choose ⋯;
      ↑((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.ENNReal.Operations

Goal state before:
pp: case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ x✝¹ + c - (x✝ + c) = x✝¹ - x✝

Tactic:
add_tsub_add_eq_tsub_right

Goal state after:
case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ x✝¹ - x✝ = x✝¹ - x✝
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ c + a - (c + b) = a - b

Tactic:
by
  simp_rw [add_comm c]
  exact ENNReal.add_sub_add_eq_sub_right hc

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

Goal state before:
pp: x : EReal
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
by
  by_cases h : x = ⊤
  · simp [h]
  · simp [h, toENNReal]

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

Goal state before:
pp: m n : ℕ
⊢ ↑m = ↑↑n ↔ m = n

Tactic:
← coe_coe_eq_natCast m,

Goal state after:
m n : ℕ
⊢ ↑↑m = ↑↑n ↔ m = n
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑m ≤ ↑↑n ↔ m ≤ n

Tactic:
← coe_coe_eq_natCast m,

Goal state after:
m n : ℕ
⊢ ↑↑m ≤ ↑↑n ↔ m ≤ n
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑m < ↑↑n ↔ m < n

Tactic:
← coe_coe_eq_natCast m,

Goal state after:
m n : ℕ
⊢ ↑↑m < ↑↑n ↔ m < n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b ≠ ∞ ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
← ENNReal.inv_ne_zero

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑(y ^ n) ≤ ↑x

Tactic:
ENNReal.coe_le_coe

Goal state after:
case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ n ≤ x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑(y ^ (n + 1))

Tactic:
ENNReal.coe_le_coe

Goal state after:
case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ x ≤ y ^ (n + 1)
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
obtain hx | hx := eq_or_ne x ⊤

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

case inr.inr
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x ≠ ∞
⊢ x ^ (-m) = (x ^ m)⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ ↑(nndist x y) ≤ ↑c ↔ nndist x y ≤ c

Tactic:
ENNReal.coe_le_coe

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ nndist x y ≤ c ↔ nndist x y ≤ c
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 ≤ ε
x' : α
⊢ x' ∈ closedBall x ε ↔ x' ∈ {x}

Tactic:
simpa [Subsingleton.allEq x x']

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 < ε
x' : α
⊢ x' ∈ ball x ε ↔ x' ∈ {x}

Tactic:
simpa [Subsingleton.allEq x x']

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

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.1 p.2 < ε} ⊆ s
ε' : ℝ
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
exact ⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩

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

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑(iInf f * a) = ↑(⨅ i, f i * a)

Tactic:
NNReal.coe_mul,

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑(iInf f) * ↑a = ↑(⨅ i, f i * a)
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑(a * ⨆ i, f i) = ↑(⨆ i, a * f i)

Tactic:
NNReal.coe_mul,

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ↑(⨆ i, f i) = ↑(⨆ i, a * f i)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : ι → α × α
p : Filter ι
⊢ Tendsto f p (𝓤 α) ↔ Tendsto (fun x ↦ dist (f x).1 (f x).2) p (𝓝 0)

Tactic:
Metric.uniformity_eq_comap_nhds_zero,

Goal state after:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : ι → α × α
p : Filter ι
⊢ Tendsto f p (comap (fun p ↦ dist p.1 p.2) (𝓝 0)) ↔ Tendsto (fun x ↦ dist (f x).1 (f x).2) p (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ (∀ (x : α), x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ↔
    ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r

Tactic:
mem_closure_iff,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ (∀ (x : α), ∀ ε > 0, ∃ b ∈ s, dist x b < ε) ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (Prod.map u u) atTop (𝓤 α) ↔ Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
Metric.uniformity_eq_comap_nhds_zero,

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (Prod.map u u) atTop (comap (fun p ↦ dist p.1 p.2) (𝓝 0)) ↔ Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
inst✝¹ : Fintype β
inst✝ : Nonempty β
a b : α
⊢ (dist (fun x ↦ a) fun x ↦ b) = dist a b

Tactic:
by
  simpa only [dist_edist] using congr_arg ENNReal.toReal (edist_pi_const a b)

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

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

Tactic:
simp [dist_pi_lt_iff hr]

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

Goal state before:
pp: α : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x : γ
s : Set γ
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun x y ↦ ε ≤ dist (f x) (f y)
⊢ UniformSpace α

Tactic:
by infer_instance

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
x : γ
hx : ∀ (i : ℕ), f x < u i
⊢ f x ≤ d

Tactic:
exact ge_of_tendsto hu_tt <| .of_forall <| fun n ↦ le_of_lt <| hx n

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (nhds a).IsCountablyGenerated

Tactic:
rw [nhds_discrete]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (pure a).IsCountablyGenerated
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
⊢ cobounded α ≤ Filter.atBot ⊔ Filter.atTop

Tactic:
have := Nonempty.of_isOrderBornology α

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
⊢ cobounded α ≤ Filter.atBot ⊔ Filter.atTop
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
← Filter.eventually_atTop_prod_self' (p := fun m =>
      ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ ↑‖∏ a ∈ s, f a‖₊ ≤ ↑(∑ a ∈ s, ‖f a‖₊)

Tactic:
by
    push_cast
    exact norm_prod_le _ _

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

Goal state before:
pp: ⊢ CompleteSpace ℝ

Tactic:
by
  apply complete_of_cauchySeq_tendsto
  intro u hu
  let c : CauSeq ℝ abs := ⟨u, Metric.cauchySeq_iff'.1 hu⟩
  refine ⟨c.lim, fun s h => ?_⟩
  rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
  have := c.equiv_lim ε ε0
  simp only [mem_map, mem_atTop_sets]
  exact this.imp fun N hN n hn => hε (hN n hn)

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℝ
h : dist x✝¹ x✝ < ε
⊢ dist (-x✝¹) (-x✝) < ε

Tactic:
by simpa only [abs_sub_comm, Real.dist_eq, neg_sub_neg] using h

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
⊢ IsTopologicalAddGroup ℝ

Tactic:
by infer_instance

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

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

Tactic:
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
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f

Tactic:
rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩

Goal state after:
case inl
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
lbot : IsBot l
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f

case inr
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)

Tactic:
by
  induction s using Finset.cons_induction
  case empty =>
    rw [Finset.sum_empty]
    exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩
  case cons k₀ s k₀_notin_s ih =>
    simp only [Finset.forall_mem_cons] at *
    simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)

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

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : β✝ → Ideal R
⊢ emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
| of_equiv e ih =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ∀ (b : α), limsup u f < b → ∀ᶠ (x : β) in f, u x < b

Tactic:
exact fun _ hc ↦ eventually_lt_of_limsup_lt hc

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

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ 0
⊢ ↑x * ⊤ = ⊤

Tactic:
rw [EReal.mul_comm, top_mul_coe_ennreal hx]

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

Goal state before:
pp: case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
hAtTop : atTop = pure Finset.univ
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hL : { filter := F }.filter ≤ atTop
hL' : ∅ ∉ { filter := F }.filter
⊢ { filter := F } = unconditional β

Tactic:
simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ sSup (⋃ j, ⋂ i, Iic (f ↑i)) = ⨆ j, ⨅ i, f ↑i

Tactic:
A,

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ sSup (⋃ j, ⋂ i, Iic (f ↑i)) = ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
A : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = ∅
⊢ sSup (⋃ j, ⋂ i, Iic (f ↑i)) = sSup ∅

Tactic:
A,

Goal state after:
case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
A : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = ∅
⊢ sSup (⋃ j, ∅) = sSup ∅
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ (b - c) * a = b * a - c * a

Tactic:
rw [sub_eq_add_neg, right_distrib_of_nonneg_of_ne_top ha ha']

Goal state after:
a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ b * a + -c * a = b * a - c * a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hf : u = fun i ↦ g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x

Tactic:
exact hu

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

Goal state before:
pp: case refine_2
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
⊢ f = 1 → HasProd f 1 L

Tactic:
rintro rfl
    exact hasProd_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : CommGroup α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : β), f x

Tactic:
by
  rw [← hf.tprod_subtype_mul_tprod_subtype_compl s]
  simp only [Finset.tprod_subtype', mul_right_inj]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ (∏'[L] (b' : β), if b' = b then a b' else 1) = a b

Tactic:
rw [tprod_eq_mulSingle b]
  · simp
  · intro b' hb'; simp [hb']

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst✝¹] {x i}
⊢ ∃ b, a ≤ b ∧ ∃ n ≥ j, y n ∈ closure[inst✝¹] {x b}

Tactic:
obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst✝¹] {x i}
b : ℕ
hb : y (c + j) ∈ closure[inst✝¹] {x b}
⊢ ∃ b, a ≤ b ∧ ∃ n ≥ j, y n ∈ closure[inst✝¹] {x b}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: b : ℝ≥0∞
⊢ IsOpen (Ico 0 b)

Tactic:
ENNReal.Ico_eq_Iio

Goal state after:
b : ℝ≥0∞
⊢ IsOpen (Iio b)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a b : ℝ≥0∞
r : ℝ≥0
x ε : ℝ≥0∞
⊢ ↑{a | a < ∞} ≃ₜ ℝ≥0

Tactic:
by
  refine (Homeomorph.setCongr ?_).trans neTopHomeomorphNNReal
  simp only [lt_top_iff_ne_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∏' (b' : β), Pi.mulSingle b a b' = a

Tactic:
rw [tprod_eq_mulSingle b]
  · simp
  · intro b' hb'; simp [hb']

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

Goal state before:
pp: case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc 0 (0 + ε)

Tactic:
zero_add,

Goal state after:
case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc 0 ε