ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{?u.37783, u_2} D<VAR>F : C ⥤ Cat<VAR>G : C ⥤ Cat<GOAL>map (𝟙 F) = 𝟙 (Cat.of (Grothendieck F))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{?u.37783, u_2} D<VAR>F : C ⥤ Cat<VAR>G : C ⥤ Cat<GOAL>∀ (X : Grothendieck F), (map (𝟙 F)).obj X = (𝟙 (Cat.of (Grothendieck F))).obj X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{?u.37783, u_2} D<VAR>F : C ⥤ Cat<VAR>G : C ⥤ Cat<GOAL>autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟙 (Cat.of (Grothendieck F))).map f ≫ eqToHom ⋯) _auto✝
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>x y : V → α<GOAL>x ⬝ᵥ adjMatrix α G *ᵥ y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Ring R<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Injective ⇑f<VAR>n : ℕ<GOAL>Submodule.map (((f.tunnel' i n).fst.subtype ∘ₗ ↑(f.tunnel' i n).snd.symm) ∘ₗ f) (Submodule.snd R M N) ≤ OrderDual.ofDual ((f.tunnel i) n)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Ring R<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Injective ⇑f<VAR>n : ℕ<GOAL>Submodule.map (f.tunnel' i n).fst.subtype (Submodule.map (↑(f.tunnel' i n).snd.symm) (Submodule.map f (Submodule.snd R M N))) ≤ OrderDual.ofDual ((f.tunnel i) n)
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>Φ : Paths V ⥤ C<GOAL>Φ = lift (of ⋙q Φ.toPrefunctor)
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>Φ : Paths V ⥤ C<GOAL>∀ (X : Paths V), Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>Φ : Paths V ⥤ C<GOAL>autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯) _auto✝
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<GOAL>Measurable fun x => map (Prod.mk x) ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<GOAL>∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => (map (Prod.mk b) ν) s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => (map (Prod.mk b) ν) s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => ν (Prod.mk b ⁻¹' s)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>QuasiIsoAt f i ↔ IsIso (homologyMap f i)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsIso (homologyMap f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>inst✝ : IsEmpty α<VAR>f : α → β<VAR>la : Filter α<VAR>lb : Filter β<GOAL>Tendsto f la lb
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<GOAL>∀ {a : α}, s.max = ↑a → a ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<GOAL>∀ {a : α}, ∅.max = ↑a → a ∈ ∅
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>b : α<VAR>s : Finset α<VAR>a✝ : b ∉ s<VAR>ih : ∀ {a : α}, s.max = ↑a → a ∈ s<GOAL>∀ {a : α}, (insert b s).max = ↑a → a ∈ insert b s
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesLimit (cospan h i) F<VAR>s : IsPullback f g h i<GOAL>IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesLimit (cospan h i) F<VAR>s : IsPullback f g h i<GOAL>((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅ ⋯.cone.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesLimit (cospan h i) F<VAR>s : IsPullback f g h i<GOAL>((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left = ?refine_1.hom ≫ ⋯.cone.π.app WalkingCospan.left
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesLimit (cospan h i) F<VAR>s : IsPullback f g h i<GOAL>((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right = ?refine_1.hom ≫ ⋯.cone.π.app WalkingCospan.right
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h₁ : Continuous f<VAR>h₂ : Injective f<VAR>h₃ : IsOpenMap f<GOAL>OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h₁ : Continuous f<VAR>h₂ : Injective f<VAR>h₃ : IsOpenMap f<GOAL>∀ (x : X), 𝓝 x = comap f (𝓝 (f x))
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{?u.88315, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>a : R<GOAL>a • φ₁.τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{?u.88315, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>a : R<GOAL>a • (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{?u.88315, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>a : R<GOAL>a • φ₁.τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{?u.88315, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>a : R<GOAL>a • (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{?u.88315, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>a : R<GOAL>a • φ₁.τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{?u.88315, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>a : R<GOAL>a • (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>q : α → Prop<GOAL>(∀ᶠ (x : α) in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>normEDS b c d (2 * (↑m + 3)) * b = normEDS b c d (↑m + 2) ^ 2 * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 5) - normEDS b c d (↑m + 1) * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 4) ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>(preNormEDS' (b ^ 4) c d (2 * (m + 3)) * if Even (2 * (m + 3)) then b else 1) * b = (preNormEDS' (b ^ 4) c d (m + 2) * if Even (m + 2) then b else 1) ^ 2 * (preNormEDS' (b ^ 4) c d (m + 3) * if Even (m + 3) then b else 1) * (preNormEDS' (b ^ 4) c d (m + 5) * if Even (m + 5) then b else 1) - (preNormEDS' (b ^ 4) c d (m + 1) * if Even (m + 1) then b else 1) * (preNormEDS' (b ^ 4) c d (m + 3) * if Even (m + 3) then b else 1) * (preNormEDS' (b ^ 4) c d (m + 4) * if Even (m + 4) then b else 1) ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>(preNormEDS' (b ^ 4) c d (m + 2) ^ 2 * preNormEDS' (b ^ 4) c d (m + 3) * preNormEDS' (b ^ 4) c d (m + 5) - preNormEDS' (b ^ 4) c d (m + 1) * preNormEDS' (b ^ 4) c d (m + 3) * preNormEDS' (b ^ 4) c d (m + 4) ^ 2) * b * b = (preNormEDS' (b ^ 4) c d (m + 2) * if Even m then b else 1) ^ 2 * (preNormEDS' (b ^ 4) c d (m + 3) * if Even m then 1 else b) * (preNormEDS' (b ^ 4) c d (m + 5) * if Even m then 1 else b) - (preNormEDS' (b ^ 4) c d (m + 1) * if Even m then 1 else b) * (preNormEDS' (b ^ 4) c d (m + 3) * if Even m then 1 else b) * (preNormEDS' (b ^ 4) c d (m + 4) * if Even m then b else 1) ^ 2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : CommSemigroup R<VAR>inst✝ : StarMul R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x * y)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>g : N → N'<VAR>r : Set N<VAR>y : N<VAR>hf : ContMDiffAt I I' n f x<VAR>hg : ContMDiffAt J J' n g y<GOAL>ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>g : N → N'<VAR>r : Set N<VAR>y : N<VAR>hf : ContMDiffWithinAt I I' n f univ x<VAR>hg : ContMDiffWithinAt J J' n g univ y<GOAL>ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) univ (x, y)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>g : N → N'<VAR>r : Set N<VAR>y : N<VAR>hf : ContMDiffWithinAt I I' n f univ x<VAR>hg : ContMDiffWithinAt J J' n g univ y<GOAL>univ = univ ×ˢ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : IsBasis p s<GOAL>h.filter = generate {U | ∃ i, p i ∧ s i = U}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : IsBasis p s<GOAL>h.filter = h.filterBasis.filter
<VAR>n m : ℕ<VAR>a b c : Fin n<GOAL>a ≤ b → a < b ∨ a = b
<VAR>n m : ℕ<VAR>a b c : Fin n<GOAL>a ≤ b → a < b ∨ ↑a = ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set β<GOAL>kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r₁ r₂ : ℝ<GOAL>⟪r₂ • x, r₁ • (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>d : Derivation R A ↥I<VAR>x : A<GOAL>(Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x
<VAR>G : Type u_1<VAR>G'✝ : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group G'✝<VAR>inst✝⁶ : Group G''<VAR>A : Type u_4<VAR>inst✝⁵ : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Group N<VAR>inst✝³ : Group P<VAR>K : Subgroup G<VAR>M : Type u_7<VAR>inst✝² : MulOneClass M<VAR>G' : Type u_8<VAR>N' : Type u_9<VAR>inst✝¹ : Group G'<VAR>inst✝ : Group N'<VAR>f : G →* N<VAR>g : G' →* N'<GOAL>(f.prodMap g).ker = f.ker.prod g.ker
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R✝ N<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>s : Finset A<VAR>hs : span R ↑s = ⊤<VAR>t : Finset M<VAR>ht : span A ↑t = ⊤<GOAL>span R (image2 (fun x x_1 => x • x_1) ↑s ↑t) = ⊤
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>((-o).areaForm x) y = ((-o.areaForm) x) y
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : MulZeroClass α<VAR>s✝ t s : Finset α<GOAL>s * 0 ⊆ 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>Quot.mk Setoid.r I = mk I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>Quot.mk Setoid.r I = ((QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range).comp (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ)) I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>Quot.mk Setoid.r I = (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range) ((MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>Quot.mk Setoid.r I = ↑I
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ✝<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f'✝ : α → β → γ✝<VAR>g✝ g'✝ : α → β → γ✝ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u✝ u' : Finset γ✝<VAR>a a' : α<VAR>b b' : β<VAR>c : γ✝<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → ε' → ε<VAR>g' : β → γ → ε'<VAR>h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)<GOAL>image2 f (image2 g ↑s ↑t) ↑u = image2 f' (↑s) (image2 g' ↑t ↑u)