mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ ∑' (i : ℕ), f ↑(i + N) ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x

Tactic:
]

Goal state after:
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ ∑' (i : ℕ), f ↑(i + N) ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x
Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)
Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j) ≫
        (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j) ≫
        (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (∐ fun X ↦ ∐ fun x ↦ projectiveSeparator C)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (∐ fun X ↦ ∐ fun x ↦ projectiveSeparator C)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case refine_1
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
n : ℕ
⊢ IntervalIntegrable f volume (↑N) (↑n + ↑N)

Tactic:
]

Goal state after:
case refine_1
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
n : ℕ
⊢ IntervalIntegrable f volume (↑N) (↑n + ↑N)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ PreservesFiniteLimits (preadditiveCoyonedaObj (generator F))

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ PreservesFiniteLimits (preadditiveCoyonedaObj (generator F))
Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ colimit.post F (coyoneda.obj (op (yoneda.obj X))) = colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
n : ℕ
⊢ ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊ = ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)

Tactic:
field [(zero_lt_one.trans (cone k)).ne']

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2

Tactic:
]

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ≤ c ^ 2

Tactic:
]

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ≤ c ^ 2
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∫ (x : ℝ) in Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
]

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∫ (x : ℝ) in Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)

Tactic:
]

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ (c⁻¹ ^ 2) ^ ↑⌊Real.log j / Real.log c⌋₊ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)

Tactic:
]

Goal state after:
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ (c⁻¹ ^ 2) ^ ↑⌊Real.log j / Real.log c⌋₊ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ 0 < 1 / j ^ 2

Tactic:
]

Goal state after:
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ 0 < 1 / j ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ Real.log j / Real.log c * Real.log (c⁻¹ ^ 2) = Real.log (1 / j ^ 2)

Tactic:
]

Goal state after:
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ Real.log j / Real.log c * Real.log (c⁻¹ ^ 2) = Real.log (1 / j ^ 2)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
⊢ 1 / j ^ 2 / (c⁻¹ ^ 2) ^ 1 / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2

Tactic:
]

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
⊢ 1 / j ^ 2 / (c⁻¹ ^ 2) ^ 1 / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ∑ k ∈ Finset.range (N + M - N), f ↑(N + k) = ∑ i ∈ Finset.range M, f ↑(i + N)

Tactic:
]

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ∑ k ∈ Finset.range (N + M - N), f ↑(N + k) = ∑ i ∈ Finset.range M, f ↑(i + N)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹

Tactic:
by ring

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2

pp: case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

pp: case h.hd
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < (c ^ i) ^ 2

Tactic:
]

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2

case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

case h.hd
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < (c ^ i) ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ (c ^ i) ^ 2 ≤ ((1 - c⁻¹)⁻¹ * ↑⌊c ^ i⌋₊) ^ 2

Tactic:
]

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ (c ^ i) ^ 2 ≤ ((1 - c⁻¹)⁻¹ * ↑⌊c ^ i⌋₊) ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
]

Goal state after:
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹ / j ^ 2)

Tactic:
]

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹ / j ^ 2)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
⊢ (∀ (d : A), ∃ c, Nonempty ((fst L R).obj c ⟶ d)) ∧
    ∀ {d : A} {c : Comma L R} (s s' : (fst L R).obj c ⟶ d), ∃ c' t, (fst L R).map t ≫ s = (fst L R).map t ≫ s'

Tactic:
]

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
⊢ (∀ (d : A), ∃ c, Nonempty ((fst L R).obj c ⟶ d)) ∧
    ∀ {d : A} {c : Comma L R} (s s' : (fst L R).obj c ⟶ d), ∃ c' t, (fst L R).map t ≫ s = (fst L R).map t ≫ s'
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((CostructuredArrow.toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((CostructuredArrow.map (colimit.ι F i)).obj
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
have htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful := .ofFullyFaithful _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((CostructuredArrow.toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((CostructuredArrow.map (colimit.ι F i)).obj
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (b : B), IsConnected (CostructuredArrow L (R.obj b))
b : B
this : (costructuredArrowSndInclusion L R b).Final
⊢ IsConnected (CostructuredArrow L (R.obj b))

Tactic:
]

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (b : B), IsConnected (CostructuredArrow L (R.obj b))
b : B
this : (costructuredArrowSndInclusion L R b).Final
⊢ IsConnected (CostructuredArrow L (R.obj b))
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : IsConnected A
inst✝ : R.Final
⊢ IsConnected A

Tactic:
]

Goal state after:
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : IsConnected A
inst✝ : R.Final
⊢ IsConnected A
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : IsConnected B
inst✝ : L.Initial
⊢ IsConnected B

Tactic:
]

Goal state after:
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : IsConnected B
inst✝ : L.Initial
⊢ IsConnected B
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom (inv iR.inv)))

Tactic:
]

Goal state after:
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom (inv iR.inv)))
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this✝¹ : (R ⋙ H).Final
this✝ :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙ StructuredArrow.map₂ u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom iR.hom))

Tactic:
]

Goal state after:
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this✝¹ : (R ⋙ H).Final
this✝ :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙ StructuredArrow.map₂ u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom iR.hom))
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j
Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ f =
    (whiskerRight (ϕ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ f =
    (whiskerRight (ϕ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i