ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ l ∈ tl, ∀ x ∈ l, x ∈ s ∨ x = -1) → C (List.map List.prod tl).sum<VAR>HL : ∀ x ∈ hd, x ∈ s ∨ x = -1<GOAL>C hd.prod
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ x ∈ tl, x ∈ s ∨ x = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : ∀ x ∈ hd :: tl, x ∈ s ∨ x = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ x ∈ tl, x ∈ s ∨ x = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ x ∈ tl, x ∈ s ∨ x = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = L.prod<VAR>hhd : hd ∈ s<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ x ∈ tl, x ∈ s ∨ x = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = L.prod<VAR>hhd : hd = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ x ∈ tl, x ∈ s ∨ x = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = -L.prod<VAR>hhd : hd ∈ s<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ x ∈ tl, x ∈ s ∨ x = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = -L.prod<VAR>hhd : hd = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>θ : Angle<GOAL>Real.tan θ.toReal = θ.tan
<VAR>a : ℝ<GOAL>frontier {z | a < z.re} = {z | z.re = a}
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>h : Fix F → α<VAR>hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)<VAR>x : Fix F<GOAL>rec g x = h x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>h : Fix F → α<VAR>hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)<VAR>x : Fix F<GOAL>∀ (x : F (Fix F)), rec g <$> x = h <$> x → rec g (mk x) = h (mk x)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : F α → α<VAR>h : Fix F → α<VAR>hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)<VAR>x✝ : Fix F<VAR>x : F (Fix F)<VAR>hyp' : rec g <$> x = h <$> x<GOAL>rec g (mk x) = h (mk x)
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c d : ↑S.objs<VAR>p : c ⟶ d<GOAL>↑(inv p) = inv ↑p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀ : ∀ (b : β), Monotone (swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>a : α<VAR>ha : a ∈ lowerBounds s<VAR>b : β<VAR>hb : b ∈ upperBounds t<GOAL>BddBelow (image2 f s t)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasColimits C<VAR>inst✝ : EnoughProjectives C<VAR>G : C<VAR>hG : IsCoseparator G<GOAL>∃ G, Projective G ∧ IsSeparator G
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasColimits C<VAR>inst✝ : EnoughProjectives C<VAR>G : C<VAR>hG : IsCoseparator G<VAR>T : Cᵒᵖ<VAR>hT₁ : Injective T<VAR>hT₂ : IsCoseparator T<GOAL>∃ G, Projective G ∧ IsSeparator G
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₃ : P<VAR>h : ¬Collinear k {p₁, p₁, p₃}<GOAL>False
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹¹ : Fintype m<VAR>inst✝¹⁰ : Fintype m₁<VAR>inst✝⁹ : Fintype m₂<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype n₁<VAR>inst✝⁶ : Fintype n₂<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : DecidableEq m₁<VAR>inst✝³ : DecidableEq m₂<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq n₁<VAR>inst✝ : DecidableEq n₂<VAR>x1 x2 : Matrix m n₁ R<VAR>y1 y2 : Matrix m n₂ R<GOAL>x1.fromColumns y1 = x2.fromColumns y2 → x1 = x2 ∧ y1 = y2
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹¹ : Fintype m<VAR>inst✝¹⁰ : Fintype m₁<VAR>inst✝⁹ : Fintype m₂<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype n₁<VAR>inst✝⁶ : Fintype n₂<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : DecidableEq m₁<VAR>inst✝³ : DecidableEq m₂<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq n₁<VAR>inst✝ : DecidableEq n₂<VAR>x1 x2 : Matrix m n₁ R<VAR>y1 y2 : Matrix m n₂ R<GOAL>(∀ (i : m) (j : n₁ ⊕ n₂), x1.fromColumns y1 i j = x2.fromColumns y2 i j) → (∀ (i : m) (j : n₁), x1 i j = x2 i j) ∧ ∀ (i : m) (j : n₂), y1 i j = y2 i j
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>(QInfty ≫ PInfty).f n = HomologicalComplex.Hom.f 0 n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>(0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>inst✝ : Finite ι<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ (i : ι), ContinuousWithinAt (F i) S x₀
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t c : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>mgf (fun x => c) μ t = rexp (t * c)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₂ F₃ : J ⥤ C<VAR>j : J<GOAL>(α_ F₁ F₂ F₃).inv.app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G : C ⥤ D<VAR>hG : CompatiblePreserving K G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>h : x.Compatible<VAR>Y : C<VAR>f : Y ⟶ Z<VAR>hf : T f<GOAL>(FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure ⋯) fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) = x f hf
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G : C ⥤ D<VAR>hG : CompatiblePreserving K G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>h : x.Compatible<VAR>Y : C<VAR>f : Y ⟶ Z<VAR>hf : T f<VAR>X : C<VAR>g : X ⟶ Z<VAR>f' : G.obj Y ⟶ G.obj X<VAR>hg : T g<VAR>eq : G.map f = f' ≫ G.map g<GOAL>(FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq } fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) = x f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ insert a s ×ˢ t ↔ (x, y) ∈ Prod.mk a '' t ∪ s ×ˢ t
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<GOAL>mk' K x y = 1 ↔ x = ↑y
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<GOAL>mk' K x y = 1 → x = ↑y
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<VAR>hxy : mk' K x y = 1<GOAL>x = ↑y
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<VAR>hxy : mk' K x y = 1<VAR>hy : (algebraMap A K) ↑y ≠ 0<GOAL>x = ↑y
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<VAR>hxy : (algebraMap A K) x = (algebraMap A K) ↑y<VAR>hy : (algebraMap A K) ↑y ≠ 0<GOAL>x = ↑y
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝ : SMul G X<VAR>B : Set X<GOAL>IsBlock G B ↔ ∀ (g g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : HasDerivWithinAt g₁ g₁' t' (h x)<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : MapsTo h s t'<VAR>hy : y = h x<GOAL>HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => ∫⁻ (b : β) in s, f a b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => ∫⁻ (b : β), f a b ∂(κ.restrict hs) a
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ZNum<GOAL>↑n.bitm1 = ↑n + ↑n - 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ZNum<GOAL>↑(- -n).bitm1 = ↑n + ↑n - 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ZNum<GOAL>-(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ZNum<VAR>this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)<GOAL>-(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<GOAL>φ.nilRank ≤ Fintype.card ι
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<GOAL>(φ.polyCharpoly (chooseBasis R L)).coeff (Fintype.card ι) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<GOAL>1 ≠ 0
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>p : ℕ<VAR>f : ℕ → α<VAR>h : Prime p<GOAL>∏ x ∈ p.properDivisors, f x = f 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Add α<VAR>b c d : WithTop α<VAR>x y : α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < c<VAR>a : α<GOAL>↑a + b < ↑a + c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Add α<VAR>c d : WithTop α<VAR>x y : α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h' h : ↑b < c<GOAL>↑a + ↑b < ↑a + c
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Semiring R<VAR>p q r✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<VAR>r : R<GOAL>((X + C r) ^ n).natDegree = n
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Mul α<VAR>a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α<VAR>i j : Fin 3<GOAL>(!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃]) i j = !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃; a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃; a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃] i j
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>(univ.pi t).Nonempty ↔ ∀ (i : ι), (t i).Nonempty
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieRing L<VAR>inst✝³ : LieAlgebra R L<VAR>inst✝² : LieAlgebra K L<VAR>L' : Type u_5<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x y : L<GOAL>((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w x : Fin 3 → R<GOAL>(crossProduct u) v ⬝ᵥ (crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w x : Fin 3 → R<GOAL>![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 0 + ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 1 + ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 2 = (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) - (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.34532, u_2} D<VAR>inst✝¹ : Category.{?u.34536, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : HasPullback π π<GOAL>MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ = equalizer.lift (P.map π.op) ⋯ ≫ (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.34532, u_2} D<VAR>inst✝¹ : Category.{?u.34536, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : HasPullback π π<GOAL>MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫ (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv = equalizer.lift (P.map π.op) ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.34532, u_2} D<VAR>inst✝¹ : Category.{?u.34536, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : HasPullback π π<GOAL>(MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫ (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv) ≫ equalizer.ι (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op) = equalizer.lift (P.map π.op) ⋯ ≫ equalizer.ι (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c : α<VAR>h : IsUnit b<VAR>a : α<GOAL>a * b / b = a
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<GOAL>mapIdx f l = map (uncurry f) l.enum
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<GOAL>List.oldMapIdx f l = map (uncurry f) l.enum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<GOAL>a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<GOAL>h = ↑(coroot α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<GOAL>h = ↑(coroot α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<GOAL>↑h = ↑(coroot α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<GOAL>h = coroot α