mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed → μ.InnerRegularWRT IsCompact IsClosed

case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT IsCompact IsClosed → μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed → μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed → μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n✝ n : ℕ
⊢ Prod.swap ⁻¹' t n = t n

Tactic:
ext

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n✝ n : ℕ
x✝ : α × α
⊢ x✝ ∈ Prod.swap ⁻¹' t n ↔ x✝ ∈ t n
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
⊢ μ.InnerRegularCompactLTTop

Tactic:
constructor

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
⊢ μ.InnerRegularWRT IsCompact fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere.real univ = ↑(dim E) * μ.real (ball 0 1)

Tactic:
simp [measureReal_def]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ 10 * r / ‖l‖ ^ 3 = 10 * r * ‖l‖ ^ (-3)

Tactic:
by norm_cast

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

Goal state before:
pp: n a : ℕ
hn : n ≠ 0
⊢ (∃ x, x ^ n = a) ↔ n.nthRoot a ^ n = a

Tactic:
constructor

Goal state after:
case mp
n a : ℕ
hn : n ≠ 0
⊢ (∃ x, x ^ n = a) → n.nthRoot a ^ n = a

case mpr
n a : ℕ
hn : n ≠ 0
⊢ n.nthRoot a ^ n = a → ∃ x, x ^ n = a
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ ℘[L] (-z) = ℘[L] z

Tactic:
by
  simp only [weierstrassP]
  rw [← (Equiv.neg L.lattice).tsum_eq]
  congr with l
  simp
  ring

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

Goal state before:
pp: case e_f
n : ℕ
a : Multiset ℂ
hn : n ≠ 0
⊢ (fun x ↦ x + ↑n) = fun j ↦ ↑n * (j / ↑n + 1)

Tactic:
ext

Goal state after:
case e_f
n : ℕ
a : Multiset ℂ
hn : n ≠ 0
x✝ : ℂ
⊢ x✝ + ↑n = ↑n * (x✝ / ↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
⊢ (FormalMultilinearSeries.ofScalars ℂ (regularizedHGFunCoeff a b)).coeff = regularizedHGFunCoeff a b

Tactic:
ext

Goal state after:
a b : Multiset ℂ
x✝ : ℕ
⊢ (FormalMultilinearSeries.ofScalars ℂ (regularizedHGFunCoeff a b)).coeff x✝ = regularizedHGFunCoeff a b x✝
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
⊢ ↑(b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) < ↑n

Tactic:
by norm_cast

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

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

Tactic:
simpa using (tendsto_const_div_atTop_nhds_zero_nat i).add_const 1

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

Goal state before:
pp: x : ℝ
⊢ sigmoid (-x) = σ (sigmoid x)

Tactic:
ext

Goal state after:
x : ℝ
⊢ ↑(sigmoid (-x)) = ↑(σ (sigmoid x))
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: ⊢ Subtype.val ⁻¹' Ioo 0 1 = Ioo 0 1

Tactic:
ext

Goal state after:
x✝ : { x // x ∈ I }
⊢ x✝ ∈ Subtype.val ⁻¹' Ioo 0 1 ↔ x✝ ∈ Ioo 0 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f

Tactic:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
x : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f

Tactic:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
x : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo a b), ‖deriv (⇑g ∘ f) a‖ₑ ≤ ‖deriv f a‖ₑ

Tactic:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv (⇑g ∘ f) x‖ₑ ≤ ‖deriv f x‖ₑ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ (fun a ↦ ‖deriv f a‖ₑ) =ᵐ[volume.restrict (Ioo a b)] fun a_1 ↦ ‖derivWithin f (Icc a b) a_1‖ₑ

Tactic:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv f x‖ₑ = ‖derivWithin f (Icc a b) x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case succ
L : PeriodPair
l₀ x : ℂ
i : ℕ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x
          else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
| succ i =>

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ -2 ≤ ↑k ∧ ↑k ≤ 2

Tactic:
constructor

Goal state after:
case left
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ -2 ≤ ↑k

case right
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ ↑k ≤ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = Complex.exp (↑k / (2 * ↑n) * ↑π * I) ^ 2

Tactic:
← Complex.exp_nat_mul

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = Complex.exp (↑2 * (↑k / (2 * ↑n) * ↑π * I))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∫ (x : ℝ), eval x (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i)

Tactic:
eval_finsetSum,

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∫ (x : ℝ), ∑ i ∈ range (2 * n), eval x (c i • ↑(chebyshevTsequence ℝ) i) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r * π ∈ Set.Icc (0 * π) (1 * π)

Tactic:
constructor

Goal state after:
case left
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ 0 * π ≤ ↑r * π

case right
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r * π ≤ 1 * π
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - l₀] (L.weierstrassPExceptSeries l₀ x) x ↑r

Tactic:
constructor

Goal state after:
case r_le
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ ↑r ≤ (L.weierstrassPExceptSeries l₀ x).radius

case r_pos
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ 0 < ↑r

case hasSum
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ {y : ℂ}, y ∈ Metric.eball 0 ↑r → HasSum (fun n ↦ (L.weierstrassPExceptSeries l₀ x n) fun x ↦ y) (℘[L - l₀] (x + y))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: m n : ℤ
⊢ ↑|n| ≤ ‖![n, m]‖

Tactic:
simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
  left
  rw [Int.abs_eq_natAbs]
  exact le_refl _

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ ↑n ≠ 0

Tactic:
by norm_cast

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ ↑n)| = 1 ↔ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ ↑n)| = 1 → ∃ k ≤ n, x = cos (↑k * π / ↑n)

case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → |eval x (T ℝ ↑n)| = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ ↑n) = 1 ↔ ∃ k ≤ n, Even k ∧ x = cos (↑k * π / ↑n)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ ↑n) = 1 → ∃ k ≤ n, Even k ∧ x = cos (↑k * π / ↑n)

case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ (∃ k ≤ n, Even k ∧ x = cos (↑k * π / ↑n)) → eval x (T ℝ ↑n) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ ↑n) = -1 ↔ ∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ ↑n) = -1 → ∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)

case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ (∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)) → eval x (T ℝ ↑n) = -1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ L.sumInvPow 0 = L.G

Tactic:
ext

Goal state after:
L : PeriodPair
x✝ : ℕ
⊢ L.sumInvPow 0 x✝ = L.G x✝
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c k : ℤ
hk : 2 ≤ k
⊢ 1 < ↑k

Tactic:
by norm_cast

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ 1 < ↑k

Tactic:
by norm_cast

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

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ 1 < 2

Tactic:
by norm_cast

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ 1 < 2

Tactic:
by norm_cast

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x ↔ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x → ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

case mpr
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ (∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)) → IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x ↔ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x → ∃ k ≤ n, x = cos (↑k * π / ↑n)

case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

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

Tactic:
ext

Goal state after:
R : Type u_1
a b u₀ : R
inst✝ : Field R
ha : a ≠ 1
x✝ : ℕ
⊢ arithGeom a b u₀ x✝ = a ^ x✝ * (u₀ - b / (1 - a)) + b / (1 - a)
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
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (arithGeom a b u₀) atTop (𝓝 (b / (1 - a)))

Tactic:
rw [arithGeom_eq' ha.ne]

Goal state after:
R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun n ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (b / (1 - a)))
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False

Tactic:
exact nk <| minFac_dvd n

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

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun n ↦ ‖(↑(n + 1) ^ (1 + k))⁻¹‖

Tactic:
rw [summable_norm_iff, summable_nat_add_iff (f := fun n : ℕ ↦ ((n : ℝ) ^ (1 + k))⁻¹)]

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun n ↦ (↑n ^ (1 + k))⁻¹
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
⊢ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) = 0

Tactic:
ext

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

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.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 : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, mem_Ico, ← Nat.add_one_le_iff] at hx 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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i + 1 ≤ b
⊢ 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 : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
simp only [Nat.cast_add, Nat.cast_one, mem_Ico, ← Nat.add_one_le_iff] at hx 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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i + 1 ≤ b
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i
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:
by
  rw [← Functor.coe_mapAddHom, ← AddCommGrpCat.hom_ofHom (preadditiveCoyonedaObj G).mapAddHom,
    ← AddCommGrpCat.epi_iff_surjective]
  let cm : ShortComplex C := ⟨kernel.ι p, p, by simp⟩
  have exact : cm.Exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel _)
  have mono : Mono cm.op.f := by dsimp [cm]; infer_instance
  let φ := preadditiveCoyonedaObj G
  have faithful : φ.Faithful := by rwa [← isSeparator_iff_faithful_preadditiveCoyonedaObj]
  apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))
  · exact exact.op.map_of_mono_of_preservesKernel _ mono inferInstance
  · simp only [ShortComplex.map_f]
    infer_instance
  · suffices φ.map.Surjective by simpa [AddCommGrpCat.epi_iff_surjective, Functor.coe_mapAddHom]
    exact fun f => ⟨f (𝟙 G), by cat_disch⟩
  · simp [AddCommGrpCat.mono_iff_injective, Functor.coe_mapAddHom, Functor.map_injective]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case e'_3.e_f
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ (fun i ↦ f ↑(i + N)) = fun n ↦ f ↑(n + (N - 1) + 1)

Tactic:
ext

Goal state after:
case e'_3.e_f
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
x✝ : ℕ
⊢ f ↑(x✝ + N) = f ↑(x✝ + (N - 1) + 1)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (generator F)

Tactic:
rw [generator]
  infer_instance

Goal state after: