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

Goal state before:
pp: case neg.inr
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖((↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).1 +
              1) *
            (↑((Equiv.prodCongrLeft fun x ↦
                        { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                          right_inv := ⋯ })
                      (Prod.map some id p)).2 -
                x) ^
              (-(↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id p)).1 +
                  2)) -
          Nat.rec
            (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).2 ^
              (-2))
            (fun n n_ih ↦ 0)
            ((Equiv.prodCongrLeft fun x ↦
                  { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
                (Prod.map some id p)).1) *
        (z - x) ^
          ((Equiv.prodCongrLeft fun x ↦
                { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
              (Prod.map some id p)).1‖ ≤
    (↑p.1 + 2) * κ ^ (-↑p.1) * (‖↑p.2 - x‖ ^ (-3) * ‖z - x‖)

Tactic:
calc
      _ = ‖(p.1 + 2 : ℂ)‖ * ‖p.2 - x‖ ^ (-3 - p.1 : ℤ) * ‖z - x‖ ^ (p.1 + 1) := by
        norm_num; ring_nf; simp
      _ = ‖(p.1 + 2 : ℂ)‖ * ((‖↑p.2 - x‖ / ‖z - x‖) ^ p.1)⁻¹ * ((‖p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖) := by
        simp [hpx, zpow_sub₀, div_pow]; field
      _ ≤ (p.1 + 2) * (κ ^ p.1)⁻¹ * ((‖p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖) := by
        gcongr
        · norm_cast
        · exact (le_div_iff₀ (by simpa [sub_eq_zero])).mpr ((mul_comm _ _).trans_le (hκ' p.2 hp).le)
      _ = _ := by simp [zpow_ofNat]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
x : α
hx : x ∈ box n
hn : n = 0
⊢ x = 0

Tactic:
hn,

Goal state after:
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
x : α
hx : x ∈ box 0
hn : n = 0
⊢ x = 0
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: x : ℤ × ℤ
⊢ ∃! n, x ∈ box n

Tactic:
by
  use max x.1.natAbs x.2.natAbs; simp only [mem_box, and_self_iff, forall_eq']

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

Goal state before:
pp: case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
have : x 1 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H1, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |cos (↑↑n * arccos x)| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
Int.cast_natCast,

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |cos (↑n * arccos x)| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
⊢ IsLocalMin (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
have k_pos : 0 < k := hk₂.pos

Goal state after:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
⊢ IsLocalMin (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : eval x ↑↑n * eval x (U ℝ (↑n - 1)) = 0
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

Tactic:
Int.cast_natCast,

Goal state after:
case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : eval x ↑n * eval x (U ℝ (↑n - 1)) = 0
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic

Goal state before:
pp: ⊢ MeromorphicNFOn tanh Set.univ

Tactic:
intro x _
  refine MeromorphicNFOn.div analyticAt_sinh analyticAt_cosh.meromorphicNFAt ?_
  grind [cosh_sq_sub_sinh_sq]

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

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * arithGeom a b u₀ n + b = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
hn,

Goal state after:
case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * (a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k) + b = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (arithGeom a b u₀) atTop atTop

Tactic:
by
  rw [arithGeom_eq' ha.ne']
  refine tendsto_atTop_add_const_right _ _ ?_
  refine Tendsto.atTop_mul_const (sub_pos.mpr h0) ?_
  exact tendsto_pow_atTop_atTop_of_one_lt ha

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n k'

Tactic:
by
  rw [← e]
  refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩
  · rw [add_mod, mod_self, add_zero, mod_mod]
    exact h.2.1
  rcases h.2.2.eq_or_lt with rfl | h2
  · exact (np rfl).elim
  rcases (succ_le_of_lt h2).eq_or_lt with h2|h2
  · refine ((h.1.trans_le h.2.2).ne ?_).elim
    have h3 : 2 ∣ minFac n := by
      rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
    simpa [dvd_prime <| minFac_prime h.one_lt.ne'] using h3
  exact h2

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

Goal state before:
pp: case hbc
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
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k) + (↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k) +
      r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
have h1 := summand_bound_of_mem_verticalStrip (k := k + 1) (by positivity) ![1, n + 1] hB haAB

Goal state after:
case hbc
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))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k) + (↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k) +
      r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)
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:
· exact Nat.zero_le M

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

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

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

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
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
⊢ c (N - 1) ≤ n

Tactic:
have : N - 1 < N := Nat.pred_lt Npos.ne'

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
aN : a + 1 ≤ N
Npos : 0 < N
this : N - 1 < N
⊢ c (N - 1) ≤ n
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
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
⊢ c (N - 1) ≤ n

Tactic:
have : N - 1 < N := Nat.pred_lt Npos.ne'

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
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
this : N - 1 < N
⊢ c (N - 1) ≤ n
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
refine tsum_le_of_sum_le' (integral_nonneg_of_ae ?_) fun s ↦ ?_
  · filter_upwards [ae_restrict_mem measurableSet_Ioi] using nonneg
  · obtain ⟨t, ht⟩ := tendsto_finset_range.eventually (Ici_mem_atTop s) |>.exists
    calc
      ∑ i ∈ s, f ↑(i + N + 1) ≤ ∑ i ∈ range t, f ↑(i + N + 1) :=
        sum_le_sum_of_subset_of_nonneg ht <| by grind
      _ = ∑ i ∈ Ico N (N + t), f ↑(i + 1) := by rw [Finset.sum_Ico_eq_sum_range]; grind
      _ ≤ ∫ (x : ℝ) in Set.Ioi (N : ℝ), f x :=
        (anti.mono <| by grind).sum_Ico_le_integral integrable nonneg

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
by
  refine tsum_le_of_sum_le' (integral_nonneg_of_ae ?_) fun s ↦ ?_
  · filter_upwards [ae_restrict_mem measurableSet_Ioi] using nonneg
  · obtain ⟨t, ht⟩ := tendsto_finset_range.eventually (Ici_mem_atTop s) |>.exists
    calc
      ∑ i ∈ s, f ↑(i + N + 1) ≤ ∑ i ∈ range t, f ↑(i + N + 1) :=
        sum_le_sum_of_subset_of_nonneg ht <| by grind
      _ = ∑ i ∈ Ico N (N + t), f ↑(i + 1) := by rw [Finset.sum_Ico_eq_sum_range]; grind
      _ ≤ ∫ (x : ℝ) in Set.Ioi (N : ℝ), f x :=
        (anti.mono <| by grind).sum_Ico_le_integral integrable nonneg

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 * (1 / (c ^ i) ^ 2)

Tactic:
mul_div_assoc',

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 * 1 / (c ^ i) ^ 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✝ : ∀ (a : A), IsConnected (StructuredArrow (L.obj a) R)
⊢ (fst L R).Final

Tactic:
by
  have (a : Aᵒᵖ) : IsConnected (CostructuredArrow R.op (L.op.obj a)) :=
    (isConnected_iff_of_equivalence (structuredArrowOpEquivalence R (L.obj a.unop))).mp
      inferInstance
  have : (snd R.op L.op).Initial := initial_snd_of_isConnected_costructuredArrow _ _
  have : ((opFunctor L R).leftOp ⋙ snd R.op L.op).Initial :=
    initial_equivalence_comp (opEquiv L R).functor.leftOp _
  have : (fst L R).op.Initial := initial_of_natIso <| opFunctorCompSnd _ _
  apply final_of_initial_op

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
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

Tactic:
refine finallySmall_of_small_weakly_terminal_set
    (⋃ i, (map (colimit.ι F i)).obj '' (s i)) (fun A => ?_)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
⊢ ∃ j ∈ ⋃ i, (CostructuredArrow.map (colimit.ι F i)).obj '' s i, Nonempty (A ⟶ j)
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory IsIndObject
P : IndObjectPresentation X.obj
Q : IndObjectPresentation Y.obj
e₁ : { pt := X.obj, ι := P.ι }.pt ≅ (colimit.cocone (P.F ⋙ yoneda)).pt :=
  P.isColimit.coconePointUniqueUpToIso (colimit.isColimit (P.F ⋙ yoneda))
e₂ : { pt := Y.obj, ι := Q.ι }.pt ≅ (colimit.cocone (Q.F ⋙ yoneda)).pt :=
  Q.isColimit.coconePointUniqueUpToIso (colimit.isColimit (Q.F ⋙ yoneda))
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
let e₃ := Iso.homCongr e₁ e₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory IsIndObject
P : IndObjectPresentation X.obj
Q : IndObjectPresentation Y.obj
e₁ : { pt := X.obj, ι := P.ι }.pt ≅ (colimit.cocone (P.F ⋙ yoneda)).pt :=
  P.isColimit.coconePointUniqueUpToIso (colimit.isColimit (P.F ⋙ yoneda))
e₂ : { pt := Y.obj, ι := Q.ι }.pt ≅ (colimit.cocone (Q.F ⋙ yoneda)).pt :=
  Q.isColimit.coconePointUniqueUpToIso (colimit.isColimit (Q.F ⋙ yoneda))
e₃ : ({ pt := X.obj, ι := P.ι }.pt ⟶ { pt := Y.obj, ι := Q.ι }.pt) ≃
  ((colimit.cocone (P.F ⋙ yoneda)).pt ⟶ (colimit.cocone (Q.F ⋙ yoneda)).pt) :=
  e₁.homCongr e₂
⊢ Small.{v, max u v} (X ⟶ Y)
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i))
      ((ConcreteCategory.hom (colimitYonedaHomIsoLimit' D F).hom) f) =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
change ((colimitYonedaHomIsoLimit' D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom ((colimitYonedaHomIsoLimit' D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i)) f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝ : (F C).Faithful
this : (G C).Faithful
⊢ (F C ⋙ G C ⋙ H C).Faithful

Tactic:
have : (H C).Faithful := IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝¹ : (F C).Faithful
this✝ : (G C).Faithful
this : (H C).Faithful
⊢ (F C ⋙ G C ⋙ H C).Faithful
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ (singleObjHomologySelfIso (ComplexShape.up ℕ) ?m.123 I.kernelFork.pt).hom ≫
      ((singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).symm ≪≫
            isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm).hom ≫
        Fork.ι (KernelFork.ofι (iCycles I.cocomplex 0) ⋯) =
    (singleObjHomologySelfIso (ComplexShape.up ℕ) ?m.123 I.kernelFork.pt).hom ≫ Fork.ι I.kernelFork

pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ ℕ

Tactic:
← cancel_epi (isoHomologyπ₀ _).hom,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ (isoHomologyπ₀ ((single C (ComplexShape.up ℕ) 0).obj I.kernelFork.pt)).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).hom ≫
        ((singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).symm ≪≫
              isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm).hom ≫
          Fork.ι (KernelFork.ofι (iCycles I.cocomplex 0) ⋯) =
    (isoHomologyπ₀ ((single C (ComplexShape.up ℕ) 0).obj I.kernelFork.pt)).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).hom ≫ Fork.ι I.kernelFork
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f + (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯
          (-↑m) ⋯ ⋯))

Tactic:
rw [Cocycle.toSingleMk_add _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ +
          Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯))