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

Goal state before:
pp: L : PeriodPair
⊢ ¬((1 / 2).den = 1 ∧ Rat.den 0 = 1)

Tactic:
norm_num

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

Goal state before:
pp: L : PeriodPair
⊢ ¬(Rat.den 0 = 1 ∧ (1 / 2).den = 1)

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ guess ≤ a / guess ^ (n + 1)

Tactic:
linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
x✝¹ : ℝ
x✝ : x✝¹ > 0
⊢ 2 < 3

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
⊢ regularizedHGFunCoeff a b n = 0 ↔ (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m

Tactic:
by
  unfold regularizedHGFunCoeff
  simp
  grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a : Multiset ℂ
i : ℂ
⊢ i ∈ a → Tendsto (fun n ↦ i / ↑n + 1) atTop (𝓝 ((fun x ↦ 1) i))

Tactic:
hi

Goal state after:
a : Multiset ℂ
i : ℂ
hi : i ∈ a
⊢ Tendsto (fun n ↦ i / ↑n + 1) atTop (𝓝 ((fun x ↦ 1) i))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁ : ¬↑x = l₀
e : l - ↑x = 0
⊢ ↑x = l₀

Tactic:
by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁ : ¬↑x = l₀
e : l - ↑x = 0
⊢ ↑x = l₀

Tactic:
by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn (fun x ↦ f ‖x‖) (ball 0 r) μ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ

Tactic:
by
      rw [← integrable_indicator_iff measurableSet_ball]
      apply integrable_congr
      filter_upwards with x
      simp [indicator]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: ⊢ 1 + 0 ≠ 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case zero
⊢ 2 ≤ (1 + 1) ^ 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑0 + 1) + 1)) ^ 2 < 1

Tactic:
norm_num

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

Goal state before:
pp: f : ℝ → ℝ
⊢ -1 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ -1 < 1

Tactic:
norm_num

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.uIoc (-1) 1) volume
⊢ -1 ≤ 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ a ^ 2 / 2 = a ^ 4 / a ^ 2 / 2

Tactic:
← mul_one_div (a ^ 4) (a ^ 2),

Goal state after:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ a ^ 2 / 2 = a ^ 4 * (1 / a ^ 2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

Tactic:
rw [integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)]; simp

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

Goal state before:
pp: n m : ℤ
this :
  ∫ (x : ℝ), eval x (2 * T ℝ n * T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
eval_mul,

Goal state after:
n m : ℤ
this :
  ∫ (x : ℝ), eval x 2 * eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
⊢ Disjoint (Finset.range i) (Finset.Ioc i n)

Tactic:
grind [Finset.disjoint_iff_ne]

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : 2 * ∑ i ∈ range n, cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ 2 ≠ 0

Tactic:
norm_num

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

Goal state before:
pp: 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.2 - x‖ ^ (-3 - ↑p.1) * ‖z - x‖ ^ (p.1 + 1)

Tactic:
norm_num

Goal state after:
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
⊢ ‖↑p.1 + 1 + 1‖ * ‖↑p.2 - x‖ ^ (-2 + (-1 + -↑p.1)) = ‖↑p.1 + 2‖ * ‖↑p.2 - x‖ ^ (-3 - ↑p.1) ∨ z - x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case ha
n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ 1 ≤ 2

Tactic:
norm_num

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

Goal state before:
pp: n : ℕ
x✝ : n + 1 ≠ 0
⊢ #(box (n + 1)) = 8 * (n + 1)

Tactic:
simp_rw [Prod.card_box_succ, card_Icc, sub_neg_eq_add]
    norm_cast
    refine tsub_eq_of_eq_add ?_
    zify
    ring

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

Goal state before:
pp: case h
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
this : d - 1 < n - 1
⊢ 1 < 2

Tactic:
norm_num

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

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

Tactic:
lift k to ℕ using (by rw [← Int.cast_nonneg_iff (R := ℝ), hk']; positivity [arccos_nonneg x])

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ↑(-2) = -2

Tactic:
norm_num

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

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : z = 0
⊢ 0 = 2 ^ 2 - 4

Tactic:
norm_num

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

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

Tactic:
eval_mul,

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.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a)

Tactic:
rw [arithGeom_eq ha n]

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (b - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)

Tactic:
rw [arithGeom_eq ha n]

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (0 - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ n) / (1 - a)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (-n) = if Even n then -fib n else fib n

Tactic:
by
  obtain ⟨n, _⟩ := n.eq_nat_or_neg
  aesop (add safe (by rw [fib_neg_natCast]))

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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ logDeriv (fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)) x = ↑π * (↑π * x).cot - 1 / x

Tactic:
logDeriv_div _ (by apply sin_pi_mul_ne_zero hz) ?_
    (DifferentiableAt.comp _ (Complex.differentiableAt_sin) (by fun_prop)) (by fun_prop),

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ logDeriv (Complex.sin ∘ fun t ↦ ↑π * t) x - logDeriv (HMul.hMul ↑π) x = ↑π * (↑π * x).cot - 1 / x

x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case ha
⊢ 0 < 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case hb
⊢ 0 < √5

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case bc
⊢ 5 < 3 ^ 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case bc
⊢ 0 < 3

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (1 + 3) / 2 = 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ Nat.Prime 5

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ 0.5 ≠ 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ 0.5 ≠ 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: i : ℕ
⊢ i ∈ ↑(Finset.range fibRec.order) → (fun n ↦ ↑(Nat.fib n)) i = (fun n ↦ (φ ^ n - ψ ^ n) / √5) i

Tactic:
hi

Goal state after:
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n ↦ ↑(Nat.fib n)) i = (fun n ↦ (φ ^ n - ψ ^ n) / √5) i
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ √5 ≠ 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
⊢ ∑ i ∈ Finset.Ico a b, f ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, g x

Tactic:
have A i (hi : i ∈ Finset.Ico a b) : IntervalIntegrable g volume i ↑(i + 1) := by
    rw [intervalIntegrable_iff_integrableOn_Ico_of_le (by simp)]
    simp only [Finset.mem_Ico, ← Nat.add_one_le_iff] at hi
    rify at hi
    exact hg.mono (by grind) le_rfl

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∑ i ∈ Finset.Ico a b, f ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, g x
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 : ℕ
⊢ i ∈ Ico a b → ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
hi

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 : ℕ
hi : i ∈ Ico a b
⊢ ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i * g ↑i ≤ f x * g (x - 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: 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 : ℕ
⊢ i ∈ Ico a b → ∀ x ∈ Ico ↑i ↑(i + 1), f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
hi

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 : ℕ
hi : i ∈ Ico a b
⊢ ∀ x ∈ Ico ↑i ↑(i + 1), f x * g (x - 1) ≤ f ↑i * g ↑i
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
⊢ i ∈ {i ∈ range N | j < c ^ i} → i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N

Tactic:
hi

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i ∈ {i ∈ range N | j < c ^ i}
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N
Module: Mathlib.CategoryTheory.Filtered.Small

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

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization,
        CofilteredClosureSmall.bundledAbstractCofilteredClosure]

Goal state after:
case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ (f ∘ ULift.down) (id { down := x }) = f x
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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom ((colimitCoyonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i))) f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }

Tactic:
simp only [colimitCoyonedaHomIsoLimit, Iso.trans_hom, Category.assoc,
    HasLimit.isoOfNatIso_hom_π]

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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((colimitHomIsoLimitYoneda (D.rightOp ⋙ coyoneda) F).hom ≫
          limit.π ((D.rightOp ⋙ coyoneda).op ⋙ yoneda.obj F) (op i) ≫
            ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app (op i)))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ J.ι ≫ desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι

Tactic:
ext
  simp [desc, descFOne, descFZero]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ { X₁ := I.cocomplex.X 0, X₂ := I.cocomplex.X (0 + 1), X₃ := I.cocomplex.X (0 + 2), f := I.cocomplex.d 0 (0 + 1),
          g := I.cocomplex.d (0 + 1) (0 + 2), zero := ⋯ }.f ≫
      (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) =
    0

Tactic:
rw [Preadditive.comp_sub, comp_descHomotopyZeroZero_assoc f comm,
          HomologicalComplex.Hom.comm, sub_self]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
x y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
this : HasDerivedCategory C
⊢ R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
this : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm y
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ I.iso.inv ≫ I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ =
    ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv) ≫ J.iso.hom

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ =
    ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv) ≫ J.iso.hom
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ (ofCocomplex Z).d 0 1 = d (Injective.ι Z)

Tactic:
by
  simp [ofCocomplex]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
x : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ ∃ f, ∃ (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = R.extEquivCohomologyClass.symm x

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ ∃ f, ∃ (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = R.extEquivCohomologyClass.symm (CohomologyClass.mk x)
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 : ℕ
x y : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
this : HasDerivedCategory C
⊢ R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
y : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
this : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm y
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 m : ℕ
hm : n + 1 = m
x : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ ∃ f, ∃ (hf : R.complex.d m n ≫ f = 0), R.extMk f m hm hf = R.extEquivCohomologyClass.symm x

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n m : ℕ
hm : n + 1 = m
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ ∃ f, ∃ (hf : R.complex.d m n ≫ f = 0), R.extMk f m hm hf = R.extEquivCohomologyClass.symm (CohomologyClass.mk x)