ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>x✝¹ : ↥(⨆ i ∈ s, p i)<VAR>x : M<VAR>hx : x ∈ ⨆ i ∈ s, p i<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<VAR>i : ι<VAR>hi : i ∈ s<GOAL>map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>x✝¹ : ↥(⨆ i ∈ s, p i)<VAR>x : M<VAR>hx : x ∈ ⨆ i ∈ s, p i<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<VAR>i : ι<VAR>hi : i ∈ s<GOAL>p i ≤ ⨆ i ∈ s, p i
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y : T<VAR>f : X ⟶ Y<GOAL>map f ⋙ forget X = forget Y
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y : T<VAR>f : X ⟶ Y<GOAL>∀ (X_1 : Under Y), (map f ⋙ forget X).obj X_1 = (forget Y).obj X_1
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y : T<VAR>f : X ⟶ Y<GOAL>autoParam (∀ (X_1 Y_1 : Under Y) (f_1 : X_1 ⟶ Y_1), (map f ⋙ forget X).map f_1 = eqToHom ⋯ ≫ (forget Y).map f_1 ≫ eqToHom ⋯) _auto✝
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : Nontrivial k<VAR>a b : G<VAR>h : (of k G) a = (of k G) b<GOAL>a = b
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.50538, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.50590, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>Y : C<VAR>f : op X ⟶ op (G.obj Y)<VAR>a✝ : ℱ.obj (op X)<GOAL>(appHom α X ≫ ℱ'.val.map f) a✝ = (ℱ.map f ≫ α.app (op Y)) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>ys₁ ys₂ : List β<GOAL>(↑(suffixLevenshtein C xs ys₂)).minimum ≤ ↑(levenshtein C xs (ys₁ ++ ys₂))
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>h : s.Nonempty<VAR>x : β<GOAL>h.some ∈ s ∧ ⊤ h.some x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<GOAL>N.FG ↔ ∃ n s, span R (range s) = N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<GOAL>(∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S✝ : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : DecidableEq ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>S : ι → Submodule R N<GOAL>⨆ i, ⨆ (_ : p i), S i = LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S✝ : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : DecidableEq ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>S : ι → Submodule R N<GOAL>⨆ i, ⨆ (_ : p i), S i ≤ LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S✝ : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : DecidableEq ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>S : ι → Submodule R N<GOAL>LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p) ≤ ⨆ i, ⨆ (_ : p i), S i
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>IH : n < a ^ n<GOAL>n + 1 < a ^ (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>IH : n < a ^ n<VAR>this : a ^ n + a ^ n ≤ a ^ n * a<GOAL>n + 1 < a ^ (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>IH : n < a ^ n<VAR>this : a ^ n + a ^ n ≤ a ^ n * a<GOAL>n + 1 < a ^ n * a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>IH : n < a ^ n<VAR>this : a ^ n + a ^ n ≤ a ^ n * a<GOAL>n + 1 < a ^ n + a ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp (a + m • p) b = toIocDiv hp a b - m
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>b - toIocDiv hp a b • p + m • p ∈ Set.Ioc (a + m • p) (a + p + m • p)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>Codisjoint N N' ↔ Codisjoint ↑N ↑N'
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n expNegInvGlue
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesEffectiveEpis<VAR>inst✝⁴ : F.ReflectsEffectiveEpis<VAR>inst✝³ : F.Full<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.EffectivelyEnough<VAR>inst✝ : Preregular D<VAR>X : C<VAR>S : Sieve X<GOAL>S ∈ (regularTopology C).sieves X ↔ S ∈ (F.inducedTopology (regularTopology D)).sieves X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesEffectiveEpis<VAR>inst✝⁴ : F.ReflectsEffectiveEpis<VAR>inst✝³ : F.Full<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.EffectivelyEnough<VAR>inst✝ : Preregular D<VAR>X : C<VAR>S : Sieve X<VAR>this : Preregular C<GOAL>S ∈ (regularTopology C).sieves X ↔ S ∈ (F.inducedTopology (regularTopology D)).sieves X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesEffectiveEpis<VAR>inst✝⁴ : F.ReflectsEffectiveEpis<VAR>inst✝³ : F.Full<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.EffectivelyEnough<VAR>inst✝ : Preregular D<VAR>X : C<VAR>S : Sieve X<VAR>this : Preregular C<GOAL>S ∈ (regularTopology C).sieves X ↔ ∃ Y π, EffectiveEpi π ∧ S.arrows π
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Epi (f ≫ g)<VAR>Z : C<VAR>a b : Z✝ ⟶ Z<VAR>w : f ≫ g ≫ a = f ≫ g ≫ b<GOAL>a = b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Epi (f ≫ g)<VAR>Z : C<VAR>a b : Z✝ ⟶ Z<VAR>w : (f ≫ g) ≫ a = (f ≫ g) ≫ b<GOAL>a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<GOAL>EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>h : Bornology.IsBounded ∅<GOAL>EMetric.diam ∅ = ENNReal.ofReal (sSup ∅ - sInf ∅)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<VAR>hne : s.Nonempty<GOAL>EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<VAR>hne : s.Nonempty<VAR>x : ℝ<VAR>hx : x ∈ s<VAR>y : ℝ<VAR>hy : y ∈ s<GOAL>dist x y ≤ sSup s - sInf s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<VAR>hne : s.Nonempty<GOAL>ENNReal.ofReal (sSup s - sInf s) ≤ EMetric.diam s
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ha : Irreducible a<GOAL>normalizedFactors a = {normalize a}
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ha : Irreducible a<VAR>p : α<VAR>a_assoc : a ~ᵤ p<VAR>hp : normalizedFactors a = {p}<GOAL>normalizedFactors a = {normalize a}
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ha : Irreducible a<VAR>p : α<VAR>a_assoc : a ~ᵤ p<VAR>hp : normalizedFactors a = {p}<VAR>p_mem : p ∈ normalizedFactors a<GOAL>normalizedFactors a = {normalize a}
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ha : Irreducible a<VAR>p : α<VAR>a_assoc : a ~ᵤ p<VAR>hp : normalizedFactors a = {p}<VAR>p_mem : p ∈ normalizedFactors a<GOAL>normalize a = p
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.boundary ⟨0, ⋯⟩ = 0
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.boundaries.min' ⋯ = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (z * y + x) y
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Φ 0 = 1
<VAR>α : Type u_1<VAR>f : α → Char → α<VAR>s : String<VAR>a : α<GOAL>foldl f a s = List.foldl f a s.data
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : Group H<VAR>g : G<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : ∀ (g : G), g ^ n = 1<GOAL>IsOfFinOrder g
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup V<VAR>inst✝¹⁰ : NormedSpace ℝ V<VAR>inst✝⁹ : StrictConvexSpace ℝ V<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : StrictConvexSpace ℝ E<VAR>inst✝³ : MetricSpace PE<VAR>inst✝² : MetricSpace PF<VAR>inst✝¹ : NormedAddTorsor E PE<VAR>inst✝ : NormedAddTorsor F PF<VAR>r : ℝ<VAR>f : PF → PE<VAR>x y z : PE<VAR>hxy : dist x y = r * dist x z<VAR>hyz : dist y z = (1 - r) * dist x z<GOAL>y = (AffineMap.lineMap x z) r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup V<VAR>inst✝¹⁰ : NormedSpace ℝ V<VAR>inst✝⁹ : StrictConvexSpace ℝ V<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : StrictConvexSpace ℝ E<VAR>inst✝³ : MetricSpace PE<VAR>inst✝² : MetricSpace PF<VAR>inst✝¹ : NormedAddTorsor E PE<VAR>inst✝ : NormedAddTorsor F PF<VAR>r : ℝ<VAR>f : PF → PE<VAR>x y z : PE<VAR>hxy : dist x y = r * dist x z<VAR>hyz : dist y z = (1 - r) * dist x z<VAR>this : y -ᵥ x ∈ [0-[ℝ]z -ᵥ x]<GOAL>y = (AffineMap.lineMap x z) r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup V<VAR>inst✝¹⁰ : NormedSpace ℝ V<VAR>inst✝⁹ : StrictConvexSpace ℝ V<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : StrictConvexSpace ℝ E<VAR>inst✝³ : MetricSpace PE<VAR>inst✝² : MetricSpace PF<VAR>inst✝¹ : NormedAddTorsor E PE<VAR>inst✝ : NormedAddTorsor F PF<VAR>r : ℝ<VAR>f : PF → PE<VAR>x y : PE<VAR>hxy : dist x y = r * dist x x<VAR>hyz : dist y x = (1 - r) * dist x x<VAR>this : y -ᵥ x ∈ [0-[ℝ]x -ᵥ x]<GOAL>y = (AffineMap.lineMap x x) r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup V<VAR>inst✝¹⁰ : NormedSpace ℝ V<VAR>inst✝⁹ : StrictConvexSpace ℝ V<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : StrictConvexSpace ℝ E<VAR>inst✝³ : MetricSpace PE<VAR>inst✝² : MetricSpace PF<VAR>inst✝¹ : NormedAddTorsor E PE<VAR>inst✝ : NormedAddTorsor F PF<VAR>r : ℝ<VAR>f : PF → PE<VAR>x y z : PE<VAR>hxy : dist x y = r * dist x z<VAR>hyz : dist y z = (1 - r) * dist x z<VAR>this : y -ᵥ x ∈ [0-[ℝ]z -ᵥ x]<VAR>hne : x ≠ z<GOAL>y = (AffineMap.lineMap x z) r
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.36381, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<GOAL>IsZero (KernelFork.ofι h.ι ⋯).pt
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.36381, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<VAR>this : S.HasHomology<GOAL>IsZero (KernelFork.ofι h.ι ⋯).pt
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.36381, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<VAR>this : S.HasHomology<GOAL>IsZero h.H
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin n<GOAL>b.flag k.castSucc ≤ b.flag k.succ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin n<GOAL>b.flag k.castSucc ≤ span R {b k} ⊔ b.flag k.castSucc
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<GOAL>|o.volumeForm v| = ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<GOAL>|o.volumeForm v| = ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<GOAL>|o.volumeForm v| = ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<GOAL>|o.volumeForm v| = ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<GOAL>|o.volumeForm v| = ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<GOAL>∏ x : Fin n.succ, |⟪b x, v x⟫_ℝ| = ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<VAR>h : ∀ (i : Fin (n + 1)), v i ≠ 0<VAR>i : Fin n.succ<GOAL>|⟪b i, v i⟫_ℝ| = ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<VAR>hb✝ : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<VAR>h : ∀ (i : Fin (n + 1)), v i ≠ 0<VAR>i : Fin n.succ<VAR>hb : b i = ‖v i‖⁻¹ • v i<GOAL>|⟪b i, v i⟫_ℝ| = ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<VAR>hb✝ : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<VAR>h : ∀ (i : Fin (n + 1)), v i ≠ 0<VAR>i : Fin n.succ<VAR>hb : b i = ‖v i‖⁻¹ • v i<GOAL>|‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)| = ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<VAR>hb✝ : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<VAR>h : ∀ (i : Fin (n + 1)), v i ≠ 0<VAR>i : Fin n.succ<VAR>hb : b i = ‖v i‖⁻¹ • v i<GOAL>‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<VAR>this : FiniteDimensional ℝ E<VAR>hdim : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v<VAR>hb✝ : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<VAR>h : ∀ (i : Fin (n + 1)), v i ≠ 0<VAR>i : Fin n.succ<VAR>hb : b i = ‖v i‖⁻¹ • v i<GOAL>0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R✝<VAR>m n : ℕ<VAR>inst✝² : CommSemiring R✝<VAR>inst✝¹ : CommSemiring S<VAR>f✝ : R✝ →+* S<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R →+* S<VAR>x : R<VAR>p : R[X]<VAR>h : (Polynomial.map f p).IsRoot (f x)<VAR>hf : Function.Injective ⇑f<GOAL>p.IsRoot x
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hα : p ∣ Fintype.card α<VAR>σ : Perm α<VAR>hσ : σ ^ p ^ n = 1<VAR>a : α<VAR>ha : σ a = a<GOAL>∃ b, σ b = b ∧ b ≠ a
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>s : Set G<GOAL>(closure s).op = closure (MulOpposite.unop ⁻¹' s)
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>s : Set G<GOAL>sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>s : Set G<VAR>a : Subgroup Gᵐᵒᵖ<GOAL>a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y ≤ x<GOAL>x \ (x \ y) = y
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : NormalWord d<GOAL>(of i) g • w = g • w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<GOAL>∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<GOAL>∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<GOAL>∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this : closedBall 0 (ε / R) ∈ 𝓝 0<GOAL>∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this : closedBall 0 (ε / R) ∈ 𝓝 0<VAR>r : 𝕜<VAR>hr : r ∈ closedBall 0 (ε / R)<GOAL>{x} + r • s ⊆ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this : closedBall 0 (ε / R) ∈ 𝓝 0<VAR>r : 𝕜<VAR>hr : r ∈ closedBall 0 (ε / R)<GOAL>(fun x_1 => -x + x_1) ⁻¹' (r • s) ⊆ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this : closedBall 0 (ε / R) ∈ 𝓝 0<VAR>r : 𝕜<VAR>hr : r ∈ closedBall 0 (ε / R)<VAR>y : E<VAR>hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)<GOAL>y ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this : closedBall 0 (ε / R) ∈ 𝓝 0<VAR>r : 𝕜<VAR>hr : r ∈ closedBall 0 (ε / R)<VAR>y : E<VAR>hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)<VAR>z : E<VAR>zs : z ∈ s<VAR>hz : r • z = -x + y<GOAL>y ∈ u