mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - ↑m)

Tactic:
simpa only [Rat.cast_intCast] using h.sub_ratCast m

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * (y ^ (2 * x) * y) = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)

Tactic:
← pow_succ,

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * y ^ (2 * x + 1) = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 0 < arcosh x

Tactic:
by
  apply log_pos
  calc
    1 < x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity

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

Goal state before:
pp: x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
obtain h | h := le_total n m
    · exact (agmSequences_fst_monotone h).trans this
    · exact this.trans (agmSequences_snd_antitone h)

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

Goal state before:
pp: p : ℝ
⊢ binEntropy p = p.negMulLog + (1 - p).negMulLog

Tactic:
by simp [binEntropy, negMulLog, ← neg_mul]

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

Goal state before:
pp: case hf
h₁ : 0 < 1 / 2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)

Tactic:
filter_upwards [Ioc_mem_nhdsGT h₁] with p hx

Goal state after:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ log (1 / 2) ≤ log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ 1 / 2 ∈ Icc 0 1

Tactic:
constructor <;> norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ EqOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (fun t ↦ t ^ (p - 1) * x / (t + x)) (Ioi 0)

Tactic:
intro t ht

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : t ∈ Ioi 0
⊢ (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) t = (fun t ↦ t ^ (p - 1) * x / (t + x)) t
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)

Tactic:
have haddl : Function.Injective addl := by intro _ _; simp [addl]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s / 2) + -1) * Gamma (s / 2 + 1) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π

Tactic:
Gamma_add_one _ (div_ne_zero hs two_ne_zero),

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s / 2) + -1) * (s / 2 * Gamma (s / 2)) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₀₁ x 0 = 0
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ

Tactic:
calc
    a ^ p = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₀₁ p t r ∂μ) a := by
      rw [nnrpow_eq_cfcₙ_real _ _]
      exact cfcₙ_congr fun r _ ↦ (hμ r (by grind)).2
    _ = _ := cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
                hbound_finite_integral ha.isSelfAdjoint

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (log b r + 1)

Tactic:
· rw [log_of_right_le_one _ hr1.le]
    have hcri : 1 < r⁻¹ := (one_lt_inv₀ hr).2 hr1
    have : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊ :=
      Nat.succ_le_of_lt (Nat.clog_pos hb <| Nat.one_lt_cast.1 <| hcri.trans_le (Nat.le_ceil _))
    rw [neg_add_eq_sub, ← neg_sub, ← Int.ofNat_one, ← Int.ofNat_sub this, zpow_neg, zpow_natCast,
      lt_inv_comm₀ hr (pow_pos (Nat.cast_pos.mpr <| zero_lt_one.trans hb) _), ← Nat.cast_pow]
    refine Nat.lt_ceil.1 ?_
    exact Nat.pow_pred_clog_lt_self hb <| Nat.one_lt_cast.1 <| hcri.trans_le <| Nat.le_ceil _

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊

Tactic:
exact Nat.log_mono_right (Nat.floor_mono h)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case integral
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₁₂ t) a ∂μ

Tactic:
case integral => calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
simp_rw [logb, div_eq_zero_iff, log_eq_zero]
  tauto

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

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
⊢ ∀ (x : ℕ → ℝ),
    Tendsto x atTop (𝓝[>] 0) →
      Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ x) atTop (𝓝 (∫ (x : E), g x ∂P))

Tactic:
intro u

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
⊢ Tendsto u atTop (𝓝[>] 0) → Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_12
L : PeriodPair
⊢ ↑L.lattice = ↑L.lattice \ {L.ω₁ / 2}

Tactic:
simp [L.ω₁_div_two_notMem_lattice]

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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
x : ℝ
hx : 0 < x
⊢ (fun x ↦ (ENNReal.ofReal (↑x ^ (dim E - 1))).toReal • f ↑x) ⟨x, hx⟩ = (fun x ↦ ↑x ^ (dim E - 1) • f ↑x) ⟨x, hx⟩

Tactic:
simp (disch := positivity) [ENNReal.toReal_ofReal]

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

Goal state before:
pp: ⊢ range sigmoid = Ioo 0 1

Tactic:
rw [sigmoid, Subtype.range_coind, Real.range_sigmoid]

Goal state after:
⊢ Subtype.val ⁻¹' Ioo 0 1 = Ioo 0 1
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ stirlingSeq 0 = 0

Tactic:
by
  rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]

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

Goal state before:
pp: x : ℝ
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
by_cases h : x ≠ -1 ∧ x ≠ 1

Goal state after:
case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)

Goal state after:
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
l : ↥L.lattice
⊢ ‖((↑l - x) ^ r)⁻¹‖ ≤ ‖↑l - x‖ ^ (-↑r)

Tactic:
rw [← zpow_natCast, ← zpow_neg, ← norm_zpow]

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

Goal state before:
pp: ⊢ (fun n ↦ ↑n !) ~[atTop] fun n ↦ √(2 * ↑n * π) * (↑n / rexp 1) ^ n

Tactic:
apply Asymptotics.isEquivalent_of_tendsto_one
  have : sqrt π ≠ 0 := by positivity
  nth_rewrite 2 [← div_self this]
  convert! tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1
  ext n
  simp [field, stirlingSeq, mul_right_comm]

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

Goal state before:
pp: case e'_2
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (∑ i ∈ range n, Complex.exp (↑k / ↑n * ↑π * I) ^ i) * (Complex.exp (↑k / ↑n * ↑π * I) - 1)

Tactic:
simp_rw [sum_mul]

Goal state after:
case e'_2
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ ∑ i ∈ range n,
      Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
        (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    ∑ i ∈ range n, Complex.exp (↑k / ↑n * ↑π * I) ^ i * (Complex.exp (↑k / ↑n * ↑π * I) - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
⊢ sumZeroes n (T ℝ k) = 0

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp [sumZeroes]
  suffices ∑ i ∈ range n, 2 * cos (k * ((2 * i + 1) / (2 * n) * π)) = 0 by
    rw [sumZeroes, mul_eq_zero_iff_left (by aesop)]
    rw [← mul_sum, mul_eq_zero_iff_left (by norm_num)] at this
    simpa [T_real_cos]
  suffices (∑ i ∈ range n, 2 * cos (k * ((2 * i + 1) / (2 * n) * π)) : ℂ) = 0 by norm_cast at this ⊢
  suffices ∑ i ∈ range n, 2 * Complex.cos (k * ((2 * i + 1) / (2 * n) * π)) = 0 by aesop
  simp_rw [Complex.two_cos, ← neg_mul, ← Int.cast_neg]
  have : (-1 : ℂ) ^ (-k) = (-1) ^ k := by rw [← Int.cast_negOnePow, ← Int.cast_negOnePow]; simp
  rw [sum_add_distrib, sum_exp hn hk, sum_exp hn (by aesop),
    Int.cast_neg, neg_div, neg_mul, neg_mul, Complex.exp_neg,
    neg_div, neg_mul, neg_mul, Complex.exp_neg, this, ← add_mul, mul_eq_zero_of_left]
  set z := exp (k / (2 * n) * π * I) with hz
  have hz₂ : exp (k / n * π * I) = z ^ 2 := by rw [hz, ← Complex.exp_nat_mul]; grind
  rw [hz₂, ← inv_pow z 2]
  field [show z ≠ 0 by grind [Complex.exp_ne_zero],
    show (z ^ 2 - 1 ≠ 0) ∧ (1 - z ^ 2 ≠ 0) by grind [exp_sub_one_ne_zero]]

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

Goal state before:
pp: n i : ℕ
hi : i ≤ n
this : 0 < ((-1) ^ i)⁻¹ * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 < (-1) ^ i * leadingCoeffC n i

Tactic:
← inv_pow,

Goal state after:
n i : ℕ
hi : i ≤ n
this : 0 < (-1)⁻¹ ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 < (-1) ^ i * leadingCoeffC n i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ n)| ≤ 1 → |x| ≤ 1

Tactic:
simpa using mt <| one_lt_abs_eval_T_real hn

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

Goal state before:
pp: L : PeriodPair
x : ℂ
i : ℕ
⊢ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l

Tactic:
L.coeff_weierstrassPExceptSeries,

Goal state after:
L : PeriodPair
x : ℂ
i : ℕ
⊢ ∑' (l : ↥L.lattice), L.weierstrassPExceptSummand (L.ω₁ / 2) x i l = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
cos_arccos (by grind) (by grind)

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑(Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).card = (U ℝ ↑n).degree

Tactic:
· rw [Finset.card_image_of_injOn, Finset.card_range, degree_U_natCast]
    exact (Finset.range n).nodup_map_iff_injOn.mp (roots_U_real_nodup n)

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

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

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
    congr
    rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]
    congr with k
    ring

Goal state after:
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
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : b / (1 - a) < arithGeom a b u₀ n
⊢ arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)

Tactic:
rw [div_lt_iff_of_neg (sub_neg.mpr ha)] at h_lt

Goal state after:
R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
⊢ arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℕ
hn0 : ¬n = 0
⊢ fib (-↑n + 1) = (-1) ^ (n + 1) * ↑(Nat.fib n) + (-1) ^ (1 + (n + 1)) * ↑(Nat.fib (n + 1))

Tactic:
symm
    calc _ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp

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

Goal state before:
pp: ⊢ ψ * φ = -1

Tactic:
rw [mul_comm]
  exact goldenRatio_mul_goldenConj

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ φ f g ≫ biprod.snd = biprod.snd ≫ g

Tactic:
dsimp [φ]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.snd = biprod.snd ≫ g
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)

Tactic:
exact (ha N (a.le_succ.trans aN)).2

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
⊢ biprod.inl ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inl ≫ 0

Tactic:
rw [biprod.inl_desc_assoc, assoc, biprod.inl_desc, comp_zero,
      ← assoc, cokernel.condition]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : Y ⊞ Z ⟶ A
hk : φ f g ≫ k = 0
⊢ (f ≫ g) ≫ biprod.inr ≫ k = 0

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : Y ⊞ Z ⟶ A
hk : φ f g ≫ k = 0
⊢ π f g ≫ cokernel.desc (f ≫ g) (biprod.inr ≫ k) ?refine_1 = k

Tactic:
all_goals
      obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_from k
      simp only [comp_add, φ_snd_assoc, biprod.ext_from_iff, inl_φ_assoc,
        BinaryBicone.inl_fst_assoc, BinaryBicone.inl_snd_assoc, zero_comp, add_zero, comp_zero,
        inr_φ_fst_assoc, neg_comp, id_comp, BinaryBicone.inr_snd_assoc, neg_add_eq_zero] at hk
      obtain ⟨hk, rfl⟩ := hk
      aesop

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ (preadditiveYoneda.obj G).Faithful

Tactic:
by
  rw [isCoseparator_iff_faithful_yoneda_obj, ← whiskering_preadditiveYoneda, Functor.comp_obj,
    Functor.whiskeringRight_obj_obj]
  exact ⟨fun h => Functor.Faithful.of_comp _ (forget AddCommGrpCat),
    fun h => Functor.Faithful.comp _ _⟩

Goal state after:
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
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
cNn : c (N - 1) ≤ n
B : N - 1 + 1 = N
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))

Tactic:
simpa [B] using (ha _ aN').1

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
⊢ Function.Surjective (preadditiveCoyonedaObj G).map

Tactic:
← Functor.coe_mapAddHom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
⊢ Function.Surjective ⇑(preadditiveCoyonedaObj G).mapAddHom
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ HasFiniteLimits A.Elements

Tactic:
exact ⟨fun J _ _ => inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

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

Tactic:
rw [G]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (F C).Faithful
⊢ Ind.yoneda.rightOp.Faithful
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

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

Tactic:
rw [G]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (F C).Full
⊢ Ind.yoneda.rightOp.Full
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

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

Tactic:
rw [G]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : PreservesFiniteLimits (F C)
⊢ PreservesFiniteLimits Ind.yoneda.rightOp