internlm/Lean-Github huggingface dataset:
Theorem: has_primitives.has_logs
Proof state before:
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv g z = deriv lf z
Tactic:
unfold_let
Proof state after:
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv (fun z => lf z + (log (f z₀) - lf z₀)) z = deriv lf z
Theorem: has_primitives.has_logs
Proof state before:
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv (fun z => lf z + (log (f z₀) - lf z₀)) z = deriv lf z
Tactic:
simp
Proof state after:
no goals
Theorem: toto
Proof state before:
f : ℝ → ℝ
a b : ℝ
hab : a < b
n : ℕ
h : ContDiffOn ℝ (↑n) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
Tactic:
induction n generalizing f
Proof state after:
case zero
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)

case succ
a b : ℝ
hab : a < b
n✝ : ℕ
n_ih✝ : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n✝) f (Icc a b) → ∃ g, ContDiff ℝ (↑n✝) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n✝)) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n✝)) g ∧ EqOn g f (Icc a b)
Theorem: toto
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)
Tactic:
case zero =>
simp only [CharP.cast_eq_zero, contDiff_zero, contDiffOn_zero] at h ⊢
refine ⟨IccExtend hab.le (restrict (Icc a b) f), h.restrict.Icc_extend', ?_⟩
exact λ t ht => IccExtend_of_mem _ _ ht
Proof state after:
no goals
Theorem: toto
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)
Tactic:
simp only [CharP.cast_eq_zero, contDiff_zero, contDiffOn_zero] at h ⊢
Proof state after:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ ∃ g, Continuous g ∧ EqOn g f (Icc a b)
Theorem: toto
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ ∃ g, Continuous g ∧ EqOn g f (Icc a b)
Tactic:
refine ⟨IccExtend hab.le (restrict (Icc a b) f), h.restrict.Icc_extend', ?_⟩
Proof state after:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ EqOn (IccExtend ⋯ (restrict (Icc a b) f)) f (Icc a b)
Theorem: toto
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ EqOn (IccExtend ⋯ (restrict (Icc a b) f)) f (Icc a b)
Tactic:
exact λ t ht => IccExtend_of_mem _ _ ht
Proof state after:
no goals
Theorem: toto
Proof state before:
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Tactic:
have h1 : ContDiffOn ℝ n (derivWithin f (Icc a b)) (Icc a b) :=
  h.derivWithin (uniqueDiffOn_Icc hab) le_rfl
Proof state after:
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Theorem: toto
Proof state before:
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Tactic:
obtain ⟨gg, h2, h3⟩ := ih h1
Proof state after:
case intro.intro
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Theorem: toto
Proof state before:
case intro.intro
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Tactic:
refine ⟨λ t => f a + ∫ u in a..t, gg u, ?_, ?_⟩
Proof state after:
case intro.intro.refine_1
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ContDiff ℝ ↑(Nat.succ n) fun t => f a + ∫ (u : ℝ) in a..t, gg u

case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ EqOn (fun t => f a + ∫ (u : ℝ) in a..t, gg u) f (Icc a b)
Theorem: toto
Proof state before:
case intro.intro.refine_1
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ContDiff ℝ ↑(Nat.succ n) fun t => f a + ∫ (u : ℝ) in a..t, gg u
Tactic:
rw [contDiff_succ_iff_deriv]
Proof state after:
case intro.intro.refine_1
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ (Differentiable ℝ fun t => f a + ∫ (u : ℝ) in a..t, gg u) ∧
    ContDiff ℝ (↑n) (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u)
Theorem: toto
Proof state before:
case intro.intro.refine_1
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ (Differentiable ℝ fun t => f a + ∫ (u : ℝ) in a..t, gg u) ∧
    ContDiff ℝ (↑n) (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u)
Tactic:
constructor
Proof state after:
case intro.intro.refine_1.left
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ Differentiable ℝ fun t => f a + ∫ (u : ℝ) in a..t, gg u

case intro.intro.refine_1.right
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ContDiff ℝ (↑n) (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u)
Theorem: toto
Proof state before:
case intro.intro.refine_1.left
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ Differentiable ℝ fun t => f a + ∫ (u : ℝ) in a..t, gg u
Tactic:
refine differentiableOn_univ.1 ((differentiableOn_integral_of_continuous ?_ h2.continuous).const_add _)
Proof state after:
case intro.intro.refine_1.left
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ∀ x ∈ univ, IntervalIntegrable gg MeasureTheory.volume a x
Theorem: toto
Proof state before:
case intro.intro.refine_1.left
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ∀ x ∈ univ, IntervalIntegrable gg MeasureTheory.volume a x
Tactic:
simp [h2.continuous.intervalIntegrable]
Proof state after:
no goals
Theorem: toto
Proof state before:
case intro.intro.refine_1.right
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ ContDiff ℝ (↑n) (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u)
Tactic:
convert h2
Proof state after:
case h.e'_10
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u) = gg
Theorem: toto
Proof state before:
case h.e'_10
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u) = gg
Tactic:
ext t
Proof state after:
case h.e'_10.h
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
⊢ deriv (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = gg t
Theorem: toto
Proof state before:
case h.e'_10.h
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
⊢ deriv (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = gg t
Tactic:
simp [deriv_const_add, h2.continuous.deriv_integral]
Proof state after:
no goals
Theorem: toto
Proof state before:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
⊢ EqOn (fun t => f a + ∫ (u : ℝ) in a..t, gg u) f (Icc a b)
Tactic:
intro t ht
Proof state after:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
⊢ (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = f t
Theorem: toto
Proof state before:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
⊢ (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = f t
Tactic:
dsimp
Proof state after:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Theorem: toto
Proof state before:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Tactic:
have l6 : Icc a t ⊆ Icc a b := Icc_subset_Icc_right ht.2
Proof state after:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Theorem: toto
Proof state before:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Tactic:
have l9 : EqOn gg (derivWithin f (Icc a b)) (uIcc a t) := h3.mono (by simp [uIcc, ht.1, l6])
Proof state after:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
l9 : EqOn gg (derivWithin f (Icc a b)) (uIcc a t)
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Theorem: toto
Proof state before:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
l9 : EqOn gg (derivWithin f (Icc a b)) (uIcc a t)
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Tactic:
have l10 := h.one_of_succ.integral_eq_sub'' hab.le ht
Proof state after:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
l9 : EqOn gg (derivWithin f (Icc a b)) (uIcc a t)
l10 : ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Theorem: toto
Proof state before:
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
l9 : EqOn gg (derivWithin f (Icc a b)) (uIcc a t)
l10 : ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Tactic:
simp [integral_congr l9, l10]
Proof state after:
no goals
Theorem: toto
Proof state before:
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
⊢ uIcc a t ⊆ Icc a b
Tactic:
simp [uIcc, ht.1, l6]
Proof state after:
no goals
Theorem: toto'
Proof state before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
cases eq_or_ne a b
Proof state after:
case inl
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
h✝ : a = b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)

case inr
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
h✝ : a ≠ b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Theorem: toto'
Proof state before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a = b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
case inl hab => exact ⟨λ _ => f a, by simp [hab, contDiff_const]⟩
Proof state after:
no goals
Theorem: toto'
Proof state before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a = b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
exact ⟨λ _ => f a, by simp [hab, contDiff_const]⟩
Proof state after:
no goals
Theorem: toto'
Proof state before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a = b
⊢ (ContDiff ℝ ↑n fun x => f a) ∧ EqOn (fun x => f a) f (uIcc a b)
Tactic:
simp [hab, contDiff_const]
Proof state after:
no goals
Theorem: toto'
Proof state before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a ≠ b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
case inr hab => exact toto (min_lt_max.2 hab) h
Proof state after:
no goals
Theorem: toto'
Proof state before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a ≠ b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
exact toto (min_lt_max.2 hab) h
Proof state after:
no goals
Theorem: SkewPolynomial.eta
Proof state before:
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q f : R[X;φ]
⊢ { toFinsupp := f.toFinsupp } = f
Tactic:
cases f
Proof state after:
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := { toFinsupp := toFinsupp✝ }.toFinsupp } = { toFinsupp := toFinsupp✝ }
Theorem: SkewPolynomial.eta
Proof state before:
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := { toFinsupp := toFinsupp✝ }.toFinsupp } = { toFinsupp := toFinsupp✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_add
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a + b } = SkewPolynomial.add { toFinsupp := a } { toFinsupp := b }
Tactic:
rw [add_def]
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_neg
Proof state before:
R : Type u
a✝ b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a : AddMonoidAlgebra S ℕ
⊢ { toFinsupp := -a } = SkewPolynomial.neg { toFinsupp := a }
Tactic:
rw [neg_def]
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_sub
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : AddMonoidAlgebra S ℕ
⊢ { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
Tactic:
rw [sub_eq_add_neg, ofFinsupp_add, ofFinsupp_neg]
Proof state after:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : AddMonoidAlgebra S ℕ
⊢ { toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }
Theorem: SkewPolynomial.ofFinsupp_sub
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : AddMonoidAlgebra S ℕ
⊢ { toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }
Tactic:
rfl
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_mul
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := AddMonoidAlgebra.mul' φ a b } = SkewPolynomial.mul { toFinsupp := a } { toFinsupp := b }
Tactic:
rw [mul_def]
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_pow
Proof state before:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = { toFinsupp := a } ^ n
Tactic:
change _ = npowRec n _
Proof state after:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
Theorem: SkewPolynomial.ofFinsupp_pow
Proof state before:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
Tactic:
induction n with
| zero        => simp [npowRec]; rfl
| succ n n_ih => simp [npowRec, pow_succ]; rw [<- n_ih, <- ofFinsupp_mul]; rfl
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_pow
Proof state before:
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ Nat.zero a } = npowRec Nat.zero { toFinsupp := a }
Tactic:
simp [npowRec]
Proof state after:
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ 0 a } = 1
Theorem: SkewPolynomial.ofFinsupp_pow
Proof state before:
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ 0 a } = 1
Tactic:
rfl
Proof state after:
no goals