ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>ker (f.prod g) = ker f ⊓ ker g
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>comap f ⊥ ⊓ comap g ⊥ = ker f ⊓ ker g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : PushoutCocone f g<VAR>ht : IsColimit t<VAR>inst✝ : Epi f<VAR>W : C<VAR>h k : t.pt ⟶ W<VAR>i : t.inr ≫ h = t.inr ≫ k<GOAL>t.inl ≫ h = t.inl ≫ k
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : ↥(Lp E 1 μ)<GOAL>setToL1 hT = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : ↥(Lp E 1 μ)<GOAL>ContinuousLinearMap.comp 0 (coeToLp α E ℝ) = setToL1SCLM α E μ hT
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>(ContinuousLinearMap.comp 0 (coeToLp α E ℝ)) f = (setToL1SCLM α E μ hT) f
<VAR>x : ℝ<GOAL>sin (π / 2 - x) = cos x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z : P<VAR>x y : V<GOAL>midpoint R x x +ᵥ midpoint R (-y) y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>a : α<VAR>t : Set β<GOAL>((piecewise hs κ η) a) t = if a ∈ s then (κ a) t else (η a) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>a : α<VAR>t : Set β<GOAL>(if a ∈ s then κ a else η a) t = if a ∈ s then (κ a) t else (η a) t
<VAR>x : WithBot ℕ<GOAL>1 ≤ x ↔ 0 < x
<VAR>x : WithBot ℕ<VAR>h : 0 < x<GOAL>1 ≤ x
<VAR>a b c : EReal<GOAL>a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁸ : Field F<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K₁<VAR>inst✝¹³ : Field K₂<VAR>inst✝¹² : Field K₃<VAR>inst✝¹¹ : Algebra F K₁<VAR>inst✝¹⁰ : Algebra F K₂<VAR>inst✝⁹ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra E K₁<VAR>inst✝⁵ : Algebra E K₂<VAR>inst✝⁴ : Algebra E K₃<VAR>inst✝³ : IsScalarTower F E K₁<VAR>inst✝² : IsScalarTower F E K₂<VAR>inst✝¹ : IsScalarTower F E K₃<VAR>inst✝ : Normal F E<VAR>σ : E ≃ₐ[F] E<VAR>a✝ : E<GOAL>((fun σ => σ.restrictNormal' E) ((fun σ => (toAlgHom F E K₁).comp ↑σ) σ)) a✝ = σ a✝
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁸ : Field F<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K₁<VAR>inst✝¹³ : Field K₂<VAR>inst✝¹² : Field K₃<VAR>inst✝¹¹ : Algebra F K₁<VAR>inst✝¹⁰ : Algebra F K₂<VAR>inst✝⁹ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra E K₁<VAR>inst✝⁵ : Algebra E K₂<VAR>inst✝⁴ : Algebra E K₃<VAR>inst✝³ : IsScalarTower F E K₁<VAR>inst✝² : IsScalarTower F E K₂<VAR>inst✝¹ : IsScalarTower F E K₃<VAR>inst✝ : Normal F E<VAR>σ : E ≃ₐ[F] E<VAR>a✝ : E<GOAL>(((toAlgHom F E K₁).comp ↑σ).restrictNormal E) a✝ = σ a✝
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁸ : Field F<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K₁<VAR>inst✝¹³ : Field K₂<VAR>inst✝¹² : Field K₃<VAR>inst✝¹¹ : Algebra F K₁<VAR>inst✝¹⁰ : Algebra F K₂<VAR>inst✝⁹ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra E K₁<VAR>inst✝⁵ : Algebra E K₂<VAR>inst✝⁴ : Algebra E K₃<VAR>inst✝³ : IsScalarTower F E K₁<VAR>inst✝² : IsScalarTower F E K₂<VAR>inst✝¹ : IsScalarTower F E K₃<VAR>inst✝ : Normal F E<VAR>σ : E ≃ₐ[F] E<VAR>a✝ : E<GOAL>(algebraMap E K₁) ((((toAlgHom F E K₁).comp ↑σ).restrictNormal E) a✝) = (algebraMap E K₁) (σ a✝)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁸ : Field F<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K₁<VAR>inst✝¹³ : Field K₂<VAR>inst✝¹² : Field K₃<VAR>inst✝¹¹ : Algebra F K₁<VAR>inst✝¹⁰ : Algebra F K₂<VAR>inst✝⁹ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra E K₁<VAR>inst✝⁵ : Algebra E K₂<VAR>inst✝⁴ : Algebra E K₃<VAR>inst✝³ : IsScalarTower F E K₁<VAR>inst✝² : IsScalarTower F E K₂<VAR>inst✝¹ : IsScalarTower F E K₃<VAR>inst✝ : Normal F E<VAR>σ : E ≃ₐ[F] E<VAR>a✝ : E<GOAL>((toAlgHom F E K₁).comp ↑σ) ((algebraMap E E) a✝) = (algebraMap E K₁) (σ a✝)
<VAR>z w : ℂ<VAR>h : z = 0 → w.re = 0 → w = 0<GOAL>abs (z ^ w) = abs z ^ w.re / rexp (z.arg * w.im)
<VAR>w : ℂ<VAR>h : 0 = 0 → w.re = 0 → w = 0<GOAL>abs (0 ^ w) = 0 ^ w.re / rexp (arg 0 * w.im)
<VAR>w : ℂ<VAR>h : 0 = 0 → w.re = 0 → w = 0<VAR>hw : w.re = 0<GOAL>abs (0 ^ w) = 0 ^ w.re / rexp (arg 0 * w.im)
<VAR>w : ℂ<VAR>h : 0 = 0 → w.re = 0 → w = 0<VAR>hw : w.re ≠ 0<GOAL>abs (0 ^ w) = 0 ^ w.re / rexp (arg 0 * w.im)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>b ∆ a ∆ a = b
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X✝ Y : Set α<VAR>e : α<VAR>ι : Type u_2<VAR>X I : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis (I i) (X i)<VAR>h_ind : M.Indep (⋃ i, I i)<GOAL>M.Basis (⋃ i, I i) (⋃ i, X i)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X✝ Y : Set α<VAR>e : α<VAR>ι : Type u_2<VAR>X I : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis (I i) (X i)<VAR>h_ind : M.Indep (⋃ i, I i)<GOAL>∀ e ∈ (⋃ i, X i) \ ⋃ i, I i, M.Dep (insert e (⋃ i, I i))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X✝ Y : Set α<VAR>e✝ : α<VAR>ι : Type u_2<VAR>X I : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis (I i) (X i)<VAR>h_ind : M.Indep (⋃ i, I i)<VAR>e : α<VAR>he' : e ∉ ⋃ i, I i<VAR>i : ι<VAR>hes : e ∈ X i<GOAL>M.Dep (insert e (⋃ i, I i))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X✝ Y : Set α<VAR>e✝ : α<VAR>ι : Type u_2<VAR>X I : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis (I i) (X i)<VAR>h_ind : M.Indep (⋃ i, I i)<VAR>e : α<VAR>he' : ∀ (x : ι), e ∉ I x<VAR>i : ι<VAR>hes : e ∈ X i<GOAL>M.Dep (insert e (⋃ i, I i))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X✝ Y : Set α<VAR>e✝ : α<VAR>ι : Type u_2<VAR>X I : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis (I i) (X i)<VAR>h_ind : M.Indep (⋃ i, I i)<VAR>e : α<VAR>he' : ∀ (x : ι), e ∉ I x<VAR>i : ι<VAR>hes : e ∈ X i<GOAL>insert e (⋃ i, I i) ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X✝ Y : Set α<VAR>e✝ : α<VAR>ι : Type u_2<VAR>X I : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis (I i) (X i)<VAR>h_ind : M.Indep (⋃ i, I i)<VAR>e : α<VAR>he' : ∀ (x : ι), e ∉ I x<VAR>i : ι<VAR>hes : e ∈ X i<GOAL>e ∈ M.E
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G✝ : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>G : Type u_9<VAR>inst✝ : LinearOrderedAddCommGroup G<VAR>f : ι → G<VAR>s : Finset ι<VAR>hf : ∀ (i : ι), 0 ≤ f i<GOAL>|∑ i ∈ s, f i| = ∑ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<GOAL>M.Base B ↔ M.Indep B ∧ ∀ (I : Set α), M.Indep I → B ⊆ I → B = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>x✝ : M.Indep B ∧ ∀ (I : Set α), M.Indep I → B ⊆ I → B = I<VAR>h : M.Indep B<VAR>h' : ∀ (I : Set α), M.Indep I → B ⊆ I → B = I<GOAL>M.Base B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>x✝ : M.Indep B ∧ ∀ (I : Set α), M.Indep I → B ⊆ I → B = I<VAR>h : M.Indep B<VAR>h' : ∀ (I : Set α), M.Indep I → B ⊆ I → B = I<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hBB' : B ⊆ B'<GOAL>M.Base B
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>x✝ : S<GOAL>((truncate n).comp (lift f f_compat)) x✝ = (f n) x✝
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<GOAL>p /ₘ 1 = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>x✝ : R<GOAL>x✝ ∈ M.nonUnitalSubsemiringClosure ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>x✝ : R<VAR>hx : x✝ ∈ M.nonUnitalSubsemiringClosure<VAR>H1 : NonUnitalSubsemiring R<VAR>H2 : H1 ∈ {S | ↑M ⊆ ↑S}<GOAL>x✝ ∈ (fun h => ↑H1) H2
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>x✝ : R<VAR>hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M<VAR>s : R<VAR>sM : s ∈ ↑M<VAR>H1 : AddSubmonoid R<VAR>H2 : H1 ∈ {S | ↑M ⊆ ↑S}<GOAL>s ∈ (fun h => ↑H1) H2
<VAR>n : ℕ<VAR>f : ℕ →. ℕ<VAR>g : Vector ℕ n → ℕ<VAR>hf : Partrec' fun v => f v.head<VAR>hg : Partrec' ↑g<GOAL>Partrec' fun v => f (g v)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M ≃ₗ[R] M<VAR>g : N ≃ₗ[R] N<VAR>n : ℕ<GOAL>congr f g ^ n = congr (f ^ n) (g ^ n)
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r✝ r : R → R → Prop<GOAL>(fun x => { toQuot := Quot.mk (Rel r) x }) 1 = 1
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r✝ r : R → R → Prop<GOAL>∀ (x y : R), { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯ }.toFun (x * y) = { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯ }.toFun x * { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯ }.toFun y
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r✝ r : R → R → Prop<GOAL>(↑{ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯ }).toFun 0 = 0
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r✝ r : R → R → Prop<GOAL>∀ (x y : R), (↑{ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯ }).toFun (x + y) = (↑{ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯ }).toFun x + (↑{ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯ }).toFun y
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>i : ℤ<GOAL>A ^ (1 + i) = A * A ^ i
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.blocks.sum = n
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>this : take c.length c.blocks = c.blocks<GOAL>c.blocks.sum = n
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>this : take c.length c.blocks = c.blocks<GOAL>↑(Fin.last n) = n
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<GOAL>Primrec fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this : Primrec G₁<GOAL>Primrec fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<GOAL>Primrec fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<GOAL>Primrec fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Primrec₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Primrec G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Primrec₂ G<VAR>a : α<VAR>n : ℕ<GOAL>G (a, List.map ((fun a n => F a (ofNat Code n)) a) (List.range n)).1 (a, List.map ((fun a n => F a (ofNat Code n)) a) (List.range n)).2 = some ((fun a n => F a (ofNat Code n)) a n)