mathlib-initiative/mathlib-tactics huggingface dataset:
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⌋₊
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n ↦ ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n ↦ ⌊c k ^ n⌋₊) n)

Tactic:
have A :
    Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / (⌊c k ^ n⌋₊ / c k ^ n))
      atTop (𝓝 (1 * c k / 1)) := by
    refine Tendsto.div (Tendsto.mul ?_ tendsto_const_nhds) ?_ one_ne_zero
    · refine tendsto_nat_floor_div_atTop.comp ?_
      exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)
    · refine tendsto_nat_floor_div_atTop.comp ?_
      exact tendsto_pow_atTop_atTop_of_one_lt (cone k)

Goal state after:
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 (𝓝 (1 * c k / 1))
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n ↦ ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n ↦ ⌊c k ^ n⌋₊) n)
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
M : ℕ
hM : 0 < M
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, ‖f x‖ = ∫ (x : ℝ) in ↑N..↑M + ↑N, f x

Tactic:
by

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 (𝓝 (1 * c k / 1))
⊢ Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))

Tactic:
by

Goal state after:
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
M : ℕ
hM : 0 < M
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, f x ≤ ∑ n ∈ Finset.range M, f ↑(n + N)

Tactic:
by

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)
⊢ Tendsto (fun n ↦ u n / ↑n) atTop (𝓝 l)

Tactic:
by

Goal state after:
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
M : ℕ
hM : 0 < M
⊢ ∑ n ∈ Finset.range M, f ↑(n + N) ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
by

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 ^ 3 = c ^ 2 * c

Tactic:
by

Goal state after:
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
⊢ IntegrableOn f (Ioi ↑N) volume

Tactic:
by

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 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹

Tactic:
by

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
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / (c ^ i) ^ 2

Tactic:
by

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
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / (c ^ i) ^ 2 = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i

Tactic:
by

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
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / (1 - c⁻¹ ^ 2) ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / (1 - c⁻¹ ^ 2)

Tactic:
by

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
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2

Tactic:
by

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
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2

Tactic:
by

Goal state after:
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 : ℕ
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, f x ≤ ∑ n ∈ Finset.Ico N (N + M), f ↑n

Tactic:
by

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
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: c : ℝ
hc : 1 < c
i : ℕ
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
by

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 < 1 - c⁻¹
k : ℕ
hk : k ∈ range N
⊢ 0 ≤ c ^ k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
⊢ Small.{max v w, u} (filteredClosure f).FullSubcategory

Tactic:
by

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 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < ↑⌊c ^ i⌋₊, 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ ∑ i ∈ range N with j < c ^ i, 1 / ↑⌊c ^ i⌋₊ ^ 2

Tactic:
by

Goal state after:
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 : ℕ
⊢ ∑ n ∈ Finset.Ico N (N + M), f ↑n = ∑ i ∈ Finset.range M, f ↑(i + N)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
by

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 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
⊢ Small.{max v w, u} (cofilteredClosure f).FullSubcategory

Tactic:
by

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 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2) ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2

Tactic:
by

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 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
⊢ IsIndObject A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A) ↔ PreservesFiniteLimits A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

Tactic:
by

Goal state after:
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
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
h : Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H)))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
by

Goal state after:
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))
j₁ j₂ : Comma L R
Q : CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToLeft j₁.right j₂.right) = L.map va₂ ≫ j₁.hom
ib : A
vb₁ : ib ⟶ Q.left
vb₂ : ib ⟶ j₂.left
heqb : L.map vb₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToRight j₁.right j₂.right) = L.map vb₂ ≫ j₂.hom
i₀ : A
il₀ : i₀ ⟶ ia
ir₀ : i₀ ⟶ ib
heq : il₀ ≫ va₁ = ir₀ ≫ vb₁
⊢ L.map (il₀ ≫ va₂) ≫ j₁.hom =
    { left := i₀, right := IsCofiltered.min j₁.right j₂.right, hom := L.map (il₀ ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.minToLeft j₁.right j₂.right)

Tactic:
by

Goal state after:
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))
j₁ j₂ : Comma L R
Q : CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToLeft j₁.right j₂.right) = L.map va₂ ≫ j₁.hom
ib : A
vb₁ : ib ⟶ Q.left
vb₂ : ib ⟶ j₂.left
heqb : L.map vb₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToRight j₁.right j₂.right) = L.map vb₂ ≫ j₂.hom
i₀ : A
il₀ : i₀ ⟶ ia
ir₀ : i₀ ⟶ ib
heq : il₀ ≫ va₁ = ir₀ ≫ vb₁
⊢ L.map (ir₀ ≫ vb₂) ≫ j₂.hom =
    { left := i₀, right := IsCofiltered.min j₁.right j₂.right, hom := L.map (il₀ ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.minToRight j₁.right j₂.right)

Tactic:
by

Goal state after:
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))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
i₀ : A
α : i₀ ⟶ j₁.left
β : i₀ ⟶ ia
hα : α ≫ u.left = β ≫ va₂ ≫ v.left
hβ : α ≫ 𝟙 j₁.left = β ≫ va₂
this : IsCofiltered.eqHom u.right v.right ≫ u.right = IsCofiltered.eqHom u.right v.right ≫ v.right
⊢ L.map (β ≫ va₂) ≫ j₁.hom =
    { left := i₀, right := IsCofiltered.eq u.right v.right, hom := L.map (β ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.eqHom u.right v.right)

Tactic:
by

Goal state after:
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
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
by

Goal state after:
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)
⊢ ∀ (j j' : Jᵒᵖ) (f : j ⟶ j'),
    (ConcreteCategory.hom
          ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))).map f))
        (Over.mkIdTerminal.from (Opposite.unop ((CostructuredArrow.toOver yoneda (colimit F)).op.obj (G.op.obj j)))) =
      Over.mkIdTerminal.from (Opposite.unop ((CostructuredArrow.toOver yoneda (colimit F)).op.obj (G.op.obj j')))

Tactic:
by

Goal state after:
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))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
i₀ : A
α : i₀ ⟶ j₁.left
β : i₀ ⟶ ia
hα : α ≫ u.left = β ≫ va₂ ≫ v.left
hβ : α ≫ 𝟙 j₁.left = β ≫ va₂
this : IsCofiltered.eqHom u.right v.right ≫ u.right = IsCofiltered.eqHom u.right v.right ≫ v.right
⊢ { left := β ≫ va₂, right := IsCofiltered.eqHom u.right v.right, w := ⋯ } ≫ u =
    { left := β ≫ va₂, right := IsCofiltered.eqHom u.right v.right, w := ⋯ } ≫ v

Tactic:
by

Goal state after:
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))
⊢ IsCofilteredOrEmpty (Comma L R)

Tactic:
by

Goal state after:
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))
⊢ Nonempty (Comma L R)

Tactic:
by

Goal state after:
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)
a : A
A' : Comma L R
s s' : (fst L R).obj A' ⟶ a
⊢ L.map (IsCofiltered.eqHom s s') ≫ A'.hom =
    { left := IsCofiltered.eq s s', right := A'.right, hom := L.map (IsCofiltered.eqHom s s') ≫ A'.hom }.hom ≫
      R.map (𝟙 A'.right)

Tactic:
by

Goal state after:
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 ≫
      (isoAux A K).hom.app i ≫
        (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K).hom.app
            i ≫
          (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm).hom.app i ≫
            colimit.ι (limit (functorToInterchange A K)) i ≫
              (colimitLimitIso (functorToInterchange A K)).hom ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j

Tactic:
ι_colimitLimitIso_limit_π_assoc,

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 ≫
      (isoAux A K).hom.app i ≫
        (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K).hom.app
            i ≫
          (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm).hom.app i ≫
            (limit.π (functorToInterchange A K) j).app i ≫
              (colimit.ι (functorToInterchange A K).flip i).app j ≫
                (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                  (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                    (K.isoWhiskerLeft
                            ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                              (Presheaf.isColimitTautologicalCocone A))).hom.app
                      j
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))
⊢ (fst L R).Initial

Tactic:
by

Goal state after:
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
⊢ IsConnected (CostructuredArrow (snd L R) b)

Tactic:
by

Goal state after:
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✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
⊢ IsFiltered (Comma L R)

Tactic:
by

Goal state after:
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✝ : ∀ (a : A), IsConnected (StructuredArrow (L.obj a) R)
⊢ (fst L R).Final

Tactic:
by

Goal state after:
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)
⊢ IsFiltered (CostructuredArrow yoneda (colimit F))

Tactic:
by

Goal state after:
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✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
⊢ (snd L R).Final

Tactic:
by

Goal state after:
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 (Comma L R)

Tactic:
by

Goal state after:
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 (Comma L R)

Tactic:
by

Goal state after: