ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.116938<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>i : ι₁<VAR>x : M₁ i<VAR>y : M₂'<GOAL>((toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i => (mk R (M₁ i) M₂').compr₂ (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)) ((lof R ι₁ M₁ i) x)) y = (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.116938<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>i : ι₁<VAR>x : M₁ i<VAR>y : M₂'<GOAL>(((mk R (M₁ i) M₂').compr₂ (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)) x) y = (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E B I X R J : Set α<VAR>M : Matroid α<GOAL>M = emptyOn α ∨ M.Nonempty
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E B I X R J : Set α<VAR>M : Matroid α<GOAL>M.E = ∅ ∨ M.Nonempty
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj (P.obj (op X))<GOAL>(Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯ ≫ colimit.ι (J.diagram P X) (op ⊤)) x = (colimit.ι (J.diagram P X) (op ⊤)) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj (P.obj (op X))<GOAL>(colimit.ι (J.diagram P X) (op ⊤)) ((Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x) = (colimit.ι (J.diagram P X) (op ⊤)) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj (P.obj (op X))<GOAL>(Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x = (Meq.equiv P ⊤).symm (Meq.mk ⊤ x)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj (P.obj (op X))<GOAL>(Meq.equiv P ⊤) ((Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x) = (Meq.equiv P ⊤) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj (P.obj (op X))<VAR>i : ⊤.Arrow<GOAL>↑((Meq.equiv P ⊤) ((Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x)) i = ↑((Meq.equiv P ⊤) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))) i
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj (P.obj (op X))<VAR>i : ⊤.Arrow<GOAL>(P.map i.f.op) x = ↑(Meq.mk ⊤ x) i
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} D'<VAR>X Y Z T : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(equiv W W.Q) ((mk W f).comp (mk W g)) = (equiv W W.Q) (mk W (f ≫ g))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.19181, u_1} C<VAR>inst✝ : Category.{?u.19185, u_2} D<VAR>F : C ⥤ Cat<VAR>X Y Z : Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(F.map (f ≫ g).base).obj X.fiber = (F.map g.base).obj ((F.map f.base).obj X.fiber)
<VAR>F : Type u<VAR>K : Type v<VAR>A : Type w<VAR>inst✝¹⁰ : Ring F<VAR>inst✝⁹ : Ring K<VAR>inst✝⁸ : AddCommGroup A<VAR>inst✝⁷ : Module F K<VAR>inst✝⁶ : Module K A<VAR>inst✝⁵ : Module F A<VAR>inst✝⁴ : IsScalarTower F K A<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : StrongRankCondition K<VAR>inst✝¹ : Module.Free F K<VAR>inst✝ : Module.Free K A<VAR>b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K<VAR>c : Basis (Module.Free.ChooseBasisIndex K A) K A := Module.Free.chooseBasis K A<GOAL>lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
<VAR>α β γ : Type u<VAR>S S' : Set (α → ℕ)<VAR>l : List (Set (α → ℕ))<VAR>d : List.Forall Dioph l<GOAL>Dioph {v | List.Forall (fun S => v ∈ S) l}
<VAR>α β γ : Type u<VAR>S S' : Set (α → ℕ)<VAR>l : List (Set (α → ℕ))<VAR>d : List.Forall Dioph l<GOAL>∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
<VAR>α β γ : Type u<VAR>S✝ S' S : Set (α → ℕ)<VAR>l : List (Set (α → ℕ))<VAR>IH : List.Forall Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl<VAR>d : List.Forall Dioph (S :: l)<GOAL>∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) (S :: l) ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
<VAR>α β γ : Type u<VAR>S✝ S' S : Set (α → ℕ)<VAR>l : List (Set (α → ℕ))<VAR>IH : List.Forall Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl<VAR>d : Dioph S ∧ List.Forall Dioph l<GOAL>∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) (S :: l) ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>f : M ≃ₗ[A] M<GOAL>LinearMap.det ↑f.symm * LinearMap.det ↑f = 1
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : WellPowered C<VAR>inst✝ : HasWidePullbacks C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>k : ∀ g ∈ s, f ≤ g<GOAL>f ≤ sInf s
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : WellPowered C<VAR>inst✝ : HasWidePullbacks C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>k : ∀ g ∈ s, f ≤ g<GOAL>underlying.obj f ⟶ underlying.obj (sInf s)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : WellPowered C<VAR>inst✝ : HasWidePullbacks C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>k : ∀ g ∈ s, f ≤ g<GOAL>?f ≫ (sInf s).arrow = f.arrow
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s<GOAL>y ∈ posTangentConeAt s x
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a✝ x y : E<VAR>h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s<VAR>a : ℕ → ℝ<VAR>ha : Tendsto a atTop (𝓝[>] 0)<VAR>has : ∀ (n : ℕ), x + a n • y ∈ s<GOAL>y ∈ posTangentConeAt s x
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a✝ x y : E<VAR>h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s<VAR>a : ℕ → ℝ<VAR>ha : Tendsto a atTop (𝓝[>] 0)<VAR>has : ∀ (n : ℕ), x + a n • y ∈ s<GOAL>Tendsto (fun n => a⁻¹ n • (fun x => a x • y) n) atTop (𝓝 y)
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a✝ x y : E<VAR>h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s<VAR>a : ℕ → ℝ<VAR>ha : Tendsto a atTop (𝓝[>] 0)<VAR>has : ∀ (n : ℕ), x + a n • y ∈ s<GOAL>(fun x => y) =ᶠ[atTop] fun n => a⁻¹ n • (fun x => a x • y) n
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a✝ x y : E<VAR>h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s<VAR>a : ℕ → ℝ<VAR>ha : Tendsto a atTop (𝓝[>] 0)<VAR>has : ∀ (n : ℕ), x + a n • y ∈ s<VAR>n : ℕ<VAR>hn : 0 < a n<GOAL>y = a⁻¹ n • a n • y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite β<VAR>f : α → β<VAR>hf : Injective f<GOAL>Nat.card α ≤ Nat.card β
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<VAR>A : 0 < μ (u ∩ s)<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<VAR>A : 0 < μ (u ∩ s)<VAR>B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<VAR>A : 0 < μ (u ∩ μ.everywherePosSubset s)<VAR>B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s<GOAL>0 < μ n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<VAR>I : Ideal S<GOAL>⇑(comap f) '' zeroLocus ↑I = zeroLocus ↑(Ideal.comap f I)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<VAR>I : Ideal S<GOAL>∀ (x : PrimeSpectrum R), (∃ x_1, I ≤ x_1.asIdeal ∧ (comap f) x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set β<VAR>hs : IsPreconnected s<VAR>f : α → β<VAR>hinj : Injective f<VAR>hf : IsClosedMap f<VAR>hsf : s ⊆ range f<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hsuv : f ⁻¹' s ⊆ u ∪ v<VAR>hsu : (f ⁻¹' s ∩ u).Nonempty<VAR>hsv : (f ⁻¹' s ∩ v).Nonempty<GOAL>(f ⁻¹' s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set β<VAR>hs : IsPreconnected s<VAR>f : α → β<VAR>hinj : Injective f<VAR>hf : IsClosedMap f<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hsuv : f ⁻¹' s ⊆ u ∪ v<VAR>hsu : (f ⁻¹' s ∩ u).Nonempty<VAR>hsv : (f ⁻¹' s ∩ v).Nonempty<VAR>hsf : f '' (f ⁻¹' s) = s<GOAL>(f ⁻¹' s ∩ (u ∩ v)).Nonempty
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.68862, u_1} C<VAR>inst✝² : Preadditive C<VAR>A : Type u_2<VAR>inst✝¹ : Category.{u_3, u_2} A<VAR>inst✝ : Abelian A<VAR>X : SimplicialObject A<VAR>n : ℕ<GOAL>(id (ChainComplex.ofHom (fun n => underlying.obj (NormalizedMooreComplex.objX X n)) (NormalizedMooreComplex.objD X) ⋯ (fun n => X _[n]) (AlternatingFaceMapComplex.objD X) ⋯ (fun n => (NormalizedMooreComplex.objX X n).arrow) ⋯)).f n = (NormalizedMooreComplex.objX X n).arrow
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<VAR>y z : α<VAR>hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y<VAR>i : ℤ<VAR>hi : (f ^ i) z = x<VAR>hyx : ¬y = x<VAR>hfyx : ¬y = f x<GOAL>f y = (swap x (f x)) y
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<VAR>y z : α<VAR>hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y<VAR>i : ℤ<VAR>hi : (f ^ i) z = x<VAR>hyx : ¬y = x<VAR>hfyx : ¬y = f x<GOAL>f y = y
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<VAR>y z : α<VAR>hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y<VAR>i : ℤ<VAR>hi : (f ^ i) z = x<VAR>hyx : ¬y = x<VAR>hfyx : ¬y = f x<VAR>hy : ¬f y = y<GOAL>False
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<VAR>y z : α<VAR>hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y<VAR>i : ℤ<VAR>hi : (f ^ i) z = x<VAR>hyx : ¬y = x<VAR>hfyx : ¬y = f x<VAR>hy : ¬f y = y<VAR>j : ℤ<VAR>hj : (f ^ j) z = y<GOAL>False
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<VAR>y z : α<VAR>hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y<VAR>i : ℤ<VAR>hi : (f ^ i) z = x<VAR>hyx : ¬y = x<VAR>hfyx : ¬y = f x<VAR>hy : ¬f y = y<VAR>j : ℤ<VAR>hj : (f ^ (j - i)) x = y<GOAL>False
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<VAR>y z : α<VAR>hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y<VAR>i : ℤ<VAR>hi : (f ^ i) z = x<VAR>hyx : ¬y = x<VAR>hfyx : ¬y = f x<VAR>hy : ¬f y = y<VAR>j : ℤ<VAR>hj : (f ^ (j - i)) x = y<VAR>hji : (f ^ (j - i)) x = x<GOAL>False
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<VAR>y z : α<VAR>hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y<VAR>i : ℤ<VAR>hi : (f ^ i) z = x<VAR>hyx : ¬y = x<VAR>hfyx : ¬y = f x<VAR>hy : ¬f y = y<VAR>j : ℤ<VAR>hj : (f ^ (j - i)) x = y<VAR>hji : (f ^ (j - i)) x = f x<GOAL>False
<VAR>x y z : PGame<GOAL>⟦(y + -z) * x⟧ = ⟦y * x⟧ + -⟦z * x⟧
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≤ 1<GOAL>Principal (fun x x_1 => x + x_1) o
<VAR>ho : 0 ≤ 1<GOAL>Principal (fun x x_1 => x + x_1) 0
<VAR>ho : 1 ≤ 1<GOAL>Principal (fun x x_1 => x + x_1) 1
<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 : α<GOAL>toIcoMod hp (p + a) b = p + toIcoMod hp a b
<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>f : E → F<VAR>t : Set E<VAR>s : Set (E →L[𝕜] F)<VAR>x : E<GOAL>fderivWithin 𝕜 f t x ∈ s ↔ DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.210892, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝ : S.HasRightHomology<VAR>A' : C<VAR>α : A ⟶ A'<GOAL>S.f ≫ k ≫ α = 0
<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>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝ : S.HasRightHomology<VAR>A' : C<VAR>α : A ⟶ A'<GOAL>S.descOpcycles k hk ≫ α = S.descOpcycles (k ≫ α) ⋯
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.base<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.base<VAR>this : IsIso (forgetToPresheafedSpace.map f)<GOAL>IsIso f
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝¹¹ : Ring 𝕜<VAR>n : ℕ<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module 𝕜 E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalAddGroup E<VAR>inst✝⁶ : ContinuousConstSMul 𝕜 E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : TopologicalAddGroup F<VAR>inst✝¹ : ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : DecidablePred fun n => p n ≠ 0<VAR>hp : ∃ n, p n ≠ 0<GOAL>p.order = Nat.find hp
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>↑(xn a1 (n + 2)) + ↑(xn a1 n) = ↑(2 * a) * ↑(xn a1 (n + 1))
<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>hg : Inducing g<GOAL>Continuous f ↔ Continuous (g ∘ f)
<VAR>α : Type u_1<VAR>inst✝ : Field α<VAR>n1 n2 k e1 e2 t1 : α<VAR>h1 : n1 * e1 = t1<VAR>h2 : n2 / e2 = 1<VAR>h3 : n1 * n2 = k<GOAL>k * (e1 / e2) = t1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonAssocSemiring α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j✝ : n<GOAL>(1 * M) i✝ j✝ = M i✝ j✝
<VAR>ι : Type u'<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>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>n : ℕ<VAR>v : Fin (n + 1) → V<GOAL>LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ span K (range (Fin.tail v))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>m : MeasurableSpace α<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<GOAL>0 ≤ setToSimpleFunc T f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>m : MeasurableSpace α<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>i : G'<VAR>hi : i ∈ f.range<GOAL>0 ≤ i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>m : MeasurableSpace α<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>i : G'<VAR>hi : i ∈ Set.range ↑f<GOAL>0 ≤ i