ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<VAR>this : f.app (op (Y a)) (y a) = G.map (π a).op x<GOAL>(f.app (op (Y a))) ((F.map (π a).op) (i.hom y)) = f.app (op (Y a)) (y a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<VAR>this : f.app (op (Y a)) (y a) = G.map (π a).op x<GOAL>(F.map (π a).op) (i.hom y) = y a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<VAR>this : f.app (op (Y a)) (y a) = G.map (π a).op x<GOAL>(i.hom ≫ F.map (π a).op) y = y a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<VAR>this : f.app (op (Y a)) (y a) = G.map (π a).op x<GOAL>((Types.productLimitCone fun a => F.obj (op (Y a))).cone.π.app { as := a } ≫ (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as)))).hom.app { as := a }) y = y a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : K[X]<GOAL>((algebraMap K[X] (RatFunc K)) p).num = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b : α<VAR>s t : Finset α<VAR>a : α<GOAL>s.erase a \ t = (s \ t).erase a
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : Type u_1<VAR>g : (a : P.A) → P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<GOAL>P.wpRec (fun a f h h' => g a (P.wPathDestLeft h) (fun i => ⟨f i, P.wPathDestRight h i⟩) h') (WType.mk a fun i => (f i).fst) (P.wPathCasesOn f' fun i => (f i).snd) = g a f' f fun i => P.wRec g (f i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : Type u_1<VAR>g : (a : P.A) → P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<GOAL>(g a (P.wPathDestLeft (P.wPathCasesOn f' fun i => (f i).snd)) (fun i => ⟨(f i).fst, P.wPathDestRight (P.wPathCasesOn f' fun i => (f i).snd) i⟩) fun i => P.wpRec (fun a f h h' => g a (P.wPathDestLeft h) (fun i => ⟨f i, P.wPathDestRight h i⟩) h') (f i).fst (P.wPathDestRight (P.wPathCasesOn f' fun i => (f i).snd) i)) = g a f' f fun i => P.wRec g (f i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : Type u_1<VAR>g : (a : P.A) → P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<GOAL>(g a f' (fun i => ⟨(f i).fst, (f i).snd⟩) fun i => P.wpRec (fun a f h h' => g a (P.wPathDestLeft h) (fun i => ⟨f i, P.wPathDestRight h i⟩) h') (f i).fst (f i).snd) = g a f' f fun i => P.wRec g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<VAR>f : α →₀ M<GOAL>f.support.card = 1 ↔ ∃ a b, b ≠ 0 ∧ f = single a b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>ξ : Rˣ<VAR>hξ : ξ ∈ rootsOfUnity ⟨k, hk⟩ R<GOAL>∃ i < k, ζ ^ i = ↑ξ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>ξ : Rˣ<VAR>hξ : ξ ∈ rootsOfUnity ⟨k, hk⟩ R<VAR>hζ' : IsPrimitiveRoot ⋯.unit ↑⟨k, hk⟩<GOAL>∃ i < k, ζ ^ i = ↑ξ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>ξ : Rˣ<VAR>hξ : ξ ∈ rootsOfUnity ⟨k, hk⟩ R<VAR>hζ' : IsPrimitiveRoot ⋯.unit ↑⟨k, hk⟩<VAR>i : ℕ<VAR>hi₁ : i < ↑⟨k, hk⟩<VAR>hi₂ : ⋯.unit ^ i = ξ<GOAL>∃ i < k, ζ ^ i = ↑ξ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>inst✝ : Fintype ι<VAR>S : ι → Set α<GOAL>(fun f => ∏ i : ι, f i) '' univ.pi S = ∏ i : ι, S i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<VAR>h₂ : 1 < s.card<GOAL>s.min' ⋯ < s.max' ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<VAR>h₂ : 1 < s.card<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : a ≠ b<GOAL>s.min' ⋯ < s.max' ⋯
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁸ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁷ : AddGroup ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : MeasurableSingletonClass ι<VAR>inst✝¹ : SecondCountableTopology ι<VAR>inst✝ : MeasurableSub₂ ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>MeasurableSet {ω | τ ω = π ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁸ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁷ : AddGroup ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : MeasurableSingletonClass ι<VAR>inst✝¹ : SecondCountableTopology ι<VAR>inst✝ : MeasurableSub₂ ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>∀ (i : ι), MeasurableSet ({ω | τ ω = π ω} ∩ {ω | τ ω ≤ i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁸ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁷ : AddGroup ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : MeasurableSingletonClass ι<VAR>inst✝¹ : SecondCountableTopology ι<VAR>inst✝ : MeasurableSub₂ ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>MeasurableSet ({ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁸ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁷ : AddGroup ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : MeasurableSingletonClass ι<VAR>inst✝¹ : SecondCountableTopology ι<VAR>inst✝ : MeasurableSub₂ ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>MeasurableSet {ω | min (τ ω) j = min (π ω) j}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁸ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁷ : AddGroup ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : MeasurableSingletonClass ι<VAR>inst✝¹ : SecondCountableTopology ι<VAR>inst✝ : MeasurableSub₂ ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>Measurable fun x => min (τ x) j
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁸ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁷ : AddGroup ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : MeasurableSingletonClass ι<VAR>inst✝¹ : SecondCountableTopology ι<VAR>inst✝ : MeasurableSub₂ ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>Measurable fun x => min (π x) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<GOAL>a = b / c ↔ c * a = b
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f g : R[X]<GOAL>(f + g).coeff n = f.coeff n + g.coeff n
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>(fun t => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<GOAL>(mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N)) = (lsmul R R).compl₁₂ (trace R M) (trace R N)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<GOAL>((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N) = ((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : Module.Dual R M<VAR>m : M<VAR>g : Module.Dual R N<VAR>n : N<GOAL>((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N))) f) m)) g) n = ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N))) f) m)) g) n
<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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ✝ ν : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>μ : Measure α<VAR>f : α → β<GOAL>AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeSup α<VAR>inst✝⁴ : OrderTop α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a✝ b✝ b a : α<GOAL>(if h : a ≤ b then (filter (fun b => a ≤ b) {b}).sup' ⋯ fun x => x else ⊤) = if a ≤ b then b else ⊤
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.108266, u_1} C<VAR>inst✝² : Category.{?u.108270, u_2} D<VAR>inst✝¹ : Category.{?u.108274, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>F.map f ≫ (fun X => colimit.ι (CostructuredArrow.proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X)))) X₂ = (fun X => colimit.ι (CostructuredArrow.proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X)))) X₁ ≫ (L ⋙ L.pointwiseLeftKanExtension F).map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.108266, u_1} C<VAR>inst✝² : Category.{?u.108270, u_2} D<VAR>inst✝¹ : Category.{?u.108274, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) = colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁) ≫ L.map f))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.108266, u_1} C<VAR>inst✝² : Category.{?u.108270, u_2} D<VAR>inst✝¹ : Category.{?u.108274, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) = colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.108266, u_1} C<VAR>inst✝² : Category.{?u.108270, u_2} D<VAR>inst✝¹ : Category.{?u.108274, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>φ : CostructuredArrow.mk (L.map f) ⟶ CostructuredArrow.mk (𝟙 (L.obj X₂)) := CostructuredArrow.homMk f ⋯<GOAL>F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) = colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>this : ∀ (t : Set β), IsOpen (s.restrict f ⁻¹' t) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s<GOAL>ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>this : ∀ (t : Set β), IsOpen (s.restrict f ⁻¹' t) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s<GOAL>(∀ (s_1 : Set β), IsOpen s_1 → IsOpen (s.restrict f ⁻¹' s_1)) ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>hs : s.Infinite<VAR>k : ℕ<VAR>this : Infinite ↑s<GOAL>∃ t ⊆ s, t.Finite ∧ t.ncard = k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>hs : s.Infinite<VAR>this : Infinite ↑s<VAR>t' : Finset ↑s<GOAL>∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>hs : s.Infinite<VAR>this : Infinite ↑s<VAR>t' : Finset ↑s<GOAL>(Subtype.val '' ↑t').ncard = t'.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>hs : s.Infinite<VAR>this : Infinite ↑s<VAR>t' : Finset ↑s<GOAL>(↑t').ncard = t'.card
<VAR>a b c d m✝ n✝ k✝ : ℕ<VAR>p q : ℕ → Prop<VAR>n m k : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<VAR>hnm : n ≤ m<VAR>hmk : m ≤ k<GOAL>leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h => le_succ_of_le h) hnm) (fun x h => le_succ_of_le ⋯) hmk
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>L : Type u_6<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : EquivLike L E F<VAR>inst✝ : LinearEquivClass L 𝕜 E F<VAR>f : L<VAR>s : Set E<VAR>b : F<GOAL>b ∈ ⇑f '' extremePoints 𝕜 s ↔ b ∈ extremePoints 𝕜 (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>L : Type u_6<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : EquivLike L E F<VAR>inst✝ : LinearEquivClass L 𝕜 E F<VAR>f : L<VAR>s : Set E<VAR>a : E<GOAL>f a ∈ ⇑f '' extremePoints 𝕜 s ↔ f a ∈ extremePoints 𝕜 (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>L : Type u_6<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : EquivLike L E F<VAR>inst✝ : LinearEquivClass L 𝕜 E F<VAR>f : L<VAR>s : Set E<VAR>a : E<VAR>this : ∀ (x y : E), ⇑f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y)<GOAL>f a ∈ ⇑f '' extremePoints 𝕜 s ↔ f a ∈ extremePoints 𝕜 (⇑f '' s)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<GOAL>∀ (x y : α), infEdist x s ≤ infEdist y s + 1 * edist x y
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>(map W' f).toJacobian.polynomialZ = (MvPolynomial.map f) W'.polynomialZ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>f : α → β<VAR>h : f 0 = 0<VAR>d : n → α<VAR>i✝ j✝ : n<GOAL>(diagonal d).map f i✝ j✝ = diagonal (fun m => f (d m)) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>f : α → β<VAR>h : f 0 = 0<VAR>d : n → α<VAR>i✝ j✝ : n<GOAL>f (if i✝ = j✝ then d i✝ else 0) = if i✝ = j✝ then f (d i✝) else 0
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀
<VAR>X Y : Scheme<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<VAR>f : X ⟶ Y<VAR>h : Function.Surjective ⇑(Scheme.Γ.map f.op)<GOAL>IsClosedImmersion f
<VAR>X Y : Scheme<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<VAR>f : X ⟶ Y<VAR>h : Function.Surjective ⇑(Scheme.Γ.map f.op)<GOAL>IsClosedImmersion (Spec.map (Scheme.Γ.map f.op))
<VAR>X Y : Scheme<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<VAR>f : X ⟶ Y<VAR>h : Function.Surjective ⇑(Scheme.Γ.map f.op)<GOAL>Function.Surjective ⇑(Scheme.Γ.map f.op)
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : IsCyclotomicExtension {1} A B<VAR>x : B<GOAL>x ∈ ⊥
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>head✝ : α<VAR>tail✝ : List α<GOAL>[].isPerm (head✝ :: tail✝) = true ↔ [] ~ head✝ :: tail✝
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(a :: l₁).isPerm l₂ = true ↔ a :: l₁ ~ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s t : Set α<GOAL>⊤ ≤ 𝓟 univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d : α<VAR>hr : Transitive r<GOAL>ReflTransGen r = ReflGen r