ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯<GOAL>Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ prod.snd ≫ prod.fst = prod.fst ≫ prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f' : Filter α<VAR>g' : Filter β<GOAL>Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>∀ x ∈ s.powerset, ∀ y ∈ s.powerset, insert a x = insert a y → x = y
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>Disjoint s.powerset (image (insert a) s.powerset)
<VAR>α : Type u_3<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>f : α → Option β → γ<VAR>as : List α<VAR>bs : List β<GOAL>zipWithLeft f as bs = zipWithLeftTR f as bs
<VAR>α : Type u_3<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>f : α → Option β → γ<VAR>as : List α<VAR>bs : List β<VAR>acc : Array γ<VAR>head✝ : α<VAR>tail✝ : List α<GOAL>zipWithLeftTR.go f (head✝ :: tail✝) [] acc = acc.toList ++ zipWithLeft f (head✝ :: tail✝) []
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<GOAL>(fun s => ↑(μ.toFun s)) K₁ ≤ (fun s => ↑(μ.toFun s)) K₂
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : MvPolynomial τ R →+* S<VAR>g : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>f ((bind₁ g) φ) = (eval₂Hom (f.comp C) fun i => f (g i)) φ
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x < y<GOAL>deriv f x < deriv f y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → ℕ → Prop<VAR>h : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, P n k<GOAL>∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v : V<GOAL>Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v : V<GOAL>G.neighborSet v ∩ Gᶜ.neighborSet v ⊆ ∅
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>h : w ∈ G.neighborSet v<VAR>h' : w ∈ Gᶜ.neighborSet v<GOAL>w ∈ ∅
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>h : w ∈ G.neighborSet v<VAR>h' : v ≠ w ∧ ¬G.Adj v w<GOAL>w ∈ ∅
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x : R[X]<VAR>y : W.CoordinateRing<GOAL>(map W f) (x • y) = Polynomial.map f x • (map W f) y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x : R[X]<VAR>y : W.CoordinateRing<GOAL>(mk (WeierstrassCurve.map W f)) (C ((mapRingHom f) x)) * (map W f) y = (mk (WeierstrassCurve.map W f).toAffine) (C (Polynomial.map f x)) * (map W f) y
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<GOAL>p 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<GOAL>p₁ 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a✝ : A<VAR>ha✝ : p a✝<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>a : A<VAR>ha : p a<GOAL>∃ φ, ClosedEmbedding ⇑φ ∧ φ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a ∧ (∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), σₙ 𝕜 (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), p (φ f)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a✝ : A<VAR>ha✝ : p a✝<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>a : A<VAR>ha : p a<VAR>ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A := (↑(inrRangeEquiv 𝕜 A).symm).comp (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)<GOAL>∃ φ, ClosedEmbedding ⇑φ ∧ φ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a ∧ (∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), σₙ 𝕜 (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), p (φ f)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a✝ : A<VAR>ha✝ : p a✝<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>a : A<VAR>ha : p a<VAR>ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A := (↑(inrRangeEquiv 𝕜 A).symm).comp (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)<VAR>coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f<GOAL>∃ φ, ClosedEmbedding ⇑φ ∧ φ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a ∧ (∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), σₙ 𝕜 (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), p (φ f)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a✝ : A<VAR>ha✝ : p a✝<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>a : A<VAR>ha : p a<VAR>ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A := (↑(inrRangeEquiv 𝕜 A).symm).comp (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)<VAR>coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f<GOAL>ClosedEmbedding ⇑ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a✝ : A<VAR>ha✝ : p a✝<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>a : A<VAR>ha : p a<VAR>ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A := (↑(inrRangeEquiv 𝕜 A).symm).comp (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)<VAR>coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f<GOAL>ψ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a✝ : A<VAR>ha✝ : p a✝<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>a : A<VAR>ha : p a<VAR>ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A := (↑(inrRangeEquiv 𝕜 A).symm).comp (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)<VAR>coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<GOAL>σₙ 𝕜 (ψ f) = Set.range ⇑f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a✝ : A<VAR>ha✝ : p a✝<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>a : A<VAR>ha : p a<VAR>ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A := (↑(inrRangeEquiv 𝕜 A).symm).comp (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)<VAR>coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<GOAL>p (ψ f)
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>x : D<GOAL>x ∈ (map φ hφ S).objs ↔ x ∈ φ.obj '' S.objs
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>φ : NormedAddGroupHom V₁ V₂<VAR>ψ : NormedAddGroupHom W₁ W₂<VAR>φ' : NormedAddGroupHom V₂ V₃<VAR>ψ' : NormedAddGroupHom W₂ W₃<VAR>hf : ψ.comp f₁ = f₂.comp φ<VAR>hf' : ψ'.comp f₂ = f₃.comp φ'<GOAL>(ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>pred : ι → Prop<VAR>inst✝ : DecidablePred pred<VAR>h : ∀ i ∈ s, w i ≠ 0 → pred i<GOAL>(affineCombination k (filter pred s) p) w = (affineCombination k s p) w
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b✝ c✝ u : αˣ<VAR>b c : α<VAR>h : ↑a⁻¹ * b = c<GOAL>b = ↑a * c
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b✝ c✝ u : αˣ<VAR>b c : α<VAR>h : b = ↑a * c<GOAL>↑a⁻¹ * b = c
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>s : Set (α × α)<VAR>h : idRel ⊆ s<VAR>t : Set (α × α)<GOAL>t ⊆ (fun x => s ○ x)^[0] t
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>s : Set (α × α)<VAR>h : idRel ⊆ s<VAR>n : ℕ<VAR>ihn : ∀ {t : Set (α × α)}, t ⊆ (fun x => s ○ x)^[n] t<VAR>t : Set (α × α)<GOAL>t ⊆ (fun x => s ○ x)^[n + 1] t
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>h : M.Basis I X<GOAL>(M ↾ X).Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>h : (M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E<GOAL>(M ↾ X).Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>h : (M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E<GOAL>∀ (I_1 : Set α), M.Indep I_1 → I_1 ⊆ X → I ⊆ I_1 → I = I_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>f : α × β → γ<VAR>x : Filter α<VAR>y : Filter β<VAR>z : Filter γ<GOAL>Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a : R<VAR>a0 : ¬a = 0<GOAL>0 / a = 0
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>a : α<GOAL>(ofInjective f hf).symm ⟨f a, ⋯⟩ = a
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>a : α<GOAL>(ofInjective f hf) ((ofInjective f hf).symm ⟨f a, ⋯⟩) = (ofInjective f hf) a
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r s : R<GOAL>r + s ∈ σ (↑ₐ s + a) ↔ r ∈ σ a
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>cos (arcsin x) = √(1 - x ^ 2)
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<VAR>this : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1<GOAL>cos (arcsin x) = √(1 - x ^ 2)
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<VAR>this : cos (arcsin x) = √(1 - sin (arcsin x) ^ 2)<GOAL>cos (arcsin x) = √(1 - x ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>x : ℕ → Set α<GOAL>(⨅ i, 𝓟 (x i)).IsCountablyGenerated
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑u ↑v ↑w<VAR>f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }<VAR>h : f (p * p.mirror) = f (q * q.mirror)<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑u ↑v ↑w<VAR>f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }<VAR>h : C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = f (q * q.mirror)<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑u ↑v ↑w<VAR>f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }<VAR>h : C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = C ↑v * (C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n))<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑u ↑v ↑w<VAR>f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }<VAR>h : C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n) = C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n)<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑u ↑v ↑w<VAR>f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }<VAR>h : m + n = m' + n ∧ n - m + k + n = n - m' + k + n ∨ ↑u = ↑w ∧ m + n = n - m' + k + n ∧ n - m + k + n = m' + n ∨ ↑u + ↑w = 0 ∧ m + n = n - m + k + n ∧ m' + n = n - m' + k + n<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑u ↑v ↑w<VAR>f : ℤ[X] → ℤ[X] := fun p => { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp }<VAR>h : m = m' ∧ n - m = n - m' ∨ u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ ↑u + ↑w = 0 ∧ m = n - m + k ∧ m' = n - m' + k<GOAL>q = p ∨ q = p.mirror
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : (i : η) → AddCommMonoid (Ms i)<VAR>inst✝² : (i : η) → Module R (Ms i)<VAR>inst✝¹ : Fintype η<VAR>inst✝ : DecidableEq η<VAR>s : (j : η) → Basis (ιs j) R (Ms j)<VAR>j : η<VAR>i : ιs j<VAR>j' : η<VAR>i' : ιs j'<VAR>hj : ¬j = j'<GOAL>((Pi.basis s).repr ((stdBasis R Ms j) ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : (i : η) → AddCommMonoid (Ms i)<VAR>inst✝² : (i : η) → Module R (Ms i)<VAR>inst✝¹ : Fintype η<VAR>inst✝ : DecidableEq η<VAR>s : (j : η) → Basis (ιs j) R (Ms j)<VAR>j : η<VAR>i : ιs j<VAR>j' : η<VAR>i' : ιs j'<VAR>hj : ¬j = j'<GOAL>({ toFun := fun f i => (s i).repr (f i), map_add' := ⋯, map_smul' := ⋯, invFun := fun f i => (s i).repr.symm (f i), left_inv := ⋯, right_inv := ⋯ } ((stdBasis R Ms j) ((s j) i)) j') i' = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : (i : η) → AddCommMonoid (Ms i)<VAR>inst✝² : (i : η) → Module R (Ms i)<VAR>inst✝¹ : Fintype η<VAR>inst✝ : DecidableEq η<VAR>s : (j : η) → Basis (ιs j) R (Ms j)<VAR>j : η<VAR>i : ιs j<VAR>j' : η<VAR>i' : ιs j'<VAR>hj : ¬j = j'<GOAL>((s j').repr ((stdBasis R Ms j) ((s j) i) j')) i' = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : (i : η) → AddCommMonoid (Ms i)<VAR>inst✝² : (i : η) → Module R (Ms i)<VAR>inst✝¹ : Fintype η<VAR>inst✝ : DecidableEq η<VAR>s : (j : η) → Basis (ιs j) R (Ms j)<VAR>j : η<VAR>i : ιs j<VAR>j' : η<VAR>i' : ιs j'<VAR>hj : ¬j = j'<GOAL>⟨j, i⟩ ≠ ⟨j', i'⟩
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<VAR>s t : Set α<VAR>a : α<GOAL>↑L = ∅ ↔ L = ⊥
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.117700, u_1} C<VAR>inst✝³ : Category.{?u.117704, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain F K m<VAR>β : Cochain G K n<VAR>h : m + 1 = n<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + -1 = p₂<VAR>h₂₃ : p₂ + n = p₃<GOAL>p₁ + m = p₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.117704, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain F K m<VAR>β : Cochain G K n<VAR>h : m + 1 = n<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + -1 = p₂<VAR>h₂₃ : p₂ + n = p₃<GOAL>(inl φ).v p₁ p₂ h₁₂ ≫ (descCochain φ α β h).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<GOAL>dist x z ≤ max (dist x y) (dist y z)
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<GOAL>dist x x ≤ max (dist x y) (dist y x)
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>hxz : x ≠ z<GOAL>dist x z ≤ max (dist x y) (dist y z)
<VAR>E : ℕ → Type u_1<VAR>x z : (n : ℕ) → E n<VAR>hxz : x ≠ z<GOAL>dist x z ≤ max (dist x x) (dist x z)
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>hxz : x ≠ z<VAR>hxy : x ≠ y<GOAL>dist x z ≤ max (dist x y) (dist y z)
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>hxy hxz : x ≠ y<GOAL>dist x y ≤ max (dist x y) (dist y y)
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>hxz : x ≠ z<VAR>hxy : x ≠ y<VAR>hyz : y ≠ z<GOAL>dist x z ≤ max (dist x y) (dist y z)
<VAR>a b c : ℕ<VAR>h : a < b<GOAL>insert a (Ico a.succ b) = Ico a b
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ.Finite<GOAL>{γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite<GOAL>{γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite<VAR>x : ↥S<GOAL>x ∈ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔ x ∈ ⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite<VAR>x : ↥S<GOAL>x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ L ×ˢ K ∧ a / b = ↑x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝¹ : CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>N : ℝ≥0<VAR>h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖<VAR>inst✝ : RingHomIsometric σ₁₂<GOAL>‖f.extend e h_dense ⋯‖ ≤ ↑N * ‖f‖