mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hsub : (support fun i ↦ logDeriv (F i)) ⊆ ↑hF.toFinset
⊢ mulSupport F ⊆ ↑hF.toFinset

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
⊢ (mulSupport fun i ↦ F i ^ d i) ⊆ ↑hd.toFinset

Tactic:
by simp +contextual [Set.subset_def, not_imp_not]

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

Goal state before:
pp: ⊢ 3 / 2 ∈ Ioi 0

Tactic:
simp

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

Goal state before:
pp: case zero
u : ℂ
hu : 0 < u.re
⊢ 1 / u = 1 / ∏ j ∈ Finset.range (0 + 1), (u + ↑j)

Tactic:
simp

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

Goal state before:
pp: case e'_3
x : ℝ
n : ℕ
⊢ ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ioc 0 1
⊢ 1 ∈ Ioc 0 1

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ici 2
⊢ 2 ∈ Ici 2

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ atTop • 𝓝 v ≤ atTop • 𝓝 v +ᵥ pure 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: 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
⊢ asymptoticNhds k P 0 = ⊤

Tactic:
by
  have ⟨p⟩ : Nonempty P := inferInstance
  rw [← asymptoticNhds_vadd_pure 0 p, asymptoticNhds_zero', vadd_pure]
  exact (Equiv.vaddConst p).surjective.filter_map_top

Goal state after:
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)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
⊢ ↑n ^ (s - 1) * ↑n ^ 1 = ↑n ^ (s - 1) * ↑n

Tactic:
simp

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

Goal state before:
pp: case refine_3.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 : 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'⟩)
hind :
  (↑(fs i)).indicator ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (↑(fs ⟨i', hi'⟩)).indicator ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
⊢ ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j

Tactic:
intro j

Goal state after:
case refine_3.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 : 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'⟩)
hind :
  (↑(fs i)).indicator ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (↑(fs ⟨i', hi'⟩)).indicator ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
j : ι
⊢ r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j
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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ᶠ (x : k) in atTop, id x • (a • v + b • u) +ᵥ p ∈ s

Tactic:
filter_upwards [eventually_ge_atTop 0] with c hc

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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ id c • (a • v + b • u) +ᵥ p ∈ s
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ = ‖f (g 0)‖

Tactic:
simp

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

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

Tactic:
| succ m IH =>

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(⇑f.contLinear + Function.const V (f 0)) (g 0)‖ = ‖f.contLinear (g 0) + (⇑f.contLinear + Function.const V (f 0)) 0‖

Tactic:
simp

Goal state after:
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
⊢ -(c • v) +ᵥ c • v +ᵥ p = p

Tactic:
simp

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
⊢ ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)

Tactic:
intro j

Goal state after:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
⊢ (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: 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 ι
hs : s.Nonempty
fs : ↑s → Finset ι
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)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
hwx : ∀ (i : ↑s), ∑ j ∈ fsx i, wx i j = 1
i : ↑s
⊢ fs i ⊆ insert (↑i) (fs i)

Tactic:
simp

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

Goal state before:
pp: 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
⊢ fs'' ⊆ Finset.univ

Tactic:
simp

Goal state after:
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
p : PE
⊢ f p =
    ((vaddConst (Classical.arbitrary PE)).trans
            (f.trans (vaddConst (f (Classical.arbitrary PE))).symm)).toRealLinearIsometryEquiv
        (p -ᵥ Classical.arbitrary PE) +ᵥ
      f (Classical.arbitrary PE)

Tactic:
simp

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))
⊢ ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)

Tactic:
simp

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
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
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
hp'w : ∀ (i : ↑Set.univ), p' ∈ line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
⊢ Set.univ.Nonempty

Tactic:
simp

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

Goal state before:
pp: case zero
z : ℂ
hz : ∀ (k : ℕ), z ≠ -↑k
⊢ Gamma (z + ↑0) / Gamma z = Polynomial.eval z (ascPochhammer ℂ 0)

Tactic:
simp

Goal state after:
case zero
z : ℂ
hz : ∀ (k : ℕ), z ≠ -↑k
⊢ ¬Gamma z = 0
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)]
i : Fin 3
c : k
j : Fin 3
⊢ i ∈ Set.univ

Tactic:
simp

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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ s.points i = (s.reindex e).points (e i)

Tactic:
simp

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

Goal state before:
pp: case e'_4
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ s.points j = (s.reindex e).points (e j)

Tactic:
simp

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)]
i : Fin 3
⊢ i ∈ Set.univ

Tactic:
simp

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

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

pp: case inr
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹

Tactic:
· rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]

Goal state after:
case inr
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case zero
m : ℕ
hs : 0 < (-↑m).re
⊢ (-↑m).re ≤ 0

Tactic:
simp

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
⊢ i + 1 ≠ i

Tactic:
simp

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

Goal state before:
pp: 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 (2 * s) * 2 ^ (1 - 2 * s) * ↑√π

Tactic:
convert! congr_arg Inv.inv (congr_fun this s) using 1

Goal state after:
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))⁻¹)⁻¹

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 ^ (2 * s - 1) / ↑√π)⁻¹
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:
simp

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
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
i : Fin 3
⊢ i + 2 ≠ i

Tactic:
simp

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

Goal state before:
pp: case e'_3.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.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ (Equiv.swap 1 j) i = i

pp: case e'_3.e'_4
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
⊢ (Equiv.swap 1 j) ((Equiv.swap 0 i) 1) = j

Tactic:
· exact Equiv.swap_apply_of_ne_of_ne hi hij

Goal state after:
case e'_3.e'_4
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
⊢ (Equiv.swap 1 j) ((Equiv.swap 0 i) 1) = j
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
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
i : Fin 3
⊢ c i * r i = c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) (i + 2)

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
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
⊢ (Equiv.swap 1 j) 1 = j

Tactic:
simp

Goal state after: