ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : LocalRing R<VAR>h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>∀ (p : ℕ), p ≠ 0 → CharP R p → P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : LocalRing R<VAR>h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<VAR>p : ℕ<VAR>p_pos : p ≠ 0<VAR>p_char : CharP R p<GOAL>P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : LocalRing R<VAR>h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<VAR>p : ℕ<VAR>p_pos : p ≠ 0<VAR>p_char : CharP R p<VAR>p_ppow : IsPrimePow p<GOAL>P
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>evalEval 0 0 W.polynomial = -W.a₆
<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✝⁷ : OrderedRing R<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>inst✝ : NoZeroSMulDivisors R V<VAR>w x z : P<VAR>h₁ : Wbtw R w x z<VAR>h : w ≠ x<VAR>h₂ : Wbtw R x w z<GOAL>False
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f✝ : X ⟶ Y<VAR>A : Rep k G<VAR>f : ofMulAction k G G ⟶ A<GOAL>(fun x => A.leftRegularHom x) ({ toFun := fun f => f.hom (Finsupp.single 1 1), map_add' := ⋯, map_smul' := ⋯ }.toFun f) = f
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f✝ : X ⟶ Y<VAR>A : Rep k G<VAR>f : ofMulAction k G G ⟶ A<VAR>x : G<GOAL>(((fun x => A.leftRegularHom x) ({ toFun := fun f => f.hom (Finsupp.single 1 1), map_add' := ⋯, map_smul' := ⋯ }.toFun f)).hom ∘ₗ Finsupp.lsingle x) 1 = (f.hom ∘ₗ Finsupp.lsingle x) 1
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f✝ : X ⟶ Y<VAR>A : Rep k G<VAR>f : ofMulAction k G G ⟶ A<VAR>x : G<VAR>this : f.hom (((ofMulAction k G G).ρ x) (Finsupp.single 1 1)) = (A.ρ x) (f.hom (Finsupp.single 1 1))<GOAL>(((fun x => A.leftRegularHom x) ({ toFun := fun f => f.hom (Finsupp.single 1 1), map_add' := ⋯, map_smul' := ⋯ }.toFun f)).hom ∘ₗ Finsupp.lsingle x) 1 = (f.hom ∘ₗ Finsupp.lsingle x) 1
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f✝ : X ⟶ Y<VAR>A : Rep k G<VAR>f : ofMulAction k G G ⟶ A<VAR>x : G<VAR>this : f.hom (((ofMulAction k G G).ρ x) (Finsupp.single 1 1)) = (A.ρ x) (f.hom (Finsupp.single 1 1))<GOAL>f.hom (Finsupp.single x 1) = f.hom (Finsupp.single x 1)
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i✝ : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>i : I<GOAL>(ι' R A) ((lof R I A i) 1) = (mkAlgHom R A) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<GOAL>∃ R, ∃ᶠ (n : ι) in l, R < x n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ¬∃ R, ∃ᶠ (n : ι) in l, R < x n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1<VAR>r : ℝ≥0<GOAL>∀ᶠ (n : ℝ≥0∞) in map (fun n => ↑(Real.nnabs (x n))) l, ↑r ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1<VAR>r : ℝ≥0<GOAL>∀ᶠ (a : ι) in l, r ≤ Real.nnabs (x a)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w : Fin 3 → R<GOAL>(crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w : Fin 3 → R<GOAL>![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 - u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1, u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 - u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2, u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 - u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0] = ![![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 2 - ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 1 + (v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2 - v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1), ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 0 - ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 2 + (v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0 - v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2), ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 1 - ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 0 + (v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1 - v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0)]
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>q : R[X]<GOAL>(gcd p q).degree ≤ p.degree
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>q : R[X]<VAR>this : (gcd p q).degree ≤ ↑p.natDegree<GOAL>(gcd p q).degree ≤ p.degree
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : OrderTopology α<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : (i : ι) → LinearOrder (π i)<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : ∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>a' b' x' : ι → α<VAR>inst✝ : Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<GOAL>Ioc a b ∈ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : OrderTopology α<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : (i : ι) → LinearOrder (π i)<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : ∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>a' b' x' : ι → α<VAR>inst✝ : Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<VAR>i : ι<VAR>x✝ : i ∈ univ<GOAL>Ioc (a i) (b i) ∈ 𝓝 (x i)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>r : R<VAR>n : ℕ<GOAL>(C r * X ^ n).eraseLead = 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>finite : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>pos : 0 < r<VAR>sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)<VAR>y✝ : E<VAR>hy : y✝ ∈ EMetric.ball 0 r<VAR>m : ℕ<VAR>hm : m ∉ Finset.range n<GOAL>((p m) fun x => y✝) = 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>finite : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>pos : 0 < r<VAR>sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)<VAR>y✝ : E<VAR>hy : y✝ ∈ EMetric.ball 0 r<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>((p m) fun x => y✝) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => c) s x = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderiv 𝕜 (fun x => c) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this : Inhabited m<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this : Inhabited m<VAR>k : α := (image b univ).max' ⋯<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this : Inhabited m<VAR>k : α := (image b univ).max' ⋯<VAR>b' : { a // b a < k } → α := fun i => b ↑i<VAR>A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this : Inhabited m<VAR>k : α := (image b univ).max' ⋯<VAR>b' : { a // b a < k } → α := fun i => b ↑i<VAR>A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k<VAR>hbi : b i = k<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this : Inhabited m<VAR>k : α := (image b univ).max' ⋯<VAR>b' : { a // b a < k } → α := fun i => b ↑i<VAR>A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k<VAR>hi : b i < (image b univ).max' ⋯<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this✝ : Inhabited m<VAR>k : α := (image b univ).max' ⋯<VAR>b' : { a // b a < k } → α := fun i => b ↑i<VAR>A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k<VAR>hi : b i < (image b univ).max' ⋯<VAR>this : Invertible A<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this✝ : Inhabited m<VAR>k : α := (image b univ).max' ⋯<VAR>b' : { a // b a < k } → α := fun i => b ↑i<VAR>A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k<VAR>hi : b i < (image b univ).max' ⋯<VAR>this : Invertible A<VAR>hA : A.BlockTriangular b'<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this✝ : Inhabited m<VAR>k : α := (image b univ).max' ⋯<VAR>b' : { a // b a < k } → α := fun i => b ↑i<VAR>A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k<VAR>hi : b i < (image b univ).max' ⋯<VAR>this : Invertible A<VAR>hA : A.BlockTriangular b'<VAR>hb' : image b' univ ⊂ image b univ<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M], M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<VAR>this✝ : Inhabited m<VAR>k : α := (image b univ).max' ⋯<VAR>b' : { a // b a < k } → α := fun i => b ↑i<VAR>A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k<VAR>hi : b i < (image b univ).max' ⋯<VAR>this : Invertible A<VAR>hA : A.BlockTriangular b'<VAR>hb' : image b' univ ⊂ image b univ<VAR>hij' : b' ⟨j, ⋯⟩ < b' ⟨i, hi⟩<GOAL>M⁻¹ i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>f : α → Option γ<VAR>g : β → Option δ<VAR>hfg : (R ⇒ Option.Rel P) f g<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<VAR>h₁ : R a b<VAR>h₂ : Forall₂ R as bs<GOAL>Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>f : α → Option γ<VAR>g : β → Option δ<VAR>hfg : (R ⇒ Option.Rel P) f g<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<VAR>h₁ : R a b<VAR>h₂ : Forall₂ R as bs<GOAL>Forall₂ P (match f a with | none => filterMap f as | some b => b :: filterMap f as) (match g b with | none => filterMap g bs | some b => b :: filterMap g bs)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : W.ContainsIdentities<VAR>J : Type<VAR>inst✝¹ : Finite J<VAR>inst✝ : HasProductsOfShape J C<VAR>hW : W.IsStableUnderProductsOfShape J<VAR>F : Discrete J ⥤ C<GOAL>(adj L hW).counit.app (F ⋙ L) = (Functor.const (Discrete J)).map ((compLimitFunctorIso L hW).hom.app F) ≫ (Functor.compConstIso (Discrete J) L).hom.app (lim.obj F) ≫ whiskerRight (constLimAdj.counit.app F) L
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁷ : AddCommMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N✝ : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : Zero M'<VAR>inst✝² : CommMonoid N✝<VAR>inst✝¹ : DecidableEq α<VAR>N : Type u_16<VAR>inst✝ : AddCommMonoid N<VAR>f : α →₀ N<VAR>a : α<GOAL>(f.sum fun x v => if x = a then v else 0) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>s : Set α<VAR>hμs : s ∈ μ.cofinite<VAR>hsm : MeasurableSet s<VAR>hfs : ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε<GOAL>∀ (i : ι), eLpNorm (sᶜᶜ.indicator (f i)) p μ ≤ ε
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v✝ : ι → M<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing R₂<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M''<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>G : Type u_10<VAR>inst✝³ : Group G<VAR>inst✝² : DistribMulAction G R<VAR>inst✝¹ : DistribMulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>v : ι → M<VAR>hv : span R (Set.range v) = ⊤<VAR>w : ι → G<GOAL>span R (Set.range (w • v)) = ⊤
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v✝ : ι → M<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing R₂<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M''<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>G : Type u_10<VAR>inst✝³ : Group G<VAR>inst✝² : DistribMulAction G R<VAR>inst✝¹ : DistribMulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>v : ι → M<VAR>hv : span R (Set.range v) = ⊤<VAR>w : ι → G<GOAL>⊤ ≤ span R (Set.range (w • v))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v✝ : ι → M<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing R₂<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M''<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>G : Type u_10<VAR>inst✝³ : Group G<VAR>inst✝² : DistribMulAction G R<VAR>inst✝¹ : DistribMulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>v : ι → M<VAR>hv : span R (Set.range v) = ⊤<VAR>w : ι → G<VAR>j : M<VAR>hj : j ∈ span R (Set.range v)<GOAL>j ∈ span R (Set.range (w • v))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v✝ : ι → M<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing R₂<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M''<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>G : Type u_10<VAR>inst✝³ : Group G<VAR>inst✝² : DistribMulAction G R<VAR>inst✝¹ : DistribMulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>v : ι → M<VAR>hv : span R (Set.range v) = ⊤<VAR>w : ι → G<VAR>j : M<VAR>hj : ∀ (p : Submodule R M), Set.range v ⊆ ↑p → j ∈ p<GOAL>∀ (p : Submodule R M), Set.range (w • v) ⊆ ↑p → j ∈ p