ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B✝ B' I J D X : Set α<VAR>e f : α<VAR>M₁ M₂ : Matroid α<VAR>hE : M₁.E = M₂.E<VAR>h : ∀ I ⊆ M₁.E, M₁.Indep I ↔ M₂.Indep I<VAR>h' : ∀ (I : Set α), M₁.Indep I ↔ M₂.Indep I := fun I => Or.elim (em (I ⊆ M₁.E)) (h I) fun h' => iff_of_false (fun hi => h' (Indep.subset_ground hi)) fun hi => h' (LE.le.trans_eq (Indep.subset_ground hi) (Eq.symm hE))<VAR>B : Set α<VAR>x✝ : B ⊆ M₁.E<GOAL>M₁.Base B ↔ M₂.Base B
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hR : 0 < ringChar R<VAR>φ : AddChar R ℂ<VAR>a : R<GOAL>(starRingEnd ℂ) (φ a) = φ⁻¹ a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hR : 0 < ringChar R<VAR>φ : AddChar R ℂ<VAR>a : R<GOAL>(starRingEnd ℂ) (φ a) = ((↑(starRingEnd ℂ)).compAddChar φ) a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h_left : IntegrableOn f (Iic b) μ<VAR>h_right : IntegrableOn f (Ioi b) μ<GOAL>∫ (x : ℝ) in Iic b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h_left : IntegrableOn f (Iic b) μ<VAR>h_right : IntegrableOn f (Ioi b) μ<GOAL>μ = μ.restrict (Iic b ∪ Ioi b)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>pn : p.natDegree ≤ n<VAR>p1 : p.coeff n = 1<VAR>a✝ : Nontrivial R<GOAL>p.leadingCoeff = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>pn : p.natDegree ≤ n<VAR>p1 : p.coeff n = 1<VAR>a✝ : Nontrivial R<GOAL>p.coeff n ≠ 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Inducing f<GOAL>(f x ~ᵢ f y) ↔ (x ~ᵢ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : OpensMeasurableSpace α<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>f✝ : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝³ : CompleteSpace F<VAR>inst✝² : LocallyCompactSpace 𝕜<VAR>inst✝¹ : MeasurableSpace 𝕜<VAR>inst✝ : OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither α F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<GOAL>StronglyMeasurable fun p => deriv (f p.1) p.2
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : OpensMeasurableSpace α<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>f✝ : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝³ : CompleteSpace F<VAR>inst✝² : LocallyCompactSpace 𝕜<VAR>inst✝¹ : MeasurableSpace 𝕜<VAR>inst✝ : OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither α F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>hα : SecondCountableTopology α<GOAL>StronglyMeasurable fun p => deriv (f p.1) p.2
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : OpensMeasurableSpace α<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>f✝ : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝³ : CompleteSpace F<VAR>inst✝² : LocallyCompactSpace 𝕜<VAR>inst✝¹ : MeasurableSpace 𝕜<VAR>inst✝ : OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither α F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>hF : SecondCountableTopology F<GOAL>StronglyMeasurable fun p => deriv (f p.1) p.2
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h : IsHausdorff I N<VAR>f : M →ₗ[R] N<VAR>g : Hausdorffification I M →ₗ[R] N<VAR>hg : g ∘ₗ of I M = f<VAR>x✝ : Hausdorffification I M<VAR>x : M<GOAL>g ((of I M) x) = (lift I f) ((of I M) x)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<VAR>f : ℕ → L → R := fun k => k • χ₁ + χ₂<GOAL>∀ᶠ (k : ℕ) in Filter.atTop, weightSpace M (k • χ₁ + χ₂) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<VAR>f : ℕ → L → R := fun k => k • χ₁ + χ₂<GOAL>Injective f
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<VAR>f : ℕ → L → R := fun k => k • χ₁ + χ₂<VAR>k l : ℕ<VAR>hkl : f k = f l<GOAL>k = l
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<VAR>f : ℕ → L → R := fun k => k • χ₁ + χ₂<VAR>k l : ℕ<VAR>hkl : ↑k • χ₁ = ↑l • χ₁<GOAL>k = l
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a⁻¹ ≤ b / c ↔ c ≤ a * b
<VAR>X₁ X₂ Y : TopCat<VAR>f : C(↑X₁, ↑Y)<VAR>g : C(↑X₂, ↑Y)<VAR>x₀ x₁ : ↑X₁<VAR>x₂ x₃ : ↑X₂<VAR>p : Path x₀ x₁<VAR>q : Path x₂ x₃<VAR>hfg : ∀ (t : ↑I), f (p t) = g (q t)<GOAL>(π.map f).map ⟦p⟧ = hcast ⋯ ≫ (π.map g).map ⟦q⟧ ≫ hcast ⋯
<VAR>X₁ X₂ Y : TopCat<VAR>f : C(↑X₁, ↑Y)<VAR>g : C(↑X₂, ↑Y)<VAR>x₀ x₁ : ↑X₁<VAR>x₂ x₃ : ↑X₂<VAR>p : Path x₀ x₁<VAR>q : Path x₂ x₃<VAR>hfg : ∀ (t : ↑I), f (p t) = g (q t)<GOAL>HEq ((π.map f).map ⟦p⟧) ((π.map g).map ⟦q⟧)
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>x✝ : Multiset α<VAR>hx✝ : x✝ ∈ Set.range val<VAR>s : Finset α<VAR>t : Multiset α<VAR>ht : t ∈ Set.Icc x✝ s.val<GOAL>t ∈ Set.range val
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMulZeroClass α β<VAR>inst✝ : CeilDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>(f ⌈/⌉ a).support ⊆ f.support
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<GOAL>(-a).val = if a = 0 then 0 else n - a.val
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<GOAL>(n - a.val) % n = if a = 0 then 0 else n - a.val
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<VAR>h : ¬a = 0<GOAL>(n - a.val) % n = if a = 0 then 0 else n - a.val
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<VAR>h : ¬a = 0<GOAL>(n - a.val) % n = n - a.val
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<VAR>h : ¬a = 0<GOAL>n - a.val < n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<VAR>h : ¬a = 0<GOAL>0 < a.val
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<VAR>h : a.val ≤ 0<GOAL>a = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>f : G → E<VAR>s : Set G<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) (f x) < r
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>1 * M = M
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>span R {1} * span R ↑M = M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>↑(⨆ i, f i).compl = ↑(⨆ i, (f i).compl)
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>alternatization (a.domCoprod b) = (alternatization a).domCoprod (alternatization b)
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>↑(alternatization (a.domCoprod b)) = ↑((alternatization a).domCoprod (alternatization b))
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>∑ xbar ∈ Finset.image Quotient.mk'' Finset.univ, ∑ y ∈ Finset.filter (fun x => ⟦x⟧ = xbar) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) = ∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand (alternatization a) (alternatization b) σ
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<GOAL>∑ y ∈ Finset.filter (fun x => ⟦x⟧ = σ) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) = domCoprod.summand (alternatization a) (alternatization b) σ
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∑ y ∈ Finset.filter (fun x => ⟦x⟧ = Quotient.mk'' σ) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∑ y ∈ Finset.filter (fun x => x⁻¹ * σ ∈ (Perm.sumCongrHom ιa ιb).range) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∑ x ∈ Finset.filter ((fun x => x⁻¹ * σ ∈ (Perm.sumCongrHom ιa ιb).range) ∘ ⇑(Equiv.toEmbedding (Equiv.mulLeft σ))) Finset.univ, Perm.sign ((Equiv.toEmbedding (Equiv.mulLeft σ)) x) • domDomCongr ((Equiv.toEmbedding (Equiv.mulLeft σ)) x) (a.domCoprod b) = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∑ x : Perm ιa × Perm ιb, Perm.sign (σ * (Perm.sumCongrHom ιa ιb) x) • domDomCongr (σ * (Perm.sumCongrHom ιa ιb) x) (a.domCoprod b) = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∑ x : Perm ιa × Perm ιb, Perm.sign (σ * (Perm.sumCongrHom ιa ιb) x) • domDomCongr (σ * (Perm.sumCongrHom ιa ιb) x) (a.domCoprod b) = ∑ x : Perm ιa × Perm ιb, Perm.sign σ • (domDomCongrEquiv σ) (Perm.sign x.1 • Perm.sign x.2 • (domDomCongr x.1 a).domCoprod (domDomCongr x.2 b))
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<VAR>σ : Perm (ιa ⊕ ιb)<VAR>al : Perm ιa<VAR>ar : Perm ιb<GOAL>Perm.sign (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) • domDomCongr (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) (a.domCoprod b) = Perm.sign σ • (domDomCongrEquiv σ) (Perm.sign al • Perm.sign ar • (domDomCongr al a).domCoprod (domDomCongr ar b))
<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 : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<VAR>σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)<VAR>σ : Perm (ιa ⊕ ιb)<VAR>al : Perm ιa<VAR>ar : Perm ιb<GOAL>Perm.sign (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) • domDomCongr (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) (a.domCoprod b) = Perm.sign σ • Perm.sign al • Perm.sign ar • domDomCongr σ ((domDomCongr al a).domCoprod (domDomCongr ar b))
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<GOAL>dist x y = dist y x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.102700, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>(-φ₁).τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + (-φ₂).τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.102700, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>-φ₂.τ₁ + -(S₁.f ≫ h.h₁ + h.h₀) = -S₁.f ≫ h.h₁ + -h.h₀ + -φ₂.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.102700, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>(-φ₁).τ₂ = S₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + (-φ₂).τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.102700, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>-φ₂.τ₂ + -(S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) = -S₁.g ≫ h.h₂ + -h.h₁ ≫ S₂.f + -φ₂.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.102700, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>(-φ₁).τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + (-φ₂).τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.102700, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>-(h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = -h.h₃ + -h.h₂ ≫ S₂.g + -φ₂.τ₃
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<GOAL>M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), Commute (stdBasisMatrix i j 1) M
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>x✝ : M ∈ Set.range ⇑(scalar n)<VAR>i j : n<VAR>r : α<VAR>hr : (scalar n) r = M<GOAL>Commute ((scalar n) r) (stdBasisMatrix i j 1)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>x✝ : M ∈ Set.range ⇑(scalar n)<VAR>i j : n<VAR>r : α<VAR>hr : (scalar n) r = M<GOAL>r • stdBasisMatrix i j 1 = MulOpposite.op r • stdBasisMatrix i j 1
<VAR>n : Int<GOAL>mkRat n 0 = 0
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>x : K<GOAL>(mixedEmbedding K) x ∈ convexBodyLT K f ↔ ∀ (w : InfinitePlace K), w x < ↑(f w)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>IsClosed ((dualPairing 𝕜 E).flip.polar s)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>IsClosed (⋂ x ∈ s, {y | ‖((dualPairing 𝕜 E) y) x‖ ≤ 1})
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>z : E<VAR>x✝ : z ∈ s<GOAL>IsClosed {y | ‖((dualPairing 𝕜 E) y) z‖ ≤ 1}
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>α : Type u_4<GOAL>IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a = 0<GOAL>fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a ≠ 0<GOAL>fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a ≠ 0<GOAL>fract a = a + 1 - ↑⌈a⌉
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a ≠ 0<GOAL>↑⌈a⌉ = ↑⌊a⌋ + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a ≠ 0<GOAL>⌈a⌉ = ⌊a⌋ + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a ≠ 0<GOAL>↑(⌊a⌋ + 1) - 1 < a ∧ a ≤ ↑(⌊a⌋ + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a ≠ 0<GOAL>↑(⌊a⌋ + 1) - 1 < a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>ha : fract a ≠ 0<GOAL>0 < fract a