ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>X Y : Mon_ C<VAR>P Q : Bimod X Y<VAR>f : P.X ≅ Q.X<VAR>f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft<VAR>f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight<GOAL>f.hom ≫ f.inv = 𝟙 P.X
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>X Y : Mon_ C<VAR>P Q : Bimod X Y<VAR>f : P.X ≅ Q.X<VAR>f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft<VAR>f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight<GOAL>f.inv ≫ f.hom = 𝟙 Q.X
<VAR>α β : Type u<VAR>c : Cardinal.{u}<GOAL>ℵ₀ < lift.{v, u} c ↔ ℵ₀ < c
<VAR>α β : Type<VAR>n : ℕ<VAR>S : Set (Vector3 ℕ n.succ)<VAR>d : Dioph S<VAR>f : Vector3 ℕ n → ℕ<VAR>df : DiophFn f<VAR>v : Fin2 n → ℕ<GOAL>((f v ::ₒ v) ∘ none :: some) ∈ S ↔ v ∈ {v | (f v :: v) ∈ S}
<VAR>α β : Type<VAR>n : ℕ<VAR>S : Set (Vector3 ℕ n.succ)<VAR>d : Dioph S<VAR>f : Vector3 ℕ n → ℕ<VAR>df : DiophFn f<VAR>v : Fin2 n → ℕ<GOAL>((f v ::ₒ v) ∘ none :: some) = f v :: v
<VAR>l r✝ : List Char<VAR>it : Iterator<VAR>n : Nat<VAR>a : Char<VAR>r : List Char<VAR>h : ValidFor l (a :: r) it<VAR>hn : n + 1 ≤ (a :: r).length<GOAL>ValidFor ((List.take (n + 1) (a :: r)).reverse ++ l) (List.drop (n + 1) (a :: r)) (it.next.nextn n)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommSemiring S<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module S N<VAR>inst✝⁶ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module S Q<VAR>inst✝¹ : Module R Q<VAR>inst✝ : IsScalarTower R S Q<VAR>g : M →ₗ[R] Q<VAR>x : M<GOAL>(h.lift g) (f x) = g x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommSemiring S<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module S N<VAR>inst✝⁶ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module S Q<VAR>inst✝¹ : Module R Q<VAR>inst✝ : IsScalarTower R S Q<VAR>g : M →ₗ[R] Q<VAR>x : M<VAR>hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m<GOAL>(h.lift g) (f x) = g x
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<GOAL>e.permCongr (Equiv.refl α') = Equiv.refl β'
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I✝ : Ideal R<VAR>hf : Function.Bijective ⇑f<VAR>I : Ideal R<VAR>H : I.IsMaximal<GOAL>(map f I).IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I✝ : Ideal R<VAR>hf : Function.Bijective ⇑f<VAR>I : Ideal R<VAR>H : I.IsMaximal<VAR>h : map f I = ⊤<GOAL>I = ⊤
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝¹¹ : Fintype m<VAR>inst✝¹⁰ : DecidableEq m<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : (i : m) → Fintype (n' i)<VAR>inst✝⁶ : (i : m) → DecidableEq (n' i)<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : TopologicalSpace 𝔸<VAR>inst✝² : TopologicalRing 𝔸<VAR>inst✝¹ : Algebra 𝕂 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>v : m → Matrix n n 𝔸<GOAL>exp 𝕂 (blockDiagonal v) = blockDiagonal (exp 𝕂 v)
<VAR>G✝ : Type u_1<VAR>inst✝¹ : DivInvMonoid G✝<VAR>a✝ b : G✝<VAR>G : Type u_2<VAR>inst✝ : SubNegMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>Int.negSucc n • a = -((n + 1) • a)
<VAR>G✝ : Type u_1<VAR>inst✝¹ : DivInvMonoid G✝<VAR>a✝ b : G✝<VAR>G : Type u_2<VAR>inst✝ : SubNegMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>Int.negSucc n • a = -(↑(n + 1) • a)
<VAR>i j k : ℤ<GOAL>(i * j).gcd (k * j) = i.gcd k * j.natAbs
<VAR>i j k : ℤ<GOAL>(i.natAbs * j.natAbs).gcd (k.natAbs * j.natAbs) = i.natAbs.gcd k.natAbs * j.natAbs
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>r : R<VAR>a : ⨂[R]^n M<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul a (algebraMap₀ r)) = r • a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁸ : NormedField R<VAR>inst✝⁷ : SeminormedAddCommGroup M<VAR>inst✝⁶ : SeminormedAddCommGroup N<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace R M<VAR>inst✝³ : NormedSpace R N<VAR>inst✝² : NormedSpace R G<VAR>inst✝¹ : NormedAddCommGroup M'<VAR>inst✝ : NormedSpace R M'<VAR>f : M →L[R] N<VAR>g : N →L[R] G<VAR>c✝ c : R<VAR>hc : c ≠ 0<VAR>li : M' →ₗᵢ[R] N<GOAL>Injective ⇑(c • li.toContinuousLinearMap)
<VAR>b : Bool<VAR>n : ℤ<GOAL>(bit b n).bodd = b
<VAR>b : Bool<VAR>n : ℤ<GOAL>(2 * n + bif b then 1 else 0).bodd = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂<GOAL>l₁ ++ l₂.diff l₁ ~ l₂
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>h : Submodule.span F (Set.range v) = ⊤<GOAL>Submodule.span F (Set.range fun x => v x ^ q ^ n) = ⊤
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>h : Submodule.span F (Set.range v) = ⊤<GOAL>Submodule.span F (Set.range fun x => v x ^ q ^ n) = Submodule.span F ↑(MonoidHom.mrange (powMonoidHom (q ^ n)))
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>h : Submodule.span F (Set.range v) = ⊤<GOAL>Set.range (DivisionSemiring.toSemiring.8 (q ^ n)) ⊆ ↑(Submodule.span F (Set.range (DivisionSemiring.toSemiring.8 (q ^ n) ∘ v)))
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>h : Submodule.span F (Set.range v) = ⊤<GOAL>DivisionSemiring.toSemiring.8 (q ^ n) '' Set.univ ⊆ ↑(Submodule.span F (DivisionSemiring.toSemiring.8 (q ^ n) '' Set.range v))
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>h : Submodule.span F (Set.range v) = ⊤<VAR>this : ExpChar E q<GOAL>DivisionSemiring.toSemiring.8 (q ^ n) '' Set.univ ⊆ ↑(Submodule.span F (DivisionSemiring.toSemiring.8 (q ^ n) '' Set.range v))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : G → E<VAR>f'✝ g' : G →L[ℝ] E<VAR>s : Set G<VAR>x✝ : G<VAR>n : ℕ∞<VAR>f : ℝ → F<VAR>f' : F<VAR>x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => ‖f x‖ ^ 2) (2 * ⟪f x, f'⟫_ℝ) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<GOAL>(↑p).coeff 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<GOAL>¬0 = 1
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<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>inst✝⁴ : Nontrivial R<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>S : Submodule R M<VAR>inst✝ : Module.Finite R ↥S<GOAL>finrank R ↥S = 0 ↔ S = ⊥
<VAR>A B : NonemptyFinLinOrd<VAR>f : A ⟶ B<GOAL>Mono f ↔ Function.Injective ⇑f
<VAR>A B : NonemptyFinLinOrd<VAR>f : A ⟶ B<GOAL>Mono f → Function.Injective ⇑f
<VAR>A B : NonemptyFinLinOrd<VAR>f : A ⟶ B<VAR>a✝ : Mono f<VAR>a₁ a₂ : ↑A<VAR>h : f a₁ = f a₂<VAR>X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))<VAR>g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := ⋯ }<VAR>g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := ⋯ }<VAR>eq : g₁ ≫ f = g₂ ≫ f<GOAL>g₁ { down := 0 } = g₂ { down := 0 }
<VAR>A B : NonemptyFinLinOrd<VAR>f : A ⟶ B<VAR>a✝ : Mono f<VAR>a₁ a₂ : ↑A<VAR>h : f a₁ = f a₂<VAR>X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))<VAR>g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := ⋯ }<VAR>g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := ⋯ }<VAR>eq : g₁ = g₂<GOAL>g₁ { down := 0 } = g₂ { down := 0 }
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h : HasStrictDerivAt f f' x<GOAL>HasStrictFDerivAt f (f' • 1) x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>ha : 1 < a<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>1 < a ^ (n + 1)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>ha : 1 < a<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>1 < a * a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : PosSMulMono α γ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>b₁ b₂ : β<VAR>hf : ∀ {b₁ b₂ : β}, True<VAR>smul : α → β → True<VAR>hb : f b₁ ≤ f b₂<GOAL>a • f b₁ ≤ a • f b₂
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝¹ : CompleteLinearOrder γ<VAR>inst✝ : DenselyOrdered γ<VAR>f : α → γ<GOAL>LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.283606, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.283613, u_2} D<VAR>X Y : C<VAR>inst✝ : HasInitial C<VAR>c : BinaryCofan X Y<VAR>h : IsVanKampenColimit c<GOAL>IsPullback (initial.to ((pair X Y).obj { as := WalkingPair.left })) (initial.to ((pair X Y).obj { as := WalkingPair.right })) c.inl c.inr
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.283606, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.283613, u_2} D<VAR>X Y : C<VAR>inst✝ : HasInitial C<VAR>c : BinaryCofan X Y<VAR>h : IsVanKampenColimit c<GOAL>mapPair (initial.to X) (𝟙 Y) ≫ c.ι = (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map c.inr
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.283606, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.283613, u_2} D<VAR>X Y : C<VAR>inst✝ : HasInitial C<VAR>c : BinaryCofan X Y<VAR>h : IsVanKampenColimit c<GOAL>IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : PartialOrder Γ<VAR>V : Type u_3<VAR>inst✝² : Zero V<VAR>inst✝¹ : SMulZeroClass R V<VAR>inst✝ : Zero Γ<VAR>r : R<VAR>x : HahnSeries Γ V<VAR>h : r • x ≠ 0<GOAL>¬(r • x).order < x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : PartialOrder Γ<VAR>V : Type u_3<VAR>inst✝² : Zero V<VAR>inst✝¹ : SMulZeroClass R V<VAR>inst✝ : Zero Γ<VAR>r : R<VAR>x : HahnSeries Γ V<VAR>h : r • x ≠ 0<VAR>hx : x ≠ 0<GOAL>¬(r • x).order < x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : PartialOrder Γ<VAR>V : Type u_3<VAR>inst✝² : Zero V<VAR>inst✝¹ : SMulZeroClass R V<VAR>inst✝ : Zero Γ<VAR>r : R<VAR>x : HahnSeries Γ V<VAR>h : r • x ≠ 0<VAR>hx : x ≠ 0<GOAL>¬⋯.min ⋯ < ⋯.min ⋯
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>n : ℕ<GOAL>(fun z => (z.im ^ n) ^ 2) = fun z => z.im ^ (2 * n)
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>n : ℕ<GOAL>(fun z => Real.exp z.re) = fun z => Real.exp z.re ^ 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫ leftHomologyMap' φ h₁ h₂ = leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫ leftHomologyMap' (𝟙 S₂) S₂.homologyData.left S₂.leftHomologyData ≫ leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData h₂
<VAR>n : ℕ<GOAL>(Λ * ↑ζ) n = log n
<VAR>n : ℕ<GOAL>Real.log ↑n = log n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ X Y Z : C<VAR>f : X ≅ Y<VAR>g g' : Y ⟶ Z<GOAL>f.hom ≫ g = f.hom ≫ g' ↔ g = g'
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>a : α<VAR>x : Quotient G α<GOAL>a ∈ x.orbit ↔ Quotient.mk'' a = x
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>a a✝ : α<GOAL>a ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' a = Quotient.mk'' a✝
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>a a✝ : α<GOAL>a ∈ orbit (Quotient.mk'' a✝) ↔ Setoid.r a a✝
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h1 : Nat.Prime (orderOf σ)<VAR>h2 : σ.support.card < 2 * orderOf σ<GOAL>σ.IsCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h1 : Nat.Prime (orderOf σ)<VAR>h2 : σ.support.card < 2 * orderOf σ<VAR>n : ℕ<VAR>hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)<GOAL>σ.IsCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h1 : Nat.Prime (orderOf σ)<VAR>n : ℕ<VAR>h2 : n = 0<VAR>hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)<GOAL>σ.IsCycle
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>N₃ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>p : Type u_19<VAR>f : m → n<VAR>hf : Surjective f<GOAL>Injective ⇑(funLeft R M f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>N₃ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>p : Type u_19<VAR>f : m → n<VAR>hf : Surjective f<VAR>g : n → m<VAR>hg : Function.RightInverse g f<GOAL>Injective ⇑(funLeft R M f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>N₃ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>p : Type u_19<VAR>f : m → n<VAR>hf : Surjective f<VAR>g : n → m<VAR>hg : Function.RightInverse g f<GOAL>LeftInverse ⇑(funLeft R M g) ⇑(funLeft R M f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>N₃ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>p : Type u_19<VAR>f : m → n<VAR>hf : Surjective f<VAR>g : n → m<VAR>hg : Function.RightInverse g f<VAR>x : n → M<GOAL>(funLeft R M g) ((funLeft R M f) x) = x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Unbounded (fun x x_1 => x < x_1) (s ∩ {b | a ≤ b}) ↔ Unbounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a x✝ : α<GOAL>a ≤ x✝ ↔ ¬x✝ < a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>↑p ^ (n + 1) * wittMul p (n + 1) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + (remainder p n - wittPolyProdRemainder p (n + 1))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>wittPolyProd p (n + 1) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + remainder p n
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<GOAL>IsDetector (op G) ↔ IsCodetector G
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>inst✝ : IsIso f<GOAL>Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<VAR>la : Filter α<VAR>lb : Filter β<GOAL>sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb
<VAR>a b : ℝ<VAR>n k : ℕ<VAR>ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)<GOAL>∫ (x : ℝ) in 0 ..π, sin x ^ (2 * (k + 1) + 1) = 2 * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 2) / (2 * ↑i + 3)
<VAR>a b : ℝ<VAR>n k : ℕ<VAR>ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)<GOAL>(sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / (↑(2 * k + 1) + 2) + (↑(2 * k + 1) + 1) / (↑(2 * k + 1) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = (2 * ↑k + 2) / (2 * ↑k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
<VAR>a b : ℝ<VAR>n k : ℕ<VAR>ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)<GOAL>(sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / ↑(2 * k + 1 + 2) + ↑(2 * k + 1 + 1) / ↑(2 * k + 1 + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = ↑(2 * k + 2) / ↑(2 * k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>hv : v ᵥ* M = 0<VAR>w : m → A<GOAL>v ⬝ᵥ M *ᵥ w = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ↥(Lp E p μ)<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C<GOAL>‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ↥(Lp E p μ)<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C<VAR>this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C<GOAL>‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P✝ : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝⁴ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝³ : Module R P✝<VAR>P : Type u_10<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : OrderedAddCommMonoid P<VAR>inst✝ : Module R P<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>(pi Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P✝ : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝⁴ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝³ : Module R P✝<VAR>P : Type u_10<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : OrderedAddCommMonoid P<VAR>inst✝ : Module R P<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>(∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (pi Q).Anisotropic ↔ ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (Q i).Anisotropic
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hn : p ^ n ≤ Nat.card ↥H<GOAL>∃ H' ≤ H, Nat.card ↥H' = p ^ n
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hn : p ^ n ≤ Nat.card ↥H<VAR>H' : Subgroup ↥H<VAR>H'card : Nat.card ↥H' = p ^ n<GOAL>∃ H' ≤ H, Nat.card ↥H' = p ^ n
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hn : p ^ n ≤ Nat.card ↥H<VAR>H' : Subgroup ↥H<VAR>H'card : Nat.card ↥H' = p ^ n<GOAL>Nat.card ↥(Subgroup.map H.subtype H') = p ^ n
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hn : p ^ n ≤ Nat.card ↥H<VAR>H' : Subgroup ↥H<VAR>H'card : Nat.card ↥H' = p ^ n<GOAL>Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hn : p ^ n ≤ Nat.card ↥H<VAR>H' : Subgroup ↥H<VAR>H'card : Nat.card ↥H' = p ^ n<VAR>e : ↥H' ≃* ↥(Subgroup.map H.subtype H') := H'.equivMapOfInjective H.subtype ⋯<GOAL>Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }<VAR>hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)<GOAL>IsConj σ τ
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }<VAR>hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)<GOAL>f.extendSubtype * σ * f.extendSubtype⁻¹ = τ
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }<VAR>hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)<GOAL>f.extendSubtype * σ = τ * f.extendSubtype