mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
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 : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k (c • u) (t • u)

Tactic:
]

Goal state after:
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
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k (c • u) (t • u)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
]

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : ∃ k, -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
]

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : ∃ k, -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
]

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma z * Gamma (1 - z) = 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case refine_1
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
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ ∑ j, (↑fs'').indicator w'' j = ∑ j ∈ fs'', w'' j

Tactic:
]

Goal state after:
case refine_1
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
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ ∑ j, (↑fs'').indicator w'' j = ∑ j ∈ fs'', w'' j
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma (-↑k) * Gamma (1 - -↑k) = 0

Tactic:
]

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma (-↑k) * Gamma (1 - -↑k) = 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inl.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₄) (s.points i₃)

Tactic:
]

Goal state after:
case inl.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₄) (s.points i₃)
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
hx : e x = x
hy : e y = y
hm : f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)

Tactic:
]

Goal state after:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
hx : e x = x
hy : e y = y
hm : f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ 0 = 0

Tactic:
]

Goal state after:
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
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ (Finset.affineCombination k Finset.univ p) ((↑fs'').indicator w'') = (Finset.affineCombination k fs'' p) w''

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
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ (Finset.affineCombination k Finset.univ p) ((↑fs'').indicator w'') = (Finset.affineCombination k fs'' p) w''
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr.inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
]

Goal state after:
case inr.inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ ↑π / sin (↑π * z) = ↑π / sin (↑π * z)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
n : ℕ
⊢ ↑n / (↑n + (1 - z)) = ↑n / (↑n + (1 - z))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₄) (s.points i₃)

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₄) (s.points i₃)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n ↦ (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) atTop (𝓝 (sin (↑π * z)))

Tactic:
]

Goal state after:
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n ↦ (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) atTop (𝓝 (sin (↑π * z)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
n : ℕ
⊢ ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2) = ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
⊢ ↑s.re = ↑s.re

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
⊢ Real.Gamma s.re ≠ 0

Tactic:
]

Goal state after:
case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
⊢ Real.Gamma s.re ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
s : ℂ
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
hs : s.re = -↑n
⊢ s.re = -↑n

Tactic:
]

Goal state after:
case pos
s : ℂ
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
hs : s.re = -↑n
⊢ s.re = -↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
⊢ ∀ (k : ℤ), ↑π * s ≠ ↑k * ↑π

Tactic:
]

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
⊢ ∀ (k : ℤ), ↑π * s ≠ ↑k * ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ 0

Tactic:
]

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
]

Goal state after:
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ r = r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℝ
n : ℕ
⊢ ↑n ^ ↑s * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x) = ↑n ^ ↑s * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inl
s : ℂ
h : s ≠ 0
⊢ (Gamma s)⁻¹ = (Gamma s)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inr
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case zero
s : ℂ
hs : 0 < s.re
⊢ DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s

Tactic:
]

Goal state after:
case zero
s : ℂ
hs : 0 < s.re
⊢ DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ DifferentiableAt ℂ (fun x ↦ x * (Gamma (x + 1))⁻¹) s

Tactic:
]

Goal state after:
case succ
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ DifferentiableAt ℂ (fun x ↦ x * (Gamma (x + 1))⁻¹) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -s.re < ↑n.succ

Tactic:
]

Goal state after:
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -s.re < ↑n.succ
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)

Tactic:
]

Goal state after:
case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (x (s.points 0)) (x (s.points 1))

Tactic:
]

Goal state after:
case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (x (s.points 0)) (x (s.points 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ u.betaIntegral v = u.betaIntegral v

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
i : Fin 3
⊢ c i * (1 - r i) = c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) (i + 1)

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
i : Fin 3
⊢ c i * (1 - r i) = c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) (i + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_2
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma s * Gamma (s + 1 / 2)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case e'_3
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ dist (s.points i) (s.points j) = dist (x (s.points 0)) (x (s.points 1))

Tactic:
]

Goal state after:
case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ dist (s.points i) (s.points j) = dist (x (s.points 0)) (x (s.points 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π

Tactic:
]

Goal state after: