ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : NoZeroDivisors 𝕜<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : ContinuousAdd 𝕜<VAR>inst✝³ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>φ ψ : ↑(characterSpace 𝕜 A)<VAR>h : RingHom.ker φ = RingHom.ker ψ<VAR>x : A<VAR>this : x - (algebraMap 𝕜 A) (ψ x) ∈ RingHom.ker φ<GOAL>φ x = ψ x
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>inst✝³ : Abelian C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>IsZero (((Tor' C (n + 1)).obj X).obj Y)
<VAR>a b c d m k✝ : ℕ<VAR>p q : ℕ → Prop<VAR>k : ℕ<VAR>h1 : 0 < m * k<VAR>h2 : m * k < m<GOAL>False
<VAR>a b c d m k : ℕ<VAR>p q : ℕ → Prop<VAR>h1 : 0 < m * 0<VAR>h2 : m * 0 < m<GOAL>False
<VAR>a b c d m k✝ : ℕ<VAR>p q : ℕ → Prop<VAR>k : ℕ<VAR>h1 : 0 < m * k<VAR>h2 : m * k < m<VAR>hk : k > 0<GOAL>False
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : DecidableEq F<GOAL>ringChar ℂ ≠ ringChar F
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<GOAL>(summand a b σ) v + (summand a b (swap i j • σ)) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>(summand a b (Quotient.mk'' σ)) v + (summand a b (swap i j • Quotient.mk'' σ)) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>(Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v + (Perm.sign (swap i j • σ) • MultilinearMap.domDomCongr (swap i j • σ) ((↑a).domCoprod ↑b)) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>(Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v + ((-1 * Perm.sign σ) • MultilinearMap.domDomCongr (swap i j * σ) ((↑a).domCoprod ↑b)) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>(Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) + -(Perm.sign σ • (↑a fun i_1 => v ((swap i j) (σ (Sum.inl i_1)))) ⊗ₜ[R'] ↑b fun i_1 => v ((swap i j) (σ (Sum.inr i_1)))) = 0
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx1 : 0 ≤ x<VAR>hx2 : x ≤ 1<VAR>hz : 0 ≤ z<GOAL>x ^ z ≤ 1
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx1 : 0 ≤ x<VAR>hx2 : x ≤ 1<VAR>hz : 0 ≤ z<GOAL>x ^ z ≤ 1 ^ z
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : L<GOAL>CompleteLattice.Independent fun χ => weightSpaceOf M χ x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : L<GOAL>CompleteLattice.Independent fun i => ↑(weightSpaceOf M i x)
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<VAR>tU tV : (subsheafToTypes P).presheaf.stalk x<VAR>h : stalkToFiber P x tU = stalkToFiber P x tV<GOAL>tU = tV
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<VAR>tU tV : (subsheafToTypes P).presheaf.stalk x<VAR>h : stalkToFiber P x tU = stalkToFiber P x tV<VAR>Q : ∃ W s, ∃ (hW : P.pred s), tU = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩ ∧ tV = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩ := ?refine_1<GOAL>tU = tV
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<VAR>tU tV : (subsheafToTypes P).presheaf.stalk x<VAR>h : stalkToFiber P x tU = stalkToFiber P x tV<GOAL>∃ W s, ∃ (hW : P.pred s), tU = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩ ∧ tV = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<VAR>tV : (subsheafToTypes P).presheaf.stalk x<VAR>U : (OpenNhds x)ᵒᵖ<VAR>fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1<VAR>hU : P.pred fU<VAR>h : stalkToFiber P x (colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) U ⟨fU, hU⟩) = stalkToFiber P x tV<GOAL>∃ W s, ∃ (hW : P.pred s), colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) U ⟨fU, hU⟩ = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩ ∧ tV = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<VAR>U : (OpenNhds x)ᵒᵖ<VAR>fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1<VAR>hU : P.pred fU<VAR>V : (OpenNhds x)ᵒᵖ<VAR>fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1<VAR>hV : P.pred fV<VAR>h : stalkToFiber P x (colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) U ⟨fU, hU⟩) = stalkToFiber P x (colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) V ⟨fV, hV⟩)<GOAL>∃ W s, ∃ (hW : P.pred s), colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) U ⟨fU, hU⟩ = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩ ∧ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) V ⟨fV, hV⟩ = (subsheafToTypes P).presheaf.germ ⟨x, ⋯⟩ ⟨s, hW⟩
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<VAR>U : (OpenNhds x)ᵒᵖ<VAR>fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1<VAR>hU : P.pred fU<VAR>V : (OpenNhds x)ᵒᵖ<VAR>fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1<VAR>hV : P.pred fV<VAR>h : stalkToFiber P x (colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) U ⟨fU, hU⟩) = stalkToFiber P x (colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj (subsheafToTypes P).presheaf) V ⟨fV, hV⟩)<GOAL>∃ W s, ∃ (hW : P.pred s), colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨s, hW⟩ ∧ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨s, hW⟩
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<VAR>U : (OpenNhds x)ᵒᵖ<VAR>fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1<VAR>hU : P.pred fU<VAR>V : (OpenNhds x)ᵒᵖ<VAR>fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1<VAR>hV : P.pred fV<VAR>h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩<GOAL>∃ W s, ∃ (hW : P.pred s), colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨s, hW⟩ ∧ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨s, hW⟩
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>U : (OpenNhds x)ᵒᵖ<VAR>fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1<VAR>hU : P.pred fU<VAR>V : (OpenNhds x)ᵒᵖ<VAR>fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1<VAR>hV : P.pred fV<VAR>h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩<VAR>W : OpenNhds x<VAR>iU : W ⟶ unop U<VAR>iV : W ⟶ unop V<VAR>w : ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)<GOAL>∃ W s, ∃ (hW : P.pred s), colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨s, hW⟩ ∧ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨s, hW⟩
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>U : (OpenNhds x)ᵒᵖ<VAR>fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1<VAR>hU : P.pred fU<VAR>V : (OpenNhds x)ᵒᵖ<VAR>fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1<VAR>hV : P.pred fV<VAR>h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩<VAR>W : OpenNhds x<VAR>iU : W ⟶ unop U<VAR>iV : W ⟶ unop V<VAR>w : ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)<GOAL>(unop (op W)).obj ⟶ (unop U).obj
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : LocalPredicate T<VAR>x : ↑X<VAR>U : (OpenNhds x)ᵒᵖ<VAR>fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1<VAR>hU : P.pred fU<VAR>V : (OpenNhds x)ᵒᵖ<VAR>fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1<VAR>hV : P.pred fV<VAR>h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩<VAR>W : OpenNhds x<VAR>iU : W ⟶ unop U<VAR>iV : W ⟶ unop V<VAR>w : ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)<GOAL>colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨fun w => fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w), ⋯⟩ ∧ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ = (subpresheafToTypes P.toPrelocalPredicate).germ ⟨x, ⋯⟩ ⟨fun w => fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w), ⋯⟩
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : Integrable f ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : Integrable f ρ<VAR>hf_ae : AEStronglyMeasurable f ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧ Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst<VAR>hf_ae : AEStronglyMeasurable f ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)
<VAR>u : ℂ<VAR>hu : 0 < u.re<GOAL>u.betaIntegral 1 = 1 / u
<VAR>u : ℂ<VAR>hu : 0 < u.re<GOAL>∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) = 1 / u
<VAR>u : ℂ<VAR>hu : 0 < u.re<GOAL>(↑1 ^ (u - 1 + 1) - ↑0 ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u
<VAR>u : ℂ<VAR>hu : 0 < u.re<GOAL>-1 < (u - 1).re
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddZeroClass G<VAR>f : k[G]<VAR>r : k<VAR>x a : G<GOAL>a + 0 = x ↔ a = x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>(aeval (Function.uncurry fun i => (![] i).coeff)) (wittZero p n) = 0
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>f : (m' → R) →ₗ[R] m → R<GOAL>(toMatrix₂' R) (B.compl₂ f) = (toMatrix₂' R) B * toMatrix' f
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>f : (m' → R) →ₗ[R] m → R<GOAL>(toMatrix₂' R) (B.compl₁₂ id f) = (toMatrix₂' R) (B ∘ₗ id) * toMatrix' f
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>arctan x⁻¹ = π / 2 - arctan x
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>-(π / 2) < π / 2 - arctan x
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>π / 2 - arctan x < π / 2
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasLeftHomology<VAR>A : C<VAR>f₁ f₂ : S.leftHomology ⟶ A<VAR>h : S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂<GOAL>f₁ = f₂
<VAR>Γ : Type u_1<VAR>R✝ : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : Semiring R✝<VAR>α : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>s t : SummableFamily Γ R α<GOAL>(s - t).hsum = s.hsum - t.hsum
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>n : ℤ<VAR>H : ℤ → Prop := fun n => ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles<GOAL>H n
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>n : ℤ<VAR>H : ℤ → Prop := fun n => ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles<VAR>H_zero : H 0<GOAL>H n
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>n : ℤ<VAR>H : ℤ → Prop := fun n => ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles<VAR>H_zero : H 0<VAR>H_one : H 1<GOAL>H n
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>n : ℤ<VAR>H : ℤ → Prop := fun n => ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles<VAR>H_zero : H 0<VAR>H_one : H 1<VAR>H_neg_one : H (-1)<GOAL>H n
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>n : ℤ<VAR>H : ℤ → Prop := fun n => ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles<VAR>H_zero : H 0<VAR>H_one : H 1<VAR>H_neg_one : H (-1)<VAR>H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c<GOAL>H n
<VAR>α : Type u<VAR>inst✝ : CommMonoid α<VAR>x y : α<VAR>ux uy : αˣ<GOAL>x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : AddCommMonoid E<VAR>n : ι<GOAL>stoppedProcess u τ n = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : AddCommMonoid E<VAR>n : ι<VAR>h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n<GOAL>stoppedProcess u τ n = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : AddCommMonoid E<VAR>n : ι<VAR>h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n<GOAL>{a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) (Finset.Iio n), {ω | τ ω = i}.indicator (u i) = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l₁ l₂ : Filter α<GOAL>𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l₁ l₂ : Filter α<VAR>h : 𝓝 l₁ ≤ 𝓝 l₂<GOAL>l₁ ≤ l₂
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l₁ l₂ : Filter α<VAR>h : 𝓝 l₁ ≤ 𝓝 l₂<GOAL>⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : ListBlank Γ<VAR>n : ℕ<GOAL>(map f l).nth n = f.f (l.nth n)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l✝ : ListBlank Γ<VAR>n : ℕ<VAR>l : List Γ<GOAL>(map f ⟦l⟧).nth n = f.f (nth ⟦l⟧ n)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l✝ : ListBlank Γ<VAR>n : ℕ<VAR>l : List Γ<GOAL>(map f (mk l)).nth n = f.f ((mk l).nth n)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l✝ : ListBlank Γ<VAR>n : ℕ<VAR>l : List Γ<GOAL>(Option.map f.f (l.get? n)).iget = f.f (l.get? n).iget
<VAR>α : Type u_1<VAR>inst✝ : Field α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : ad ≠ 0<VAR>hbd : bd ≠ 0<VAR>hgcd : gcd ≠ 0<GOAL>(a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>min (min a b) c = min a (min b c)
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>min (min a b) c ≤ a
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>min (min a b) c ≤ min b c
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>hxy : x ≠ y<GOAL>openSegment 𝕜 x y = Ioo (min x y) (max x y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>hxy : x ≠ y<VAR>h : x < y<GOAL>openSegment 𝕜 x y = Ioo (min x y) (max x y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>hxy : x ≠ y<VAR>h : y < x<GOAL>openSegment 𝕜 x y = Ioo (min x y) (max x y)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂<GOAL>Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>h : (fun y => ∃ x, f x = y) = fun x => True<GOAL>Surjective f