ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u_1<VAR>Q : β → Prop<VAR>u v : β → Cofix F α<VAR>h : ∀ (x : β), Q x → ∃ a f' f₀ f₁, (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧ (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧ ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'<VAR>x✝¹ : β<VAR>Qx : Q x✝¹<VAR>R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'<VAR>x y : Cofix F α<VAR>x✝ : R x y<VAR>x' : β<VAR>Qx' : Q x'<VAR>xeq : x = u x'<VAR>yeq : y = v x'<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f₀ f₁ : (P F).last.B a → Cofix F α<VAR>ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩<VAR>vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩<VAR>h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'<GOAL>∃ a f₀ f₁, x.dest = MvQPF.abs ⟨a, f₀⟩ ∧ y.dest = MvQPF.abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R (f₀ i j) (f₁ i j)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u_1<VAR>Q : β → Prop<VAR>u v : β → Cofix F α<VAR>h : ∀ (x : β), Q x → ∃ a f' f₀ f₁, (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧ (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧ ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'<VAR>x✝¹ : β<VAR>Qx : Q x✝¹<VAR>R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'<VAR>x y : Cofix F α<VAR>x✝ : R x y<VAR>x' : β<VAR>Qx' : Q x'<VAR>xeq : x = u x'<VAR>yeq : y = v x'<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f₀ f₁ : (P F).last.B a → Cofix F α<VAR>ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩<VAR>vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩<VAR>h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'<GOAL>∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R ((P F).appendContents f' f₀ i j) ((P F).appendContents f' f₁ i j)
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>(fderivWithin ℝ f s a) y ≤ 0
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>0 y ≤ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>x y : R<GOAL>x - y ∈ ker f ↔ f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>inst✝ : CompleteSpace γ<VAR>a : α<GOAL>Tendsto f (comap e (𝓝 a)) (𝓝 (⋯.extend f a))
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
<VAR>a b : ℝ<VAR>n : ℕ<VAR>this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ (2 * 0 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 2 * (1 - u ^ 2) ^ 0<GOAL>∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>i : K →+* L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : DecidableEq L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (algebraMap K L) P<VAR>r : L<VAR>hr : r ∈ P.aroots L<GOAL>(aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>i : K →+* L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : DecidableEq L<VAR>P : K[X]<VAR>hP : Splits (algebraMap K L) P<VAR>r : L<VAR>hr : r ∈ P.aroots L<VAR>hmo : (map (algebraMap K L) P).Monic<GOAL>(aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>i : K →+* L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : DecidableEq L<VAR>P : K[X]<VAR>r : L<VAR>hr : r ∈ P.aroots L<VAR>hmo : (map (algebraMap K L) P).Monic<VAR>hP : Splits (RingHom.id L) (map (algebraMap K L) P)<GOAL>(aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>i : K →+* L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : DecidableEq L<VAR>P : K[X]<VAR>r : L<VAR>hr : r ∈ P.aroots L<VAR>hmo : (map (algebraMap K L) P).Monic<VAR>hP : Splits (RingHom.id L) (map (algebraMap K L) P)<GOAL>eval r (derivative (map (algebraMap K L) P)) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>i : K →+* L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : DecidableEq L<VAR>P : K[X]<VAR>r : L<VAR>hr : r ∈ P.aroots L<VAR>hmo : (map (algebraMap K L) P).Monic<VAR>hP : Splits (RingHom.id L) (map (algebraMap K L) P)<GOAL>eval r (derivative (Multiset.map (fun a => X - C a) (map (algebraMap K L) P).roots).prod) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<VAR>h : 1 ∈ s<GOAL>zeroLocus s = ∅
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<VAR>h : 1 ∈ s<GOAL>∀ (x : PrimeSpectrum R), x ∉ zeroLocus s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<VAR>h : 1 ∈ s<VAR>x : PrimeSpectrum R<VAR>hx : x ∈ zeroLocus s<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<VAR>h : 1 ∈ s<VAR>x : PrimeSpectrum R<VAR>hx : s ⊆ ↑x.asIdeal<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<VAR>h : 1 ∈ s<VAR>x : PrimeSpectrum R<VAR>hx : s ⊆ ↑x.asIdeal<VAR>x_prime : x.asIdeal.IsPrime<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<VAR>h : 1 ∈ s<VAR>x : PrimeSpectrum R<VAR>hx : s ⊆ ↑x.asIdeal<VAR>x_prime : x.asIdeal.IsPrime<VAR>eq_top : x.asIdeal = ⊤<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h_le : f ≤ᶠ[ae μ] g<VAR>h : ∃ᵐ (x : α) ∂μ, f x ≠ g x<GOAL>∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h_le : f ≤ᶠ[ae μ] g<VAR>h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ<GOAL>¬∃ᵐ (x : α) ∂μ, f x ≠ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h_le : f ≤ᶠ[ae μ] g<VAR>h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ<GOAL>∀ᵐ (x : α) ∂μ, f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → β<VAR>e : α ≃ β<VAR>this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)<VAR>hinj : Injective f<GOAL>Surjective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → β<VAR>e : α ≃ β<VAR>this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)<VAR>hsurj : Surjective f<GOAL>Injective f
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x t) (F' x t) x<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ ball x₀ ε, HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ ball x₀ ε, HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>h_bound : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ ball x₀ ε, HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ ball x₀ ε, HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))<VAR>hF_meas : (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧ ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>a✝ a i : α<VAR>ha0 : a ≠ 0<VAR>hi : Irreducible i<VAR>ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>x✝ : i * a ≠ 0<VAR>s : Multiset α<VAR>hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a<GOAL>(i ::ₘ s).prod ~ᵤ i * a
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>a✝ a i : α<VAR>ha0 : a ≠ 0<VAR>hi : Irreducible i<VAR>ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>x✝ : i * a ≠ 0<VAR>s : Multiset α<VAR>hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a<GOAL>i * s.prod ~ᵤ i * a
<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✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>f : M₂' →ₗ[R] M₂<GOAL>(toMatrix₂ b₁ b₂') (B.compl₂ f) = (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>f : M₂' →ₗ[R] M₂<GOAL>((toMatrix b₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) f = (toMatrix₂ b₁ b₂) (B ∘ₗ id) * (toMatrix b₂' b₂) f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>i j : ι<VAR>hij : i < j<VAR>b : Basis ι 𝕜 E<GOAL>(b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>i j : ι<VAR>hij : i < j<VAR>b : Basis ι 𝕜 E<VAR>this : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)<GOAL>(b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>i j : ι<VAR>hij : i < j<VAR>b : Basis ι 𝕜 E<VAR>this✝ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)<VAR>this : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (⇑b '' Set.Iio j)<GOAL>(b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>i j : ι<VAR>hij : i < j<VAR>b : Basis ι 𝕜 E<VAR>this✝¹ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)<VAR>this✝ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (⇑b '' Set.Iio j)<VAR>this : ↑(b.repr (gramSchmidt 𝕜 (⇑b) i)).support ⊆ Set.Iio j<GOAL>(b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<GOAL>μ.restrict s = 0 ↔ μ s = 0
<VAR>α β : CompleteLat<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget CompleteLat).obj α<GOAL>({ toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ } ≫ { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : CompleteLat<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget CompleteLat).obj β<GOAL>({ toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ } ≫ { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>a b : ℕ<GOAL>count p (a + b) = count (fun k => p (k + b)) a + count p b
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>a b : ℕ<GOAL>count (fun k => p (b + k)) a + count p b = count (fun k => p (k + b)) a + count p b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : PseudoMetricSpace X<VAR>inst✝² : PseudoMetricSpace Y<VAR>inst✝¹ : EquivLike F X Y<VAR>inst✝ : DilationEquivClass F X Y<VAR>e : F<GOAL>map (⇑e) (cobounded X) = cobounded Y
<VAR>α : Type u_1<VAR>s✝ t : Multiset (Multiset α)<VAR>a : Multiset α<VAR>s : Multiset (Multiset α)<VAR>ih : (s + t).Sections = s.Sections.bind fun m => map (fun x => m + x) t.Sections<GOAL>(a ::ₘ s + t).Sections = (a ::ₘ s).Sections.bind fun m => map (fun x => m + x) t.Sections
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>α : Ext X Y n<VAR>m : ℕ<VAR>β : Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>((-α).comp β h).hom = (-α.comp β h).hom
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hqn : n < q<GOAL>φ ≫ (Hσ q).f (n + 1) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hqn : n < q<GOAL>φ ≫ ((AlternatingFaceMapComplex.obj X).d (n + 1) n ≫ hσ' q n (n + 1) ⋯ + hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hqn : n < q<GOAL>φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < b<VAR>h₂ : b < a<GOAL>False
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hq : ↑q.num ≠ 0<GOAL>↑q⁻¹ = (↑q)⁻¹
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R : ℝ<GOAL>circleMap c R '' Ioc 0 (2 * π) = sphere c |R|
<VAR>α : Type u_1<VAR>inst✝² : CommRing α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>gcd a b = gcd a c
<VAR>α : Type u_1<VAR>inst✝² : CommRing α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>gcd a b ∣ c
<VAR>α : Type u_1<VAR>inst✝² : CommRing α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>gcd a c ∣ b
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ : Type u<VAR>g₁ : Ring X₁<VAR>g₂ : Ring X₂<VAR>m₁ : Algebra R X₁<VAR>m₂ : Algebra R X₂<VAR>e : X₁ ≃ₐ[R] X₂<VAR>x : (forget (AlgebraCat R)).obj (AlgebraCat.of R X₁)<GOAL>(↑e ≫ ↑e.symm) x = (𝟙 (AlgebraCat.of R X₁)) x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ : Type u<VAR>g₁ : Ring X₁<VAR>g₂ : Ring X₂<VAR>m₁ : Algebra R X₁<VAR>m₂ : Algebra R X₂<VAR>e : X₁ ≃ₐ[R] X₂<VAR>x : (forget (AlgebraCat R)).obj (AlgebraCat.of R X₂)<GOAL>(↑e.symm ≫ ↑e) x = (𝟙 (AlgebraCat.of R X₂)) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.81832, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(↑(fst φ)).v p q hpq ≫ (inl φ).v q p ⋯ + (snd φ).v p p ⋯ ≫ (inr φ).f p = 𝟙 ((mappingCone φ).X p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)<VAR>IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []<VAR>l : List α<VAR>p : l ~ is ++ t :: ts<GOAL>(∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)<VAR>IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []<VAR>l : List α<VAR>p : l ~ is ++ t :: ts<GOAL>(∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)<VAR>IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []<VAR>l : List α<VAR>p : l ~ is ++ t :: ts<VAR>is' : List α<VAR>p' : is' ~ t :: is<VAR>e : l = is' ++ ts<GOAL>(∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)<VAR>IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []<VAR>l : List α<VAR>p : l ~ is ++ t :: ts<VAR>m : l ∈ ts.permutationsAux (t :: is)<GOAL>(∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
<VAR>a : Code × ℕ<GOAL>(rfindOpt fun b => evaln (((a, b).2, (a, b).1.1), (a, b).1.2).1.1 (((a, b).2, (a, b).1.1), (a, b).1.2).1.2 (((a, b).2, (a, b).1.1), (a, b).1.2).2) = a.1.eval a.2
<VAR>K : Type u_1<VAR>inst✝ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>q : Stmt₂<GOAL>q ∈ stmts₁ q
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>β : Type u_2<VAR>inst✝ : DecidableRel R<VAR>f : β → α<VAR>x : β<VAR>xs : List β<GOAL>pwFilter R (map f (x :: xs)) = map f (pwFilter (fun x y => R (f x) (f y)) (x :: xs))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring α<VAR>inst✝² : Semiring β<VAR>inst✝¹ : Algebra R α<VAR>inst✝ : Algebra R β<VAR>r : R<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r<GOAL>((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r