harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_mul {n} (p q : R[X]) :
    derivative^[n] (p * q) =
      ∑ k ∈ range n.succ, (n.choose k • (derivative^[n - k] p * derivative^[k] q))

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)) =
    ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k + 1] p * (⇑derivative)^[k] q) +
      ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
  smul_add, sum_add_distrib]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ (⇑derivative)^[n + 1] (p * q) =
    derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q))

Tactic:
rw [Function.iterate_succ_apply', IH]

Result:
no goals

Proof state:
case succ.e_a.refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ n.choose 0 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
rw [Nat.choose_zero_right, tsub_zero]

Result:
no goals

Proof state:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k ∈ range n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
rw [mem_range] at hk

Result:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)
-- Mathlib/GroupTheory/GroupAction/Basic.lean
lemma Module.stabilizer_units_eq_bot_of_ne_zero {x : M} (hx : x ≠ 0) :
    MulAction.stabilizer Rˣ x = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
g : Rˣ
hg : ↑g • x = x
⊢ g ∈ ⊥

Tactic:
ext

Result:
case a
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
g : Rˣ
hg : ↑g • x = x
⊢ ↑g = ↑1

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
g : Rˣ
hg : ↑g • x = x
⊢ ↑g = ↑1

Tactic:
rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x ≤ ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x ≤ ⊥

Tactic:
intro g (hg : g.val • x = x)

Result:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
g : Rˣ
hg : ↑g • x = x
⊢ g ∈ ⊥
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem neg_pi_lt_toReal (θ : Angle) : -π < θ.toReal

Proof state:
θ : Angle
⊢ -π < θ.toReal

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ -π < (↑x✝).toReal

Proof state:
case h
x✝ : ℝ
⊢ -π < (↑x✝).toReal

Tactic:
exact left_lt_toIocMod _ _ _

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_singleton (a : α) : ({a} : Finset α).erase a = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a}.erase a = ∅

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a x : α
⊢ x ∈ {a}.erase a ↔ x ∈ ∅

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a x : α
⊢ x ∈ {a}.erase a ↔ x ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem UniqueDiffWithinAt.mono_nhds (h : UniqueDiffWithinAt 𝕜 s x) (st : 𝓝[s] x ≤ 𝓝[t] x) :
    UniqueDiffWithinAt 𝕜 t x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s t : Set E
st : 𝓝[s] x ≤ 𝓝[t] x
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ (𝓝[s] x).NeBot
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) ∧ (𝓝[t] x).NeBot

Tactic:
exact ⟨h.1.mono <| Submodule.span_mono <| tangentCone_mono_nhds st, h.2.mono st⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s t : Set E
h : UniqueDiffWithinAt 𝕜 s x
st : 𝓝[s] x ≤ 𝓝[t] x
⊢ UniqueDiffWithinAt 𝕜 t x

Tactic:
simp only [uniqueDiffWithinAt_iff] at *

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s t : Set E
st : 𝓝[s] x ≤ 𝓝[t] x
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) ∧ x ∈ closure t

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s t : Set E
st : 𝓝[s] x ≤ 𝓝[t] x
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) ∧ x ∈ closure t

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot] at h ⊢

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s t : Set E
st : 𝓝[s] x ≤ 𝓝[t] x
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ (𝓝[s] x).NeBot
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) ∧ (𝓝[t] x).NeBot
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_pairSep {p} {x y z : ZFSet.{u}} :
    z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = pair a b ∧ p a b

Proof state:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
⊢ z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

Tactic:
refine mem_sep.trans ⟨And.right, fun e => ⟨?_, e⟩⟩

Result:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
e : ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
⊢ z ∈ (x ∪ y).powerset.powerset

Proof state:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
e : ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
⊢ z ∈ (x ∪ y).powerset.powerset

Tactic:
rcases e with ⟨a, ax, b, bY, rfl, pab⟩

Result:
case intro.intro.intro.intro.intro
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
⊢ a.pair b ∈ (x ∪ y).powerset.powerset

Proof state:
case intro.intro.intro.intro.intro
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
⊢ ∀ ⦃z : ZFSet.{u}⦄, z = {a} ∨ z = {a, b} → ∀ ⦃z_1 : ZFSet.{u}⦄, z_1 ∈ z → z_1 ∈ x ∨ z_1 ∈ y

Tactic:
rintro u (rfl | rfl) v <;> simp only [mem_singleton, mem_pair]

Result:
case intro.intro.intro.intro.intro.inl
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
v : ZFSet.{u}
⊢ v = a → v ∈ x ∨ v ∈ y

case intro.intro.intro.intro.intro.inr
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
v : ZFSet.{u}
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y

Proof state:
case intro.intro.intro.intro.intro.inr
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
v : ZFSet.{u}
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y

Tactic:
rintro (rfl | rfl) <;> [left; right] <;> assumption

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.inl
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
v : ZFSet.{u}
⊢ v = a → v ∈ x ∨ v ∈ y

Tactic:
rintro rfl

Result:
case intro.intro.intro.intro.intro.inl
p : ZFSet.{u} → ZFSet.{u} → Prop
x y b : ZFSet.{u}
bY : b ∈ y
v : ZFSet.{u}
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y

Proof state:
case intro.intro.intro.intro.intro.inl
p : ZFSet.{u} → ZFSet.{u} → Prop
x y b : ZFSet.{u}
bY : b ∈ y
v : ZFSet.{u}
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y

Tactic:
exact Or.inl ax

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
⊢ a.pair b ∈ (x ∪ y).powerset.powerset

Tactic:
simp only [mem_powerset, subset_def, mem_union, pair, mem_pair]

Result:
case intro.intro.intro.intro.intro
p : ZFSet.{u} → ZFSet.{u} → Prop
x y a : ZFSet.{u}
ax : a ∈ x
b : ZFSet.{u}
bY : b ∈ y
pab : p a b
⊢ ∀ ⦃z : ZFSet.{u}⦄, z = {a} ∨ z = {a, b} → ∀ ⦃z_1 : ZFSet.{u}⦄, z_1 ∈ z → z_1 ∈ x ∨ z_1 ∈ y
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
/-- The `q`-expansion of `f` is an `FPowerSeries` representing `cuspFunction n f`. -/
lemma hasFPowerSeries_cuspFunction [NeZero n] [ModularFormClass F Γ(n) k] :
    HasFPowerSeriesOnBall (cuspFunction n f) (qExpansionFormalMultilinearSeries n f) 0 1

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
⊢ HasFPowerSeriesOnBall (cuspFunction n f) (qExpansionFormalMultilinearSeries n f) 0 1

Tactic:
refine ⟨qExpansionFormalMultilinearSeries_radius n f, zero_lt_one, fun hy ↦ ?_⟩

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
y✝ : ℂ
hy : y✝ ∈ EMetric.ball 0 1
⊢ HasSum (fun n_1 => (qExpansionFormalMultilinearSeries n f n_1) fun x => y✝) (cuspFunction n f (0 + y✝))

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
y✝ : ℂ
hy : y✝ ∈ EMetric.ball 0 1
⊢ HasSum (fun n_1 => (qExpansionFormalMultilinearSeries n f n_1) fun x => y✝) (cuspFunction n f (0 + y✝))

Tactic:
rw [EMetric.mem_ball, edist_zero_right, enorm_eq_nnnorm, ENNReal.coe_lt_one_iff,
  ← NNReal.coe_lt_one, coe_nnnorm] at hy

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
y✝ : ℂ
hy : ‖y✝‖ < 1
⊢ HasSum (fun n_1 => (qExpansionFormalMultilinearSeries n f n_1) fun x => y✝) (cuspFunction n f (0 + y✝))

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
y✝ : ℂ
hy : ‖y✝‖ < 1
⊢ HasSum (fun n_1 => (qExpansionFormalMultilinearSeries n f n_1) fun x => y✝) (cuspFunction n f (0 + y✝))

Tactic:
simpa [qExpansionFormalMultilinearSeries] using hasSum_qExpansion_of_abs_lt n f hy

Result:
no goals
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
/-- As `x → 0`, `f x` decays faster than any power of `x`. -/
lemma hf_zero' (r : ℝ) : P.f =O[𝓝[>] 0] (· ^ r)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
r : ℝ
⊢ P.f =O[𝓝[>] 0] fun x => x ^ r

Tactic:
simpa using (P.hg₀ ▸ P.hf_zero r :)

Result:
no goals
-- Mathlib/CategoryTheory/GlueData.lean
theorem t'_comp_eq_pullbackSymmetry (i j k : D.J) :
    D.t' j k i ≫ D.t' k i j =
      (pullbackSymmetry _ _).hom ≫ D.t' j i k ≫ (pullbackSymmetry _ _).hom

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ D.t' j k i ≫ D.t' k i j =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom

Tactic:
trans inv (D.t' i j k)

Result:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)

C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ inv (D.t' i j k) =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ inv (D.t' i j k) ≫ pullback.fst (D.f i j) (D.f i k) =
    ((pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom) ≫
      pullback.fst (D.f i j) (D.f i k)

Tactic:
simp [t_fac, t_fac_assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)

Tactic:
exact IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ inv (D.t' i j k) =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom

Tactic:
rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]

Result:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ inv (D.t' i j k) ≫ pullback.fst (D.f i j) (D.f i k) =
    ((pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom) ≫
      pullback.fst (D.f i j) (D.f i k)
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem iterate_derivative_at_0 (n ν : ℕ) :
    (Polynomial.derivative^[ν] (bernsteinPolynomial R n ν)).eval 0 =
      (ascPochhammer R ν).eval ((n - (ν - 1) : ℕ) : R)

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)

Tactic:
induction' ν with ν ih generalizing n

Result:
case pos.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
h : 0 ≤ n
⊢ eval 0 ((⇑derivative)^[0] (bernsteinPolynomial R n 0)) = eval (↑(n - (0 - 1))) (ascPochhammer R 0)

case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
⊢ eval 0 ((⇑derivative)^[ν + 1] (bernsteinPolynomial R n (ν + 1))) = eval (↑(n - (ν + 1 - 1))) (ascPochhammer R (ν + 1))
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_caratheodory :
    MeasurableSpace.pi ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory

Proof state:
case intro.intro.hs
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    piPremeasure (fun i => (μ i).toOuterMeasure) (t ∩ (fun b => b i) ⁻¹' s) +
        piPremeasure (fun i => (μ i).toOuterMeasure) (t \ (fun b => b i) ⁻¹' s) ≤
      piPremeasure (fun i => (μ i).toOuterMeasure) t

Tactic:
intro t

Result:
case intro.intro.hs
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (fun i => (μ i).toOuterMeasure) (t ∩ (fun b => b i) ⁻¹' s) +
      piPremeasure (fun i => (μ i).toOuterMeasure) (t \ (fun b => b i) ⁻¹' s) ≤
    piPremeasure (fun i => (μ i).toOuterMeasure) t

Proof state:
case intro.intro.hs.refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
rintro j - _

Result:
case intro.intro.hs.refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ (μ j).toOuterMeasure (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Proof state:
case intro.intro.hs.refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ (μ j).toOuterMeasure (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
gcongr

Result:
case intro.intro.hs.refine_3.h.h
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t \ (fun b => b i) ⁻¹' s ⊆ t
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem toLp_coeFn (f : Lp E p μ) (hf : MemLp f p μ) : hf.toLp f = f

Proof state:
case mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
hf : MemLp (↑↑⟨val✝, property✝⟩) p μ
⊢ MemLp.toLp (↑↑⟨val✝, property✝⟩) hf = ⟨val✝, property✝⟩

Tactic:
simp [MemLp.toLp]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hf : MemLp (↑↑f) p μ
⊢ MemLp.toLp (↑↑f) hf = f

Tactic:
cases f

Result:
case mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
hf : MemLp (↑↑⟨val✝, property✝⟩) p μ
⊢ MemLp.toLp (↑↑⟨val✝, property✝⟩) hf = ⟨val✝, property✝⟩
-- Mathlib/LinearAlgebra/Semisimple.lean
@[simp]
lemma isSemisimple_sub_algebraMap_iff {μ : R} :
    (f - algebraMap R (End R M) μ).IsSemisimple ↔ f.IsSemisimple

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
p : Submodule R M
h : p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p
x : M
hx : x ∈ p
⊢ x ∈ Submodule.comap f p

Tactic:
simpa using p.add_mem (h hx) (p.smul_mem μ hx)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p

Tactic:
refine fun p ↦ ⟨fun h x hx ↦ ?_, fun h x hx ↦ p.sub_mem (h hx) (p.smul_mem μ hx)⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
p : Submodule R M
h : p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p
x : M
hx : x ∈ p
⊢ x ∈ Submodule.comap f p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f - (algebraMap R (End R M)) μ).IsSemisimple ↔ f.IsSemisimple

Tactic:
suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
  simp [mem_invtSubmodule, isSemisimple_iff, this]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
this : ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
⊢ (f - (algebraMap R (End R M)) μ).IsSemisimple ↔ f.IsSemisimple

Tactic:
simp [mem_invtSubmodule, isSemisimple_iff, this]

Result:
no goals
-- Mathlib/NumberTheory/FermatPsp.lean
theorem probablePrime_iff_modEq (n : ℕ) {b : ℕ} (h : 1 ≤ b) :
    ProbablePrime n b ↔ b ^ (n - 1) ≡ 1 [MOD n]

Proof state:
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
⊢ 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
apply Nat.modEq_of_dvd

Result:
case mp.a
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
⊢ ↑n ∣ ↑(b ^ (n - 1)) - ↑1

Proof state:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]

Tactic:
rw [Nat.ModEq.comm]

Result:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]

Proof state:
n b : ℕ
h : 1 ≤ b
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]

Tactic:
have : 1 ≤ b ^ (n - 1) := one_le_pow₀ h

Result:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]

Proof state:
case mp.a
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
⊢ ↑n ∣ ↑(b ^ (n - 1)) - ↑1

Tactic:
exact mod_cast h₁

Result:
no goals

Proof state:
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ n.ProbablePrime b

Tactic:
exact mod_cast Nat.ModEq.dvd h₁

Result:
no goals

Proof state:
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ 1 ≡ b ^ (n - 1) [MOD n] → n.ProbablePrime b

Tactic:
intro h₁

Result:
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ n.ProbablePrime b

Proof state:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
constructor

Result:
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b → 1 ≡ b ^ (n - 1) [MOD n]

case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ 1 ≡ b ^ (n - 1) [MOD n] → n.ProbablePrime b

Proof state:
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b → 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
intro h₁

Result:
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
⊢ 1 ≡ b ^ (n - 1) [MOD n]
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem ofReal_average {f : α → ℝ} (hf : Integrable f μ) (hf₀ : 0 ≤ᵐ[μ] f) :
    ENNReal.ofReal (⨍ x, f x ∂μ) = (∫⁻ x, ENNReal.ofReal (f x) ∂μ) / μ univ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ

Tactic:
obtain rfl | hμ := eq_or_ne μ 0

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ
hf : Integrable f 0
hf₀ : 0 ≤ᶠ[ae 0] f
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂0) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) / 0 univ

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ

Tactic:
rw [average_eq, smul_eq_mul, ← toReal_inv, ofReal_mul toReal_nonneg,
  ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
  ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]

Result:
no goals

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ
hf : Integrable f 0
hf₀ : 0 ≤ᶠ[ae 0] f
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂0) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) / 0 univ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma mkPrecomp_id (f : S.obj Y ⟶ T) : mkPrecomp f (𝟙 Y) = eqToHom (by simp)

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals