harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
/-- When `s.re > 1`, the map `n ↦ n^(-s)` is norm-summable. -/
lemma summable_riemannZetaSummand (hs : 1 < s.re) :
    Summable (fun n ↦ ‖riemannZetaSummandHom (ne_zero_of_one_lt_re hs) n‖)

Proof state:
s : ℂ
hs : 1 < s.re
⊢ Summable fun n => ‖↑n ^ (-s)‖

Tactic:
convert Real.summable_nat_rpow_inv.mpr hs with n

Result:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ‖↑n ^ (-s)‖ = (↑n ^ s.re)⁻¹

Proof state:
s : ℂ
hs : 1 < s.re
⊢ Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖

Tactic:
simp only [riemannZetaSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
s : ℂ
hs : 1 < s.re
⊢ Summable fun n => ‖↑n ^ (-s)‖

Proof state:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ‖↑n ^ (-s)‖ = (↑n ^ s.re)⁻¹

Tactic:
rw [← ofReal_natCast,
  norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
  neg_re, Real.rpow_neg <| Nat.cast_nonneg n]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
/-- We can combine the logs in `log (1 + z * I) + -log (1 - z * I)` into one.
This is only used in `hasSum_arctan`. -/
lemma hasSum_arctan_aux {z : ℂ} (hz : ‖z‖ < 1) :
    log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))

Proof state:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π

Tactic:
have c₂ := add_lt_add b₁.2 b₂.2

Result:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)
c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg
c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2
⊢ (1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
-- Mathlib/Topology/ContinuousOn.lean
theorem union_mem_nhds_of_mem_nhdsWithin {b : α}
    {I₁ I₂ : Set α} (h : Set.univ = I₁ ∪ I₂)
    {L : Set α} (hL : L ∈ nhdsWithin b I₁)
    {R : Set α} (hR : R ∈ nhdsWithin b I₂) : L ∪ R ∈ nhds b

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ R ⊆ L ∪ R

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ⊆ L ∪ R

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝 b

Tactic:
rw [← nhdsWithin_univ b, h, nhdsWithin_union]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝[I₁] b ⊔ 𝓝[I₂] b

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝[I₁] b ⊔ 𝓝[I₂] b

Tactic:
exact ⟨mem_of_superset hL (by simp), mem_of_superset hR (by simp)⟩

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_mul {p q : ℝ} (hp : 0 ≤ p) :
    ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

Proof state:
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

Tactic:
simp only [ENNReal.ofReal, ← coe_mul, Real.toNNReal_mul hp]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Basic.lean
/-- In characteristic zero if there is no torsion, the correspondence between roots and coroots is
unique.

Formally, the point is that the hypothesis `hc` depends only on the range of the coroot mappings. -/
@[ext]
protected lemma ext [CharZero R] [NoZeroSMulDivisors R M]
    {P₁ P₂ : RootPairing ι R M N}
    (he : P₁.toPerfectPairing = P₂.toPerfectPairing)
    (hr : P₁.root = P₂.root)
    (hc : range P₁.coroot = range P₂.coroot) :
    P₁ = P₂

Proof state:
case h.hx
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ ?m.36057 ∈ span R (range ⇑P₁.root)

Tactic:
exact Submodule.subset_span (mem_range_self i)

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Basic.lean
/-- In characteristic zero if there is no torsion, the correspondence between roots and coroots is
unique.

Formally, the point is that the hypothesis `hc` depends only on the range of the coroot mappings. -/
@[ext]
protected lemma ext [CharZero R] [NoZeroSMulDivisors R M]
    {P₁ P₂ : RootPairing ι R M N}
    (he : P₁.toPerfectPairing = P₂.toPerfectPairing)
    (hr : P₁.root = P₂.root)
    (hc : range P₁.coroot = range P₂.coroot) :
    P₁ = P₂

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ ((span R (range ⇑P₁.root)).subtype.dualMap ∘ₗ P₁.toLin.flip) (P₁.coroot i) =
    ((span R (range ⇑P₁.root)).subtype.dualMap ∘ₗ P₁.toLin.flip) (P₂.coroot i)

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply]

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ (span R (range ⇑P₁.root)).subtype.dualMap (P₁.toLin.flip (P₁.coroot i)) =
    (span R (range ⇑P₁.root)).subtype.dualMap (P₁.toLin.flip (P₂.coroot i))

Proof state:
case h.H
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hc' : P₁.coroot = P₂.coroot
i j : ι
⊢ P₁.root j - (P₁.flip (P₁.coroot i)) (P₁.root j) • P₁.root i =
    P₂.root j - (P₂.flip (P₂.coroot i)) (P₂.root j) • P₂.root i

Tactic:
simp only [hr, he, hc']

Result:
no goals

Proof state:
case h.hg₁
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ (P₁.toLin.flip (P₂.coroot i)) (P₁.root i) = 2

Tactic:
exact hr ▸ he ▸ P₂.coroot_root_two i

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma inv_nonpos_of_nonpos {a : EReal} (h : a ≤ 0) : a⁻¹ ≤ 0

Proof state:
a : EReal
h : a ≤ 0
⊢ a⁻¹ ≤ 0

Tactic:
cases a with
| h_bot | h_top => simp
| h_real a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h

Result:
no goals

Proof state:
case h_top
h : ⊤ ≤ 0
⊢ ⊤⁻¹ ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case h_real
a : ℝ
h : ↑a ≤ 0
⊢ (↑a)⁻¹ ≤ 0

Tactic:
rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]

Result:
case h_real
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0

Proof state:
case h_real
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0

Tactic:
exact EReal.coe_nonpos.1 h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_sUnion_le {α : Type u} (A : Set (Set α)) : #(⋃₀ A) ≤ #A * ⨆ s : A, #s

Proof state:
α : Type u
A : Set (Set α)
⊢ #↑(⋃ i, ↑i) ≤ #↑A * ⨆ s, #↑↑s

Tactic:
apply mk_iUnion_le

Result:
no goals

Proof state:
α : Type u
A : Set (Set α)
⊢ #↑(⋃₀ A) ≤ #↑A * ⨆ s, #↑↑s

Tactic:
rw [sUnion_eq_iUnion]

Result:
α : Type u
A : Set (Set α)
⊢ #↑(⋃ i, ↑i) ≤ #↑A * ⨆ s, #↑↑s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem unattach_flatten {p : α → Prop} {l : List (List { x // p x })} :
    l.flatten.unattach = (l.map unattach).flatten

Proof state:
α : Type u_1
p : α → Prop
l : List (List { x // p x })
⊢ l.flatten.unattach = (map unattach l).flatten

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : List (List { x // p x })
⊢ map (fun x => x.val) l.flatten = (map (fun l => map (fun x => x.val) l) l).flatten

Proof state:
α : Type u_1
p : α → Prop
l : List (List { x // p x })
⊢ map (fun x => x.val) l.flatten = (map (fun l => map (fun x => x.val) l) l).flatten

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
/-- The jacobian of the composition of presentations is the product of the jacobians. -/
@[simp]
lemma comp_jacobian_eq_jacobian_smul_jacobian : (Q.comp P).jacobian = P.jacobian • Q.jacobian

Proof state:
case h.e'_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (aeval (Q.comp P).val)
      (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
          (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    (aeval (Q.comp P).val) ((Q.comp P).jacobiMatrix.toBlocks₁₁.det * (Q.comp P).jacobiMatrix.toBlocks₂₂.det)

Tactic:
congr

Result:
case h.e'_2.h.e_6.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
        (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    (Q.comp P).jacobiMatrix.toBlocks₁₁.det * (Q.comp P).jacobiMatrix.toBlocks₂₂.det

Proof state:
case intro.intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Tactic:
rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
  jacobiMatrix_comp_₁₂]

Result:
case intro.intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (algebraMap (Q.comp P).Ring T)
      (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
          (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    P.jacobian • Q.jacobian
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma comp_add [∀ (a : M), (shiftFunctor C a).Additive]
    {a b c : M} (α : ShiftedHom X Y a) (β₁ β₂ : ShiftedHom Y Z b) (h : b + a = c) :
    α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
X Y Z : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem pullbackZeroZeroIso_inv_snd (X Y : C) [HasBinaryProduct X Y] :
    (pullbackZeroZeroIso X Y).inv ≫ pullback.snd 0 0 = prod.snd

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).inv ≫ pullback.snd 0 0 = prod.snd

Tactic:
dsimp [pullbackZeroZeroIso]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd ⋯,
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.snd 0 0 =
    prod.snd

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd ⋯,
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.snd 0 0 =
    prod.snd

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_zero_sub_comm (a b : α) : toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)

Tactic:
rw [← neg_sub, toIcoMod_neg, neg_zero]

Result:
no goals
-- Mathlib/NumberTheory/AbelSummation.lean
theorem sum_mul_eq_sub_integral_mul {b : ℝ} (hb : 0 ≤ b)
    (hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t)
    (hf_int : IntegrableOn (deriv f) (Set.Icc 0 b)) :
    ∑ k ∈ Icc 0 ⌊b⌋₊, f k * c k =
      f b * (∑ k ∈ Icc 0 ⌊b⌋₊, c k) - ∫ t in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _)]

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ ∑ k ∈ cons 0 (Ioc 0 ⌊b⌋₊) ⋯, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ f 0 * c 0 + (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 0 * c 0 - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ ∑ k ∈ cons 0 (Ioc 0 ⌊b⌋₊) ⋯, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
rw [sum_cons, ← Nat.floor_zero (α := ℝ), sum_mul_eq_sub_sub_integral_mul c le_rfl hb hf_diff
  hf_int, Nat.floor_zero, Nat.cast_zero, Icc_self, sum_singleton]

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ f 0 * c 0 + (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 0 * c 0 - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.and_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a && b) = false

Proof state:
a b : Bool
h : a = false
⊢ (a && b) = false

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
@[simp] lemma mem_sup : a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
induction' s using cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMinOn.fderivWithin_nonneg (h : IsLocalMinOn f s a)
    (hy : y ∈ posTangentConeAt s a) : (0 : ℝ) ≤ (fderivWithin ℝ f s a : E → ℝ) y

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ 0 y

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ (fderivWithin ℝ f s a) y

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ 0 y

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
⊢ 0 ≤ (fderivWithin ℝ f s a) y

Tactic:
exact
  if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonneg hf.hasFDerivWithinAt hy
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
⊢ 0 ≤ (fderivWithin ℝ f s a) y

Tactic:
classical
exact
  if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonneg hf.hasFDerivWithinAt hy
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem mem_localTrivAt_baseSet (b : B) : b ∈ (Z.localTrivAt b).baseSet

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ (Z.localTrivAt b).baseSet

Tactic:
rw [localTrivAt, ← baseSet_at]

Result:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ Z.baseSet (Z.indexAt b)

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ Z.baseSet (Z.indexAt b)

Tactic:
exact Z.mem_baseSet_at b

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
lemma range_eq_Icc_zero_sub_one (n : ℕ) (hn : n ≠ 0) : range n = Icc 0 (n - 1)

Proof state:
case h
n : ℕ
hn : n ≠ 0
b : ℕ
⊢ b ∈ range n ↔ b ∈ Icc 0 (n - 1)

Tactic:
simp_all only [mem_Icc, zero_le, true_and, mem_range]

Result:
case h
n : ℕ
hn : n ≠ 0
b : ℕ
⊢ b < n ↔ b ≤ n - 1

Proof state:
n : ℕ
hn : n ≠ 0
⊢ range n = Icc 0 (n - 1)

Tactic:
ext b

Result:
case h
n : ℕ
hn : n ≠ 0
b : ℕ
⊢ b ∈ range n ↔ b ∈ Icc 0 (n - 1)

Proof state:
case h
n : ℕ
hn : n ≠ 0
b : ℕ
⊢ b < n ↔ b ≤ n - 1

Tactic:
exact lt_iff_le_pred (zero_lt_of_ne_zero hn)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem exists_lfpApprox_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
    a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Proof state:
case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
exact h_fab

Result:
no goals

Proof state:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : a = b
⊢ False

Tactic:
exact h_nab h_eq

Result:
no goals

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑b < (succ #α).ord ∧ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
apply And.intro b.prop

Result:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b

Proof state:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : ↑a = ↑b
⊢ False

Tactic:
rw [Subtype.coe_inj] at h_eq

Result:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : a = b
⊢ False