ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>p1 p2 p3 : P<GOAL>‖p1 -ᵥ p3‖ * ‖p1 -ᵥ p3‖ = ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + ‖p3 -ᵥ p2‖ * ‖p3 -ᵥ p2‖ - 2 * ‖p1 -ᵥ p2‖ * ‖p3 -ᵥ p2‖ * Real.cos (∠ p1 p2 p3)
<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>p1 p2 p3 : P<GOAL>‖p1 -ᵥ p3‖ * ‖p1 -ᵥ p3‖ = ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + ‖p3 -ᵥ p2‖ * ‖p3 -ᵥ p2‖ - 2 * ‖p1 -ᵥ p2‖ * ‖p3 -ᵥ p2‖ * Real.cos (InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2))
<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>p1 p2 p3 : P<GOAL>p1 -ᵥ p3 = p1 -ᵥ p2 - (p3 -ᵥ p2)
<VAR>θ : Angle<VAR>hpi : ¬θ = ↑π<GOAL>(2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2
<VAR>θ : Angle<VAR>hpi : ¬θ = ↑π<GOAL>(2 • θ).sign = θ.sign ↔ |θ.toReal| < π / 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type w<VAR>f : ι → Filter α<VAR>m : α → β<VAR>p : ι → Prop<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}<VAR>ne : ∃ i, p i<GOAL>map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type w<VAR>f : ι → Filter α<VAR>m : α → β<VAR>p : ι → Prop<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}<VAR>ne : ∃ i, p i<VAR>this : Nonempty (Subtype p)<GOAL>map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type w<VAR>f : ι → Filter α<VAR>m : α → β<VAR>p : ι → Prop<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}<VAR>ne : ∃ i, p i<VAR>this : Nonempty (Subtype p)<GOAL>map m (⨅ x, f ↑x) = ⨅ x, map m (f ↑x)
<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>inst✝ : AffineSpace V P<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<GOAL>Set.range (s.face h).points = s.points '' ↑fs
<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>S✝ S : L.Substructure M<VAR>x : M<GOAL>x ∈ S.subtype.toHom.range ↔ x ∈ S
<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>S✝ S : L.Substructure M<VAR>x : M<GOAL>(∃ y, ↑y = x) ↔ x ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>b : β<VAR>x : α<GOAL>x ∈ ⇑e ⁻¹' Ioi b ↔ x ∈ Ioi (e.symm b)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsSubgroup s<GOAL>1 ∈ f ⁻¹' s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsSubgroup s<GOAL>∀ {a b : G}, a ∈ f ⁻¹' s → b ∈ f ⁻¹' s → a * b ∈ f ⁻¹' s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsSubgroup s<GOAL>∀ {a : G}, a ∈ f ⁻¹' s → a⁻¹ ∈ f ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X : PartialFun<VAR>a : (partialFunToPointed ⋙ pointedToPartialFun).obj X<GOAL>(fun a => ⟨some a, ⋯⟩) ((fun a => Option.get ↑a ⋯) a) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X✝ Y✝ : PartialFun<VAR>f : X✝ ⟶ Y✝<VAR>a : (𝟭 PartialFun).obj X✝<VAR>b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝<GOAL>(b ∈ (f a).bind fun x => Part.some ⟨some x, ⋯⟩) ↔ b ∈ (Part.some ⟨some a, ⋯⟩).bind (PFun.toSubtype (fun x => ¬x = none) (Option.elim' none fun a => (f a).toOption) ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X✝ Y✝ : PartialFun<VAR>f : X✝ ⟶ Y✝<VAR>a : (𝟭 PartialFun).obj X✝<VAR>b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝<GOAL>(b ∈ (f a).bind fun x => Part.some ⟨some x, ⋯⟩) ↔ b ∈ (PFun.toSubtype (fun x => ¬x = none) (Option.elim' none fun a => (f a).toOption) ∘ Subtype.val) ⟨some a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X✝ Y✝ : PartialFun<VAR>f : X✝ ⟶ Y✝<VAR>a : (𝟭 PartialFun).obj X✝<VAR>b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝<GOAL>(∃ a_1 ∈ f a, b ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑b = Option.elim' none (fun a => (f a).toOption) ↑⟨some a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X Y : Pointed<VAR>f : X ⟶ Y<VAR>a : X.X<VAR>ha : a ≠ X.point<GOAL>((pointedToPartialFun ⋙ partialFunToPointed).map f ≫ ((fun X => Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) Y).hom).toFun (some ⟨a, ha⟩) = (((fun X => Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) X).hom ≫ (𝟭 Pointed).map f).toFun (some ⟨a, ha⟩)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R w y z<VAR>h₂ : Sbtw R w x y<GOAL>Sbtw R w x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R w y z<VAR>h₂ : Sbtw R w x y<GOAL>x ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>w x y : P<VAR>h₂ : Sbtw R w x y<VAR>h₁ : Wbtw R w y x<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁴ : DistribLattice α<VAR>inst✝³ : OrderBot α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidablePred SupIrred<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet (a ⊔ b)) = Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a) ∪ Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet b)
<VAR>α : Type u_1<VAR>inst✝⁴ : DistribLattice α<VAR>inst✝³ : OrderBot α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidablePred SupIrred<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>Fintype.finsetOrderIsoSet.symm (birkhoffSet a ∪ birkhoffSet b) = Fintype.finsetOrderIsoSet.symm (birkhoffSet a) ∪ Fintype.finsetOrderIsoSet.symm (birkhoffSet b)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>x y : OnePoint X<GOAL>Inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x', x = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<GOAL>∃ I J, M.Basis I X ∧ M.Basis J Y ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>I : Set α<VAR>hI : M.Basis I X<GOAL>∃ I J, M.Basis I X ∧ M.Basis J Y ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J✝ X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>I : Set α<VAR>hI : M.Basis I X<VAR>J : Set α<VAR>hJ : M.Basis J Y<VAR>hIJ : I ⊆ J<GOAL>∃ I J, M.Basis I X ∧ M.Basis J Y ∧ I ⊆ J
<VAR>k : ℕ<VAR>c : Code<VAR>n x : ℕ<VAR>h : x ∈ evaln (k + 1) c n<GOAL>∀ {o : Option ℕ}, (x ∈ do guard (n ≤ k) o) → n < k + 1
<VAR>R M : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>x : ι → M<GOAL>IsTrivialRelation f x ↔ VanishesTrivially R f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p a ≠ multiplicity p b<GOAL>multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p a ≠ multiplicity p b<VAR>hab : multiplicity p a < multiplicity p b<GOAL>multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p a ≠ multiplicity p b<VAR>hab : multiplicity p a = multiplicity p b<GOAL>multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p a ≠ multiplicity p b<VAR>hab : multiplicity p b < multiplicity p a<GOAL>multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>i✝ : (i : o) × m' i<VAR>j✝ : (i : o) × n' i<GOAL>blockDiagonal' 0 i✝ j✝ = 0 i✝ j✝
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<VAR>a : R<GOAL>eval a (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>s : Set α<VAR>hf : UniformInducing f<GOAL>TotallyBounded (f '' s) ↔ TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>s : Set α<VAR>hf : UniformInducing f<VAR>hs : TotallyBounded (f '' s)<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>s : Set α<VAR>hf : UniformInducing f<VAR>hs : TotallyBounded (f '' s)<GOAL>∀ i ∈ 𝓤 β, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ Prod.map f f ⁻¹' id i}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>s : Set α<VAR>hf : UniformInducing f<VAR>hs : TotallyBounded (f '' s)<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<GOAL>∃ t_1, t_1.Finite ∧ s ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>s : Set α<VAR>hf : UniformInducing f<VAR>hs : TotallyBounded (f '' s)<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>u : Set α<VAR>hfin : u.Finite<VAR>h : f '' s ⊆ ⋃ y ∈ f '' u, {x | (x, y) ∈ t}<GOAL>∃ t_1, t_1.Finite ∧ s ⊆ ⋃ y ∈ t_1, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>s : Set α<VAR>hf : UniformInducing f<VAR>hs : TotallyBounded (f '' s)<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>u : Set α<VAR>hfin : u.Finite<VAR>h : f '' s ⊆ ⋃ y ∈ f '' u, {x | (x, y) ∈ t}<GOAL>s ⊆ ⋃ y ∈ u, {x | (x, y) ∈ Prod.map f f ⁻¹' id t}
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>α✝ : Type w<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>α : Type w<GOAL>HasColimitsOfShape (Discrete α) C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).card + (s ∪ t).card = s.card + t.card
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Div G<VAR>m : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>β : Type u_4<VAR>inst✝⁴ : CanonicallyOrderedAddCommMonoid β<VAR>inst✝³ : Sub β<VAR>inst✝² : OrderedSub β<VAR>x✝ : MeasurableSpace β<VAR>inst✝¹ : MeasurableSub₂ β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasurableSet {x | f x = g x}
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Div G<VAR>m : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>β : Type u_4<VAR>inst✝⁴ : CanonicallyOrderedAddCommMonoid β<VAR>inst✝³ : Sub β<VAR>inst✝² : OrderedSub β<VAR>x✝ : MeasurableSpace β<VAR>inst✝¹ : MeasurableSub₂ β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>this : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}<GOAL>MeasurableSet {x | f x = g x}
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Div G<VAR>m : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>β : Type u_4<VAR>inst✝⁴ : CanonicallyOrderedAddCommMonoid β<VAR>inst✝³ : Sub β<VAR>inst✝² : OrderedSub β<VAR>x✝ : MeasurableSpace β<VAR>inst✝¹ : MeasurableSub₂ β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>this : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}<GOAL>MeasurableSet ({a | (f - g) a = 0} ∩ {a | (g - f) a = 0})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>inst✝ : DecidableEq α<VAR>hd : α<VAR>tl : List α<VAR>m : α<VAR>hm : m ∈ argmax f (hd :: tl)<VAR>a : α<VAR>ha : a ∈ hd :: tl<VAR>ham : f m ≤ f a<GOAL>indexOf m (hd :: tl) ≤ indexOf a (hd :: tl)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>inst✝ : DecidableEq α<VAR>hd : α<VAR>tl : List α<VAR>m a : α<VAR>ha : a ∈ hd :: tl<VAR>ham : f m ≤ f a<VAR>hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m<GOAL>(bif hd == m then 0 else indexOf m tl + 1) ≤ bif hd == a then 0 else indexOf a tl + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>inst✝ : DecidableEq α<VAR>hd : α<VAR>tl : List α<VAR>m a : α<VAR>ha : a ∈ hd :: tl<VAR>ham : f m ≤ f a<VAR>val✝ : α<VAR>hm : (if f hd < f val✝ then some val✝ else some hd) = some m<VAR>h : argmax f tl = some val✝<GOAL>(bif hd == m then 0 else indexOf m tl + 1) ≤ bif hd == a then 0 else indexOf a tl + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>inst✝ : DecidableEq α<VAR>hd : α<VAR>tl : List α<VAR>m a : α<VAR>ha : a ∈ hd :: tl<VAR>ham : f m ≤ f a<VAR>val✝ : α<VAR>hm : (if f hd < f val✝ then some val✝ else some hd) = some m<VAR>h : argmax f tl = some val✝<GOAL>(if hd = m then 0 else indexOf m tl + 1) ≤ if hd = a then 0 else indexOf a tl + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a d₁ : α<VAR>t₁ : List α<VAR>ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁<VAR>h : a ∈ d₁ :: t₁<GOAL>indexOf a (d₁ :: t₁ ++ l₂) = indexOf a (d₁ :: t₁)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a d₁ : α<VAR>t₁ : List α<VAR>ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁<VAR>h : a ∈ d₁ :: t₁<GOAL>indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a d₁ : α<VAR>t₁ : List α<VAR>ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁<VAR>h : a ∈ d₁ :: t₁<VAR>hh : ¬d₁ = a<GOAL>indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x✝ : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hg : ∀ (n : α), Differentiable 𝕜 (g n)<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n<VAR>hg0 : Summable fun n => g n y₀<VAR>x : 𝕜<GOAL>deriv (fun y => ∑' (n : α), g n y) x = ∑' (n : α), deriv (g n) x
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<GOAL>∃ a, (f.val.app (op U)) a = t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<VAR>V_cover : U ≤ iSup V<GOAL>∃ a, (f.val.app (op U)) a = t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<VAR>V_cover : U ≤ iSup V<VAR>x y : ↥U<GOAL>(F.val.map ((V x).infLELeft (V y)).op) (sf x) = (F.val.map ((V x).infLERight (V y)).op) (sf y)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<VAR>V_cover : U ≤ iSup V<VAR>x y : ↥U<GOAL>∀ (x_1 : ↥(V x ⊓ V y)), (F.presheaf.germ x_1) ((F.val.map ((V x).infLELeft (V y)).op) (sf x)) = (F.presheaf.germ x_1) ((F.val.map ((V x).infLERight (V y)).op) (sf y))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<VAR>V_cover : U ≤ iSup V<VAR>x y : ↥U<VAR>z : ↥(V x ⊓ V y)<GOAL>(F.presheaf.germ z) ((F.val.map ((V x).infLELeft (V y)).op) (sf x)) = (F.presheaf.germ z) ((F.val.map ((V x).infLERight (V y)).op) (sf y))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<VAR>V_cover : U ≤ iSup V<VAR>x y : ↥U<VAR>z : ↥(V x ⊓ V y)<GOAL>((stalkFunctor C ↑⟨↑z, ⋯⟩).map f.val) ((F.presheaf.germ z) ((F.val.map ((V x).infLELeft (V y)).op) (sf x))) = ((stalkFunctor C ↑⟨↑z, ⋯⟩).map f.val) ((F.presheaf.germ z) ((F.val.map ((V x).infLERight (V y)).op) (sf y)))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<VAR>V_cover : U ≤ iSup V<VAR>x y : ↥U<VAR>z : ↥(V x ⊓ V y)<GOAL>(germ G.val z) ((f.val.app (op (V x ⊓ V y))) ((F.val.map ((V x).infLELeft (V y)).op) (sf x))) = (germ G.val z) ((f.val.app (op (V x ⊓ V y))) ((F.val.map ((V x).infLERight (V y)).op) (sf y)))