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

Goal state before:
pp: case mk
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 : NonarchAddGroupSeminorm 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
toZeroHom✝ : ZeroHom E ℝ
add_le_max'✝ : ∀ (r s : E), toZeroHom✝.toFun (r + s) ≤ max (toZeroHom✝.toFun r) (toZeroHom✝.toFun s)
neg'✝ : ∀ (r : E), toZeroHom✝.toFun (-r) = toZeroHom✝.toFun r
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    (fun f ↦ f.toFun) { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }

Tactic:
congr

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    I

Tactic:
have hnd : mk' K n d = k := choose_spec (choose_spec (exists_mk'_eq R⁰ k))

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    I
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ sSup (range fun p ↦ ↑p x) = sSup ((fun x_1 ↦ x_1 x) '' s)

Tactic:
congr

Goal state after:
E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ (range fun p ↦ ↑p x) = (fun x_1 ↦ x_1 x) '' s
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : Group E
p q : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝¹ :
  ∀ (x : E), { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }.toFun x = 0 → x = 1
toGroupSeminorm✝ : GroupSeminorm E
eq_one_of_map_eq_zero'✝ : ∀ (x : E), toGroupSeminorm✝.toFun x = 0 → x = 1
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }

Tactic:
congr

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

Goal state before:
pp: case mk
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 : 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
toNonarchAddGroupSeminorm✝ : NonarchAddGroupSeminorm E
eq_zero_of_map_eq_zero'✝ : ∀ (x : E), toNonarchAddGroupSeminorm✝.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)
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { 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'✝¹ } =
    { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }

Tactic:
congr

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhdsGE hmem with ⟨b, hab, hmem', hsub⟩

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a

Tactic:
exact iSup₂_le h

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

Goal state before:
pp: case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤

Tactic:
· contrapose!
    intro h
    exact ⟨x.toReal, le_coe_toReal h⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ count K v 1 = 0

Tactic:
by
  have h1 : (1 : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑(1 : Ideal R) := by
    rw [(algebraMap R K).map_one, Ideal.one_eq_top, coeIdeal_top, mul_one, inv_one,
      spanSingleton_one]
  rw [count_well_defined K v one_ne_zero h1, Ideal.span_singleton_one, Ideal.one_eq_top, sub_self]

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≤ b * c
⊢ a / c ≤ b

Tactic:
by_cases h0 : c = 0

Goal state after:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b

case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ ∃ n > 0, ↑n * a < b

Tactic:
rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩

Goal state after:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n)⁻¹ * a < b
⊢ ∃ n > 0, ↑n * a < b
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β) =
    ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | max (edist p.1.1 p.2.1) (edist p.1.2 p.2.2) < ε}

Tactic:
by
    simp [PseudoEMetricSpace.uniformity_edist, ← iInf_inf_eq, ofPred_and]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, eball x ε ⊆ s

Tactic:
simp [isOpen_iff_nhds, mem_nhds_iff]

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 := toPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ } =
    { toPseudoEMetricSpace := toPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }

Tactic:
congr

Goal state after:
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✝¹ = toPseudoEMetricSpace✝
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mk.mk
α : Type u_2
inst✝ : TopologicalSpace α
toEDist✝¹ : EDist α
edist_self✝¹ : ∀ (x : α), edist x x = 0
edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝¹ : (uniformSpaceOfEDist edist edist_self✝¹ edist_comm✝¹ edist_triangle✝¹).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝¹ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝ : (uniformSpaceOfEDist edist edist_self✝ edist_comm✝ edist_triangle✝).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  { toEDist := toEDist✝¹, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
        topology_le := topology_le✝¹, topology_eq_on_restrict := topology_eq_on_restrict✝¹ }.toEDist =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }.toEDist
⊢ { toEDist := toEDist✝¹, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
      topology_le := topology_le✝¹, topology_eq_on_restrict := topology_eq_on_restrict✝¹ } =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }

Tactic:
congr

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 := toWeakPseudoEMetricSpace✝¹, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝¹ } =
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace✝, eq_of_edist_eq_zero := eq_of_edist_eq_zero✝ }

Tactic:
congr

Goal state after:
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✝¹ = toWeakPseudoEMetricSpace✝
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 := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ } =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }

Tactic:
congr

Goal state after:
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✝¹ = toPseudoMetricSpace✝
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
      0

Tactic:
have h_subset :
    {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count (Associates.mk J).factors : ℤ) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0} ⊆
    {v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪
      {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}} := by
    intro v hv
    have hv_irred : Irreducible v.asIdeal := v.irreducible
    by_contra h_notMem
    rw [mem_union, mem_ofPred_eq, mem_ofPred_eq] at h_notMem
    push Not at h_notMem
    rw [← Associates.count_ne_zero_iff_dvd ha_ne_zero hv_irred, not_not,
      ← Associates.count_ne_zero_iff_dvd hJ_ne_zero hv_irred, not_not] at h_notMem
    rw [mem_ofPred_eq, h_notMem.1, h_notMem.2, sub_self] at hv
    exact hv (Eq.refl 0)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
h_subset :
  {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0} ⊆
    {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
      0
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝ : Group E
f : GroupSeminorm E
x y : E
⊢ f (x⁻¹ * y) = f (y⁻¹ * x)

Tactic:
convert! map_inv_eq_map f (y⁻¹ * x) using 2; group

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
this : ∃ a K, J * K = Ideal.span {a} ∧ I + K = ⊤
⊢ ∃ a, J * I ⊔ Ideal.span {a} = J

Tactic:
by
    obtain ⟨a, K, e, e'⟩ := this
    exact ⟨a, by rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]⟩

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

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

Tactic:
simpa only [mul_comm] using iInf_mul f a

Goal state after:
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_iSup

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

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

Tactic:
exact ciSup_le' H

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

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

Tactic:
exact ciSup_le' H

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | dist p.1 p.2 < i} ⊆ {p | dist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
simp only [subset_def, Prod.forall, gt_iff_lt, preimage_ofPred_eq, Prod.map_apply, mem_ofPred]

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

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : t.Countable
hsub : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩

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

Goal state before:
pp: b : ℝ
⊢ {b} = ⋂ r, ⋂ (_ : r > 0), Icc (b - r) (b + r)

Tactic:
simp [Icc_eq_closedBall, biInter_basis_nhds Metric.nhds_basis_closedBall]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ ⨅ j, ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j} =
    ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
congr

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ (fun j ↦ ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j}) = fun ε ↦
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Topology.EMetricSpace.Pi

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ ⨅ (_ : 0 < ε), ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
congr

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ (fun j ↦ ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε}) = fun x ↦ 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Analysis.Normed.Group.Real

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

Tactic:
congr

Goal state after:
r : ℝ
hr : 0 ≤ r
⊢ r = ‖r‖
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
⊢ ‖single i y‖ₑ = ‖y‖ₑ

Tactic:
by simp [enorm, Pi.nnnorm_single]

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

Goal state before:
pp: case refine_2
α : 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 : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u

Tactic:
have : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x := by simp [nhdsWithin_inter, mem_inf_of_left,
    self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]

Goal state after:
case refine_2
α : 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 : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
this : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
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:
by
  rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]

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

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

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

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

Goal state before:
pp: 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' ⊓
      (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * (spanSingleton R⁰ (I'.divMod I J') * I) =
    J
H' : ¬I'.divMod I J' = 0
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J

Tactic:
inv_mul_cancel_left₀ (by simpa [spanSingleton_eq_zero_iff] using H')

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
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J