harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
/-- This is Lemma 2.5 (b) from [Geck](Geck2017). -/
lemma root_add_root_mem_of_mem_of_mem (hk : α k + α i - α j ∈ Φ)
    (hkj : α k ≠ - α i) (hk' : α k - α j ∈ Φ) :
    α k + α i ∈ Φ

Proof state:
case h.e'_5
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : P.root k ≠ -P.root i
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
⊢ -(-P.root k + P.root j - P.root i) = P.root k + P.root i - P.root j

Tactic:
module

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma of_id_snd : IsPushout f (𝟙 _) (𝟙 _) f := IsPushout.of_vert_isIso ⟨by simp⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X : C
f : Z ⟶ X
⊢ f ≫ 𝟙 X = 𝟙 Z ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_mul_exp_add_div_pow_atTop (b c : ℝ) (n : ℕ) (hb : 0 < b) :
    Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop

Proof state:
case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => (b * rexp x + c) / x ^ 0) atTop atTop

Tactic:
simp only [pow_zero, div_one]

Result:
case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * rexp x + c) atTop atTop

Proof state:
b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (fun x => (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => (b * rexp x + c) / x ^ 0) atTop atTop

case inr
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => (b * rexp x + c) / x ^ n) atTop atTop

Proof state:
case inr
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
simp only [add_div, mul_div_assoc]

Result:
case inr
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => b * (rexp x / x ^ n) + c / x ^ n) atTop atTop

Proof state:
case inr
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => b * (rexp x / x ^ n) + c / x ^ n) atTop atTop

Tactic:
exact
  ((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add
    (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))

Result:
no goals

Proof state:
case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * rexp x + c) atTop atTop

Tactic:
exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.isBasis_setOf_insert_isBasis (hI : M.Indep I) :
    M.IsBasis I {x | M.IsBasis I (insert x I)}

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I I

Tactic:
exact hI.isBasis_self

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ I

Tactic:
simpa using (hu.eq_of_isBasis he.1).symm

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I (insert e I)

Tactic:
rw [insert_eq_of_mem he]

Result:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x | M.IsBasis I (insert x I)}

Tactic:
refine hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _))
  (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)

Result:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I (insert e I)

case refine_2
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ I
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Ioo (x y : ℝ) : Real.toEReal '' Ioo x y = Ioo ↑x ↑y

Proof state:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Ioo x y) = Ioo ↑x ↑y

Tactic:
rw [WithTop.image_coe_Ioo, WithBot.image_coe_Ioo]

Result:
x y : ℝ
⊢ Ioo ↑↑x ↑↑y = Ioo ↑x ↑y

Proof state:
x y : ℝ
⊢ Ioo ↑↑x ↑↑y = Ioo ↑x ↑y

Tactic:
rfl

Result:
no goals

Proof state:
x y : ℝ
⊢ Real.toEReal '' Ioo x y = Ioo ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Result:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Ioo x y) = Ioo ↑x ↑y
-- Mathlib/Data/Finset/Union.lean
lemma erase_biUnion (f : α → Finset β) (s : Finset α) (b : β) :
    (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b : β
⊢ (s.biUnion f).erase b = s.biUnion fun x => (f x).erase b

Tactic:
ext a

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b a : β
⊢ a ∈ (s.biUnion f).erase b ↔ a ∈ s.biUnion fun x => (f x).erase b

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b a : β
⊢ (¬a = b ∧ ∃ a_1 ∈ s, a ∈ f a_1) ↔ ∃ a_1 ∈ s, ¬a = b ∧ a ∈ f a_1

Tactic:
tauto

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b a : β
⊢ a ∈ (s.biUnion f).erase b ↔ a ∈ s.biUnion fun x => (f x).erase b

Tactic:
simp only [mem_biUnion, not_exists, not_and, mem_erase, ne_eq]

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b a : β
⊢ (¬a = b ∧ ∃ a_1 ∈ s, a ∈ f a_1) ↔ ∃ a_1 ∈ s, ¬a = b ∧ a ∈ f a_1
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_hasBinaryProduct [HasBinaryProduct X Y] [HasZeroObject C] [HasZeroMorphisms C] :
    IsPullback Limits.prod.fst Limits.prod.snd (0 : X ⟶ 0) (0 : Y ⟶ 0)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ IsPullback prod.fst prod.snd 0 0

Tactic:
convert @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
  <;> subsingleton

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma ofHoms_iff {ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) {A B : C} (g : A ⟶ B) :
    ofHoms f g ↔ ∃ i, Arrow.mk g = Arrow.mk (f i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ ofHoms f g ↔ ∃ i, Arrow.mk g = Arrow.mk (f i)

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ ofHoms f g → ∃ i, Arrow.mk g = Arrow.mk (f i)

case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ (∃ i, Arrow.mk g = Arrow.mk (f i)) → ofHoms f g

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ (∃ i, Arrow.mk g = Arrow.mk (f i)) → ofHoms f g

Tactic:
rintro ⟨i, h⟩

Result:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f g

Proof state:
case mp.mk
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X✝ Y✝ : ι → C
f : (i : ι) → X✝ i ⟶ Y✝ i
X Y : C
i : ι
⊢ ∃ i_1, Arrow.mk (f i) = Arrow.mk (f i_1)

Tactic:
exact ⟨i, rfl⟩

Result:
no goals

Proof state:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)

Tactic:
constructor

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ ofHoms f g → ∃ i, Arrow.mk g = Arrow.mk (f i)

Tactic:
rintro ⟨i⟩

Result:
case mp.mk
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X✝ Y✝ : ι → C
f : (i : ι) → X✝ i ⟶ Y✝ i
X Y : C
i : ι
⊢ ∃ i_1, Arrow.mk (f i) = Arrow.mk (f i_1)

Proof state:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f g

Tactic:
rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]

Result:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiableOn_apply (i : ι) (s' : Set (∀ i, F' i)) :
    DifferentiableOn (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) s'

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
s' : Set ((i : ι) → F' i)
h : DifferentiableOn 𝕜 (fun f i' => f i') s' → ∀ (i : ι), DifferentiableOn 𝕜 (fun x => x i) s'
⊢ DifferentiableOn 𝕜 (fun f => f i) s'

Tactic:
apply h

Result:
case a
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
s' : Set ((i : ι) → F' i)
h : DifferentiableOn 𝕜 (fun f i' => f i') s' → ∀ (i : ι), DifferentiableOn 𝕜 (fun x => x i) s'
⊢ DifferentiableOn 𝕜 (fun f i' => f i') s'

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
s' : Set ((i : ι) → F' i)
⊢ DifferentiableOn 𝕜 (fun f => f i) s'

Tactic:
have h := ((differentiableOn_pi (𝕜 := 𝕜)
           (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (s := s'))).1

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
s' : Set ((i : ι) → F' i)
h : DifferentiableOn 𝕜 (fun f i' => f i') s' → ∀ (i : ι), DifferentiableOn 𝕜 (fun x => x i) s'
⊢ DifferentiableOn 𝕜 (fun f => f i) s'

Proof state:
case a
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
s' : Set ((i : ι) → F' i)
h : DifferentiableOn 𝕜 (fun f i' => f i') s' → ∀ (i : ι), DifferentiableOn 𝕜 (fun x => x i) s'
⊢ DifferentiableOn 𝕜 (fun f i' => f i') s'

Tactic:
apply differentiableOn_id

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma min_eq_left (h : a ≤ b) : min a b = a

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a = min a b

Tactic:
apply eq_min (le_refl _) h

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ ∀ {d : α}, d ≤ a → d ≤ b → d ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a

Tactic:
apply Eq.symm

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a = min a b

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
d✝ : α
a✝¹ : d✝ ≤ a
a✝ : d✝ ≤ b
⊢ d✝ ≤ a

Tactic:
assumption

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ ∀ {d : α}, d ≤ a → d ≤ b → d ≤ a

Tactic:
intros

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
d✝ : α
a✝¹ : d✝ ≤ a
a✝ : d✝ ≤ b
⊢ d✝ ≤ a
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
@[simp, mfld_simps] lemma sum_chartAt_inr_apply {x y : M'} :
    (chartAt H (.inr x : M ⊕ M')) (Sum.inr y) = (chartAt H x) y

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
⊢ ↑(chartAt H (Sum.inr x)) (Sum.inr y) = ↑(chartAt H x) y

Tactic:
haveI : Nonempty H := nonempty_of_chartedSpace x

Result:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
this : Nonempty H
⊢ ↑(chartAt H (Sum.inr x)) (Sum.inr y) = ↑(chartAt H x) y

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
this : Nonempty H
⊢ ↑(chartAt H (Sum.inr x)) (Sum.inr y) = ↑(chartAt H x) y

Tactic:
rw [ChartedSpace.sum_chartAt_inr]

Result:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
this : Nonempty H
⊢ ↑((chartAt H x).lift_openEmbedding ⋯) (Sum.inr y) = ↑(chartAt H x) y

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
this : Nonempty H
⊢ ↑((chartAt H x).lift_openEmbedding ⋯) (Sum.inr y) = ↑(chartAt H x) y

Tactic:
exact PartialHomeomorph.lift_openEmbedding_apply _ _

Result:
no goals
-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylor_mean_remainder {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)
    (hf : ContDiffOn ℝ n f (Icc x₀ x))
    (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x))
    (gcont : ContinuousOn g (Icc x₀ x))
    (gdiff : ∀ x_1 : ℝ, x_1 ∈ Ioo x₀ x → HasDerivAt g (g' x_1) x_1)
    (g'_ne : ∀ x_1 : ℝ, x_1 ∈ Ioo x₀ x → g' x_1 ≠ 0) :
    ∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - x') ^ n / n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'

Proof state:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y =
    (f x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Tactic:
rw [mul_comm, ← div_left_inj' (g'_ne y hy), mul_div_cancel_right₀ _ (g'_ne y hy)] at h

Result:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Proof state:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x
⊢ (x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reverse_add_C (p : R[X]) (t : R) :
    reverse (p + C t) = reverse p + C t * X ^ p.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
t : R
⊢ (p + C t).reverse = p.reverse + C t * X ^ p.natDegree

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem IsAntichain.eq_setOf_maximal (ht : IsAntichain (· ≤ ·) t)
    (h : ∀ x, Maximal (· ∈ s) x → x ∈ t) (hs : ∀ a ∈ t, ∃ b, b ≤ a ∧ Maximal (· ∈ s) b) :
    {x | Maximal (· ∈ s) x} = t

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 => x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x => x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x => x ∈ s) b
⊢ {x | Maximal (fun x => x ∈ s) x} = t

Tactic:
refine Set.ext fun x ↦ ⟨h _, fun hx ↦ ?_⟩

Result:
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 => x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x => x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x => x ∈ s) b
x : α
hx : x ∈ t
⊢ x ∈ {x | Maximal (fun x => x ∈ s) x}

Proof state:
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 => x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x => x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x => x ∈ s) b
x : α
hx : x ∈ t
⊢ x ∈ {x | Maximal (fun x => x ∈ s) x}

Tactic:
obtain ⟨y, hyx, hy⟩ := hs x hx

Result:
case intro.intro
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 => x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x => x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x => x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun x => x ∈ s) y
⊢ x ∈ {x | Maximal (fun x => x ∈ s) x}

Proof state:
case intro.intro
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 => x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x => x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x => x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun x => x ∈ s) y
⊢ x ∈ {x | Maximal (fun x => x ∈ s) x}

Tactic:
rwa [← ht.eq (h y hy) hx hyx]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Fork.equalizer_ext (s : Fork f g) {W : C} {k l : W ⟶ s.pt} (h : k ≫ s.ι = l ≫ s.ι) :
    ∀ j : WalkingParallelPair, k ≫ s.π.app j = l ≫ s.π.app j
  | zero => h
  | one => by
    have : k ≫ ι s ≫ f = l ≫ ι s ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.ι ≫ f = l ≫ s.ι ≫ f

Tactic:
simp only [← Category.assoc]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ (k ≫ s.ι) ≫ f = (l ≫ s.ι) ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
⊢ k ≫ s.π.app one = l ≫ s.π.app one

Tactic:
rw [s.app_one_eq_ι_comp_left, this]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem zero_trim (hm : m ≤ m0) : (0 : Measure α).trim hm = (0 : @Measure α m)

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
hm : m ≤ m0
⊢ Measure.trim 0 hm = 0

Tactic:
simp [Measure.trim, @OuterMeasure.toMeasure_zero _ m]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
theorem padicValNat_eq_emultiplicity [hp : Fact p.Prime] {n : ℕ} (hn : 0 < n) :
    padicValNat p n = emultiplicity p n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ ↑(padicValNat p n) = emultiplicity p n

Tactic:
rw [(finiteMultiplicity_iff.2 ⟨hp.out.ne_one, hn⟩).emultiplicity_eq_multiplicity]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ ↑(padicValNat p n) = ↑(multiplicity p n)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ ↑(padicValNat p n) = ↑(multiplicity p n)

Tactic:
exact_mod_cast padicValNat_def hn

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_rotation_pi_div_two_right_smul (x : V) (r : ℝ) :
    ⟪r • x, o.rotation (π / 2 : ℝ) x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ inner (r • x) ((o.rotation ↑(π / 2)) x) = 0

Tactic:
rw [real_inner_comm, inner_rotation_pi_div_two_left_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top {p q : ℝ} (hp0_lt : 0 < p) (hq0 : 0 ≤ q)
    {f g : α → ℝ≥0∞} (hf_top : ∫⁻ a, f a ^ p ∂μ = ⊤) (hg_nonzero : (∫⁻ a, g a ^ q ∂μ) ≠ 0) :
    (∫⁻ a, (f * g) a ∂μ) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ q ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
rw [hf_top, ENNReal.top_rpow_of_pos hp0_inv_lt]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = ⊤ * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = ⊤ * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
simp [hq0, hg_nonzero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
have hp0_inv_lt : 0 < 1 / p := by simp [hp0_lt]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
refine le_trans le_top (le_of_eq ?_)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
⊢ 0 < 1 / p

Tactic:
simp [hp0_lt]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma StrictAnti.mem_lowerBounds_image (hf : StrictAnti f) :
    f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s

Tactic:
simp [upperBounds, lowerBounds, hf.le_iff_le]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
@[simp 1100, norm_cast]
lemma norm_real (r : ℝ) : ‖(r : ℂ)‖ = ‖r‖

Proof state:
r : ℝ
⊢ ‖↑r‖ = ‖r‖

Tactic:
simp [norm_def, Real.sqrt_mul_self_eq_abs]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem Ioc_mem_nhds_iff [NoMaxOrder α] {a b x : α} : Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b x : α
⊢ Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
rw [← interior_Ioc, mem_interior_iff_mem_nhds]

Result:
no goals