ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>x✝ : Cᵒᵖ<GOAL>(F.map (⊤.toMultiequalizer P) ≫ (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤)) ≫ colimit.ι (J.diagram (P ⋙ F) (unop x✝)) (op ⊤) = ⊤.toMultiequalizer (P ⋙ F) ≫ colimit.ι (J.diagram (P ⋙ F) (unop x✝)) (op ⊤)
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>x✝ : Cᵒᵖ<GOAL>F.map (⊤.toMultiequalizer P) ≫ (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤) = ⊤.toMultiequalizer (P ⋙ F)
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>x✝ : Cᵒᵖ<GOAL>∀ (a : ((unop (op ⊤)).index (P ⋙ F)).L), (F.map (⊤.toMultiequalizer P) ≫ (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤)) ≫ Multiequalizer.ι ((unop (op ⊤)).index (P ⋙ F)) a = ⊤.toMultiequalizer (P ⋙ F) ≫ Multiequalizer.ι ((unop (op ⊤)).index (P ⋙ F)) a
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>x✝ : Cᵒᵖ<VAR>a : ((unop (op ⊤)).index (P ⋙ F)).L<GOAL>(F.map (⊤.toMultiequalizer P) ≫ (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤)) ≫ Multiequalizer.ι ((unop (op ⊤)).index (P ⋙ F)) a = ⊤.toMultiequalizer (P ⋙ F) ≫ Multiequalizer.ι ((unop (op ⊤)).index (P ⋙ F)) a
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>x✝ : Cᵒᵖ<VAR>a : ((unop (op ⊤)).index (P ⋙ F)).L<GOAL>F.map (⊤.toMultiequalizer P ≫ Multiequalizer.ι ((unop (op ⊤)).index P) a) = ⊤.toMultiequalizer (P ⋙ F) ≫ Multiequalizer.ι ((unop (op ⊤)).index (P ⋙ F)) a
<VAR>α : Type u_1<VAR>inst✝¹ : OrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>x : ↑(Icc 0 1)<GOAL>1 - ↑x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → Set (Set α)<VAR>s : Set β<VAR>h_pi : ∀ b ∈ s, IsPiSystem (g b)<VAR>t : Set α<VAR>h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)<GOAL>∃ T f, ↑T ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → Set (Set α)<VAR>s : Set β<VAR>h_pi : ∀ b ∈ s, IsPiSystem (g b)<VAR>t : Set α<VAR>h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)<VAR>this : t ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)<GOAL>∃ T f, ↑T ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → Set (Set α)<VAR>s : Set β<VAR>h_pi : ∀ b ∈ s, IsPiSystem (g b)<VAR>T : Finset (Subtype s)<VAR>f : Subtype s → Set α<VAR>h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b<VAR>h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)<VAR>this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)<GOAL>∃ T_1 f_1, ↑T_1 ⊆ s ∧ ⋂ b ∈ T, f b = ⋂ b ∈ T_1, f_1 b ∧ ∀ b ∈ T_1, f_1 b ∈ g b
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>h0 : p * q ≠ 0<GOAL>(p * q).primPart = p.primPart * q.primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>h0 : ¬C (p * q).content = 0<GOAL>(p * q).primPart = p.primPart * q.primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>h0 : ¬C (p * q).content = 0<GOAL>C (p * q).content * (p * q).primPart = C (p * q).content * (p.primPart * q.primPart)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>h0 : ¬C (p * q).content = 0<GOAL>C p.content * p.primPart * (C q.content * q.primPart) = C (p * q).content * (p.primPart * q.primPart)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>h0 : ¬C (p * q).content = 0<GOAL>C p.content * p.primPart * (C q.content * q.primPart) = C p.content * C q.content * (p.primPart * q.primPart)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>Z X : C<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<GOAL>∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>Z X : C<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>Y' : C<VAR>f' : (shiftFunctor C 1).obj X ⟶ Y'<VAR>g' : Y' ⟶ (shiftFunctor C 1).obj Z<VAR>mem : Triangle.mk h f' g' ∈ distinguishedTriangles<GOAL>∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>Z X : C<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>Y' : C<VAR>f' : (shiftFunctor C 1).obj X ⟶ Y'<VAR>g' : Y' ⟶ (shiftFunctor C 1).obj Z<VAR>mem : Triangle.mk h f' g' ∈ distinguishedTriangles<VAR>T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate<GOAL>∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>Z X : C<VAR>h : Z ⟶ (shiftFunctor C 1).obj X<VAR>Y' : C<VAR>f' : (shiftFunctor C 1).obj X ⟶ Y'<VAR>g' : Y' ⟶ (shiftFunctor C 1).obj Z<VAR>mem : Triangle.mk h f' g' ∈ distinguishedTriangles<VAR>T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate<GOAL>Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h ≅ (Triangle.mk h f' g').invRotate.invRotate
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<VAR>b : β<GOAL>b ∈ (p.bind f).support ↔ b ∈ ⋃ a ∈ p.support, (f a).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x y : β<GOAL>(const x - const y).LimZero ↔ x = y
<VAR>n : ℕ<GOAL>IsCyclic (QuaternionGroup 1)
<VAR>n : ℕ<GOAL>orderOf ?x = Fintype.card (QuaternionGroup 1)
<VAR>n : ℕ<GOAL>QuaternionGroup 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : Subsingleton α<VAR>a b : α<GOAL>b ∈ {a} ↔ b ∈ univ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<VAR>x : E × F<GOAL>x ∈ ↑(v.prod w).parallelepiped ↔ x ∈ ↑(v.parallelepiped.prod w.parallelepiped)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<VAR>x : E × F<GOAL>(∃ t ∈ Icc 0 1, x = ∑ i : ι ⊕ ι', t i • (v.prod w) i) ↔ (∃ t ∈ Icc 0 1, x.1 = ∑ i : ι, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i : ι', t i • w i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<VAR>x : E × F<VAR>t : ι → ℝ<VAR>ht1 : t ∈ Icc 0 1<VAR>ht2 : x.1 = ∑ i : ι, t i • v i<VAR>s : ι' → ℝ<VAR>hs1 : s ∈ Icc 0 1<VAR>hs2 : x.2 = ∑ i : ι', s i • w i<GOAL>∃ t ∈ Icc 0 1, x = ∑ i : ι ⊕ ι', t i • (v.prod w) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<VAR>x : E × F<VAR>t : ι → ℝ<VAR>ht1 : t ∈ Icc 0 1<VAR>ht2 : x.1 = ∑ i : ι, t i • v i<VAR>s : ι' → ℝ<VAR>hs1 : s ∈ Icc 0 1<VAR>hs2 : x.2 = ∑ i : ι', s i • w i<GOAL>Sum.elim t s ∈ Icc 0 1 ∧ x = ∑ i : ι ⊕ ι', Sum.elim t s i • (v.prod w) i
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(contractLeft d) ((contractLeft d') x) = -(contractLeft d') ((contractLeft d) x)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>r : R<GOAL>(contractLeft d) ((contractLeft d') ((algebraMap R (CliffordAlgebra Q)) r)) = -(contractLeft d') ((contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r))
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x y : CliffordAlgebra Q<VAR>hx : (contractLeft d) ((contractLeft d') x) = -(contractLeft d') ((contractLeft d) x)<VAR>hy : (contractLeft d) ((contractLeft d') y) = -(contractLeft d') ((contractLeft d) y)<GOAL>(contractLeft d) ((contractLeft d') (x + y)) = -(contractLeft d') ((contractLeft d) (x + y))
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>m : CliffordAlgebra Q<VAR>x : M<VAR>hx : (contractLeft d) ((contractLeft d') m) = -(contractLeft d') ((contractLeft d) m)<GOAL>(contractLeft d) ((contractLeft d') ((ι Q) x * m)) = -(contractLeft d') ((contractLeft d) ((ι Q) x * m))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>filter (fun x => p x.1) (s ×ˢ t) = filter p s ×ˢ t
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>B : Matrix m n R<VAR>hA : IsUnit A.det<GOAL>(B * A).rank = B.rank
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>B : Matrix m n R<VAR>hA : IsUnit A.det<GOAL>Function.Surjective ⇑A.mulVecLin
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>B : Matrix m n R<VAR>hA : IsUnit A.det<VAR>v : n → R<GOAL>∃ a, A.mulVecLin a = v
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : Preorder M<VAR>inst✝² : Preorder β<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>f : β → M<VAR>n✝ : ℕ<VAR>hf : StrictMono f<VAR>n : ℕ<VAR>x✝ : n.succ.succ ≠ 0<GOAL>StrictMono fun x => f x ^ n.succ.succ
<VAR>a✝ b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : IsNat b nb<VAR>pe' : IsInt (a ^ nb) (Int.negOfNat ne)<GOAL>IsInt (a ^ b) (Int.negOfNat ne)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<GOAL>∏ i ∈ n.divisors, cyclotomic' i K = X ^ n - 1
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<GOAL>slope f a b = slope f b a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Monoid R<VAR>inst✝¹ : NonUnitalNonAssocSemiring A<VAR>inst✝ : DistribMulAction R A<VAR>r₁ r₂ : R<GOAL>0 = r₁ • 0 + r₂ • 0 + 0 * 0
<VAR>α : Type u<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ExistsMulOfLE α<VAR>a b : α<VAR>h : a < b<GOAL>∃ c, 1 < c ∧ a * c = b
<VAR>α : Type u<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ExistsMulOfLE α<VAR>a c : α<VAR>h : a < a * c<GOAL>∃ c_1, 1 < c_1 ∧ a * c_1 = a * c
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>val✝¹ : X<VAR>val✝ : Y<GOAL>glueDist Ψ Φ ε (Sum.inl val✝¹).swap (Sum.inr val✝).swap = glueDist Φ Ψ ε (Sum.inl val✝¹) (Sum.inr val✝)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>val✝¹ : Y<VAR>val✝ : X<GOAL>glueDist Ψ Φ ε (Sum.inr val✝¹).swap (Sum.inl val✝).swap = glueDist Φ Ψ ε (Sum.inr val✝¹) (Sum.inl val✝)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>(map φ P).toPoly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>C (φ P.a) * (Multiset.map (fun a => X - C a) {x, y, z}).prod = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>x y : α<VAR>hne : x ≠ y<GOAL>{x, y}.encard = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u✝ u : Finset α<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : 𝒜 ⊆ u.powerset<VAR>hℬ : ℬ ⊆ u.powerset<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f g μ : Finset α → β<VAR>s t u : Finset α<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : 𝒜 ⊆ ∅.powerset<VAR>hℬ : ℬ ⊆ ∅.powerset<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a✝ : α<VAR>f g μ : Finset α → β<VAR>s t u✝ : Finset α<VAR>a : α<VAR>u : Finset α<VAR>hu : a ∉ u<VAR>ih : ∀ {f₁ f₂ f₃ f₄ : Finset α → β}, 0 ≤ f₁ → 0 ≤ f₂ → 0 ≤ f₃ → 0 ≤ f₄ → (∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) → ∀ {𝒜 ℬ : Finset (Finset α)}, 𝒜 ⊆ u.powerset → ℬ ⊆ u.powerset → (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : 𝒜 ⊆ (insert a u).powerset<VAR>hℬ : ℬ ⊆ (insert a u).powerset<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a✝ : α<VAR>f g μ : Finset α → β<VAR>s t u✝ : Finset α<VAR>a : α<VAR>u : Finset α<VAR>hu : a ∉ u<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : 𝒜 ⊆ (insert a u).powerset<VAR>hℬ : ℬ ⊆ (insert a u).powerset<VAR>ih : (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤ (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a✝ : α<VAR>f g μ : Finset α → β<VAR>s t u✝ : Finset α<VAR>a : α<VAR>u : Finset α<VAR>hu : a ∉ u<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : 𝒜 ⊆ (insert a u).powerset<VAR>hℬ : ℬ ⊆ (insert a u).powerset<VAR>ih : (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤ (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s<VAR>this : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a✝ : α<VAR>f g μ : Finset α → β<VAR>s t u✝ : Finset α<VAR>a : α<VAR>u : Finset α<VAR>hu : a ∉ u<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : 𝒜 ⊆ (insert a u).powerset<VAR>hℬ : ℬ ⊆ (insert a u).powerset<VAR>ih : (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤ (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s<VAR>this✝ : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset<VAR>this : 𝒜 ⊻ ℬ ⊆ (insert a u).powerset<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x - y) = (equivShrink α) x - (equivShrink α) y
<VAR>α : Type u_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x - y) = (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) - (equivShrink α).symm ((equivShrink α) y))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>U : Set (PrimeSpectrum R[X])<VAR>s : Set R[X]<VAR>z : zeroLocus s = Uᶜ<GOAL>IsOpen (⇑(PrimeSpectrum.comap C) '' U)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>U : Set (PrimeSpectrum R[X])<VAR>s : Set R[X]<VAR>z : zeroLocus s = Uᶜ<GOAL>IsOpen (⋃ i, ⇑(PrimeSpectrum.comap C) '' (zeroLocus {↑i})ᶜ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>U : Set (PrimeSpectrum R[X])<VAR>s : Set R[X]<VAR>z : zeroLocus s = Uᶜ<GOAL>IsOpen (⋃ i, imageOfDf ↑i)
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p : S[X]<VAR>r : R<VAR>hp : p ∈ lifts (algebraMap R S)<GOAL>r • p ∈ lifts (algebraMap R S)
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p : S[X]<VAR>r : R<VAR>hp : p ∈ (mapAlg R S).range<GOAL>r • p ∈ (mapAlg R S).range
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S : IntermediateField K L<VAR>n : ℕ<GOAL>↑n ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>4096 < rexp 16
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>12 * log 2 < 16
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 12 * 0.6931471808 < 16<GOAL>12 * log 2 < 16
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>q : PMF (α → β)<VAR>p : PMF α<VAR>b : β<GOAL>(q.seq p) b = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>q : PMF (α → β)<VAR>p : PMF α<VAR>b : β<GOAL>(∑' (a : α → β), q a * ∑' (a_1 : α), if b = a a_1 then p a_1 else 0) = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0