ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric<VAR>i : (PGame.mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>((PGame.mk α✝ β✝ a✝¹ a✝).moveLeft i).Numeric
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Membership P L<VAR>inst✝¹ : HasLines P L<VAR>p : P<VAR>l : L<VAR>h : p ∉ l<VAR>inst✝ : Finite { l // p ∈ l }<VAR>hf : ¬Infinite { p // p ∈ l }<VAR>this : Fintype { p // p ∈ l }<GOAL>pointCount P l ≤ lineCount L p
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Membership P L<VAR>inst✝¹ : HasLines P L<VAR>p : P<VAR>l : L<VAR>h : p ∉ l<VAR>inst✝ : Finite { l // p ∈ l }<VAR>hf : ¬Infinite { p // p ∈ l }<VAR>this : Fintype { p // p ∈ l }<VAR>val✝ : Fintype { l // p ∈ l }<GOAL>pointCount P l ≤ lineCount L p
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Membership P L<VAR>inst✝¹ : HasLines P L<VAR>p : P<VAR>l : L<VAR>h : p ∉ l<VAR>inst✝ : Finite { l // p ∈ l }<VAR>hf : ¬Infinite { p // p ∈ l }<VAR>this : Fintype { p // p ∈ l }<VAR>val✝ : Fintype { l // p ∈ l }<GOAL>Fintype.card { p // p ∈ l } ≤ Fintype.card { l // p ∈ l }
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<GOAL>sSup {J | IsAtom J ∧ J ≤ I} = I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<GOAL>sSup {J | IsAtom J ∧ J ≤ I} ≤ I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<GOAL>I ≤ sSup {J | IsAtom J ∧ J ≤ I}
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : ¬I = ⊥<GOAL>I ≤ sSup {J | IsAtom J ∧ J ≤ I}
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<GOAL>I ≤ sSup {J | IsAtom J ∧ J ≤ I}
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<VAR>J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J<GOAL>I ≤ J ⊔ J' ⊓ I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<VAR>J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J<GOAL>J ⊔ J' = ⊤
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>a✝ : ∀ (y : LieIdeal K L), (invImage (fun x => finrank K ↥↑x) instWellFoundedRelationOfSizeOf).1 y I → sSup {J | IsAtom J ∧ J ≤ y} = y<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>h✝ : IsAtom J ∧ J ≤ I<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<VAR>J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J<VAR>this : I ≤ J ⊔ J' ⊓ I<GOAL>(invImage (fun x => finrank K ↥↑x) instWellFoundedRelationOfSizeOf).1 (J' ⊓ I) I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>a✝ : ∀ (y : LieIdeal K L), (invImage (fun x => finrank K ↥↑x) instWellFoundedRelationOfSizeOf).1 y I → sSup {J | IsAtom J ∧ J ≤ y} = y<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>h✝ : IsAtom J ∧ J ≤ I<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<VAR>J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J<VAR>this : I ≤ J ⊔ J' ⊓ I<GOAL>↑(J' ⊓ I) < ↑I
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>a✝ : ∀ (y : LieIdeal K L), (invImage (fun x => finrank K ↥↑x) instWellFoundedRelationOfSizeOf).1 y I → sSup {J | IsAtom J ∧ J ≤ y} = y<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>h✝ : IsAtom J ∧ J ≤ I<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<VAR>J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J<VAR>this : I ≤ J ⊔ J' ⊓ I<VAR>hIJ' : I ≤ J'<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>a✝ : ∀ (y : LieIdeal K L), (invImage (fun x => finrank K ↥↑x) instWellFoundedRelationOfSizeOf).1 y I → sSup {J | IsAtom J ∧ J ≤ y} = y<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>h✝ : IsAtom J ∧ J ≤ I<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<VAR>J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J<VAR>this : I ≤ J ⊔ J' ⊓ I<VAR>hIJ' : I ≤ J'<GOAL>J = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>a✝ : ∀ (y : LieIdeal K L), (invImage (fun x => finrank K ↥↑x) instWellFoundedRelationOfSizeOf).1 y I → sSup {J | IsAtom J ∧ J ≤ y} = y<VAR>hI : ¬I = ⊥<VAR>J : LieIdeal K L<VAR>h✝ : IsAtom J ∧ J ≤ I<VAR>hJ : IsAtom J<VAR>hJI : J ≤ I<VAR>J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J<VAR>this : I ≤ J ⊔ J' ⊓ I<VAR>hIJ' : I ≤ J'<GOAL>J ≤ ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>h : ∀ x ∈ s, f x ≠ 1 → x ∈ t<GOAL>∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<GOAL>inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g = (range (lTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<GOAL>∀ (x : Q ⊗[R] N), (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) x = (range (lTensor Q f)).mkQ x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<GOAL>(inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) y = (range (lTensor Q f)).mkQ y
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>cyclesMap' (φ - φ') h₁ h₂ = cyclesMap' φ h₁ h₂ - cyclesMap' φ' h₁ h₂
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty<VAR>hsu : s ∩ u = ∅<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty<VAR>hsu : (s ∩ u).Nonempty<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<GOAL>f '' s ∈ 𝓝 (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<VAR>t : Set E<VAR>hts : t ⊆ s<VAR>ht : IsOpen t<VAR>xt : x ∈ t<GOAL>f '' s ∈ 𝓝 (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<VAR>t : Set E<VAR>hts : t ⊆ s<VAR>ht : IsOpen t<VAR>xt : x ∈ t<VAR>this : f '' t ∈ 𝓝 (f x)<GOAL>f '' s ∈ 𝓝 (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : Nonempty ι<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<GOAL>l (sSup s) = sSup (l '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<GOAL>Set.range ⇑(comap f) = zeroLocus ↑(ker f)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<GOAL>⇑(comap f) '' Set.univ = zeroLocus ↑(ker f)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<GOAL>Set.univ = zeroLocus ↑⊥
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>A : ℝ<VAR>x : α<VAR>h : |f x| < A<GOAL>truncation f A x = f x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>A : ℝ<VAR>x : α<VAR>h : |f x| < A<GOAL>f x ∉ Set.Ioc (-A) A → 0 = f x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>A : ℝ<VAR>x : α<VAR>h : |f x| < A<VAR>H : f x ∉ Set.Ioc (-A) A<GOAL>f x ∈ Set.Ioc (-A) A
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n✝ m n : ℕ<VAR>h : orderOf x ∣ n<GOAL>x ^ n = 1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x : V<VAR>p : Submodule K V<GOAL>p ⩿ span K {x} ⊔ p
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x : V<VAR>p q : Submodule K V<VAR>hpq : p < q<VAR>hqp : q < span K {x} ⊔ p<GOAL>span K {x} ⊔ p ≤ q
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x : V<VAR>p q : Submodule K V<VAR>hpq : p < q<VAR>hqp : q < span K {x} ⊔ p<VAR>y : V<VAR>hyq : y ∈ q<VAR>hyp : y ∉ p<GOAL>span K {x} ⊔ p ≤ q
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x : V<VAR>p q : Submodule K V<VAR>hpq : p < q<VAR>hqp : q < span K {x} ⊔ p<VAR>c : K<VAR>z : V<VAR>hz : z ∈ p<VAR>hyq : c • x + z ∈ q<VAR>hyp : c • x + z ∉ p<GOAL>span K {x} ⊔ p ≤ q
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x : V<VAR>p q : Submodule K V<VAR>hpq : p < q<VAR>hqp : q < span K {x} ⊔ p<VAR>z : V<VAR>hz : z ∈ p<VAR>hyq : 0 • x + z ∈ q<VAR>hyp : 0 • x + z ∉ p<GOAL>span K {x} ⊔ p ≤ q
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x : V<VAR>p q : Submodule K V<VAR>hpq : p < q<VAR>hqp : q < span K {x} ⊔ p<VAR>c : K<VAR>z : V<VAR>hz : z ∈ p<VAR>hyq : c • x + z ∈ q<VAR>hyp : c • x + z ∉ p<VAR>hc : c ≠ 0<GOAL>span K {x} ⊔ p ≤ q
<VAR>α : Type u_1<VAR>inst✝⁴ : DistribLattice α<VAR>inst✝³ : OrderBot α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidablePred SupIrred<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet (a ⊓ b)) = Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a) ∩ Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet b)
<VAR>α : Type u_1<VAR>inst✝⁴ : DistribLattice α<VAR>inst✝³ : OrderBot α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidablePred SupIrred<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>Fintype.finsetOrderIsoSet.symm (birkhoffSet a ∩ birkhoffSet b) = Fintype.finsetOrderIsoSet.symm (birkhoffSet a) ∩ Fintype.finsetOrderIsoSet.symm (birkhoffSet b)
<VAR>u : ℤˣ<GOAL>u ^ 2 = 1
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>p✝ p' : Submodule R M<VAR>q q' : Submodule R₂ M₂<VAR>x✝ : M<VAR>σ₂₁ : R₂ →+* R<VAR>inst✝³ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝² : RingHomInvPair σ₂₁ σ₁₂<VAR>F : Type u_9<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>i : Injective ⇑f<VAR>p : Submodule R M<VAR>x : ↥(map f p)<GOAL>f ↑((equivMapOfInjective f i p).symm x) = ↑x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>i j : ι<VAR>a : 𝒜 i<VAR>b : ℬ j<GOAL>(((TensorProduct.directSum R R 𝒜 ℬ).trans (LinearEquiv.ofLinear (gradedCommAux R 𝒜 ℬ) (gradedCommAux R ℬ 𝒜) ⋯ ⋯)).trans (TensorProduct.directSum R R ℬ 𝒜).symm) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j) b) = (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>i j : ι<VAR>a : 𝒜 i<VAR>b : ℬ j<GOAL>(TensorProduct.directSum R R ℬ 𝒜).symm ((gradedCommAux R 𝒜 ℬ) ((TensorProduct.directSum R R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j) b))) = (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>j : ι<VAR>hj : ¬c.Rel j (c.next j)<GOAL>(desc φ α hα).f j = sndX φ j ≫ α.f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp' : p ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f g : α → β<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : ∀ x ∈ s, dist (f x) (g x) ≤ c<VAR>hp : ¬p = 0<VAR>this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x => c) x‖<GOAL>eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp' : p ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f g : α → β<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : ∀ x ∈ s, dist (f x) (g x) ≤ c<VAR>hp : ¬p = 0<VAR>this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x => c) x‖<GOAL>eLpNorm (s.indicator fun x => c) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp' : p ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f g : α → β<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : ∀ x ∈ s, dist (f x) (g x) ≤ c<VAR>hp : ¬p = 0<VAR>this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x => c) x‖<GOAL>↑‖c‖₊ * μ s ^ (1 / p.toReal) ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp' : p ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f g : α → β<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : ∀ x ∈ s, dist (f x) (g x) ≤ c<VAR>hp : ¬p = 0<VAR>this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x => c) x‖<GOAL>↑‖c‖₊ = ENNReal.ofReal c
<VAR>cs : List Char<VAR>c : Char<VAR>cs' : List Char<GOAL>(if { byteIdx := utf8Len cs + c.utf8Size } = 0 then 0 else utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + c.utf8Size }) = { byteIdx := utf8Len cs }
<VAR>cs : List Char<VAR>c : Char<VAR>cs' : List Char<GOAL>utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + c.utf8Size } = { byteIdx := utf8Len cs }
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>inst✝ : Subsingleton α<VAR>g : α → β<VAR>x y : α<GOAL>f x = g y ↔ f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>inst✝ : Subsingleton α<VAR>g : α → β<VAR>x y : α<VAR>h : f x = g y<VAR>z : α<GOAL>f z = g z
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>inst✝ : Subsingleton α<VAR>g : α → β<VAR>x y : α<VAR>h : f = g<GOAL>f x = g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<VAR>f : α → β<GOAL>MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), MapsTo f s (t i j)
<VAR>p q : ℤ[X]<GOAL>p.IsUnitTrinomial ↔ p.support.card = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
<VAR>p q : ℤ[X]<VAR>hp : p.support.card = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)<GOAL>p.IsUnitTrinomial
<VAR>q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>x y z : ℤ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<VAR>hp : (C x * X ^ k + C y * X ^ m + C z * X ^ n).support.card = 3 ∧ ∀ k_1 ∈ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)<GOAL>(C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial