ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>∑' (i : ℕ), m (s i) ≤ m (⋃ i, s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>⨆ i, ∑ a ∈ Finset.range i, m (s a) ≤ m (⋃ i, s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>n : ℕ<GOAL>∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>n : ℕ<VAR>this : ∑ i ∈ Finset.range n, m (univ ∩ s i) = m (univ ∩ ⋃ i, ⋃ (_ : i < n), s i)<GOAL>∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>n : ℕ<VAR>this : ∑ x ∈ Finset.range n, m (s x) = m (⋃ i, ⋃ (_ : i < n), s i)<GOAL>∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>n : ℕ<VAR>this : ∑ x ∈ Finset.range n, m (s x) = m (⋃ i, ⋃ (_ : i < n), s i)<GOAL>m (⋃ i, ⋃ (_ : i < n), s i) ≤ m (⋃ i, s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : α ≃ β<VAR>e' : β ≃ γ<VAR>e : α ≃ β<VAR>f' : PartialEquiv β γ<VAR>f'' : PartialEquiv γ δ<GOAL>(e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<GOAL>(closure L).toFun ↑∅ = ⊥
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Ici a = Ico ↑a ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝³ : DivInvMonoid G₀<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : ContinuousMul G₀<VAR>f : α → G₀<VAR>s : Set α<VAR>l : Filter α<VAR>inst✝ : TopologicalSpace α<VAR>hf : ContinuousOn f s<VAR>y : G₀<GOAL>ContinuousOn (fun x => f x / y) s
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>b : α<VAR>l : List α<GOAL>insertionSort r (b :: l) ~ b :: l
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X][Y]<VAR>q : R[X]<VAR>x y : R<GOAL>evalEval (f x) (f y) (map (mapRingHom f) p) = f (evalEval x y p)
<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>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : ↥H<VAR>hx : x ∈ corootSpace α<GOAL>(LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) x) = 0
<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>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : ↥H<VAR>hx : x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<GOAL>(LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) x) = 0
<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>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x x✝ : ↥H<VAR>h✝ : x✝ ∈ {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<GOAL>(LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) x✝) = 0
<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>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : ↥H<GOAL>(LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) 0) = 0
<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>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x x✝ : ↥H<VAR>hx✝ : x✝ ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<VAR>y✝ : ↥H<VAR>hy✝ : y✝ ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<VAR>a✝¹ : (LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) x✝) = 0<VAR>a✝ : (LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) y✝) = 0<GOAL>(LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) (x✝ + y✝)) = 0
<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>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : ↥H<VAR>a✝¹ : R<VAR>x✝ : ↥H<VAR>hx✝ : x✝ ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<VAR>a✝ : (LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) x✝) = 0<GOAL>(LinearMap.trace R ↥↑(weightSpaceChain M α χ p q)) ((toEnd R ↥H ↥↑(weightSpaceChain M α χ p q)) (a✝¹ • x✝)) = 0
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>R : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>c : R<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun y => c • f y) (c • f') x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<GOAL>n + b + a = n + (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel G.Adj<VAR>n : ℕ<VAR>a b c : α<VAR>s : Finset α<GOAL>G.cliqueFinset n = ∅ ↔ G.CliqueFree n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m✝ : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x : E<VAR>m : ℕ<VAR>hm : m ∉ Finset.range n<GOAL>((p m) fun x_1 => x) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m✝ : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x : E<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>((p m) fun x_1 => x) = 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>k : ℕ<VAR>h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)<VAR>m : ℕ<GOAL>LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + (m + 1)))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>k : ℕ<VAR>h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)<VAR>m : ℕ<GOAL>LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>k : ℕ<VAR>h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)<VAR>m : ℕ<GOAL>LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<GOAL>0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>x y : γ<GOAL>0 = nndist x y ↔ x = y
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>s : Trident f<VAR>j : J<GOAL>s.π.app zero ≫ f j = s.π.app one
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>factorization (a * b) = factorization a + factorization 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>f x₀ = g x₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<GOAL>∀ (i : ℕ), P.coeff i • Q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<GOAL>∃ n, ∀ m > n, P.coeff m • Q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<GOAL>∀ (n : ℕ), (∀ m > n, P.coeff m • Q = 0) → P.coeff n • Q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<GOAL>P.coeff l • Q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>h✝ : (P.coeff l • Q).natDegree < Q.natDegree<GOAL>P.coeff l • Q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<GOAL>P.coeff l • Q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<GOAL>P.coeff l * Q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<GOAL>P.coeff l * Q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<GOAL>(P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<GOAL>∑ x ∈ antidiagonal (l + m), P.coeff x.1 * Q.coeff x.2 = P.coeff l * Q.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<GOAL>∀ b ∈ antidiagonal (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<GOAL>∀ (a b : ℕ), a + b = l + m → (a = l → ¬b = m) → P.coeff a * Q.coeff b = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<VAR>i j : ℕ<VAR>hij : i + j = l + m<VAR>H : i = l → ¬j = m<GOAL>P.coeff i * Q.coeff j = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<VAR>i j : ℕ<VAR>hij : i + j = l + m<VAR>H : i = l → ¬j = m<VAR>hi : i < l<GOAL>P.coeff i * Q.coeff j = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>m : ℕ := Q.natDegree<VAR>i j : ℕ<VAR>IH : ∀ m > i, P.coeff m • Q = 0<VAR>hl : (P.coeff i • Q).natDegree = Q.natDegree<VAR>hij : i + j = i + m<VAR>H : i = i → ¬j = m<GOAL>P.coeff i * Q.coeff j = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<VAR>hQ : P * Q = 0<VAR>l : ℕ<VAR>IH : ∀ m > l, P.coeff m • Q = 0<VAR>hl : (P.coeff l • Q).natDegree = Q.natDegree<VAR>m : ℕ := Q.natDegree<VAR>i j : ℕ<VAR>hij : i + j = l + m<VAR>H : i = l → ¬j = m<VAR>hi : l < i<GOAL>P.coeff i * Q.coeff j = 0
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : G →ₗᵢ[𝕜] G'<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonUnitalSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x y z : ⨂[R] (i : ι), A i<GOAL>(mul ((mul x) y)) z = (mul x) ((mul y) z)
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonUnitalSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x y z : ⨂[R] (i : ι), A i<GOAL>(LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) mul ∘ₗ mul = (((LinearMap.llcomp R (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) mul.flip ∘ₗ mul)).flip
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonUnitalSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x✝ y✝ z✝ : ⨂[R] (i : ι), A i<VAR>x y z : (i : ι) → A i<GOAL>(((((((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) mul ∘ₗ mul).compMultilinearMap (tprod R)) x).compMultilinearMap (tprod R)) y).compMultilinearMap (tprod R)) z = ((((((((LinearMap.llcomp R (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) mul.flip ∘ₗ mul)).flip.compMultilinearMap (tprod R)) x).compMultilinearMap (tprod R)) y).compMultilinearMap (tprod R)) z
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonUnitalSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x✝ y✝ z✝ : ⨂[R] (i : ι), A i<VAR>x y z : (i : ι) → A i<GOAL>(tprod R) x * (tprod R) y * (tprod R) z = (tprod R) x * ((tprod R) y * (tprod R) z)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>f : C ⟶ D<VAR>hom : (i j : ι) → D.X i ⟶ E.X j<VAR>n : ι<GOAL>(f ≫ nullHomotopicMap hom).f n = (nullHomotopicMap fun i j => f.f i ≫ hom i j).f n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>f : C ⟶ D<VAR>hom : (i j : ι) → D.X i ⟶ E.X j<VAR>n : ι<GOAL>f.f n ≫ (D.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ E.dTo n) = C.dFrom n ≫ f.f (c.next n) ≫ hom (c.next n) n + (f.f n ≫ hom n (c.prev n)) ≫ E.dTo n
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>enc₀ : enc default = Vector.replicate n false<VAR>x✝ : Cfg₁<VAR>l₁ : Option Λ<VAR>v : σ<VAR>T : Tape Γ<GOAL>FRespects (step (tr enc dec M)) (trCfg enc enc₀) (trCfg enc enc₀ { l := l₁, var := v, Tape := T }) (step M { l := l₁, var := v, Tape := T })
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>enc₀ : enc default = Vector.replicate n false<VAR>x✝ : Cfg₁<VAR>l₁ : Option Λ<VAR>v : σ<VAR>L R : ListBlank Γ<GOAL>FRespects (step (tr enc dec M)) (trCfg enc enc₀) (trCfg enc enc₀ { l := l₁, var := v, Tape := Tape.mk' L R }) (step M { l := l₁, var := v, Tape := Tape.mk' L R })
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>enc₀ : enc default = Vector.replicate n false<VAR>x✝ : Cfg₁<VAR>v : σ<VAR>L R : ListBlank Γ<VAR>l₁ : Λ<GOAL>FRespects (step (tr enc dec M)) (trCfg enc enc₀) (trCfg enc enc₀ { l := some l₁, var := v, Tape := Tape.mk' L R }) (step M { l := some l₁, var := v, Tape := Tape.mk' L R })
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>enc₀ : enc default = Vector.replicate n false<VAR>x✝ : Cfg₁<VAR>v : σ<VAR>L R : ListBlank Γ<VAR>l₁ : Λ<GOAL>∀ (q : Stmt₁) (R : ListBlank Γ), Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R)) (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>enc₀ : enc default = Vector.replicate n false<VAR>x✝ : Cfg₁<VAR>v : σ<VAR>L : ListBlank Γ<VAR>q : Stmt₁<VAR>R : ListBlank Γ<GOAL>Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R)) (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
<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>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>B✝ : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>inst✝ : IsDomain R₁<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>b : Basis ι R₁ M₁<GOAL>B.SeparatingLeft ↔ ((toMatrix₂ b b) B).det ≠ 0