ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>h : TendstoUniformly F f p<GOAL>TendstoUniformlyOnFilter F f p ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<VAR>y : Set β<GOAL>∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (f a') (f a))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g : ι → α<VAR>inst✝¹ : AddCommMonoidWithOne α<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Finset ι<GOAL>↑(filter p s).card = ∑ a ∈ s, if p a then 1 else 0
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<GOAL>↑a - ↑a / 2 = ↑a / 2
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α β γ : TypeVec.{u} n<VAR>f : α ⟹ β<VAR>g : β ⟹ γ<VAR>x : F α<GOAL>(g ⊚ f) <$$> x = g <$$> f <$$> x
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α β γ : TypeVec.{u} n<VAR>f : α ⟹ β<VAR>g : β ⟹ γ<VAR>x : F α<GOAL>abs ((g ⊚ f) <$$> repr x) = abs (g <$$> f <$$> repr x)
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : DivisionRing L<VAR>inst✝¹ : DivisionRing M<VAR>S : Type u_1<VAR>inst✝ : SetLike S K<VAR>h : SubfieldClass S K<VAR>x : K<VAR>s : S<VAR>q : ℚ≥0<VAR>hx : x ∈ s<GOAL>q • x ∈ s
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, ↑x ^ r = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]<VAR>hr : r + 1 ≠ 0<VAR>hab : ¬0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hab : ¬0 ∉ [[a, b]]<VAR>h : -1 < r.re<GOAL>∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hab : ¬0 ∉ [[a, b]]<VAR>h : -1 < r.re<GOAL>∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hab : ¬0 ∉ [[a, b]]<VAR>h : -1 < r.re<VAR>c : ℝ<GOAL>∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hab : ¬0 ∉ [[a, b]]<VAR>h : -1 < r.re<VAR>c : ℝ<GOAL>ContinuousOn (fun c => ↑c ^ (r + 1) / (r + 1)) [[0, c]]
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hab : ¬0 ∉ [[a, b]]<VAR>h : -1 < r.re<VAR>c : ℝ<GOAL>∀ x ∈ Set.Ioo (min 0 c) (max 0 c), HasDerivWithinAt (fun c => ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hab : ¬0 ∉ [[a, b]]<VAR>h : -1 < r.re<VAR>c : ℝ<GOAL>IntervalIntegrable (fun y => ↑y ^ r) MeasureTheory.volume 0 c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R✝ : Type u_3<VAR>S✝ : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>a b c : R<GOAL>abv (a - c) ≤ abv (a - b) + abv (b - c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<GOAL>DecompositionMonoid (Associates α) ↔ DecompositionMonoid α
<VAR>q : ℚ<VAR>r : ℝ<GOAL>↑(q • r) = q • ↑r
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹² : Category.{u_3, u_1} C<VAR>inst✝¹¹ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹⁰ : HasShift C ℤ<VAR>inst✝⁹ : Preadditive C<VAR>inst✝⁸ : HasZeroObject C<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : Pretriangulated C<VAR>inst✝⁵ : HasShift D ℤ<VAR>inst✝⁴ : L.CommShift ℤ<VAR>inst✝³ : L.EssSurj<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>X : D<GOAL>contractibleTriangle X ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹² : Category.{u_3, u_1} C<VAR>inst✝¹¹ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹⁰ : HasShift C ℤ<VAR>inst✝⁹ : Preadditive C<VAR>inst✝⁸ : HasZeroObject C<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : Pretriangulated C<VAR>inst✝⁵ : HasShift D ℤ<VAR>inst✝⁴ : L.CommShift ℤ<VAR>inst✝³ : L.EssSurj<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>X : D<GOAL>contractibleTriangle X ≅ L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>g : ℝ → ℝ<VAR>hg : 0 ≤ᶠ[ae volume] g<VAR>hg_int : Integrable g volume<GOAL>∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>X : Type u_2<VAR>m : X<GOAL>Quot.mk (Rel R X) (Pre.of m) = ι R m
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasColimits C<VAR>j : J<VAR>k : K<GOAL>colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).inv ≫ (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom = colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasColimits C<VAR>j : J<VAR>k : K<GOAL>((colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv) ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).inv) ≫ (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom = colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasColimits C<VAR>j : J<VAR>k : K<GOAL>G.map (𝟙 j, 𝟙 k) ≫ colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k = colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasColimits C<VAR>j : J<VAR>k : K<GOAL>𝟙 (G.obj (j, k)) ≫ colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k = colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<GOAL>sqrt x = x ^ (1 / 2)
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<GOAL>↑(sqrt x) = ↑(x ^ (1 / 2))
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<GOAL>√↑x = ↑x ^ (1 / 2)
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm α<VAR>e : α ≃ Fin n<VAR>h : ∀ (x : α), f x ≠ x → x ∈ []<GOAL>signAux ((e.symm.trans f).trans e) = signAux2 [] f
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm α<VAR>e : α ≃ Fin n<VAR>h : ∀ (x : α), f x ≠ x → x ∈ []<VAR>this : f = 1<GOAL>signAux ((e.symm.trans f).trans e) = signAux2 [] f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : CommRing B<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra A K<VAR>inst✝¹² : Algebra B L<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : IsScalarTower A B L<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsFractionRing A K<VAR>inst✝⁴ : IsIntegralClosure B A L<VAR>inst✝³ : IsFractionRing B L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsDomain B<VAR>I J : Submodule B L<GOAL>I ≤ Jᵛ ↔ I * J ≤ 1ᵛ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Setoid α)<VAR>x y : α<GOAL>⟦x⟧ = ⟦y⟧ ↔ ∀ s ∈ S, s.Rel x y
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>ι : Sort u_2<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>u : UniformSpace α<VAR>h : (𝓤 α).HasBasis p s<GOAL>u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y => (x, y) ∉ s i
<VAR>x y : ℝ<GOAL>↑(tan x) = ↑(sin x / cos x)
<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>G : D ⥤ C<VAR>h : G ⊣ F<VAR>X' X : Cᵒᵖ<VAR>Y : Dᵒᵖ<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.op.obj Y<GOAL>((h.homEquiv (Opposite.unop Y) (Opposite.unop X')) (g.unop ≫ f.unop)).op = (F.map f.unop).op ≫ ((h.homEquiv (Opposite.unop Y) (Opposite.unop X)) g.unop).op
<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>G : D ⥤ C<VAR>h : G ⊣ F<VAR>X' X : Cᵒᵖ<VAR>Y : Dᵒᵖ<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.op.obj Y<GOAL>(h.unit.app (Opposite.unop Y) ≫ F.map (g.unop ≫ f.unop)).op = (F.map f.unop).op ≫ (h.unit.app (Opposite.unop Y) ≫ F.map g.unop).op
<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>G : D ⥤ C<VAR>h : G ⊣ F<VAR>X' : Cᵒᵖ<VAR>X Y : Dᵒᵖ<VAR>f : F.op.obj X' ⟶ X<VAR>g : X ⟶ Y<GOAL>((h.homEquiv (Opposite.unop Y) (Opposite.unop X')).symm (g.unop ≫ f.unop)).op = ((h.homEquiv (Opposite.unop X) (Opposite.unop X')).symm f.unop).op ≫ (G.map g.unop).op
<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>G : D ⥤ C<VAR>h : G ⊣ F<VAR>X' : Cᵒᵖ<VAR>X Y : Dᵒᵖ<VAR>f : F.op.obj X' ⟶ X<VAR>g : X ⟶ Y<GOAL>(G.map (g.unop ≫ f.unop) ≫ h.counit.app (Opposite.unop X')).op = (G.map f.unop ≫ h.counit.app (Opposite.unop X')).op ≫ (G.map g.unop).op
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.sc' i j k).homologyπ ≫ (K.homologyIsoSc' i j k hi hk).inv = (K.cyclesIsoSc' i j k hi hk).inv ≫ K.homologyπ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>hg : Monotone g<VAR>s : Set β<GOAL>(∃ i ∈ f, ∃ x ∈ g i, id x ⊆ s) ↔ ∃ t ∈ f, s ∈ g t
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>inst✝⁸ : Category.{u_8, u_1} C₁<VAR>inst✝⁷ : Category.{u_9, u_2} C₂<VAR>inst✝⁶ : Category.{?u.4583, u_3} D<VAR>inst✝⁵ : Category.{u_7, u_4} D₁<VAR>inst✝⁴ : Category.{u_6, u_5} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G : C₁ ⥤ D₂<VAR>G' : D₁ ⥤ D₂<VAR>inst✝¹ : Lifting L₁ W₁ G G'<VAR>F : C₂ ⥤ D₁<VAR>F' : D₂ ⥤ D₁<VAR>inst✝ : Lifting L₂ W₂ F F'<VAR>α : G ⋙ F' ≅ L₁<VAR>β : F ⋙ G' ≅ L₂<VAR>X : C₂<GOAL>(liftNatTrans L₂ W₂ (F ⋙ G') L₂ (F' ⋙ G') (𝟭 D₂) β.hom).app (L₂.obj X) = (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>inst✝⁸ : Category.{u_8, u_1} C₁<VAR>inst✝⁷ : Category.{u_9, u_2} C₂<VAR>inst✝⁶ : Category.{?u.4583, u_3} D<VAR>inst✝⁵ : Category.{u_7, u_4} D₁<VAR>inst✝⁴ : Category.{u_6, u_5} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G : C₁ ⥤ D₂<VAR>G' : D₁ ⥤ D₂<VAR>inst✝¹ : Lifting L₁ W₁ G G'<VAR>F : C₂ ⥤ D₁<VAR>F' : D₂ ⥤ D₁<VAR>inst✝ : Lifting L₂ W₂ F F'<VAR>α : G ⋙ F' ≅ L₁<VAR>β : F ⋙ G' ≅ L₂<VAR>X : C₂<GOAL>(Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X ≫ (Lifting.iso L₂ W₂ L₂ (𝟭 D₂)).inv.app X = (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>inst✝⁸ : Category.{u_8, u_1} C₁<VAR>inst✝⁷ : Category.{u_9, u_2} C₂<VAR>inst✝⁶ : Category.{?u.4583, u_3} D<VAR>inst✝⁵ : Category.{u_7, u_4} D₁<VAR>inst✝⁴ : Category.{u_6, u_5} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G : C₁ ⥤ D₂<VAR>G' : D₁ ⥤ D₂<VAR>inst✝¹ : Lifting L₁ W₁ G G'<VAR>F : C₂ ⥤ D₁<VAR>F' : D₂ ⥤ D₁<VAR>inst✝ : Lifting L₂ W₂ F F'<VAR>α : G ⋙ F' ≅ L₁<VAR>β : F ⋙ G' ≅ L₂<VAR>X : C₂<GOAL>G'.map ((Lifting.iso' W₂).hom.app X) ≫ β.hom.app X ≫ 𝟙 (L₂.obj X) = G'.map ((Lifting.iso' W₂).hom.app X) ≫ β.hom.app X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Ico a b) = Ico ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Ico ↑a ↑b)) = Ico ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : x ∈ Ico ↑a ↑b<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : ↑a ≤ x ∧ x < ↑b<GOAL>p x
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>r : R<GOAL>(expand R p) ((monomial q) r) = (monomial (q * p)) r
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>min ↑a ↑b ≤ ↑c ↔ min a b ≤ c
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Matrix n n α → Matrix n n α[X] := fun M => M.map ⇑C + X • 1<VAR>f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix<VAR>f'_inv : ∀ (M : Matrix n n α), f' (g M) = M<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Matrix n n α → Matrix n n α[X] := fun M => M.map ⇑C + X • 1<VAR>f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix<VAR>f'_inv : ∀ (M : Matrix n n α), f' (g M) = M<VAR>f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Matrix n n α → Matrix n n α[X] := fun M => M.map ⇑C + X • 1<VAR>f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix<VAR>f'_inv : ∀ (M : Matrix n n α), f' (g M) = M<VAR>f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate<VAR>f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Matrix n n α → Matrix n n α[X] := fun M => M.map ⇑C + X • 1<VAR>f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix<VAR>f'_inv : ∀ (M : Matrix n n α), f' (g M) = M<VAR>f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate<VAR>f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N<VAR>hu : ∀ (M : Matrix n n α), IsRegular (g M).det<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum fun x => 0) s = 0 s
<VAR>f✝ : ℝ → ℝ<VAR>x✝ f' : ℝ<VAR>s : Set ℝ<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>h₁ : DifferentiableAt ℝ f x<VAR>h₂ : f x ≠ 0<GOAL>deriv (log ∘ f) x = logDeriv f x
<VAR>f✝ : ℝ → ℝ<VAR>x✝ f' : ℝ<VAR>s : Set ℝ<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>h₁ : DifferentiableAt ℝ f x<VAR>h₂ : f x ≠ 0<GOAL>deriv (log ∘ f) x = deriv (fun x => log (f x)) x
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>t : RBNode α<GOAL>any p t = true ↔ Any (fun x => p x = true) t
<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>x✝⁵ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk xl xr xL xR) → Subsingleton y.Short<VAR>a b : (mk xl xr xL xR).Short<VAR>α β : Type u_1<VAR>L : α → PGame<VAR>R : β → PGame<VAR>x✝⁴ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk α β L R) → Subsingleton y.Short<VAR>h✝³ : mk xl xr xL xR = mk α β L R<VAR>α_eq✝¹ : xl = α<VAR>L✝² : xl → PGame<VAR>inst✝³ : Fintype xl<VAR>β_eq✝¹ : xr = β<VAR>R✝² : xr → PGame<VAR>inst✝² : Fintype xr<VAR>a_eq✝³ : HEq xL L✝²<VAR>x✝³ : (i : xl) → (xL i).Short<VAR>a_eq✝² : HEq xR R✝²<VAR>x✝² : (j : xr) → (xR j).Short<VAR>h✝² : HEq a (Short.mk x✝³ x✝²)<VAR>α✝ β✝ : Type u_1<VAR>L✝¹ : α✝ → PGame<VAR>R✝¹ : β✝ → PGame<VAR>h✝¹ : mk xl xr xL xR = mk α✝ β✝ L✝¹ R✝¹<VAR>α_eq✝ : xl = α✝<VAR>L✝ : xl → PGame<VAR>inst✝¹ : Fintype xl<VAR>β_eq✝ : xr = β✝<VAR>R✝ : xr → PGame<VAR>inst✝ : Fintype xr<VAR>a_eq✝¹ : HEq xL L✝<VAR>x✝¹ : (i : xl) → (xL i).Short<VAR>a_eq✝ : HEq xR R✝<VAR>x✝ : (j : xr) → (xR j).Short<VAR>h✝ : HEq b (Short.mk x✝¹ x✝)<VAR>x : xl<GOAL>(invImage (fun x => x) instWellFoundedRelation).1 (xL x) (mk α β L R)
<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>x✝⁵ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk xl xr xL xR) → Subsingleton y.Short<VAR>a b : (mk xl xr xL xR).Short<VAR>α β : Type u_1<VAR>L : α → PGame<VAR>R : β → PGame<VAR>x✝⁴ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk α β L R) → Subsingleton y.Short<VAR>h✝³ : mk xl xr xL xR = mk α β L R<VAR>α_eq✝¹ : xl = α<VAR>L✝² : xl → PGame<VAR>inst✝³ : Fintype xl<VAR>β_eq✝¹ : xr = β<VAR>R✝² : xr → PGame<VAR>inst✝² : Fintype xr<VAR>a_eq✝³ : HEq xL L✝²<VAR>x✝³ : (i : xl) → (xL i).Short<VAR>a_eq✝² : HEq xR R✝²<VAR>x✝² : (j : xr) → (xR j).Short<VAR>h✝² : HEq a (Short.mk x✝³ x✝²)<VAR>α✝ β✝ : Type u_1<VAR>L✝¹ : α✝ → PGame<VAR>R✝¹ : β✝ → PGame<VAR>h✝¹ : mk xl xr xL xR = mk α✝ β✝ L✝¹ R✝¹<VAR>α_eq✝ : xl = α✝<VAR>L✝ : xl → PGame<VAR>inst✝¹ : Fintype xl<VAR>β_eq✝ : xr = β✝<VAR>R✝ : xr → PGame<VAR>inst✝ : Fintype xr<VAR>a_eq✝¹ : HEq xL L✝<VAR>x✝¹ : (i : xl) → (xL i).Short<VAR>a_eq✝ : HEq xR R✝<VAR>x✝ : (j : xr) → (xR j).Short<VAR>h✝ : HEq b (Short.mk x✝¹ x✝)<VAR>x : xr<GOAL>(invImage (fun x => x) instWellFoundedRelation).1 (xR x) (mk α β L R)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : CoalgebraCat R<GOAL>ModuleCat.ofHom Coalgebra.comul ≫ ModuleCat.ofHom Coalgebra.counit ▷ ModuleCat.of R ↑X.toModuleCat = (λ_ (ModuleCat.of R ↑X.toModuleCat)).inv
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : CoalgebraCat R<GOAL>ModuleCat.ofHom Coalgebra.comul ≫ ModuleCat.of R ↑X.toModuleCat ◁ ModuleCat.ofHom Coalgebra.counit = (ρ_ (ModuleCat.of R ↑X.toModuleCat)).inv
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : CoalgebraCat R<GOAL>ModuleCat.ofHom Coalgebra.comul ≫ ModuleCat.of R ↑X.toModuleCat ◁ ModuleCat.ofHom Coalgebra.comul = ModuleCat.ofHom Coalgebra.comul ≫ ModuleCat.ofHom Coalgebra.comul ▷ ModuleCat.of R ↑X.toModuleCat ≫ (α_ (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat)).hom
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : CoalgebraCat R<GOAL>ModuleCat.ofHom Coalgebra.comul ≫ X.toModuleCat ◁ ModuleCat.ofHom Coalgebra.comul = ModuleCat.ofHom Coalgebra.comul ≫ ModuleCat.ofHom Coalgebra.comul ▷ X.toModuleCat ≫ (α_ X.toModuleCat X.toModuleCat X.toModuleCat).hom
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>h : a ≠ b<GOAL>∏ x ∈ {a, b}, f x = f a * f b
<VAR>V : Type<VAR>G : SimpleGraph V<VAR>inst✝² : G.LocallyFinite<VAR>inst✝¹ : Fact G.Preconnected<VAR>inst✝ : Infinite V<GOAL>G.end.Nonempty
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n✝ n : σ →₀ ℕ<VAR>hnn : n ≠ 0<VAR>a : R<VAR>m : σ →₀ ℕ<GOAL>MvPolynomial.coeff m ((trunc R n) ((C σ R) a)) = MvPolynomial.coeff m (MvPolynomial.C a)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Exact ⇑(map I f) ⇑(map I g)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>map I g ∘ₗ map I f = 0
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>y : AdicCompletion I N<GOAL>y ∈ ker (map I g) → y ∈ range (map I f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p✝ : γ → δ → Prop<VAR>r p : α → β → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>hst : Rel r s t<VAR>h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b<GOAL>Rel p s t
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K✝ : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : AddCommGroup M✝<VAR>inst✝¹¹ : AddCommGroup M'<VAR>inst✝¹⁰ : AddCommGroup M''<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>a b : R<VAR>x y : M✝<VAR>K : Type u_8<VAR>M : Type u_9<VAR>L : Type u_10<VAR>inst✝⁶ : CommRing K<VAR>inst✝⁵ : Semiring M<VAR>inst✝⁴ : Algebra K M<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : NoZeroSMulDivisors K L<GOAL>LinearIndependent K AlgHom.toLinearMap