mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∏ x ∈ Finset.range n, (s + 1 + ↑x) = ∏ k ∈ Finset.range n, (s + ↑(k + 1))

pp: case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s

Tactic:
·

Goal state after:
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∏ x ∈ Finset.range n, (s + 1 + ↑x) = ∏ k ∈ Finset.range n, (s + ↑(k + 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s

Tactic:
·

Goal state after:
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ≠ 0

pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ∫ (x : ℝ) in 0..1, ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) =
    ∫ (x : ℝ) in 0..1, ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1))

Tactic:
·

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ≠ 0
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
⊢ ¬s.Nonempty → 0 ∉ asymptoticCone k s

pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
x✝ : s.Nonempty
⊢ 0 ∈ asymptoticCone k s

Tactic:
·

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
⊢ ¬s.Nonempty → 0 ∉ asymptoticCone k s
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
x✝ : s.Nonempty
⊢ 0 ∈ asymptoticCone k s

Tactic:
·

Goal state after:
case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
x✝ : s.Nonempty
⊢ 0 ∈ asymptoticCone k s
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
v : V
h : v ∈ asymptoticCone k s
hc : 0 ≤ 0
⊢ 0 • v ∈ asymptoticCone k s

pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
c : k
v : V
hc✝ : 0 ≤ c
h : v ∈ asymptoticCone k s
hc : 0 < c
⊢ c • v ∈ asymptoticCone k s

Tactic:
·

Goal state after:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
v : V
h : v ∈ asymptoticCone k s
hc : 0 ≤ 0
⊢ 0 • v ∈ asymptoticCone k s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
n : ℕ
⊢ IntervalIntegrable (fun x ↦ ↑x ^ (s - 1)) volume 0 ↑n

pp: case hg
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
n : ℕ
⊢ ContinuousOn (fun x ↦ ↑((1 - x / ↑n) ^ n)) (uIcc 0 ↑n)

Tactic:
·

Goal state after:
case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
n : ℕ
⊢ IntervalIntegrable (fun x ↦ ↑x ^ (s - 1)) volume 0 ↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
n : ℕ
⊢ IntervalIntegrable (fun x ↦ ↑x ^ (s - 1)) volume 0 ↑n

Tactic:
refine intervalIntegral.intervalIntegrable_cpow' ?_

Goal state after:
case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ -1 < (s - 1).re
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
c : k
v : V
hc✝ : 0 ≤ c
h : v ∈ asymptoticCone k s
hc : 0 < c
⊢ c • v ∈ asymptoticCone k s

Tactic:
·

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
c : k
v : V
hc✝ : 0 ≤ c
h : v ∈ asymptoticCone k s
hc : 0 < c
⊢ c • v ∈ asymptoticCone k s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hg
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
n : ℕ
⊢ ContinuousOn (fun x ↦ ↑((1 - x / ↑n) ^ n)) (uIcc 0 ↑n)

Tactic:
·

Goal state after:
case hg
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
n : ℕ
⊢ ContinuousOn (fun x ↦ ↑((1 - x / ↑n) ^ n)) (uIcc 0 ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ ?f₁ =ᶠ[atTop] fun n ↦ f n x

pp: case h
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto ?f₁ atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))

pp: case f₁
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ ℕ → ℂ

Tactic:
·

Goal state after:
case hl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ ?f₁ =ᶠ[atTop] fun n ↦ f n x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case h
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto (fun n ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))

Tactic:
·

Goal state after:
case h
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto (fun n ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ (fun n ↦ ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) = fun n ↦ ∫ (a : ℝ) in Ioi 0, f n a

pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ ∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)

Tactic:
·

Goal state after:
case e'_3
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ (fun n ↦ ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) = fun n ↦ ∫ (a : ℝ) in Ioi 0, f n a
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
⊢ (Finset.affineCombination k (fs ⟨i', hi'⟩) p) w' = p'

pp: case refine_3
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
⊢ ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j

Tactic:
·

Goal state after:
case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
⊢ (Finset.affineCombination k (fs ⟨i', hi'⟩) p) w' = p'
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case refine_3
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
⊢ ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j

Tactic:
·

Goal state after:
case refine_3
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
⊢ ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ ∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)

Tactic:
·

Goal state after:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ ∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : Convex k s
this : ∀ {s : Set V}, Convex k s → IsClosed[inst✝²] s → Convex k (asymptoticCone k s)
hs' : ¬IsClosed[inst✝²] s
⊢ Convex k (asymptoticCone k s)

pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
⊢ Convex k (asymptoticCone k s)

Tactic:
·

Goal state after:
case inr
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : Convex k s
this : ∀ {s : Set V}, Convex k s → IsClosed[inst✝²] s → Convex k (asymptoticCone k s)
hs' : ¬IsClosed[inst✝²] s
⊢ Convex k (asymptoticCone k s)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : ↑n < x
⊢ ‖(Ioc 0 ↑n).indicator (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)

pp: case inr
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ ‖(Ioc 0 ↑n).indicator (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
·

Goal state after:
case inl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : ↑n < x
⊢ ‖(Ioc 0 ↑n).indicator (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : Convex k ∅
hs' : IsClosed[inst✝²] ∅
⊢ Convex k (asymptoticCone k ∅)

pp: case inr
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
⊢ Convex k (asymptoticCone k s)

Tactic:
·

Goal state after:
case inl
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : Convex k ∅
hs' : IsClosed[inst✝²] ∅
⊢ Convex k (asymptoticCone k ∅)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inr
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ ‖(Ioc 0 ↑n).indicator (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
·

Goal state after:
case inr
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ ‖(Ioc 0 ↑n).indicator (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case e'_3
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
i : ↑s
r : k
hr :
  (Finset.affineCombination k (fs i) p) ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
j : ι
hj : ¬j = ↑i
hind :
  (↑(fs i)).indicator ((1 - r) • Pi.single (↑i) 1 + r • w i) j =
    (↑(fs ⟨i', hi'⟩)).indicator ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩) j
⊢ (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j =
    (↑(fs ⟨i', hi'⟩)).indicator ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩) j

Tactic:
·

Goal state after:
case e'_3
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
i : ↑s
r : k
hr :
  (Finset.affineCombination k (fs i) p) ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
j : ι
hj : ¬j = ↑i
hind :
  (↑(fs i)).indicator ((1 - r) • Pi.single (↑i) 1 + r • w i) j =
    (↑(fs ⟨i', hi'⟩)).indicator ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩) j
⊢ (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j =
    (↑(fs ⟨i', hi'⟩)).indicator ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩) j
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.inl
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
hs : ⌊1 - re 0⌋₊ = m + 1
⊢ Tendsto (GammaSeq 0) atTop (𝓝 (Gamma 0))

pp: case succ.inr
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
·

Goal state after:
case succ.inl
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
hs : ⌊1 - re 0⌋₊ = m + 1
⊢ Tendsto (GammaSeq 0) atTop (𝓝 (Gamma 0))