ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : ConcreteCategory.forget.obj (pullback f g)<GOAL>(pullbackIsoProdSubtype f g).hom x = ⟨((pullback.fst f g) x, (pullback.snd f g) x), ⋯⟩
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : ConcreteCategory.forget.obj (pullback f g)<GOAL>↑((pullbackIsoProdSubtype f g).hom x) = ↑⟨((pullback.fst f g) x, (pullback.snd f g) x), ⋯⟩
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : ConcreteCategory.forget.obj (pullback f g)<GOAL>(↑((pullbackIsoProdSubtype f g).hom x)).1 = (↑⟨((pullback.fst f g) x, (pullback.snd f g) x), ⋯⟩).1
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : ConcreteCategory.forget.obj (pullback f g)<GOAL>(↑((pullbackIsoProdSubtype f g).hom x)).2 = (↑⟨((pullback.fst f g) x, (pullback.snd f g) x), ⋯⟩).2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I' : ClassGroup S<GOAL>∃ a, mkMMem bS adm a = I'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : Ideal S<VAR>hI : I ∈ (Ideal S)⁰<GOAL>∃ a, mkMMem bS adm a = mk0 ⟨I, hI⟩
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : Ideal S<VAR>hI : I ∈ (Ideal S)⁰<VAR>J : ↥(Ideal S)⁰<VAR>mk0_eq_mk0 : mk0 ⟨I, hI⟩ = mk0 J<VAR>J_dvd : (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ∈ ↑J<GOAL>∃ a, mkMMem bS adm a = mk0 ⟨I, hI⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s✝ t✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>filter p s ∩ filter (fun a => ¬p a) t = ∅
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : HasZeroObject C<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹³ : Pretriangulated C<VAR>inst✝¹² : Category.{u_5, u_2} D<VAR>inst✝¹¹ : HasZeroObject D<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁷ : Pretriangulated D<VAR>inst✝⁶ : Category.{u_6, u_3} A<VAR>inst✝⁵ : Abelian A<VAR>F✝ : C ⥤ A<VAR>inst✝⁴ : F✝.IsHomological<VAR>L : C ⥤ D<VAR>inst✝³ : L.CommShift ℤ<VAR>inst✝² : L.IsTriangulated<VAR>inst✝¹ : L.mapArrow.EssSurj<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>inst✝ : G.IsHomological<GOAL>F.IsHomological
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : HasZeroObject C<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹³ : Pretriangulated C<VAR>inst✝¹² : Category.{u_5, u_2} D<VAR>inst✝¹¹ : HasZeroObject D<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁷ : Pretriangulated D<VAR>inst✝⁶ : Category.{u_6, u_3} A<VAR>inst✝⁵ : Abelian A<VAR>F✝ : C ⥤ A<VAR>inst✝⁴ : F✝.IsHomological<VAR>L : C ⥤ D<VAR>inst✝³ : L.CommShift ℤ<VAR>inst✝² : L.IsTriangulated<VAR>inst✝¹ : L.mapArrow.EssSurj<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>inst✝ : G.IsHomological<VAR>this : F.PreservesZeroMorphisms<GOAL>F.IsHomological
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : HasZeroObject C<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹³ : Pretriangulated C<VAR>inst✝¹² : Category.{u_5, u_2} D<VAR>inst✝¹¹ : HasZeroObject D<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁷ : Pretriangulated D<VAR>inst✝⁶ : Category.{u_6, u_3} A<VAR>inst✝⁵ : Abelian A<VAR>F✝ : C ⥤ A<VAR>inst✝⁴ : F✝.IsHomological<VAR>L : C ⥤ D<VAR>inst✝³ : L.CommShift ℤ<VAR>inst✝² : L.IsTriangulated<VAR>inst✝¹ : L.mapArrow.EssSurj<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>inst✝ : G.IsHomological<VAR>this✝ : F.PreservesZeroMorphisms<VAR>this : (L ⋙ F).IsHomological<GOAL>F.IsHomological
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : HasZeroObject C<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹³ : Pretriangulated C<VAR>inst✝¹² : Category.{u_5, u_2} D<VAR>inst✝¹¹ : HasZeroObject D<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁷ : Pretriangulated D<VAR>inst✝⁶ : Category.{u_6, u_3} A<VAR>inst✝⁵ : Abelian A<VAR>F✝ : C ⥤ A<VAR>inst✝⁴ : F✝.IsHomological<VAR>L : C ⥤ D<VAR>inst✝³ : L.CommShift ℤ<VAR>inst✝² : L.IsTriangulated<VAR>inst✝¹ : L.mapArrow.EssSurj<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>inst✝ : G.IsHomological<VAR>this✝ : F.PreservesZeroMorphisms<VAR>this : (L ⋙ F).IsHomological<VAR>T : Triangle D<VAR>hT : T ∈ distinguishedTriangles<GOAL>∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : HasZeroObject C<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹³ : Pretriangulated C<VAR>inst✝¹² : Category.{u_5, u_2} D<VAR>inst✝¹¹ : HasZeroObject D<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁷ : Pretriangulated D<VAR>inst✝⁶ : Category.{u_6, u_3} A<VAR>inst✝⁵ : Abelian A<VAR>F✝ : C ⥤ A<VAR>inst✝⁴ : F✝.IsHomological<VAR>L : C ⥤ D<VAR>inst✝³ : L.CommShift ℤ<VAR>inst✝² : L.IsTriangulated<VAR>inst✝¹ : L.mapArrow.EssSurj<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>inst✝ : G.IsHomological<VAR>this✝ : F.PreservesZeroMorphisms<VAR>this : (L ⋙ F).IsHomological<VAR>T : Triangle D<VAR>hT✝ : T ∈ distinguishedTriangles<VAR>hT : T ∈ L.essImageDistTriang<GOAL>∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : HasZeroObject C<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹³ : Pretriangulated C<VAR>inst✝¹² : Category.{u_5, u_2} D<VAR>inst✝¹¹ : HasZeroObject D<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁷ : Pretriangulated D<VAR>inst✝⁶ : Category.{u_6, u_3} A<VAR>inst✝⁵ : Abelian A<VAR>F✝ : C ⥤ A<VAR>inst✝⁴ : F✝.IsHomological<VAR>L : C ⥤ D<VAR>inst✝³ : L.CommShift ℤ<VAR>inst✝² : L.IsTriangulated<VAR>inst✝¹ : L.mapArrow.EssSurj<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e✝ : L ⋙ F ≅ G<VAR>inst✝ : G.IsHomological<VAR>this✝ : F.PreservesZeroMorphisms<VAR>this : (L ⋙ F).IsHomological<VAR>T : Triangle D<VAR>hT : T ∈ distinguishedTriangles<VAR>T₀ : Triangle C<VAR>e : T ≅ L.mapTriangle.obj T₀<VAR>hT₀ : T₀ ∈ distinguishedTriangles<GOAL>∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card + Fintype.card ↑(G.commonNeighbors v w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w) + Fintype.card ↑(G.commonNeighbors v w)
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card + (G.commonNeighbors v w).toFinset.card = 2 * k
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<GOAL>M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<GOAL>M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>ha : a ≠ 0<VAR>h : a = c * b⁻¹<GOAL>a * b = c
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>ha : a ≠ 0<VAR>h : a = c * b⁻¹<GOAL>b ≠ 0
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>h : MultilinearMap R t E<VAR>x✝ : (i : ι) → s i<GOAL>((lift h ∘ₗ map f).compMultilinearMap (tprod R)) x✝ = ((lift (h.compLinearMap f)).compMultilinearMap (tprod R)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : PredOrder α<VAR>a b i : α<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i<VAR>hin : ¬IsMax (succ^[n + 1 - 1] i)<GOAL>pred^[n + 1] (succ^[n + 1] i) = i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : PredOrder α<VAR>a b i : α<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i<VAR>hin : ¬IsMax (succ^[n] i)<GOAL>pred^[n + 1] (succ^[n + 1] i) = i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : PredOrder α<VAR>a b i : α<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i<VAR>hin : ¬IsMax (succ^[n] i)<VAR>h_not_max : ¬IsMax (succ^[n - 1] i)<GOAL>pred^[n + 1] (succ^[n + 1] i) = i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : PredOrder α<VAR>a b i : α<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i<VAR>hin : ¬IsMax (succ^[n] i)<VAR>h_not_max : ¬IsMax (succ^[n - 1] i)<GOAL>(pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : PredOrder α<VAR>a b i : α<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i<VAR>hin : ¬IsMax (succ^[n] i)<VAR>h_not_max : ¬IsMax (succ^[n - 1] i)<GOAL>pred^[n] (pred (succ (succ^[n] i))) = i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : PredOrder α<VAR>a b i : α<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i<VAR>hin : ¬IsMax (succ^[n] i)<VAR>h_not_max : ¬IsMax (succ^[n - 1] i)<GOAL>pred^[n] (succ^[n] i) = i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>p✝ q✝ : R[X]<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>p q : T[X]<VAR>hpq : p * q ≠ 0<GOAL>(p * q).aroots S = p.aroots S + q.aroots S
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>p✝ q✝ : R[X]<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>p q : T[X]<VAR>hpq : p * q ≠ 0<GOAL>map (algebraMap T S) p * map (algebraMap T S) q ≠ 0
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q✝ : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i✝ : Fin n<VAR>y : α i✝.castSucc<VAR>z : α (last n)<VAR>β : Type u_1<VAR>a : β<VAR>q : Fin n → β<VAR>b : β<VAR>i : Fin (n.succ + 1)<VAR>h : ¬i = 0<VAR>j : Fin (n + 1) := i.pred h<VAR>ji : j = i.pred h<GOAL>cons a (snoc q b) i = snoc (cons a q) b i
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q✝ : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i✝ : Fin n<VAR>y : α i✝.castSucc<VAR>z : α (last n)<VAR>β : Type u_1<VAR>a : β<VAR>q : Fin n → β<VAR>b : β<VAR>i : Fin (n.succ + 1)<VAR>h : ¬i = 0<VAR>j : Fin (n + 1) := i.pred h<VAR>ji : j = i.pred h<VAR>this : i = j.succ<GOAL>cons a (snoc q b) i = snoc (cons a q) b i
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q✝ : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i✝ : Fin n<VAR>y : α i✝.castSucc<VAR>z : α (last n)<VAR>β : Type u_1<VAR>a : β<VAR>q : Fin n → β<VAR>b : β<VAR>i : Fin (n.succ + 1)<VAR>h : ¬i = 0<VAR>j : Fin (n + 1) := i.pred h<VAR>ji : j = i.pred h<VAR>this : i = j.succ<GOAL>snoc q b j = snoc (cons a q) b j.succ
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q✝ : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i✝ : Fin n<VAR>y : α i✝.castSucc<VAR>z : α (last n)<VAR>β : Type u_1<VAR>a : β<VAR>q : Fin n → β<VAR>b : β<VAR>i : Fin (n.succ + 1)<VAR>h : ¬i = 0<VAR>j : Fin (n + 1) := i.pred h<VAR>ji : j = i.pred h<VAR>this : i = j.succ<VAR>h' : ¬↑j < n<GOAL>snoc q b j = snoc (cons a q) b j.succ
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q✝ : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i✝ : Fin n<VAR>y : α i✝.castSucc<VAR>z : α (last n)<VAR>β : Type u_1<VAR>a : β<VAR>q : Fin n → β<VAR>b : β<VAR>i : Fin (n.succ + 1)<VAR>h : ¬i = 0<VAR>j : Fin (n + 1) := i.pred h<VAR>ji : j = i.pred h<VAR>this : i = j.succ<VAR>h' : ¬↑j < n<GOAL>snoc q b (last n) = snoc (cons a q) b (last n.succ)
<VAR>x y : PartENat<GOAL>(x + y).toWithTop = x.toWithTop + y.toWithTop
<VAR>x y : PartENat<GOAL>(⊤ + ⊤).toWithTop = ⊤.toWithTop + ⊤.toWithTop
<VAR>x y : PartENat<GOAL>∀ (n : ℕ), (↑n + ⊤).toWithTop = (↑n).toWithTop + ⊤.toWithTop
<VAR>x y : PartENat<GOAL>∀ (n : ℕ), (⊤ + ↑n).toWithTop = ⊤.toWithTop + (↑n).toWithTop
<VAR>x y : PartENat<GOAL>∀ (n n_1 : ℕ), (↑n + ↑n_1).toWithTop = (↑n).toWithTop + (↑n_1).toWithTop
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>ha : a ∈ Ico 0 p<GOAL>↑a = 0 ↔ a = 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>ha : a ∈ Ico 0 p<VAR>h0 : 0 ∈ Ico 0 (0 + p)<GOAL>↑a = 0 ↔ a = 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>ha : a ∈ Ico 0 p<VAR>h0 : 0 ∈ Ico 0 (0 + p)<VAR>ha' : a ∈ Ico 0 (0 + p)<GOAL>↑a = 0 ↔ a = 0
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module A M₁<VAR>inst✝⁵ : SMulCommClass R A M₁<VAR>inst✝⁴ : SMulCommClass A R M₁<VAR>inst✝³ : IsScalarTower R A M₁<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Invertible 2<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm A M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>this : Subsingleton (Invertible 2)<GOAL>associated ((BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂)) ((BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂))) = (BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>V : Type u_8<VAR>N : Type u_9<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Invertible 2<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>Q : QuadraticForm K V<VAR>hQ : LinearMap.SeparatingLeft (associated Q)<GOAL>∃ w, Equivalent Q (weightedSumSquares K w)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>V : Type u_8<VAR>N : Type u_9<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Invertible 2<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>Q : QuadraticForm K V<VAR>hQ : LinearMap.SeparatingLeft (associated Q)<VAR>v : Basis (Fin (FiniteDimensional.finrank K V)) K V<VAR>hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v<GOAL>∃ w, Equivalent Q (weightedSumSquares K w)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>V : Type u_8<VAR>N : Type u_9<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Invertible 2<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>Q : QuadraticForm K V<VAR>hQ : LinearMap.SeparatingLeft (associated Q)<VAR>v : Basis (Fin (FiniteDimensional.finrank K V)) K V<VAR>hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v<VAR>hv₂ : ∀ (i : Fin (FiniteDimensional.finrank K V)), ¬LinearMap.IsOrtho ((associatedHom K) Q) (v i) (v i)<GOAL>∃ w, Equivalent Q (weightedSumSquares K w)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>V : Type u_8<VAR>N : Type u_9<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Invertible 2<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>Q : QuadraticForm K V<VAR>hQ : LinearMap.SeparatingLeft (associated Q)<VAR>v : Basis (Fin (FiniteDimensional.finrank K V)) K V<VAR>hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v<VAR>hv₂ : ∀ (i : Fin (FiniteDimensional.finrank K V)), ¬Q (v i) = 0<GOAL>∃ w, Equivalent Q (weightedSumSquares K w)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>opcyclesMap' φ h₁ h₂ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
<VAR>α✝ : Type u_1<VAR>A✝ : α✝ → PSet<VAR>i : (mk α✝ A✝).Type<GOAL>(mk α✝ A✝).Func i ∈ mk α✝ A✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : R →+* S<VAR>r : B<VAR>s : Set R<VAR>left✝ : s.Finite<VAR>hsr : IsIntegral (↥(Subring.closure s)) r<GOAL>IsIntegral R r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology α<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology α<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>ContinuousWithinAt f s (x.1, x.2) ↔ ContinuousWithinAt (fun x_1 => f ((x.1, x.2).1, x_1)) {b | ((x.1, x.2).1, b) ∈ s} (x.1, x.2).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology α<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>Tendsto f (map (Prod.mk x.1) (𝓝 x.2 ⊓ 𝓟 (Prod.mk x.1 ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔ Tendsto (fun x_1 => f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))
<VAR>R : Type u<VAR>inst✝¹⁰ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : Algebra R A<VAR>B : Type u<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsScalarTower R A B<VAR>inst✝³ : FormallyUnramified R A<VAR>inst✝² : FormallyUnramified A B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>f₁ = f₂
<VAR>R : Type u<VAR>inst✝¹⁰ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : Algebra R A<VAR>B : Type u<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsScalarTower R A B<VAR>inst✝³ : FormallyUnramified R A<VAR>inst✝² : FormallyUnramified A B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<VAR>e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)<GOAL>f₁ = f₂