ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : EvenHom Q A<VAR>x : CliffordAlgebra Q<VAR>x_property : x ∈ even Q<VAR>val✝ : CliffordAlgebra Q<VAR>property✝ : val✝ ∈ even Q<GOAL>(((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) ↑⟨val✝, property✝⟩)) ↑⟨x, x_property⟩).1 = (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩
<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : EvenHom Q A<VAR>x : CliffordAlgebra Q<VAR>x_property : x ∈ even Q<VAR>val✝ : CliffordAlgebra Q<VAR>property✝ : val✝ ∈ even Q<GOAL>(((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) val✝)) x).1 = (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>a : R<VAR>x y : M<GOAL>polar (⇑Q) x (a • y) = a • polar (⇑Q) x y
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>s : Set V<VAR>inst✝¹ : Nonempty ↑s<VAR>inst✝ : Fintype ↑s<VAR>lin_ind : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>card_eq : s.toFinset.card = finrank K V<GOAL>⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯) = Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>Ici x = {x} ↔ IsTop x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<VAR>h : Ici x = {x}<VAR>y : α<GOAL>y ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<VAR>h : Ici x = {x}<VAR>y : α<VAR>H : x < y<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<VAR>h : Ici x = {x}<VAR>y : α<VAR>H : x < y<VAR>this : y ∈ Ici x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<VAR>h : Ici x = {x}<VAR>y : α<VAR>H : x < y<VAR>this : y = x<GOAL>False
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<GOAL>Injective ⇑(LinearMap.lTensor M₃ g₁)
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<GOAL>∀ (a : M₃ ⊗[R] N₁), (LinearMap.lTensor M₃ g₁) a = 0 → a = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>x : M₃ ⊗[R] N₁<VAR>hx : (LinearMap.lTensor M₃ g₁) x = 0<GOAL>x = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>x : M₂ ⊗[R] N₁<VAR>hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0<GOAL>(LinearMap.rTensor N₁ f₂) x = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>x : M₂ ⊗[R] N₁<VAR>hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0<VAR>this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0<GOAL>(LinearMap.rTensor N₁ f₂) x = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>x : M₂ ⊗[R] N₁<VAR>hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0<VAR>this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0<VAR>y : M₁ ⊗[R] N₂<VAR>hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x<GOAL>(LinearMap.rTensor N₁ f₂) x = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>x : M₂ ⊗[R] N₁<VAR>hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0<VAR>this✝ : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0<VAR>y : M₁ ⊗[R] N₂<VAR>hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x<VAR>this : (LinearMap.lTensor M₁ g₂) y = 0<GOAL>(LinearMap.rTensor N₁ f₂) x = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>x : M₂ ⊗[R] N₁<VAR>hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0<VAR>this✝ : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0<VAR>z : M₁ ⊗[R] N₁<VAR>hy : (LinearMap.rTensor N₂ f₁) ((LinearMap.lTensor M₁ g₁) z) = (LinearMap.lTensor M₂ g₁) x<VAR>this : (LinearMap.lTensor M₁ g₂) ((LinearMap.lTensor M₁ g₁) z) = 0<GOAL>(LinearMap.rTensor N₁ f₂) x = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>z : M₁ ⊗[R] N₁<VAR>this✝ : (LinearMap.lTensor M₁ g₂) ((LinearMap.lTensor M₁ g₁) z) = 0<VAR>hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) ((LinearMap.rTensor N₁ f₁) z)) = 0<VAR>this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) ((LinearMap.rTensor N₁ f₁) z)) = 0<VAR>hy : (LinearMap.rTensor N₂ f₁) ((LinearMap.lTensor M₁ g₁) z) = (LinearMap.lTensor M₂ g₁) ((LinearMap.rTensor N₁ f₁) z)<GOAL>(LinearMap.rTensor N₁ f₂) ((LinearMap.rTensor N₁ f₁) z) = 0
<VAR>R : Type u_7<VAR>S : Type ?u.148131<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : LocalRing R<VAR>M : Type ?u.148593<VAR>N : Type ?u.148596<VAR>inst✝¹⁷ : AddCommGroup M<VAR>inst✝¹⁶ : AddCommGroup N<VAR>inst✝¹⁵ : Module R M<VAR>inst✝¹⁴ : Module R N<VAR>P : Type ?u.149736<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R M₃<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : AddCommGroup N₂<VAR>inst✝² : Module R N₂<VAR>inst✝¹ : AddCommGroup N₃<VAR>inst✝ : Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Surjective ⇑f₂<VAR>hgexact : Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Surjective ⇑g₂<VAR>hfinj : Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Injective ⇑(LinearMap.lTensor M₂ g₁)<VAR>z : M₁ ⊗[R] N₁<VAR>this✝ : (LinearMap.lTensor M₁ g₂) ((LinearMap.lTensor M₁ g₁) z) = 0<VAR>hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) ((LinearMap.rTensor N₁ f₁) z)) = 0<VAR>this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) ((LinearMap.rTensor N₁ f₁) z)) = 0<VAR>hy : (LinearMap.rTensor N₂ f₁) ((LinearMap.lTensor M₁ g₁) z) = (LinearMap.lTensor M₂ g₁) ((LinearMap.rTensor N₁ f₁) z)<GOAL>(LinearMap.rTensor N₁ 0) z = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Lattice β<VAR>f : α → β<VAR>s : Set α<VAR>a b : α<VAR>hf : AntitoneOn f [[a, b]]<GOAL>MapsTo f [[a, b]] [[f a, f b]]
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<GOAL>dist (dist x y) (dist x z) ≤ dist y z
<VAR>R : Type u_1<VAR>inst✝¹ : Rack R<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>f : R →◃ Quandle.Conj G<VAR>a b c : PreEnvelGroup R<GOAL>mapAux f ((a.mul b).mul c) = mapAux f (a.mul (b.mul c))
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>a : A 0<GOAL>(of A 0) (a ^ 0) = (of A 0) a ^ 0
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>a : A 0<VAR>n : ℕ<GOAL>(of A 0) (a ^ (n + 1)) = (of A 0) a ^ (n + 1)
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>LSeriesSummable ((fun n => χ ↑n) * f) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<VAR>n : ℕ<GOAL>‖((fun n => χ ↑n) * f) n‖ ≤ ‖f n‖
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<VAR>n : ℕ<GOAL>‖χ ↑n‖ * ‖f n‖ ≤ ‖f n‖
<VAR>C : Type u_1<VAR>inst✝¹⁵ : Category.{u_6, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹⁴ : Category.{u_4, u_2} A<VAR>inst✝¹³ : HasWeakSheafify J A<VAR>inst✝¹² : (constantSheaf J A).Faithful<VAR>inst✝¹¹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝¹⁰ : Category.{u_5, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁹ : HasWeakSheafify J A<VAR>inst✝⁸ : HasWeakSheafify J B<VAR>inst✝⁷ : (constantSheaf J A).Faithful<VAR>inst✝⁶ : (constantSheaf J A).Full<VAR>inst✝⁵ : (constantSheaf J B).Faithful<VAR>inst✝⁴ : (constantSheaf J B).Full<VAR>inst✝³ : J.PreservesSheafification U<VAR>inst✝² : J.HasSheafCompose U<VAR>F : Sheaf J A<VAR>inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms<VAR>inst✝ : IsDiscrete J ht ((sheafCompose J U).obj F)<VAR>f : (sheafCompose J U).obj (((sheafSections J A).obj (op t) ⋙ constantSheaf J A).obj F) ⟶ (sheafCompose J U).obj ((𝟭 (Sheaf J A)).obj F) := (sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)<GOAL>IsDiscrete J ht F
<VAR>C : Type u_1<VAR>inst✝¹⁵ : Category.{u_6, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹⁴ : Category.{u_4, u_2} A<VAR>inst✝¹³ : HasWeakSheafify J A<VAR>inst✝¹² : (constantSheaf J A).Faithful<VAR>inst✝¹¹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝¹⁰ : Category.{u_5, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁹ : HasWeakSheafify J A<VAR>inst✝⁸ : HasWeakSheafify J B<VAR>inst✝⁷ : (constantSheaf J A).Faithful<VAR>inst✝⁶ : (constantSheaf J A).Full<VAR>inst✝⁵ : (constantSheaf J B).Faithful<VAR>inst✝⁴ : (constantSheaf J B).Full<VAR>inst✝³ : J.PreservesSheafification U<VAR>inst✝² : J.HasSheafCompose U<VAR>F : Sheaf J A<VAR>inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms<VAR>inst✝ : IsDiscrete J ht ((sheafCompose J U).obj F)<VAR>f : (sheafCompose J U).obj (((sheafSections J A).obj (op t) ⋙ constantSheaf J A).obj F) ⟶ (sheafCompose J U).obj ((𝟭 (Sheaf J A)).obj F) := (sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)<VAR>this : IsIso ((sheafToPresheaf J B).map f)<GOAL>IsDiscrete J ht F
<VAR>C : Type u_1<VAR>inst✝¹⁵ : Category.{u_6, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹⁴ : Category.{u_4, u_2} A<VAR>inst✝¹³ : HasWeakSheafify J A<VAR>inst✝¹² : (constantSheaf J A).Faithful<VAR>inst✝¹¹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝¹⁰ : Category.{u_5, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁹ : HasWeakSheafify J A<VAR>inst✝⁸ : HasWeakSheafify J B<VAR>inst✝⁷ : (constantSheaf J A).Faithful<VAR>inst✝⁶ : (constantSheaf J A).Full<VAR>inst✝⁵ : (constantSheaf J B).Faithful<VAR>inst✝⁴ : (constantSheaf J B).Full<VAR>inst✝³ : J.PreservesSheafification U<VAR>inst✝² : J.HasSheafCompose U<VAR>F : Sheaf J A<VAR>inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms<VAR>inst✝ : IsDiscrete J ht ((sheafCompose J U).obj F)<VAR>f : (sheafCompose J U).obj (((sheafSections J A).obj (op t) ⋙ constantSheaf J A).obj F) ⟶ (sheafCompose J U).obj ((𝟭 (Sheaf J A)).obj F) := (sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)<VAR>this✝ : IsIso ((sheafToPresheaf J B).map f)<VAR>this : IsIso f<GOAL>IsDiscrete J ht F
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>(fun x => x * b) ⁻¹' 1 = {b⁻¹}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrderTop α<VAR>inst✝ : DecidableEq α<VAR>a a✝ : α<GOAL>a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>⨆ g, ⨆ (_ : ↑g ≤ fun a => s.indicator f a), g.lintegral μ ≤ ⨆ g, ⨆ (_ : ↑g ≤ fun a => f a), g.lintegral (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<GOAL>g.lintegral μ ≤ ⨆ g, ⨆ (_ : ↑g ≤ fun a => f a), g.lintegral (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<VAR>this : ↑g ≤ f<GOAL>g.lintegral μ ≤ ⨆ g, ⨆ (_ : ↑g ≤ fun a => f a), g.lintegral (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<VAR>this : ↑g ≤ f<GOAL>g.lintegral μ = g.lintegral (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<VAR>this : ↑g ≤ f<GOAL>∑ x ∈ g.range, x * μ (↑g ⁻¹' {x}) = ∑ y ∈ g.range, y * μ (↑g ⁻¹' {y} ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<VAR>this : ↑g ≤ f<VAR>t : ℝ≥0∞<VAR>H : ¬t = 0<VAR>x : α<GOAL>x ∈ ↑g ⁻¹' {t} ↔ x ∈ ↑g ⁻¹' {t} ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<VAR>this : ↑g ≤ f<VAR>t : ℝ≥0∞<VAR>H : ¬t = 0<VAR>x : α<GOAL>↑g x = t → x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<VAR>this : ↑g ≤ f<VAR>x : α<VAR>H : ¬↑g x = 0<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>g : α →ₛ ℝ≥0∞<VAR>hg : ↑g ≤ fun a => s.indicator f a<VAR>this : ↑g ≤ f<VAR>x : α<VAR>H : x ∉ s<GOAL>↑g x = 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>count a l = l.length ↔ ∀ (b : α), b ∈ l → a = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>(∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true) ↔ ∀ (b : α), b ∈ l → a = b