harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) :
    (n - 1) ! * n.ascFactorial k = (n + k - 1)!

Proof state:
n k : ℕ
h : 0 < n
⊢ (n - 1)! * n.ascFactorial k = (n + k - 1)!

Tactic:
rw [Nat.sub_add_comm h, Nat.sub_one]

Result:
n k : ℕ
h : 0 < n
⊢ n.pred ! * n.ascFactorial k = (n.pred + k)!

Proof state:
n k : ℕ
h : 0 < n
⊢ n.pred ! * n.ascFactorial k = (n.pred + k)!

Tactic:
nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]

Result:
n k : ℕ
h : 0 < n
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!

Proof state:
n k : ℕ
h : 0 < n
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!

Tactic:
rw [Nat.sub_one, factorial_mul_ascFactorial]

Result:
no goals
-- Mathlib/Order/Height.lean
theorem chainHeight_insert_of_forall_lt (a : α) (ha : ∀ b ∈ s, b < a) :
    (insert a s).chainHeight = s.chainHeight + 1

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
ha : ∀ b ∈ s, b < a
⊢ (⇑ofDual ⁻¹' insert a s).chainHeight = (⇑ofDual ⁻¹' s).chainHeight + 1

Tactic:
exact chainHeight_insert_of_forall_gt _ ha

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
ha : ∀ b ∈ s, b < a
⊢ (insert a s).chainHeight = s.chainHeight + 1

Tactic:
rw [← chainHeight_dual, ← chainHeight_dual s]

Result:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
ha : ∀ b ∈ s, b < a
⊢ (⇑ofDual ⁻¹' insert a s).chainHeight = (⇑ofDual ⁻¹' s).chainHeight + 1
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_one [Fintype n] [DecidableEq n] (M : Matrix m n α) :
    M * (1 : Matrix n n α) = M

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (M * 1) i✝ j✝ = M i✝ j✝

Tactic:
rw [← diagonal_one, mul_diagonal, mul_one]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
⊢ M * 1 = M

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (M * 1) i✝ j✝ = M i✝ j✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem update_update (self : Buckets α β) (i d d' h h') :
    (self.update i d h).update i d' h' = self.update i d' h

Proof state:
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d d' : AssocList α β
h : i.toNat < self.val.size
h' : i.toNat < (self.update i d h).val.size
⊢ (self.update i d h).update i d' h' = self.update i d' h

Tactic:
simp only [update, Array.uset, Array.length_toList]

Result:
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d d' : AssocList α β
h : i.toNat < self.val.size
h' : i.toNat < (self.update i d h).val.size
⊢ ⟨(self.val.set i.toNat d h).set i.toNat d' ⋯, ⋯⟩ = ⟨self.val.set i.toNat d' h, ⋯⟩

Proof state:
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d d' : AssocList α β
h : i.toNat < self.val.size
h' : i.toNat < (self.update i d h).val.size
⊢ ⟨(self.val.set i.toNat d h).set i.toNat d' ⋯, ⋯⟩ = ⟨self.val.set i.toNat d' h, ⋯⟩

Tactic:
congr 1

Result:
case e_val
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d d' : AssocList α β
h : i.toNat < self.val.size
h' : i.toNat < (self.update i d h).val.size
⊢ (self.val.set i.toNat d h).set i.toNat d' ⋯ = self.val.set i.toNat d' h

Proof state:
case e_val
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d d' : AssocList α β
h : i.toNat < self.val.size
h' : i.toNat < (self.update i d h).val.size
⊢ (self.val.set i.toNat d h).set i.toNat d' ⋯ = self.val.set i.toNat d' h

Tactic:
rw [Array.set_set]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma supDegree_esymm [Nontrivial R] (him : i < m) :
    ofLex (supDegree toLex <| esymm (Fin m) R (i + 1)) = accumulate n m (Finsupp.single i 1)

Proof state:
case h
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x => 1) j = (accumulate n m) (⇑fun₀ | i => 1) j

Tactic:
simp_rw [Finsupp.indicator_apply, dite_eq_ite, mem_Iic, accumulate_apply, Finsupp.single_apply,
  sum_ite_eq, mem_filter, mem_univ, true_and, Fin.le_def]

Result:
no goals

Proof state:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
⊢ ⇑(ofLex (supDegree (⇑toLex) (esymm (Fin m) R (↑i + 1)))) = (accumulate n m) ⇑fun₀ | i => 1

Tactic:
rw [(supDegree_monic_esymm him).1, ofLex_toLex]

Result:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
⊢ ⇑(Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x => 1) = (accumulate n m) ⇑fun₀ | i => 1

Proof state:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
⊢ ⇑(Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x => 1) = (accumulate n m) ⇑fun₀ | i => 1

Tactic:
ext j

Result:
case h
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x => 1) j = (accumulate n m) (⇑fun₀ | i => 1) j
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : ℝ}
    (hf : ContinuousOn f (Icc a b)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ContinuousOn B (Icc a b))
    (hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x)
    -- `bound` actually says `liminf (f z - f x) / (z - x) ≤ B' x`
    (bound : ∀ x ∈ Ico a b, ∀ r, B' x < r → ∃ᶠ z in 𝓝[>] x, slope f x z < r) :
    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x

Proof state:
case hB'
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ x ∈ Ico a b, HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.17301 x) (Ici x) x

Tactic:
intro x hx

Result:
case hB'
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.17301 x) (Ici x) x

Proof state:
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ B x

Tactic:
have : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0 :=
  continuousWithinAt_const.add (continuousWithinAt_id.mul continuousWithinAt_const)

Result:
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0
⊢ f x ≤ B x

Proof state:
case ha
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ f a ≤ B a + r * (a - a)

Tactic:
rwa [sub_self, mul_zero, add_zero]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_congr {f g : α → β} (h : ∀ x ∈ v.support, f x = g x) :
    v.mapDomain f = v.mapDomain g :=
  Finset.sum_congr rfl fun _ H => by simp only [h _ H]

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f g : α → β
h : ∀ x ∈ v.support, f x = g x
x✝ : α
H : x✝ ∈ v.support
⊢ (fun a => single (f a)) x✝ (v x✝) = (fun a => single (g a)) x✝ (v x✝)

Tactic:
simp only [h _ H]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.Set.exists_isOpen_le_add (A : Set α) (μ : Measure α) [OuterRegular μ] {ε : ℝ≥0∞}
    (hε : ε ≠ 0) : ∃ U, U ⊇ A ∧ IsOpen U ∧ μ U ≤ μ A + ε

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : μ A = ⊤
⊢ μ univ ≤ μ A + ε

Tactic:
simp only [H, _root_.top_add, le_top]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε

Tactic:
rcases eq_or_ne (μ A) ∞ with (H | H)

Result:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : μ A = ⊤
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε

case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : μ A ≠ ⊤
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε

Proof state:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : μ A ≠ ⊤
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε

Tactic:
rcases A.exists_isOpen_lt_add H hε with ⟨U, AU, U_open, hU⟩

Result:
case inr.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : μ A ≠ ⊤
U : Set α
AU : U ⊇ A
U_open : IsOpen U
hU : μ U < μ A + ε
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε

Proof state:
case inr.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : μ A ≠ ⊤
U : Set α
AU : U ⊇ A
U_open : IsOpen U
hU : μ U < μ A + ε
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε

Tactic:
exact ⟨U, AU, U_open, hU.le⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : μ A = ⊤
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε

Tactic:
exact ⟨univ, subset_univ _, isOpen_univ, by simp only [H, _root_.top_add, le_top]⟩

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem exists_pow_nat_eq [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x

Proof state:
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ z ^ n = x

Tactic:
simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz

Result:
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
⊢ ∃ z, z ^ n = x

Tactic:
obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this

Result:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ ∃ z, z ^ n = x

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ (X ^ n - C x).degree ≠ 0

Tactic:
rw [degree_X_pow_sub_C hn x]

Result:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0

Proof state:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ ∃ z, z ^ n = x

Tactic:
use z

Result:
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ z ^ n = x

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ∃ z, z ^ n = x

Tactic:
have : degree (X ^ n - C x) ≠ 0 := by
  rw [degree_X_pow_sub_C hn x]
  exact ne_of_gt (WithBot.coe_lt_coe.2 hn)

Result:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
⊢ ∃ z, z ^ n = x

Proof state:
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x

Tactic:
exact sub_eq_zero.1 hz

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0

Tactic:
exact ne_of_gt (WithBot.coe_lt_coe.2 hn)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_fdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : fdiv (a * b) b = a :=
  if b0 : 0 ≤ b then by
    rw [fdiv_eq_ediv _ b0, mul_ediv_cancel _ H]
  else
    match a, b, Int.not_le.1 b0 with
    | 0, _, _ => by simp [Int.zero_mul]
    | succ a, -[b+1], _ => congrArg ofNat <| Nat.mul_div_cancel (succ a) b.succ_pos
    | -[a+1], -[b+1], _ => congrArg negSucc <| Nat.div_eq_of_lt_le
      (Nat.le_of_lt_succ <| Nat.mul_lt_mul_of_pos_right a.lt_succ_self b.succ_pos)
      (Nat.lt_succ_self _)

Proof state:
a b x✝¹ : Int
x✝ : x✝¹ < 0
H : x✝¹ ≠ 0
b0 : ¬0 ≤ x✝¹
⊢ (0 * x✝¹).fdiv x✝¹ = 0

Tactic:
simp [Int.zero_mul]

Result:
no goals

Proof state:
a b : Int
H : b ≠ 0
b0 : 0 ≤ b
⊢ (a * b).fdiv b = a

Tactic:
rw [fdiv_eq_ediv _ b0, mul_ediv_cancel _ H]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sMod_mod (p i : ℕ) : sMod p i % (2 ^ p - 1) = sMod p i

Proof state:
p i : ℕ
⊢ sMod p i % (2 ^ p - 1) = sMod p i

Tactic:
cases i <;> simp [sMod]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma sqrt_mul_self (x : ℝ≥0) : sqrt (x * x) = x

Proof state:
x : ℝ≥0
⊢ sqrt (x * x) = x

Tactic:
rw [← sq, sqrt_sq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem toGerm_eq (f : α →ₘ[μ] β) : f.toGerm = (f : α → β)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ f.toGerm = ↑↑f

Tactic:
rw [← mk_toGerm, mk_coeFn]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem le_radius_of_summable (h : Summable fun n => ‖p n‖ * (r : ℝ) ^ n) : ↑r ≤ p.radius :=
  p.le_radius_of_summable_nnnorm <| by
    simp only [← coe_nnnorm] at h
    exact mod_cast h

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : Summable fun n => ↑‖p n‖₊ * ↑r ^ n
⊢ Summable fun n => ‖p n‖₊ * r ^ n

Tactic:
exact mod_cast h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : Summable fun n => ‖p n‖ * ↑r ^ n
⊢ Summable fun n => ‖p n‖₊ * r ^ n

Tactic:
simp only [← coe_nnnorm] at h

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : Summable fun n => ↑‖p n‖₊ * ↑r ^ n
⊢ Summable fun n => ‖p n‖₊ * r ^ n
-- Mathlib/Algebra/Order/Nonneg/Basic.lean
theorem pow_nonneg {a : α} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ a ^ n
  | 0 => by
    rw [pow_zero]
    exact zero_le_one
  | n + 1 => by
    rw [pow_succ]
    exact mul_nonneg (pow_nonneg H _) H

Proof state:
α : Type u_1
inst✝³ : MonoidWithZero α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : PosMulMono α
a : α
H : 0 ≤ a
⊢ 0 ≤ a ^ 0

Tactic:
rw [pow_zero]

Result:
α : Type u_1
inst✝³ : MonoidWithZero α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : PosMulMono α
a : α
H : 0 ≤ a
⊢ 0 ≤ 1

Proof state:
α : Type u_1
inst✝³ : MonoidWithZero α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : PosMulMono α
a : α
H : 0 ≤ a
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MonoidWithZero α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : PosMulMono α
a : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)

Tactic:
rw [pow_succ]

Result:
α : Type u_1
inst✝³ : MonoidWithZero α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : PosMulMono α
a : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n * a

Proof state:
α : Type u_1
inst✝³ : MonoidWithZero α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : PosMulMono α
a : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n * a

Tactic:
exact mul_nonneg (pow_nonneg H _) H

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_succ_eval {S : Type*} [Ring S] (n : ℕ) (k : S) :
    (descPochhammer S (n + 1)).eval k = (descPochhammer S n).eval k * (k - n)

Proof state:
S : Type u_1
inst✝ : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - ↑n)

Tactic:
rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
  eval_C_mul, Nat.cast_comm, ← mul_sub]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem coprodᵢ_neBot_iff' :
    NeBot (Filter.coprodᵢ f) ↔ (∀ i, Nonempty (α i)) ∧ ∃ d, NeBot (f d)

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ (Filter.coprodᵢ f).NeBot ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ d, (f d).NeBot

Tactic:
simp only [Filter.coprodᵢ, iSup_neBot, ← exists_and_left, ← comap_eval_neBot_iff']

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sum_eq_iff_sum_smul_moebius_eq [AddCommGroup R] {f g : ℕ → R} :
    (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd = f n

Proof state:
case h.succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ ∑ i ∈ (n + 1).divisors, f' i = g' (n + 1)

Tactic:
simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', if_false, ZeroHom.coe_mk]

Result:
case h.succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ ∑ i ∈ (n + 1).divisors, f' i = g' (n + 1)

Proof state:
case h.zero
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ 0 > 0 → ∑ i ∈ divisors 0, f i = g 0 ↔ (↑ζ • f') 0 = g' 0

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ ∀ (a : ℕ), (μ • g') a = f' a ↔ a > 0 → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a

Tactic:
intro n

Result:
case h
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ (μ • g') n = f' n ↔ n > 0 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Proof state:
case h.succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ (μ • g') (n + 1) = f' (n + 1) ↔ n + 1 > 0 → ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g x.2 = f (n + 1)

Tactic:
simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', smul_apply, if_false,
  ZeroHom.coe_mk]

Result:
case h.succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g' x.2 = f' (n + 1) ↔
    ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g x.2 = f (n + 1)
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem zero_smul' [Zero R] [SMulWithZero R V] {x : HahnModule Γ' R V} :
    (0 : HahnSeries Γ R) • x = 0

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnModule Γ' R V
⊢ 0 • x = 0

Tactic:
ext

Result:
case h.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnModule Γ' R V
x✝ : Γ'
⊢ ((of R).symm (0 • x)).coeff x✝ = ((of R).symm 0).coeff x✝

Proof state:
case h.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnModule Γ' R V
x✝ : Γ'
⊢ ((of R).symm (0 • x)).coeff x✝ = ((of R).symm 0).coeff x✝

Tactic:
simp [coeff_smul]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
theorem hurwitzZeta_neg_nat (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
    hurwitzZeta x (-k) =
    -1 / (k + 1) * ((Polynomial.bernoulli (k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ)

Proof state:
case intro.inr
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n + 1)) =
    -1 / (↑(2 * n + 1) + 1) *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1 + 1)))

Tactic:
exact_mod_cast hurwitzZeta_one_sub_two_mul_nat (by omega : n + 1 ≠ 0) hx

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n ≠ 0
⊢ n ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ n + 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (-↑k) =
    -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))

Tactic:
rcases Nat.even_or_odd' k with ⟨n, (rfl | rfl)⟩

Result:
case intro.inl
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n)) =
    -1 / (↑(2 * n) + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1)))

case intro.inr
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n + 1)) =
    -1 / (↑(2 * n + 1) + 1) *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1 + 1)))

Proof state:
case intro.inl
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n)) =
    -1 / (↑(2 * n) + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1)))

Tactic:
exact_mod_cast hurwitzZeta_neg_two_mul_nat (by omega : n ≠ 0) hx

Result:
no goals