harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem GammaSeq_add_one_left (s : ℂ) {n : ℕ} (hn : n ≠ 0) :
    GammaSeq (s + 1) n / s = n / (n + 1 + s) * GammaSeq s n

Proof state:
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
x✝ : x ∈ Finset.range n
⊢ s + 1 + ↑x = s + ↑(x + 1)

Tactic:
push_cast

Result:
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
x✝ : x ∈ Finset.range n
⊢ s + 1 + ↑x = s + (↑x + 1)

Proof state:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) * ↑n ! / ((∏ x ∈ Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) =
    ↑n * ↑n ^ s * ↑n ! / ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * (↑n + 1 + s) * s)

Tactic:
congr 3

Result:
case e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) = ↑n * ↑n ^ s

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))

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

Proof state:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ Finset.range n = Finset.range n

Tactic:
rfl

Result:
no goals

Proof state:
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
x✝ : x ∈ Finset.range n
⊢ s + 1 + ↑x = s + (↑x + 1)

Tactic:
ring

Result:
no goals

Proof state:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) * ↑n ! / ((∏ x ∈ Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) = ↑n / (↑n + 1 + s) * s.GammaSeq n

Tactic:
conv_rhs =>
  rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc,
    ← mul_assoc, mul_comm _ (Finset.prod _ _)]

Result:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) * ↑n ! / ((∏ x ∈ Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) =
    ↑n * ↑n ^ s * ↑n ! / ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * (↑n + 1 + s) * s)

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

Tactic:
abel

Result:
no goals

Proof state:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ (s + 1).GammaSeq n / s = ↑n / (↑n + 1 + s) * s.GammaSeq n

Tactic:
conv_lhs => rw [GammaSeq, Finset.prod_range_succ, div_div]

Result:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) * ↑n ! / ((∏ x ∈ Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) = ↑n / (↑n + 1 + s) * s.GammaSeq n

Proof state:
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))

Tactic:
refine Finset.prod_congr (by rfl) fun x _ => ?_

Result:
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
x✝ : x ∈ Finset.range n
⊢ s + 1 + ↑x = s + ↑(x + 1)

Proof state:
case e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) = ↑n * ↑n ^ s

Tactic:
rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma nhdsWithin_top : 𝓝[≠] (⊤ : EReal) = (atTop).map Real.toEReal

Proof state:
case pos
x : EReal
hx : x < ⊤
hx_bot : x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
simp [hx_bot]

Result:
no goals

Proof state:
case h

⊢ ∀ i < ⊤, ∃ i', True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ

Tactic:
simp only [EReal.image_coe_Ici, true_and]

Result:
case h

⊢ ∀ i < ⊤, ∃ i', Ico ↑i' ⊤ ⊆ Ici i ∩ {⊤}ᶜ

Proof state:
case neg
x : EReal
hx : x < ⊤
hx_bot : ¬x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
lift x to ℝ using ⟨hx.ne_top, hx_bot⟩

Result:
case neg.intro
x : ℝ
hx : ↑x < ⊤
hx_bot : ¬↑x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici ↑x ∩ {⊤}ᶜ

Proof state:
case h'
x✝¹ : ℝ
x : EReal
x✝ : x ∈ Ici ↑x✝¹ ∩ {⊤}ᶜ
h1 : ↑x✝¹ ≤ x
h2 : x ∈ {⊤}ᶜ
⊢ x ∈ Ico ↑x✝¹ ⊤

Tactic:
simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]

Result:
no goals

Proof state:
case neg.intro
x : ℝ
hx : ↑x < ⊤
hx_bot : ¬↑x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici ↑x ∩ {⊤}ᶜ

Tactic:
refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩

Result:
case neg.intro
x✝¹ : ℝ
hx : ↑x✝¹ < ⊤
hx_bot : ¬↑x✝¹ = ⊥
x : EReal
x✝ : x ∈ Ico ↑x✝¹ ⊤
h1 : ↑x✝¹ ≤ x
h2 : x < ⊤
⊢ x ∈ Ici ↑x✝¹ ∩ {⊤}ᶜ

Proof state:
⊢ 𝓝[≠] ⊤ = map Real.toEReal atTop

Tactic:
apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)

Result:
case h

⊢ ∀ i < ⊤, ∃ i', True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ

case h'

⊢ ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'

Proof state:
case h

⊢ ∀ i < ⊤, ∃ i', Ico ↑i' ⊤ ⊆ Ici i ∩ {⊤}ᶜ

Tactic:
intro x hx

Result:
case h
x : EReal
hx : x < ⊤
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Proof state:
case h
x : EReal
hx : x < ⊤
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
by_cases hx_bot : x = ⊥

Result:
case pos
x : EReal
hx : x < ⊤
hx_bot : x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

case neg
x : EReal
hx : x < ⊤
hx_bot : ¬x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Proof state:
case neg.intro
x✝¹ : ℝ
hx : ↑x✝¹ < ⊤
hx_bot : ¬↑x✝¹ = ⊥
x : EReal
x✝ : x ∈ Ico ↑x✝¹ ⊤
h1 : ↑x✝¹ ≤ x
h2 : x < ⊤
⊢ x ∈ Ici ↑x✝¹ ∩ {⊤}ᶜ

Tactic:
simp [h1, h2.ne_top]

Result:
no goals

Proof state:
case h'

⊢ ∀ (i' : ℝ), ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Ico ↑i' ⊤

Tactic:
refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩

Result:
case h'
x✝¹ : ℝ
x : EReal
x✝ : x ∈ Ici ↑x✝¹ ∩ {⊤}ᶜ
h1 : ↑x✝¹ ≤ x
h2 : x ∈ {⊤}ᶜ
⊢ x ∈ Ico ↑x✝¹ ⊤

Proof state:
case h'

⊢ ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'

Tactic:
simp only [EReal.image_coe_Ici, true_implies]

Result:
case h'

⊢ ∀ (i' : ℝ), ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Ico ↑i' ⊤
-- Mathlib/Data/List/Permutation.lean
theorem length_permutations'Aux (s : List α) (x : α) :
    length (permutations'Aux x s) = length s + 1

Proof state:
α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).length = s.length + 1

Tactic:
induction' s with y s IH

Result:
case nil
α : Type u_1
x : α
⊢ (permutations'Aux x []).length = [].length + 1

case cons
α : Type u_1
x y : α
s : List α
IH : (permutations'Aux x s).length = s.length + 1
⊢ (permutations'Aux x (y :: s)).length = (y :: s).length + 1

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : (permutations'Aux x s).length = s.length + 1
⊢ (permutations'Aux x (y :: s)).length = (y :: s).length + 1

Tactic:
simpa using IH

Result:
no goals

Proof state:
case nil
α : Type u_1
x : α
⊢ (permutations'Aux x []).length = [].length + 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_xor {x y : BitVec w} :
    (x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k

Proof state:
case pred
w k : Nat
x y : BitVec w
i : Nat
h : i < k
⊢ (setWidth k (x ^^^ y)).getLsbD i = (setWidth k x ^^^ setWidth k y).getLsbD i

Tactic:
simp [h]

Result:
no goals

Proof state:
w k : Nat
x y : BitVec w
⊢ setWidth k (x ^^^ y) = setWidth k x ^^^ setWidth k y

Tactic:
ext i h

Result:
case pred
w k : Nat
x y : BitVec w
i : Nat
h : i < k
⊢ (setWidth k (x ^^^ y)).getLsbD i = (setWidth k x ^^^ setWidth k y).getLsbD i
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma mkPostcomp_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
    mkPostcomp f (g ≫ g') = mkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom (by simp)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((f ≫ T.map g) ≫ T.map g') = mk (f ≫ T.map (g ≫ g'))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y Y' Y'' : C
T : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mkPostcomp f (g ≫ g') = mkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
lemma stdAddChar_coe (j : ℤ) :
    stdAddChar (j : ZMod N) = exp (2 * π * I * j / N)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ stdAddChar ↑j = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
simp [stdAddChar, toCircle_intCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Asymm (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)]
    {l₁ l₂ l₃ : List α} (h : l₂ ≤ l₃) :
    l₁ ++ l₂ ≤ l₁ ++ l₃

Proof state:
case cons
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
h : l₂ ≤ l₃
a : α
l₁ : List α
ih : l₁ ++ l₂ ≤ l₁ ++ l₃
⊢ a :: l₁ ++ l₂ ≤ a :: l₁ ++ l₃

Tactic:
simp [cons_le_cons_iff, ih]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ l₃ : List α
h : l₂ ≤ l₃
⊢ l₁ ++ l₂ ≤ l₁ ++ l₃

Tactic:
induction l₁ with
| nil => simp [h]
| cons a l₁ ih => simp [cons_le_cons_iff, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
h : l₂ ≤ l₃
⊢ [] ++ l₂ ≤ [] ++ l₃

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem norm_sub_eq_lintegral (f g : α →₁[μ] β) : ‖f - g‖ = (∫⁻ x, ‖f x - g x‖ₑ ∂μ).toReal

Proof state:
case e_a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (fun a => ‖↑↑(f - g) a‖ₑ) =ᶠ[ae μ] fun a => ‖↑↑f a - ↑↑g a‖ₑ

Tactic:
filter_upwards [Lp.coeFn_sub f g] with _ ha

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ ‖↑↑(f - g) a✝‖ₑ = ‖↑↑f a✝ - ↑↑g a✝‖ₑ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ‖f - g‖ = (∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ).toReal

Tactic:
rw [norm_def]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (∫⁻ (a : α), ‖↑↑(f - g) a‖ₑ ∂μ).toReal = (∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ).toReal

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ ‖↑↑(f - g) a✝‖ₑ = ‖↑↑f a✝ - ↑↑g a✝‖ₑ

Tactic:
simp only [ha, Pi.sub_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (∫⁻ (a : α), ‖↑↑(f - g) a‖ₑ ∂μ).toReal = (∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ).toReal

Tactic:
congr 1

Result:
case e_a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ∫⁻ (a : α), ‖↑↑(f - g) a‖ₑ ∂μ = ∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ

Proof state:
case e_a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ∫⁻ (a : α), ‖↑↑(f - g) a‖ₑ ∂μ = ∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ

Tactic:
rw [lintegral_congr_ae]

Result:
case e_a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (fun a => ‖↑↑(f - g) a‖ₑ) =ᶠ[ae μ] fun a => ‖↑↑f a - ↑↑g a‖ₑ
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma norm_le_iff_le_algebraMap (a : A) {r : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖ ≤ r ↔ a ≤ (algebraMap ℝ A) r

Tactic:
rw [le_algebraMap_iff_spectrum_le]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Proof state:
case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : autoParam (0 ≤ a) _auto✝
h✝ : Nontrivial A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
exact ⟨fun h x hx ↦ Real.le_norm_self x |>.trans (spectrum.norm_le_norm_of_mem hx) |>.trans h,
  fun h ↦ h ‖a‖ <| norm_mem_spectrum_of_nonneg⟩

Result:
no goals

Proof state:
case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : autoParam (0 ≤ a) _auto✝
h : Subsingleton A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
simp [Subsingleton.elim a 0, hr]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
obtain (h | _) := subsingleton_or_nontrivial A

Result:
case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : autoParam (0 ≤ a) _auto✝
h : Subsingleton A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : autoParam (0 ≤ a) _auto✝
h✝ : Nontrivial A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- With Mathlib's particular conventions, we have `ζ 1 ≠ 0`. -/
lemma _root_.riemannZeta_one_ne_zero : riemannZeta 1 ≠ 0

Proof state:
this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ 0 ≤ 4 * π

Tactic:
positivity

Result:
no goals

Proof state:
case refine_1

⊢ γ < 1

Tactic:
exact Real.eulerMascheroniConstant_lt_two_thirds.trans (by norm_num)

Result:
no goals

Proof state:
case refine_2

⊢ 1 < Real.log (4 * π)

Tactic:
rw [lt_log_iff_exp_lt (by positivity)]

Result:
case refine_2

⊢ rexp 1 < 4 * π

Proof state:
this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ riemannZeta 1 ≠ 0

Tactic:
simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π),
  push_cast]

Result:
no goals

Proof state:
⊢ 0 ≤ 4

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ (γ - Real.log (4 * π)) / 2 ≠ 0

Tactic:
refine div_ne_zero (sub_lt_zero.mpr (lt_trans ?_ ?_ (b := 1))).ne two_ne_zero

Result:
case refine_1

⊢ γ < 1

case refine_2

⊢ 1 < Real.log (4 * π)

Proof state:
⊢ riemannZeta 1 ≠ 0

Tactic:
suffices (γ - (4 * π).log) / 2 ≠ 0 by
  simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π),
    push_cast]

Result:
⊢ (γ - Real.log (4 * π)) / 2 ≠ 0

Proof state:
⊢ 0 < 4 * π

Tactic:
positivity

Result:
no goals

Proof state:
case refine_2

⊢ rexp 1 < 4 * π

Tactic:
exact (lt_trans Real.exp_one_lt_d9 (by norm_num)).trans_le
  <| mul_le_mul_of_nonneg_left two_le_pi (by norm_num)

Result:
no goals

Proof state:
⊢ 2 / 3 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 2.7182818286 < 4 * 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_sub_C (hp : 0 < degree p) : degree (p - C a) = degree p

Proof state:
R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p - C a).degree = p.degree

Tactic:
rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]

Result:
no goals
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_X_pow_isSolvable (n : ℕ) : IsSolvable (X ^ n : F[X]).Gal

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
⊢ IsSolvable (X ^ n).Gal

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_lt_neg {a b : Int} (h : a < b) : -b < -a

Proof state:
a b : Int
h : a < b
this : 0 < -a + b
⊢ -b < -a

Tactic:
have : 0 + -b < -a + b + -b := Int.add_lt_add_right this (-b)

Result:
a b : Int
h : a < b
this✝ : 0 < -a + b
this : 0 + -b < -a + b + -b
⊢ -b < -a

Proof state:
a b : Int
h : a < b
this✝ : 0 < -a + b
this : 0 + -b < -a + b + -b
⊢ -b < -a

Tactic:
rwa [Int.add_neg_cancel_right, Int.zero_add] at this

Result:
no goals

Proof state:
a b : Int
h : a < b
⊢ -b < -a

Tactic:
have : 0 < -a + b := Int.add_left_neg a ▸ Int.add_lt_add_left h (-a)

Result:
a b : Int
h : a < b
this : 0 < -a + b
⊢ -b < -a
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem circleIntegral_eq_zero_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 ≤ R) {f : ℂ → E}
    {c : ℂ} {s : Set ℂ} (hs : s.Countable) (hc : ContinuousOn f (closedBall c R))
    (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) : (∮ z in C(c, R), f z) = 0

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, R), f z) = 0

Tactic:
rcases h0.eq_or_lt with (rfl | h0)

Result:
case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
h0 : 0 ≤ 0
hc : ContinuousOn f (closedBall c 0)
hd : ∀ z ∈ ball c 0 \ s, DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, 0), f z) = 0

case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
h0 : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), f z) = 0

Proof state:
case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
h0 : 0 ≤ 0
hc : ContinuousOn f (closedBall c 0)
hd : ∀ z ∈ ball c 0 \ s, DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, 0), f z) = 0

Tactic:
apply circleIntegral.integral_radius_zero

Result:
no goals

Proof state:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
h0 : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), f z) = 0

Tactic:
calc
  (∮ z in C(c, R), f z) = ∮ z in C(c, R), (z - c)⁻¹ • (z - c) • f z :=
    (circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _).symm
  _ = (2 * ↑π * I : ℂ) • (c - c) • f c :=
    (circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable h0 hs
      ((continuousOn_id.sub continuousOn_const).smul hc) fun z hz =>
      (differentiableAt_id.sub_const _).smul (hd z hz))
  _ = 0 := by rw [sub_self, zero_smul, smul_zero]

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
h0 : 0 < R
⊢ (2 * ↑π * I) • (c - c) • f c = 0

Tactic:
rw [sub_self, zero_smul, smul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldrM_toList [Monad m]
    (f : α → β → m β) (init : β) (arr : Array α) :
    arr.toList.foldrM f init = arr.foldrM f init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
⊢ List.foldrM f init arr.toList = foldrM f init arr

Tactic:
rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem isUniformInducing_equivBoundedOfCompact : IsUniformInducing (equivBoundedOfCompact α β) :=
  IsUniformInducing.mk'
    (by
      simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]
      exact fun s =>
        ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
          ⟨{ p | ∀ x, (p.1 x, p.2 x) ∈ b }, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩,
            fun f g h => hs fun x _ => h x⟩,
          fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
          ⟨⟨Set.univ, { p | dist p.1 p.2 ≤ ε }⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩,
            fun ⟨f, g⟩ h => hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ i,
        (IsCompact i.1 ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
          {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ i.2} ⊆ s) ↔
      ∃ t,
        (∃ i, 0 < i ∧ {p | dist p.1 p.2 ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s

Tactic:
exact fun s =>
  ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
    ⟨{ p | ∀ x, (p.1 x, p.2 x) ∈ b }, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩,
      fun f g h => hs fun x _ => h x⟩,
    fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
    ⟨⟨Set.univ, { p | dist p.1 p.2 ≤ ε }⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩,
      fun ⟨f, g⟩ h => hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    s ∈ uniformity C(α, β) ↔
      ∃ t ∈ uniformity (α →ᵇ β),
        ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s

Tactic:
simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ i,
        (IsCompact i.1 ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
          {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ i.2} ⊆ s) ↔
      ∃ t,
        (∃ i, 0 < i ∧ {p | dist p.1 p.2 ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getLast_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs → P a) (h : xs.pmap f H ≠ []) :
    (xs.pmap f H).getLast h = f (xs.getLast (by simpa using h)) (H _ (getLast_mem _))

Proof state:
α : Type ?u.80902
β : Type ?u.80938
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : pmap f xs H ≠ []
⊢ xs ≠ []

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : pmap f xs H ≠ []
⊢ (pmap f xs H).reverse.head ⋯ = f (xs.reverse.head ⋯) ⋯

Tactic:
simp only [reverse_pmap, head_pmap, head_reverse]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : pmap f xs H ≠ []
⊢ (pmap f xs H).getLast h = f (xs.getLast ⋯) ⋯

Tactic:
simp only [getLast_eq_head_reverse]

Result:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : pmap f xs H ≠ []
⊢ (pmap f xs H).reverse.head ⋯ = f (xs.reverse.head ⋯) ⋯