harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
lemma isSheaf_coherent_of_projective_of_comp [Preregular C] [FinitaryExtensive C]
    [∀ (X : C), Projective X]
    [ReflectsFiniteProducts s]
    (hF : IsSheaf (coherentTopology C) (F ⋙ s)) : IsSheaf (coherentTopology C) F

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
⊢ IsSheaf (coherentTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢

Result:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : PreservesFiniteProducts (F ⋙ s)
⊢ PreservesFiniteProducts F

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : PreservesFiniteProducts (F ⋙ s)
⊢ PreservesFiniteProducts F

Tactic:
exact ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩⟩⟩⟩

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem monomial_sum_index {α : Type*} (s : Finset α) (f : α → σ →₀ ℕ) (a : R) :
    monomial (∑ i ∈ s, f i) a = C a * ∏ i ∈ s, monomial (f i) 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
⊢ (monomial (∑ i ∈ s, f i)) a = C a * ∏ i ∈ s, (monomial (f i)) 1

Tactic:
rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem smul_mat_cons (x : α) (v : n' → α) (A : Fin m → n' → α) :
    x • vecCons v A = vecCons (x • v) (x • A)

Proof state:
case h.h
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin m.succ
x✝ : n'
⊢ (x • vecCons v A) i x✝ = vecCons (x • v) (x • A) i x✝

Tactic:
refine Fin.cases ?_ ?_ i <;> simp

Result:
no goals

Proof state:
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
⊢ x • vecCons v A = vecCons (x • v) (x • A)

Tactic:
ext i

Result:
case h.h
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin m.succ
x✝ : n'
⊢ (x • vecCons v A) i x✝ = vecCons (x • v) (x • A) i x✝
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
/-- A version of δ_comp_δ with indices in ℕ satisfying relevant inequalities. -/
lemma δ_comp_δ_nat {n} (i j : ℕ) (hi : i < n + 2) (hj : j < n + 2) (H : i ≤ j) :
    δ ⟨i, hi⟩ ≫ δ ⟨j + 1, by omega⟩ = δ ⟨j, hj⟩ ≫ δ ⟨i, by omega⟩ :=
  δ_comp_δ (n := n) (i := ⟨i, by omega⟩) (j := ⟨j, by omega⟩) (by simpa)

Proof state:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ i < n + 1 + 2

Tactic:
omega

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ j < n + 2

Tactic:
omega

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ j + 1 < n + 1 + 2

Tactic:
omega

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ i < n + 2

Tactic:
omega

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simpa

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem finite_left_iff (h : IsComplement S H) : Finite S ↔ H.FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex

Tactic:
exact ⟨fun _ ↦ finiteIndex_of_finite_quotient H, fun _ ↦ finite_quotient_of_finiteIndex H⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ Finite ↑S ↔ H.FiniteIndex

Tactic:
rw [← h.leftQuotientEquiv.finite_iff]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Ici_mul_Ici_subset' (a b : α) : Ici a * Ici b ⊆ Ici (a * b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ici b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ici (a * b)

Tactic:
exact mul_le_mul' hya hzb

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ Ici a * Ici b ⊆ Ici (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ici b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ici (a * b)
-- Mathlib/Data/Fin/Rev.lean
lemma succAbove_rev_right (p : Fin (n + 1)) (i : Fin n) :
    p.succAbove i.rev = (p.rev.succAbove i).rev

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev

Tactic:
rw [succAbove_rev_left, rev_rev]

Result:
no goals
-- Mathlib/Data/Int/Order/Lemmas.lean
theorem natAbs_lt_iff_mul_self_lt {a b : ℤ} : a.natAbs < b.natAbs ↔ a * a < b * b

Proof state:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ ↑a.natAbs < ↑b.natAbs

Tactic:
exact Int.ofNat_lt.symm

Result:
no goals

Proof state:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]

Result:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ ↑a.natAbs < ↑b.natAbs
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma card_mul_expect (s : Finset ι) (f : ι → M) :
    #s * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : Semiring M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
⊢ ↑(#s) * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
rw [← nsmul_eq_mul, card_smul_expect]

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem isOpen_setOf_mem_nhds_and_isMaxOn_norm {f : E → F} {s : Set E}
    (hd : DifferentiableOn ℂ f s) : IsOpen {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
hd : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
⊢ Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)

Tactic:
exact (norm_eventually_eq_of_isLocalMax hd <| hz.2.isLocalMax hz.1).mono fun x hx y hy =>
  le_trans (hz.2 hy).out hx.ge

Result:
no goals

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
⊢ Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)

Tactic:
replace hd : ∀ᶠ w in 𝓝 z, DifferentiableAt ℂ f w := hd.eventually_differentiableAt hz.1

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
hd : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
⊢ Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
⊢ IsOpen {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}

Tactic:
refine isOpen_iff_mem_nhds.2 fun z hz => (eventually_eventually_nhds.2 hz.1).and ?_

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
⊢ Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem Spec_zeroLocus {R : CommRingCat} (s : Set Γ(Spec R, ⊤)) :
    (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)

Proof state:
case h.e'_2.h.e'_3
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ s = ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

Tactic:
rw [Set.image_preimage_eq]

Result:
case h.e'_2.h.e'_3.h
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv)

Proof state:
case h.e'_2.h.e'_3.h
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv)

Tactic:
exact (ConcreteCategory.bijective_of_isIso (C := CommRingCat) _).2

Result:
no goals

Proof state:
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

Tactic:
convert Spec_zeroLocus_eq_zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)

Result:
case h.e'_2.h.e'_3
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ s = ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
lemma quotientInfToPiQuotient_inj (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] :
    Injective (quotientInfToPiQuotient I)

Proof state:
R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ Injective ⇑(quotientInfToPiQuotient I)

Tactic:
rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_eq_add_one_sub_fract (ha : fract a ≠ 0) : (⌈a⌉ : α) = a + 1 - fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - fract a

Tactic:
rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - (a + 1 - ↑⌈a⌉)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - (a + 1 - ↑⌈a⌉)

Tactic:
abel

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_ite_empty_left {x : α} [Decidable p] {l : Vector α 0} :
    (x ∈ if p then #v[] else l) ↔ ¬ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : Vector α 0
⊢ (x ∈ if p then { toArray := #[], size_toArray := ⋯ } else l) ↔ ¬p ∧ x ∈ l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem dist_circumcenter_eq_circumradius' {n : ℕ} (s : Simplex ℝ P n) :
    ∀ i, dist s.circumcenter (s.points i) = s.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ dist s.circumcenter (s.points i) = s.circumradius

Tactic:
rw [dist_comm]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ dist (s.points i) s.circumcenter = s.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ dist (s.points i) s.circumcenter = s.circumradius

Tactic:
exact dist_circumcenter_eq_circumradius _ _

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ ∀ (i : Fin (n + 1)), dist s.circumcenter (s.points i) = s.circumradius

Tactic:
intro i

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ dist s.circumcenter (s.points i) = s.circumradius
-- Mathlib/Algebra/Lie/Free.lean
theorem lift_of_apply (f : X → L) (x) : lift R f (of R x) = f x

Proof state:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x : X
⊢ ((lift R) f) (of R x) = f x

Tactic:
rw [← @Function.comp_apply _ _ _ (lift R f) (of R) x, of_comp_lift]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_lt_iff_of_nonempty_compact [Nonempty α] [CompactSpace α] {f : α →ᵇ β} {M : ℝ} :
    ‖f‖ < M ↔ ∀ x, ‖f x‖ < M

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 < M ↔ ∀ (x : α), dist (f x) 0 < M

Tactic:
exact dist_lt_iff_of_nonempty_compact

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
simp_rw [norm_def, ← dist_zero_right]

Result:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 < M ↔ ∀ (x : α), dist (f x) 0 < M
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem atLeastTwo_false_mid   : atLeastTwo a false c = (a && c)

Proof state:
a c : Bool
⊢ a.atLeastTwo false c = (a && c)

Tactic:
simp [atLeastTwo]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.even_sub_one {p : ℕ} (hp : p.Prime) (h2 : p ≠ 2) : Even (p - 1) :=
  let ⟨n, hn⟩ := hp.odd_of_ne_two h2; ⟨n, by rw [hn, Nat.add_sub_cancel, two_mul]⟩

Proof state:
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ p - 1 = n + n

Tactic:
rw [hn, Nat.add_sub_cancel, two_mul]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem ftaylorSeriesWithin_insert :
    ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s

Proof state:
case h.h
𝕜 : 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
x y : E
n : ℕ
⊢ ftaylorSeriesWithin 𝕜 f (insert x s) y n = ftaylorSeriesWithin 𝕜 f s y n

Tactic:
apply iteratedFDerivWithin_insert

Result:
no goals

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
x : E
⊢ ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s

Tactic:
ext y n : 2

Result:
case h.h
𝕜 : 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
x y : E
n : ℕ
⊢ ftaylorSeriesWithin 𝕜 f (insert x s) y n = ftaylorSeriesWithin 𝕜 f s y n
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma ΨSq_even (m : ℤ) : W.ΨSq (2 * m) =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) -
      W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.ΨSq (2 * m) =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq

Tactic:
rw [ΨSq, preΨ_even, if_pos <| even_two_mul _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[]

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ { toList := toList✝ }.push a ≠ #[]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
xs : Array α
⊢ xs.push a ≠ #[]

Tactic:
cases xs

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ { toList := toList✝ }.push a ≠ #[]
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem self_eq_nnrealPart_sub_nnrealPart_neg (f : α →ᵇ ℝ) :
    ⇑f = (↑) ∘ f.nnrealPart - (↑) ∘ (-f).nnrealPart

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ f x = f x ⊔ 0 - -f x ⊔ 0

Tactic:
simp only [max_zero_sub_max_neg_zero_eq_self]

Result:
no goals

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ f x = (toReal ∘ ⇑f.nnrealPart - toReal ∘ ⇑(-f).nnrealPart) x

Tactic:
dsimp

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ f x = f x ⊔ 0 - -f x ⊔ 0

Proof state:
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ ⇑f = toReal ∘ ⇑f.nnrealPart - toReal ∘ ⇑(-f).nnrealPart

Tactic:
funext x

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ f x = (toReal ∘ ⇑f.nnrealPart - toReal ∘ ⇑(-f).nnrealPart) x
-- Mathlib/Data/Sum/Interval.lean
lemma Ico_inl_inl :
    Ico (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ico a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ico a₁ a₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_add (c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c'

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ ofScalars E (c + c') = ofScalars E c + ofScalars E c'

Tactic:
unfold ofScalars

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ (fun n => (c + c') n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    (fun n => c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) + fun n =>
      c' n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ (fun n => (c n + c' n) • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) = fun i =>
    c i • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 i E + c' i • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 i E

Tactic:
exact funext fun n ↦ Module.add_smul (c n) (c' n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ (fun n => (c + c') n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    (fun n => c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) + fun n =>
      c' n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E

Tactic:
simp_rw [Pi.add_apply, Pi.add_def _ _]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ (fun n => (c n + c' n) • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) = fun i =>
    c i • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 i E + c' i • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 i E
-- Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean
theorem disjoint_splitCenterBox (I : Box ι) {s t : Set ι} (h : s ≠ t) :
    Disjoint (I.splitCenterBox s : Set (ι → ℝ)) (I.splitCenterBox t)

Proof state:
case intro.h
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t
i : ι
⊢ i ∈ s ↔ i ∈ t

Tactic:
rw [← hs.2, ← ht.2]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(I.splitCenterBox s) ⊓ ↑(I.splitCenterBox t) ≤ ⊥

Tactic:
rintro y ⟨hs, ht⟩

Result:
case intro
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(I.splitCenterBox s)
ht : y ∈ ↑(I.splitCenterBox t)
⊢ y ∈ ⊥

Proof state:
case intro.h
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(I.splitCenterBox s)
ht : y ∈ ↑(I.splitCenterBox t)
i : ι
⊢ i ∈ s ↔ i ∈ t

Tactic:
rw [mem_coe, mem_splitCenterBox] at hs ht

Result:
case intro.h
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t
i : ι
⊢ i ∈ s ↔ i ∈ t

Proof state:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ Disjoint ↑(I.splitCenterBox s) ↑(I.splitCenterBox t)

Tactic:
rw [disjoint_iff_inf_le]

Result:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(I.splitCenterBox s) ⊓ ↑(I.splitCenterBox t) ≤ ⊥

Proof state:
case intro
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(I.splitCenterBox s)
ht : y ∈ ↑(I.splitCenterBox t)
⊢ s = t

Tactic:
ext i

Result:
case intro.h
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(I.splitCenterBox s)
ht : y ∈ ↑(I.splitCenterBox t)
i : ι
⊢ i ∈ s ↔ i ∈ t

Proof state:
case intro
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(I.splitCenterBox s)
ht : y ∈ ↑(I.splitCenterBox t)
⊢ y ∈ ⊥

Tactic:
apply h

Result:
case intro
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(I.splitCenterBox s)
ht : y ∈ ↑(I.splitCenterBox t)
⊢ s = t
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem mem_iSup {ι : Sort*} (p : ι → Submonoid M) {m : M} :
    (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [closure_singleton_le_iff_mem]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]

Result:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive (attr := simp)] lemma mabs_inv (a : α) : |a⁻¹|ₘ = |a|ₘ

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ mabs a⁻¹ = mabs a

Tactic:
simp [mabs, sup_comm]

Result:
no goals