harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem basicOpen_eq_of_affine {R : CommRingCat} (f : R) :
    (Spec R).basicOpen ((Scheme.ΓSpecIso R).inv f) = PrimeSpectrum.basicOpen f

Proof state:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f

Tactic:
suffices IsUnit (StructureSheaf.toStalk R x f) ↔ f ∉ PrimeSpectrum.asIdeal x by exact this

Result:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ IsUnit ((ConcreteCategory.hom (StructureSheaf.toStalk (↑R) x)) f) ↔ f ∉ x.asIdeal

Proof state:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ x ∈ ↑((Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔ x ∈ ↑(PrimeSpectrum.basicOpen f)

Tactic:
simp only [SetLike.mem_coe, Scheme.mem_basicOpen_top, Opens.coe_top]

Result:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f

Proof state:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ IsUnit ((ConcreteCategory.hom (StructureSheaf.toStalk (↑R) x)) f) ↔ f ∉ x.asIdeal

Tactic:
rw [← isUnit_map_iff (StructureSheaf.stalkToFiberRingHom R x).hom,
  StructureSheaf.stalkToFiberRingHom_toStalk]

Result:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ IsUnit ((algebraMap ↑R ↑(CommRingCat.of (Localization.AtPrime x.asIdeal))) f) ↔ f ∉ x.asIdeal

Proof state:
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
this : IsUnit ((ConcreteCategory.hom (StructureSheaf.toStalk (↑R) x)) f) ↔ f ∉ x.asIdeal
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f

Tactic:
exact this

Result:
no goals

Proof state:
R : CommRingCat
f : ↑R
⊢ (Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f) = PrimeSpectrum.basicOpen f

Tactic:
ext x

Result:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ x ∈ ↑((Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔ x ∈ ↑(PrimeSpectrum.basicOpen f)

Proof state:
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ IsUnit ((algebraMap ↑R ↑(CommRingCat.of (Localization.AtPrime x.asIdeal))) f) ↔ f ∉ x.asIdeal

Tactic:
exact
  (IsLocalization.AtPrime.isUnit_to_map_iff (Localization.AtPrime (PrimeSpectrum.asIdeal x))
      (PrimeSpectrum.asIdeal x) f :
    _)

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem preimage_mul_left_singleton :
    preimage {b} (a * ·) (mul_right_injective _).injOn = {a⁻¹ * b}

Proof state:
α : Type u_2
inst✝ : Group α
a b : α
⊢ {b}.preimage (fun x => a * x) ⋯ = {a⁻¹ * b}

Tactic:
classical rw [← image_mul_left', image_singleton]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
a b : α
⊢ {b}.preimage (fun x => a * x) ⋯ = {a⁻¹ * b}

Tactic:
rw [← image_mul_left', image_singleton]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubVSubWeights_self [DecidableEq ι] (i : ι) :
    weightedVSubVSubWeights k i i = 0

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
⊢ weightedVSubVSubWeights k i i = 0

Tactic:
simp [weightedVSubVSubWeights]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
lemma _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
    AddEquiv.finsuppUnique.symm d = single () d

Proof state:
M : Type u_13
inst✝ : AddZeroClass M
d : M
⊢ (AddEquiv.finsuppUnique.symm d) default = d

Tactic:
simp [AddEquiv.finsuppUnique]

Result:
no goals

Proof state:
M : Type u_13
inst✝ : AddZeroClass M
d : M
⊢ AddEquiv.finsuppUnique.symm d = single () d

Tactic:
rw [Finsupp.unique_single (AddEquiv.finsuppUnique.symm d), Finsupp.unique_single_eq_iff]

Result:
M : Type u_13
inst✝ : AddZeroClass M
d : M
⊢ (AddEquiv.finsuppUnique.symm d) default = d
-- Mathlib/Order/Atoms.lean
theorem isAtomic_iff [OrderBot α] [OrderBot β] (f : α ≃o β) :
    IsAtomic α ↔ IsAtomic β

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : α ≃o β
⊢ IsAtomic α ↔ IsAtomic β

Tactic:
simp only [isAtomic_iff, f.surjective.forall, f.surjective.exists, ← map_bot f, f.eq_iff_eq,
  f.le_iff_le, f.isAtom_iff]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Formula for `cosZeta` as a Dirichlet series in the convergence range, with sum over `ℕ`. -/
lemma hasSum_nat_cosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ Real.cos (2 * π * a * n) / (n : ℂ) ^ s) (cosZeta a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
have := (hasSum_int_cosZeta a hs).nat_add_neg

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (cosZeta (↑a) s + cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n => ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
⊢ HasSum (fun n => ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
simp_rw [push_cast, Complex.cos, neg_mul]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
⊢ HasSum (fun n => (cexp (2 * ↑π * ↑a * ↑n * I) + cexp (-(2 * ↑π * ↑a * ↑n * I))) / 2 / ↑n ^ s) (cosZeta (↑a) s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
⊢ HasSum (fun n => (cexp (2 * ↑π * ↑a * ↑n * I) + cexp (-(2 * ↑π * ↑a * ↑n * I))) / 2 / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
exact this.congr_fun fun n ↦ by rw [show 2 * π * a * n * I = 2 * π * I * a * n by ring]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (cosZeta (↑a) s + cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n => ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
simp_rw [abs_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero, Int.cast_zero,
  zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero, ← add_div,
  div_right_comm _ _ (2 : ℂ)] at this

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
⊢ HasSum (fun n => ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
n : ℕ
⊢ (cexp (2 * ↑π * ↑a * ↑n * I) + cexp (-(2 * ↑π * ↑a * ↑n * I))) / 2 / ↑n ^ s =
    (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s

Tactic:
rw [show 2 * π * a * n * I = 2 * π * I * a * n by ring]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
n : ℕ
⊢ 2 * ↑π * ↑a * ↑n * I = 2 * ↑π * I * ↑a * ↑n

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subtype_mul_prod_subtype {α β : Type*} [Fintype α] [CommMonoid β] (p : α → Prop)
    (f : α → β) [DecidablePred p] :
    (∏ i : { x // p x }, f i) * ∏ i : { x // ¬p x }, f i = ∏ i, f i

Proof state:
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ (∏ i : { x // p x }, f ↑i) * ∏ i : { x // ¬p x }, f ↑i = ∏ i : α, f i

Tactic:
rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]

Result:
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i : α, f i

case h
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ ∀ (x : α), x ∈ sᶜ ↔ ¬p x

case h
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ ∀ (x : α), x ∈ s ↔ p x

Proof state:
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
⊢ (∏ i : { x // p x }, f ↑i) * ∏ i : { x // ¬p x }, f ↑i = ∏ i : α, f i

Tactic:
let s := { x | p x }.toFinset

Result:
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ (∏ i : { x // p x }, f ↑i) * ∏ i : { x // ¬p x }, f ↑i = ∏ i : α, f i

Proof state:
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i : α, f i

Tactic:
exact Finset.prod_mul_prod_compl _ _

Result:
no goals

Proof state:
case h
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ ∀ (x : α), x ∈ s ↔ p x

Tactic:
simp [s]

Result:
no goals

Proof state:
case h
α : Type u_9
β : Type u_10
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := {x | p x}.toFinset
⊢ ∀ (x : α), x ∈ sᶜ ↔ ¬p x

Tactic:
simp [s]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem L1.dist_eq_integral_dist (f g : α →₁[μ] H) : dist f g = ∫ a, dist (f a) (g a) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
⊢ dist f g = ∫ (a : α), dist (↑↑f a) (↑↑g a) ∂μ

Tactic:
simp only [dist_eq_norm, L1.norm_eq_integral_norm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
⊢ ∫ (a : α), ‖↑↑(f - g) a‖ ∂μ = ∫ (a : α), ‖↑↑f a - ↑↑g a‖ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
⊢ ∫ (a : α), ‖↑↑(f - g) a‖ ∂μ = ∫ (a : α), ‖↑↑f a - ↑↑g a‖ ∂μ

Tactic:
exact integral_congr_ae <| (Lp.coeFn_sub _ _).fun_comp norm

Result:
no goals
-- Mathlib/Data/Finsupp/Fin.lean
theorem cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ y = 0

Tactic:
rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]

Result:
no goals

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : y ≠ 0
⊢ cons y s ≠ 0

Tactic:
contrapose! h with c

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ y = 0
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuous_iff_range {F : ι → β → α} :
    UniformEquicontinuous F ↔ UniformEquicontinuous ((↑) : range F → β → α) :=
  ⟨fun h => by rw [← comp_rangeSplitting F]; exact h.comp _, fun h =>
    h.comp (rangeFactorization F)⟩

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)

Tactic:
exact h.comp _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous Subtype.val

Tactic:
rw [← comp_rangeSplitting F]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)
-- Mathlib/Data/Part.lean
@[simp] lemma toOption_isSome (o : Part α) [Decidable o.Dom] : o.toOption.isSome ↔ o.Dom

Proof state:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
by_cases h : o.Dom <;> simp [h, toOption]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem diam_image (s : Set α) : Metric.diam ((f : α → β) '' s) = ratio f * Metric.diam s

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ Metric.diam (⇑f '' s) = ↑(ratio f) * Metric.diam s

Tactic:
simp [Metric.diam, ediam_image, ENNReal.toReal_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Properties.lean
/-- The `componentCompl`s chosen by an end are all infinite. -/
lemma end_componentCompl_infinite (e : G.end) (K : (Finset V)ᵒᵖ) :
    ((e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K).supp.Infinite

Proof state:
V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
⊢ (ComponentCompl.supp (↑e K)).Infinite

Tactic:
refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)

Result:
V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ L
⊢ ∃ D, ComponentCompl.hom h D = ↑e K

Proof state:
V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ L
⊢ ∃ D, ComponentCompl.hom h D = ↑e K

Tactic:
change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h

Result:
V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ Opposite.unop (Opposite.op L)
⊢ ∃ D, ComponentCompl.hom h D = ↑e K

Proof state:
V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ Opposite.unop (Opposite.op L)
⊢ ∃ D, ComponentCompl.hom h D = ↑e K

Tactic:
exact ⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem affineCombination_eq_centerMass {ι : Type*} {t : Finset ι} {p : ι → E} {w : ι → R}
    (hw₂ : ∑ i ∈ t, w i = 1) : t.affineCombination R p w = centerMass t w p

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ ∑ i ∈ t, w i • (p i -ᵥ 0) = ∑ i ∈ t, w i • p i

Tactic:
simp_rw [vsub_eq_sub, sub_zero]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ (affineCombination R t p) w = t.centerMass w p

Tactic:
rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
  Finset.weightedVSubOfPoint_apply, vadd_eq_add, add_zero, t.centerMass_eq_of_sum_1 _ hw₂]

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ ∑ i ∈ t, w i • (p i -ᵥ 0) = ∑ i ∈ t, w i • p i
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_top_iff' (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToOn N f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        ∀ m : ℕ, ∀ x ∈ s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpToOn N f p s ↔
    (∀ x ∈ s, (p x 0).curry0 = f x) ∧ ∀ (m : ℕ), ∀ x ∈ s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x

Tactic:
refine ⟨fun h => ⟨h.1, fun m => h.2 m (natCast_lt_of_coe_top_le_withTop hN _)⟩, fun h =>
  ⟨h.1, fun m _ => h.2 m, fun m _ x hx =>
    (h.2 m x hx).continuousWithinAt⟩⟩

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ENormedSpace.lean
theorem map_smul (c : 𝕜) (x : V) : e (c • x) = ‖c‖₊ * e x

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * (↑‖c⁻¹‖₊ * ↑e (c • x)) = ↑e (c • x)

Tactic:
rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top,
  one_mul]
  <;> simp [hc]

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)

Tactic:
by_cases hc : c = 0

Result:
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
hc : c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)

case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)

Proof state:
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
hc : c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)

Tactic:
simp [hc]

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * ↑e x = ↑‖c‖₊ * ↑e (c⁻¹ • c • x)

Tactic:
rw [inv_smul_smul₀ hc]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)

Tactic:
calc
  (‖c‖₊ : ℝ≥0∞) * e x = ‖c‖₊ * e (c⁻¹ • c • x) := by rw [inv_smul_smul₀ hc]
  _ ≤ ‖c‖₊ * (‖c⁻¹‖₊ * e (c • x)) := mul_le_mul_left' (e.map_smul_le' _ _) _
  _ = e (c • x) := by
    rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top,
      one_mul]
      <;> simp [hc]

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
⊢ ↑e (c • x) = ↑‖c‖₊ * ↑e x

Tactic:
apply le_antisymm (e.map_smul_le' c x)

Result:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
c : 𝕜
x : V
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem eq_of_comp_right_eq {f g : Y ⟶ Z} (w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) :
    f = g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
Y Z : C
f g : Y ⟶ Z
w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
⊢ f = g

Tactic:
convert w (𝟙 Y) <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_comp (p q : R[X]) :
    derivative (p.comp q) = derivative q * p.derivative.comp q

Proof state:
case h_monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ C a✝ * (↑n✝ * q ^ (n✝ - 1) * derivative q) = derivative q * (C a✝ * ↑n✝ * q ^ (n✝ - 1))

Tactic:
ring

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
⊢ derivative (p.comp q) = derivative q * (derivative p).comp q

Tactic:
induction p using Polynomial.induction_on'

Result:
case h_add
R : Type u
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : derivative (p✝.comp q) = derivative q * (derivative p✝).comp q
a✝ : derivative (q✝.comp q) = derivative q * (derivative q✝).comp q
⊢ derivative ((p✝ + q✝).comp q) = derivative q * (derivative (p✝ + q✝)).comp q

case h_monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q

Proof state:
case h_monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q

Tactic:
simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C,
  zero_mul, C_eq_natCast, zero_add, RingHom.map_mul]

Result:
case h_monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ C a✝ * (↑n✝ * q ^ (n✝ - 1) * derivative q) = derivative q * (C a✝ * ↑n✝ * q ^ (n✝ - 1))

Proof state:
case h_add
R : Type u
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : derivative (p✝.comp q) = derivative q * (derivative p✝).comp q
a✝ : derivative (q✝.comp q) = derivative q * (derivative q✝).comp q
⊢ derivative ((p✝ + q✝).comp q) = derivative q * (derivative (p✝ + q✝)).comp q

Tactic:
simp [*, mul_add]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
lemma cons_sub_of_le (a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ a ::ₘ s - t = a ::ₘ (s - t)

Tactic:
rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_degreeLT {n : ℕ} {f : R[X]} : f ∈ degreeLT R n ↔ degree f < n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ f ∈ degreeLT R n ↔ f.degree < ↑n

Tactic:
rw [degreeLT, Submodule.mem_iInf]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), f ∈ ⨅ (_ : i ≥ n), LinearMap.ker (lcoeff R i)) ↔ f.degree < ↑n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), f ∈ ⨅ (_ : i ≥ n), LinearMap.ker (lcoeff R i)) ↔ f.degree < ↑n

Tactic:
conv_lhs => intro i; rw [Submodule.mem_iInf]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ f.degree < ↑n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ b ∈ f.support, ↑b < ↑n

Tactic:
conv_rhs =>
  simp only [mem_support_iff]
  intro b
  rw [Nat.cast_withBot, WithBot.coe_lt_coe, lt_iff_not_le, Ne, not_imp_not]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), n ≤ b → f.coeff b = 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ b ∈ f.support, ↑b < ↑n

R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n

Tactic:
rotate_left

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n

R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ b ∈ f.support, ↑b < ↑n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n

Tactic:
apply WithBot.bot_lt_coe

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), n ≤ b → f.coeff b = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ f.degree < ↑n

Tactic:
rw [degree, Finset.max_eq_sup_coe]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ f.support.sup WithBot.some < ↑n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ f.support.sup WithBot.some < ↑n

Tactic:
rw [Finset.sup_lt_iff ?_]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ b ∈ f.support, ↑b < ↑n

R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ici_diff_Ioi_same : Ici a \ Ioi a = {a}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ Ici a \ Ioi a = {a}

Tactic:
rw [← Ici_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 left_mem_Ici)]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_def {f g : MonoidAlgebra k G} :
    f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
⊢ f * g = sum f fun a₁ b₁ => sum g fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)

Tactic:
rfl

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
⊢ f * g = sum f fun a₁ b₁ => sum g fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)

Tactic:
with_unfolding_all rfl

Result:
no goals