mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hbc.h₁
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

pp: case h₂
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
·

Goal state after:
case hbc.h₁
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case hv.a
⊢ (fun n ↦ (√5)⁻¹ * φ ^ n) ∈ fibRec.solSpace

pp: case hv.a
⊢ (fun n ↦ (√5)⁻¹ * ψ ^ n) ∈ fibRec.solSpace

Tactic:
·

Goal state after:
case hv.a
⊢ (fun n ↦ (√5)⁻¹ * φ ^ n) ∈ fibRec.solSpace
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case hv.a
⊢ (fun n ↦ (√5)⁻¹ * ψ ^ n) ∈ fibRec.solSpace

Tactic:
·

Goal state after:
case hv.a
⊢ (fun n ↦ (√5)⁻¹ * ψ ^ n) ∈ fibRec.solSpace
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case h₂
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
·

Goal state after:
case h₂
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case inl
n : ℕ
⊢ ↑(Int.fib ↑n) = (φ ^ ↑n - ψ ^ ↑n) / √5

pp: case inr
n : ℕ
⊢ ↑(Int.fib (-↑n)) = (φ ^ (-↑n) - ψ ^ (-↑n)) / √5

Tactic:
·

Goal state after:
case inl
n : ℕ
⊢ ↑(Int.fib ↑n) = (φ ^ ↑n - ψ ^ ↑n) / √5
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case inr
n : ℕ
⊢ ↑(Int.fib (-↑n)) = (φ ^ (-↑n) - ψ ^ (-↑n)) / √5

Tactic:
·

Goal state after:
case inr
n : ℕ
⊢ ↑(Int.fib (-↑n)) = (φ ^ (-↑n) - ψ ^ (-↑n)) / √5
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hf
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x + (↑n + 1) ≠ 0

pp: case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0

Tactic:
·

Goal state after:
case hf
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x + (↑n + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0

Tactic:
·

Goal state after:
case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ 2 ≤ ↑k + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: case refine_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
l : ℝ
hl : l < h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b

pp: case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L

Tactic:
·

Goal state after:
case refine_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
l : ℝ
hl : l < h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L

Tactic:
·

Goal state after:
case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + iteratedDerivWithin k (fun x ↦ -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -((-1) ^ k * ↑k ! * z ^ (-1 + -↑k))

pp: case hf
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z

pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z

Tactic:
·

Goal state after:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + iteratedDerivWithin k (fun x ↦ -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -((-1) ^ k * ↑k ! * z ^ (-1 + -↑k))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hf
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z

pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z

Tactic:
·

Goal state after:
case hf
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z

Tactic:
·

Goal state after:
case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 0 < k + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hab
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ M

pp: case hf
k M : ℕ
c : ℝ
hc : 0 < c
⊢ MonotoneOn (fun x ↦ x ^ k) (Icc ↑0 ↑M)

pp: case hg
k M : ℕ
c : ℝ
hc : 0 < c
⊢ AntitoneOn (fun x ↦ rexp (-(c * x))) (Icc (↑0 - 1) (↑M - 1))

pp: case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
·

Goal state after:
case hab
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ M
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hf
k M : ℕ
c : ℝ
hc : 0 < c
⊢ MonotoneOn (fun x ↦ x ^ k) (Icc ↑0 ↑M)

pp: case hg
k M : ℕ
c : ℝ
hc : 0 < c
⊢ AntitoneOn (fun x ↦ rexp (-(c * x))) (Icc (↑0 - 1) (↑M - 1))

pp: case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
·

Goal state after:
case hf
k M : ℕ
c : ℝ
hc : 0 < c
⊢ MonotoneOn (fun x ↦ x ^ k) (Icc ↑0 ↑M)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hg
k M : ℕ
c : ℝ
hc : 0 < c
⊢ AntitoneOn (fun x ↦ rexp (-(c * x))) (Icc (↑0 - 1) (↑M - 1))

pp: case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
·

Goal state after:
case hg
k M : ℕ
c : ℝ
hc : 0 < c
⊢ AntitoneOn (fun x ↦ rexp (-(c * x))) (Icc (↑0 - 1) (↑M - 1))
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
·

Goal state after:
case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
·

Goal state after:
case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))
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
N : ℕ
hN : n + 1 ≤ c N
⊢ n < c N

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGrpCat).PreservesEpimorphisms
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGrpCat).PreservesEpimorphisms
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyonedaObj P ⋙ forget (ModuleCat (End P)ᵐᵒᵖ)).PreservesEpimorphisms
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyonedaObj P ⋙ forget (ModuleCat (End P)ᵐᵒᵖ)).PreservesEpimorphisms
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : i + 1 ≤ a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i)

Tactic:
rify at hi this ⊢

Goal state after:
case h
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + (↑i + 1), f x ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + (↑i + 1), f (x₀ + ↑i)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inl ≫ 0

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0

Tactic:
·

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inl ≫ 0
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h₁
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 : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ u (c N) - ↑(c N) * l ≤ ε * ↑(c N)

pp: case hbc
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 : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) - ↑(c (N - 1)) ≤ ε * ↑(c (N - 1))

Tactic:
·

Goal state after:
case h₁
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 : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ u (c N) - ↑(c N) * l ≤ ε * ↑(c N)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hbc
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 : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) - ↑(c (N - 1)) ≤ ε * ↑(c (N - 1))

Tactic:
·

Goal state after:
case hbc
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 : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) - ↑(c (N - 1)) ≤ ε * ↑(c (N - 1))
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : i + 1 ≤ a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x

Tactic:
rify at hi this ⊢

Goal state after:
case h
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + (↑i + 1), f (x₀ + (↑i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + (↑i + 1), f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤
    ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x

Tactic:
gcongr with i hi
    rw [Finset.mem_range, ← Nat.add_one_le_iff] at hi
    have := hf.intervalIntegrable_subset _ hi
    rify at hi this ⊢
    exact integral_mono_on (by simp) (by simp) this fun _ _ ↦ by apply hf <;> grind

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₁)

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)

pp: case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₁)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)

pp: case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)

Tactic:
·

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)

Tactic:
·

Goal state after:
case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)
Module: Mathlib.Analysis.SumIntegralComparisons

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

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

Tactic:
·

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₁)

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)

pp: case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₁)