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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-a)
this : log =o[𝓝[>] 0] fun t ↦ t ^ (a - b)
t : ℝ
⊢ (fun x ↦ log x • f x) t = (fun t ↦ log t • f t) t

Tactic:
rfl

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

Goal state before:
pp: case e'_3
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
⊢ rexp (-x) * x ^ (a * s + b * t - 1) = f a s x * f b t x

Tactic:
have B : x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1)) := by
      rw [← rpow_add hx, hab']; congr 1; ring

Goal state after:
case e'_3
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
B : x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1))
⊢ rexp (-x) * x ^ (a * s + b * t - 1) = f a s x * f b t x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
this : ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    ↑π * z * A * ((1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ))

Tactic:
grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
⊢ log (Γ (y + 1)) = (log ∘ Γ) y + log y

Tactic:
Gamma_add_one hy.ne',

Goal state after:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
⊢ log (y * Γ y) = (log ∘ Γ) y + log y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ log (Γ (y + 1)) = (log ∘ Γ) y + log y

Tactic:
Gamma_add_one hy.ne',

Goal state after:
case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ log (y * Γ y) = (log ∘ Γ) y + log y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: ⊢ Icc 1 2 ⊆ Ioi 0

Tactic:
grind

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)
⊢ x ∈ Ioo 1 2

Tactic:
grind

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
⊢ y ∈ Ioc 0 1 ∨ y ∈ Icc 1 2 ∨ y ∈ Ici 2

Tactic:
grind

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
v : V
p : P
⊢ ⨆ i, map ((fun x ↦ x +ᵥ p) ∘ fun x ↦ x +ᵥ i) (atTop • 𝓝 v) = ⨆ p, map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)

Tactic:
Function.comp_def

Goal state after:
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
v : V
p : P
⊢ ⨆ i, map (fun x ↦ (x +ᵥ i) +ᵥ p) (atTop • 𝓝 v) = ⨆ p, map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s : ℝ
hs : s ≠ 0
⊢ (s + 1).doublingGamma = s * s.doublingGamma

Tactic:
rw [doublingGamma, doublingGamma, (by abel : s + 1 - 1 = s - 1 + 1), add_div, add_assoc,
    add_halves (1 : ℝ), Gamma_add_one (div_ne_zero hs two_ne_zero), rpow_add two_pos, rpow_one]

Goal state after:
s : ℝ
hs : s ≠ 0
⊢ Γ (s / 2 + 1 / 2) * (s / 2 * Γ (s / 2)) * (2 ^ (s - 1) * 2) / √π =
    s * (Γ (s / 2) * Γ (s / 2 + 1 / 2) * 2 ^ (s - 1) / √π)
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
v : V
p : P
⊢ asymptoticNhds k P v = atTop • 𝓝 v +ᵥ pure p

Tactic:
rw [← asymptoticNhds_eq_smul, asymptoticNhds_vadd_pure]

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

Goal state before:
pp: case e'_11
⊢ Ioi (-1) = Ioi (-(1 / 2 / (1 / 2)))

Tactic:
div_self (@one_half_pos ℝ _).ne'

Goal state after:
case e'_11
⊢ Ioi (-1) = Ioi (-1)
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
f : α → k
g : α → V
v : V
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 v)
⊢ Tendsto (fun x ↦ f x • g x) l (asymptoticNhds k V v)

Tactic:
rw [asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂]

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
f : α → k
g : α → V
v : V
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 v)
⊢ Tendsto (fun x ↦ f x • g x) l (map (fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v))
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
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
v : V
p : P
⊢ ∀ (x : Set P),
    (∃ s ∈ atTop,
        ∃ t, (∃ t_1 ∈ 𝓝 v, ∀ x ∈ t_1, t ∈ 𝓝 x) ∧ Set.image2 (fun x1 x2 ↦ x1 • x2) s t ⊆ (fun x ↦ x +ᵥ p) ⁻¹' x) →
      ∃ t ∈ 𝓝 v, ∀ x_1 ∈ t, ∃ s ∈ atTop, ∃ t ∈ 𝓝 x_1, Set.image2 (fun x1 x2 ↦ x1 • x2) s t ⊆ (fun x ↦ x +ᵥ p) ⁻¹' x

Tactic:
grind

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)]
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
key : ∏ i, dist (t.points (i + 1)) (p i) = ∏ i, dist (p i) (t.points (i + 2))
⊢ ∏ i, dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2)) = 1

Tactic:
rw [Fin.prod_univ_three] at key ⊢

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)]
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
key :
  dist (t.points (0 + 1)) (p 0) * dist (t.points (1 + 1)) (p 1) * dist (t.points (2 + 1)) (p 2) =
    ∏ i, dist (p i) (t.points (i + 2))
⊢ dist (t.points (0 + 1)) (p 0) / dist (p 0) (t.points (0 + 2)) *
        (dist (t.points (1 + 1)) (p 1) / dist (p 1) (t.points (1 + 2))) *
      (dist (t.points (2 + 1)) (p 2) / dist (p 2) (t.points (2 + 2))) =
    1
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
S : Set (Set P)
hS : S.Finite
⊢ asymptoticCone k (⋃ i ∈ S, i) = ⋃ s ∈ S, asymptoticCone k s

Tactic:
asymptoticCone_biUnion hS

Goal state after:
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
S : Set (Set P)
hS : S.Finite
⊢ ⋃ i ∈ S, asymptoticCone k i = ⋃ s ∈ S, asymptoticCone k s
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
s : Set P
⊢ asymptoticCone k (asymptoticCone k s) = asymptoticCone k s

Tactic:
ext
  simp_rw [mem_asymptoticCone_iff, ← Filter.frequently_bind, asymptoticNhds_bind_asymptoticNhds]

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

Goal state before:
pp: m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ↑(m + 1) ≤ 1 - s.re ∧ 1 - s.re < ↑(m + 1) + 1
hsne : s ≠ 0
⊢ s.re ≤ -↑m

Tactic:
grind

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

Goal state before:
pp: m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ↑(m + 1) ≤ 1 - s.re ∧ 1 - s.re < ↑(m + 1) + 1
hsne : s ≠ 0
this : s.re ≤ -↑m
⊢ s.re ≤ 0

Tactic:
grind

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
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
hp'x : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fsx i) p) (wx i)]
w' : ι → k
fs' : Finset ι
h :
  ∑ j ∈ fs', w' j = 1 ∧
    (Finset.affineCombination k fs' p) w' = p' ∧
      ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fsx i) \ {↑i}).indicator (wx i) j = (↑fs' \ {↑i}).indicator w' j
i : ↑s
r : k
hr : ∀ (j : ι), r * (↑(fsx i) \ {↑i}).indicator (wx i) j = (↑fs' \ {↑i}).indicator w' j
j : ι
⊢ (if j ∈ fs i ∧ ¬j = ↑i then w i j else 0) = if j ∈ fs i ∧ ¬j = ↑i then if j ∈ fs i then w i j else 0 else 0

Tactic:
grind

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
x✝ : PE
⊢ f.toRealAffineIsometryEquiv.toIsometryEquiv x✝ = f x✝

Tactic:
rfl

Goal state after:
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ LeftInverse
    (fun y ↦
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩)
    fun x ↦ if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩

Tactic:
grind

Goal state after:
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ RightInverse
    (fun y ↦
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩)
    fun x ↦ if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩

Tactic:
grind

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

Goal state before:
pp: case zero
z : ℂ
hz : ∀ (k : ℕ), z ≠ -↑k
⊢ ¬Gamma z = 0

Tactic:
grind

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

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (z : ℂ), (∀ (k : ℕ), z ≠ -↑k) → Gamma (z + ↑n) / Gamma z = Polynomial.eval z (ascPochhammer ℂ n)
z : ℂ
hz : ∀ (k : ℕ), z ≠ -↑k
⊢ Gamma (z + ↑n + 1) = Gamma (z + ↑n) * (z + ↑n)

Tactic:
grind

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

Goal state before:
pp: case inr
⊢ 0⁻¹ = 0 * (Gamma 1)⁻¹

Tactic:
inv_zero,

Goal state after:
case inr
⊢ 0 = 0 * (Gamma 1)⁻¹
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:
by
    convert! congr_arg Inv.inv (congr_fun this s) using 1
    · rw [mul_inv, inv_inv, inv_inv]
    · rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ ((expSeries 𝕜 (tsze R M) (n + 1)) fun x_1 ↦ x).snd = ((expSeries 𝕜 R n) fun x_1 ↦ x.fst) • x.snd

Tactic:
expSeries_apply_eq,

Goal state after:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ ((↑(n + 1).factorial)⁻¹ • x ^ (n + 1)).snd = ((↑n.factorial)⁻¹ • x.fst ^ n) • x.snd
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case «0»
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)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
hi : c ((fun i ↦ i) ⟨0, ⋯⟩) = 0
hw'i1 : w' ((fun i ↦ i) ⟨0, ⋯⟩ + 1) = 0
hw'i2 : w' ((fun i ↦ i) ⟨0, ⋯⟩ + 2) = 0
⊢ w' ((fun i ↦ i) ⟨0, ⋯⟩) = w' 0 + w' 1 + w' 2

Tactic:
grind

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

Goal state before:
pp: case «1»
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)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
hi : c ((fun i ↦ i) ⟨1, ⋯⟩) = 0
hw'i1 : w' ((fun i ↦ i) ⟨1, ⋯⟩ + 1) = 0
hw'i2 : w' ((fun i ↦ i) ⟨1, ⋯⟩ + 2) = 0
⊢ w' ((fun i ↦ i) ⟨1, ⋯⟩) = w' 0 + w' 1 + w' 2

Tactic:
grind

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

Goal state before:
pp: case «2»
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)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
hi : c ((fun i ↦ i) ⟨2, ⋯⟩) = 0
hw'i1 : w' ((fun i ↦ i) ⟨2, ⋯⟩ + 1) = 0
hw'i2 : w' ((fun i ↦ i) ⟨2, ⋯⟩ + 2) = 0
⊢ w' ((fun i ↦ i) ⟨2, ⋯⟩) = w' 0 + w' 1 + w' 2

Tactic:
grind

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✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
hr0 : ∀ (i : Fin 3), r i ≠ 0
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ ∏ i, r i / (1 - r i) = 1

Tactic:
Finset.prod_div_distrib,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
hr0 : ∀ (i : Fin 3), r i ≠ 0
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ (∏ x, r x) / ∏ x, (1 - r x) = 1
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ 1 ≤ n

Tactic:
grind

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

Goal state before:
pp: case refine_2.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
t : Triangle R P
i₃ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₃ : i ≠ i₃
h₂₃ : j ≠ i₃
h₁₂ : i ≠ j
h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃)
h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points j)

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: x : ℍ
⊢ √((equivTuple ℝ) x 0 ^ 2 + (equivTuple ℝ) x 1 ^ 2 + (equivTuple ℝ) x 2 ^ 2 + (equivTuple ℝ) x 3 ^ 2) =
    √(x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case calc_1.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : q ^ 2 = -↑(normSq q)
k : ℝ := ↑(2 * n)!
⊢ (-1) ^ n * (↑‖q‖ * ↑‖q‖) ^ n = (-1) ^ n * (↑‖q‖ * ↑‖q‖) ^ n

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case hbc
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ n < 2 * n

Tactic:
grind

Goal state after: