mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
⊢ HasFPowerSeriesAt ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ if i = 0 then ℘[L - l] l else (↑i + 1) * L.sumInvPow l (i + 2)) l

Tactic:
by
  obtain ⟨r, h₁, h₂⟩ := Metric.nhds_basis_closedBall.mem_iff.mp
    (L.compl_lattice_sdiff_singleton_mem_nhds l)
  lift r to NNReal using h₁.le
  simpa [weierstrassPExceptSeries] using
    (L.hasFPowerSeriesOnBall_weierstrassPExcept l l r h₁ h₂).hasFPowerSeriesAt

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0

Tactic:
rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
hz : z ≠ l₀
⊢ (z - l₀) ^ 2 ≠ 0

Tactic:
simpa [sub_eq_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
⊢ (Multiset.map (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Multiset.range n)).Nodup

Tactic:
by
  refine (Finset.range n).nodup_map_iff_injOn.mpr ?_
  apply injOn_cos.comp
  · intro x hx y hy hxy
    field_simp at hxy
    aesop
  · refine fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩
    field_simp
    norm_cast
    grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ -1 ≤ eval x (T ℝ ↑n)

Tactic:
refine (abs_le.mp (abs_eval_T_real_le_one n (by grind))).1

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case inl
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
h✝ : Even k
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

pp: case inr
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
h✝ : Odd k
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
case inl hk₂ => exact .inr (isLocalMax_T_real hn hk₀ hk₁ hk₂)

Goal state after:
case inr
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
h✝ : Odd k
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ 0 < fib (2 * n + 1)

Tactic:
grind [fib_two_mul_add_one_eq_natFib_natAbs, Nat.fib_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ∀ (b : ℤ), ((↑1 * x - ↑b) * (↑1 * x + ↑b))⁻¹ = (x - ↑b)⁻¹ * (x + ↑b)⁻¹

Tactic:
simp [mul_comm]

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..↑M, x ^ k * rexp (c - c * x) ≤ ↑k ! / c ^ (k + 1) * rexp c

Tactic:
simp only [sub_eq_add_neg, Real.exp_add, mul_comm (rexp c), ← mul_assoc]

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..↑M, x ^ k * rexp (-(c * x)) * rexp c ≤ ↑k ! / c ^ (k + 1) * rexp c
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
⊢ a + 1 ≤ N

Tactic:
by_contra! h

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
⊢ False
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
⊢ False

Tactic:
have cNM : c N ≤ M := by
        apply le_max'
        apply mem_image_of_mem
        exact mem_range.2 h

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
cNM : c N ≤ M
⊢ False
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
⊢ a + 1 ≤ N

Tactic:
by_contra! h

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
⊢ False
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
⊢ False

Tactic:
have cNM : c N ≤ M := by
        apply le_max'
        apply mem_image_of_mem
        exact mem_range.2 h

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
cNM : c N ≤ M
⊢ False
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i

Tactic:
apply integral_le_sum_Ico_of_le (f := fun x ↦ f x * g x) hab

Goal state after:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f x * g (x - 1) ≤ f ↑i * g ↑i

case hg
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ IntegrableOn (fun x ↦ f x * g (x - 1)) (Ico ↑a ↑b) volume
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f ⟨0, id { down := x }⟩ = { obj := f x, property := ⋯ }.obj

Tactic:
· simp only [FilteredClosureSmall.abstractFilteredClosureRealization,
          FilteredClosureSmall.bundledAbstractFilteredClosure]
        rfl

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

Goal state before:
pp: case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f
      ⟨(Max.max n m).succ, ⋯.mpr (FilteredClosureSmall.InductiveStep.max ⋯ ⋯ x y)⟩ =
    {
        obj :=
          max (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
            (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
· simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
      rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
      rfl

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

Goal state before:
pp: case coeq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f
      ⟨(Max.max n m).succ, ⋯.mpr (FilteredClosureSmall.InductiveStep.coeq ⋯ ⋯ x y g g')⟩ =
    { obj := coeq g g', property := ⋯ }.obj

Tactic:
· simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
      rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
      rfl

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

Goal state before:
pp: case min.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f (max n m).succ).fst

Tactic:
simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]

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)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
⊢ IsIndObject A

Tactic:
have hq : Nonempty (FinalModel (CostructuredArrow yoneda A)) := Nonempty.map
    (Functor.Final.lift (fromFinalModel (CostructuredArrow yoneda A))) IsFiltered.nonempty

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
hq : Nonempty (FinalModel (CostructuredArrow yoneda A))
⊢ IsIndObject A
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 ≫
        (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

Tactic:
← NatTrans.comp_app_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 ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((preservesLimitIso
                    (coyoneda ⋙
                      (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                    K).hom ≫
                (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.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 ≫
        ((preservesLimitIso
                    (coyoneda ⋙
                      (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                    K).hom ≫
                (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

Tactic:
← NatTrans.comp_app_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 ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        (((preservesLimitIso
                      (coyoneda ⋙
                        (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                      K).hom ≫
                  (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm).hom) ≫
                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.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) ≫
                (functorToInterchangeIso A K).inv.app 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

Tactic:
← NatTrans.comp_app_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 ≫
      (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) ≫
                (functorToInterchangeIso A K).inv.app j).app
            i ≫
          (colimit.ι (functorToInterchange A K).flip i ≫
                  (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