ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>S : Set G<VAR>inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>hG : 0 < Fintype.card G<VAR>a : G<VAR>ha : a ∈ S<VAR>key : ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t], (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t<VAR>mono : Monotone fun n => Fintype.card ↑(S ^ n)<VAR>n : ℕ<VAR>h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))<VAR>h₂ : S ^ n * {a} = S ^ (n + 1)<VAR>x : G<VAR>hx : x ∈ S ^ (n + 1)<GOAL>x * a * a⁻¹ ∈ S ^ (n + 1)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>m : M<GOAL>(m, 0) ∈ fst R M M₂
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>∀ (x y : ↥(fst R M M₂)), (fun x => (↑x).1) (x + y) = (fun x => (↑x).1) x + (fun x => (↑x).1) y
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>∀ (m : R) (x : ↥(fst R M M₂)), { toFun := fun x => (↑x).1, map_add' := ⋯ }.toFun (m • x) = (RingHom.id R) m • { toFun := fun x => (↑x).1, map_add' := ⋯ }.toFun x
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<VAR>y : M₂<VAR>hy : (x, y) ∈ fst R M M₂<GOAL>(fun m => ⟨(m, 0), ⋯⟩) ({ toFun := fun x => (↑x).1, map_add' := ⋯, map_smul' := ⋯ }.toFun ⟨(x, y), hy⟩) = ⟨(x, y), hy⟩
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<VAR>y : M₂<VAR>hy✝ : (x, y) ∈ fst R M M₂<VAR>hy : y = 0<GOAL>(fun m => ⟨(m, 0), ⋯⟩) ({ toFun := fun x => (↑x).1, map_add' := ⋯, map_smul' := ⋯ }.toFun ⟨(x, y), hy✝⟩) = ⟨(x, y), hy✝⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>LiftRel (fun x x_1 => x = x_1) s.think s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²² : Semiring R₁<VAR>inst✝²¹ : Semiring R₂<VAR>inst✝²⁰ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁹ : TopologicalSpace M₁<VAR>inst✝¹⁸ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁷ : TopologicalSpace M'₁<VAR>inst✝¹⁶ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace M₂<VAR>inst✝¹⁴ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹³ : TopologicalSpace M₃<VAR>inst✝¹² : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹¹ : TopologicalSpace M₄<VAR>inst✝¹⁰ : AddCommMonoid M₄<VAR>inst✝⁹ : Module R₁ M₁<VAR>inst✝⁸ : Module R₁ M'₁<VAR>inst✝⁷ : Module R₂ M₂<VAR>inst✝⁶ : Module R₃ M₃<VAR>inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>F : Type u_9<VAR>inst✝⁴ : Module R₁ M₂<VAR>inst✝³ : TopologicalSpace R₁<VAR>inst✝² : ContinuousSMul R₁ M₂<VAR>inst✝¹ : ContinuousSMul R₁ M₁<VAR>inst✝ : ContinuousAdd M₁<VAR>x y : M₁<GOAL>(toSpanSingleton R₁ (x + y)) 1 = (toSpanSingleton R₁ x + toSpanSingleton R₁ y) 1
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : toNat (Module.rank R M) = toNat ↑n<GOAL>finrank R M = n
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : toNat (Module.rank R M) = n<GOAL>finrank R M = n
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>φ : (n : ℕ) × L.BoundedFormula α n<GOAL>(fun l => (listDecode l)[0]?) ((fun φ => φ.snd.listEncode) φ) = some φ
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>φ : (n : ℕ) × L.BoundedFormula α n<VAR>h : listDecode ([φ].bind fun φ => φ.snd.listEncode) = [φ]<GOAL>(fun l => (listDecode l)[0]?) ((fun φ => φ.snd.listEncode) φ) = some φ
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>φ : (n : ℕ) × L.BoundedFormula α n<VAR>h : listDecode φ.snd.listEncode = [φ]<GOAL>(fun l => (listDecode l)[0]?) ((fun φ => φ.snd.listEncode) φ) = some φ
<VAR>n m : ℕ<GOAL>n.succ * m = 0 → n.succ = 0 ∨ m = 0
<VAR>n m : ℕ<GOAL>n * m + m = 0 → n.succ = 0 ∨ m = 0
<VAR>n m : ℕ<VAR>h : n * m + m = 0<GOAL>n.succ = 0 ∨ m = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : AffineSubspace k P<GOAL>affineSpan k ↑s = s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : AffineSubspace k P<GOAL>affineSpan k ↑s ≤ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : AffineSubspace k P<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s<VAR>v : V<VAR>hv : v ∈ vectorSpan k ↑s<GOAL>v +ᵥ p1 ∈ ↑s
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>h : N ↪[L] P<VAR>f g : M ↪[L] N<VAR>hfg : h.comp f = h.comp g<VAR>x : M<GOAL>f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CompactSpace α<VAR>inst✝² : MetricSpace β<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>inst✝ : Nonempty α<GOAL>dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>L R : ListBlank Γ<GOAL>(Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons R.head L) R.tail
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>L R : ListBlank Γ<GOAL>∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>L R : ListBlank Γ<VAR>L✝ : Tape Bool<VAR>i : ℕ<VAR>IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝<GOAL>(Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L✝) = L✝
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hc : p.IsPath<VAR>h : u ∈ p.support<GOAL>((p.takeUntil u h).append (p.dropUntil u h)).IsPath
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Mod α<VAR>a b : α<GOAL>some a % some b = some (a % b)
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>𝓝 0 = ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>n : ℤ<GOAL>Tendsto floor (𝓝[≥] ↑n) (pure n)
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>hn : n ≤ sInf {m | p m}<GOAL>sInf {m | p (m + n)} + n = sInf {m | p m}
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>hn : n ≤ sInf {m | p m}<VAR>h : {m | p (m + n)} = ∅<GOAL>sInf {m | p (m + n)} + n = sInf {m | p m}
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>hn : n ≤ sInf {m | p m}<VAR>m : ℕ<VAR>hm : m ∈ {m | p (m + n)}<GOAL>sInf {m | p (m + n)} + n = sInf {m | p m}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Icc a b = Icc (e.symm a) (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>e : α ≃ β<GOAL>⇑e '' univ = univ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = ↑π ↔ Collinear ℝ {p₁, p₂, p₃}
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>a : (P F).A<VAR>f : (P F).B a → (P F).W<GOAL>mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦WType.mk a f⟧
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>a : (P F).A<VAR>f : (P F).B a → (P F).W<VAR>this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧<GOAL>mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦WType.mk a f⟧
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>a : (P F).A<VAR>f : (P F).B a → (P F).W<VAR>this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧<GOAL>Setoid.r (Wrepr (WType.mk a f)) (WType.mk a f)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>|x - ↑(round x)| ≤ 1 / 2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>this : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2<GOAL>x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2<VAR>this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1<GOAL>x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s✝ t : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>s : Finset α<VAR>hs : G.IsClique ↑s<VAR>ht : (map f s).Nontrivial<GOAL>(SimpleGraph.map f G).IsClique ↑(map f s)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ : 0 ≤ δ<VAR>hscard : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>htcard : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ : 0 ≤ δ<VAR>hscard : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>htcard : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>h : δ < 1<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ : 0 ≤ δ<VAR>hscard : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>htcard : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>h : 1 ≤ δ<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ : 0 ≤ δ<VAR>hscard : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>htcard : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>h : 1 ≤ δ<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ δ + δ
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>p : CommSq f g h i<GOAL>i.op ≫ g.op = h.op ≫ f.op
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>inst✝ : Monoid H<VAR>f : G →* H<VAR>x : G<VAR>h : IsOfFinOrder x<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : x ^ n = 1<GOAL>∃ n, 0 < n ∧ f x ^ n = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι ι' : Type u<VAR>r : ι → ι → Prop<VAR>r' : ι' → ι' → Prop<VAR>inst✝¹ : IsWellOrder ι r<VAR>inst✝ : IsWellOrder ι' r'<VAR>o : Ordinal.{u}<VAR>ho : type r = o<VAR>ho' : type r' = o<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>i : ι<GOAL>familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι ι' : Type u<VAR>r : ι → ι → Prop<VAR>r' : ι' → ι' → Prop<VAR>inst✝¹ : IsWellOrder ι r<VAR>inst✝ : IsWellOrder ι' r'<VAR>o : Ordinal.{u}<VAR>ho : type r = o<VAR>ho' : type r' = o<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>i : ι<VAR>j : ι'<VAR>hj : typein r' j = typein r i<GOAL>familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι ι' : Type u<VAR>r : ι → ι → Prop<VAR>r' : ι' → ι' → Prop<VAR>inst✝¹ : IsWellOrder ι r<VAR>inst✝ : IsWellOrder ι' r'<VAR>o : Ordinal.{u}<VAR>ho : type r = o<VAR>ho' : type r' = o<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>i : ι<VAR>j : ι'<VAR>hj : typein r' j = typein r i<GOAL>f (typein r' j) ⋯ ≤ sup (familyOfBFamily' r' ho' f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<VAR>has : a ∉ s<GOAL>(insert a s).encard = s.encard + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>n : ℕ<VAR>h : 1 < n<GOAL>(fun x => x ^ n) =o[𝓝 0] fun x => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>n : ℕ<VAR>h : 1 < n<VAR>x✝ : 𝕜<GOAL>x✝ = x✝ ^ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>S : Set (Set H)<GOAL>(⋃₀ S).innerDualCone = sInf (innerDualCone '' S)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝¹ : Category.{max v u, w} D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x✝ : (J.Cover X)ᵒᵖ<GOAL>(J.diagramNatTrans (𝟙 P) X).app x✝ = (𝟙 (J.diagram P X)).app x✝
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝¹ : Category.{max v u, w} D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x✝ : (J.Cover X)ᵒᵖ<VAR>i : ((unop x✝).index P).L<GOAL>(J.diagramNatTrans (𝟙 P) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i = (𝟙 (J.diagram P X)).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝¹ : Category.{max v u, w} D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x✝ : (J.Cover X)ᵒᵖ<VAR>i : ((unop x✝).index P).L<GOAL>Multiequalizer.lift ((unop x✝).index P) (multiequalizer ((unop x✝).index P)) (fun i => Multiequalizer.ι ((unop x✝).index P) i ≫ 𝟙 (P.obj (op i.Y))) ⋯ ≫ Multiequalizer.ι ((unop x✝).index P) i = 𝟙 (multiequalizer ((unop x✝).index P)) ≫ Multiequalizer.ι ((unop x✝).index P) i
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝¹ : Category.{max v u, w} D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x✝ : (J.Cover X)ᵒᵖ<VAR>i : ((unop x✝).index P).L<GOAL>Multiequalizer.ι ((unop x✝).index P) i ≫ 𝟙 (P.obj (op i.Y)) = Multiequalizer.ι ((unop x✝).index P) i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)<VAR>xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)<VAR>xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0<VAR>hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)<VAR>xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0<VAR>hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)<VAR>xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0<VAR>hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)<VAR>xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0<VAR>hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)<VAR>xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0<VAR>hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y = iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!