ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ : List α<VAR>f : α → β<VAR>l : List α<VAR>ihl : map f l ∈ {l | ∀ x ∈ l, x ∈ range f} → map f l ∈ range (map f)<VAR>a : α<VAR>hl : f a :: map f l ∈ {l | ∀ x ∈ l, x ∈ range f}<GOAL>f a :: map f l ∈ range (map f)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<GOAL>Measurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<GOAL>Measurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<GOAL>Measurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<GOAL>Measurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<GOAL>Measurable (U n)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_meas : Measurable fun p => u (↑p.1) p.2<GOAL>Measurable (U n)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_meas : Measurable fun p => u (↑p.1) p.2<VAR>this : (fun p => u (↑(t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2)<GOAL>Measurable (U n)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_meas : Measurable fun p => u (↑p.1) p.2<VAR>this : (fun p => u (↑(t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2)<GOAL>Measurable ((fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_meas : Measurable fun p => u (↑p.1) p.2<VAR>this : (fun p => u (↑(t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2)<GOAL>Measurable fun p => ⟨↑(t_sf n) p.1, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v : Fin 2 → R<VAR>hab : IsCoprime (v 0) (v 1)<VAR>A : SL(2, R)<GOAL>IsCoprime ((↑A *ᵥ v) 0) ((↑A *ᵥ v) 1)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<GOAL>p ⊓ ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⨆ μ, ⨆ k, p ⊓ (f.genEigenspace μ) k
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<GOAL>p ⊓ ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⨆ μ, p ⊓ ⨆ i, (f.genEigenspace μ) i
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>m : V<VAR>hm : m ∈ p ⊓ ⨆ μ, ⨆ k, (f.genEigenspace μ) k<GOAL>m ∈ ⨆ μ, p ⊓ ⨆ i, (f.genEigenspace μ) i
<VAR>I : Type u<VAR>inst✝²⁵ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝²⁴ : Category.{u_2, u_1} C<VAR>inst✝²³ : MonoidalCategory C<VAR>X₁ X₂ X₃ X₄ : GradedObject I C<VAR>inst✝²² : X₁.HasTensor X₂<VAR>inst✝²¹ : X₂.HasTensor X₃<VAR>inst✝²⁰ : X₃.HasTensor X₄<VAR>inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄<VAR>inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄<VAR>inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄<VAR>inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)<VAR>inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄<VAR>inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄<VAR>inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄<VAR>inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄<VAR>inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄<VAR>inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)<VAR>inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄<GOAL>tensorHom (associator X₁ X₂ X₃).hom (𝟙 X₄) ≫ (associator X₁ (tensorObj X₂ X₃) X₄).hom ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).hom = (associator (tensorObj X₁ X₂) X₃ X₄).hom ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).hom
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>|re z| ≤ ‖z‖
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>re z * re z ≤ normSq z
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : Field k<VAR>f : R →+* k<GOAL>IsUnit (map f p) ↔ IsUnit p
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (n + 1)<VAR>hj₁ : n + 1 ≤ ↑j + (q + 1)<GOAL>(φ ≫ (𝟙 (X _[n + 1]) + (Hσ q).f (n + 1))) ≫ X.δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (n + 1)<VAR>hj₁ : n + 1 ≤ ↑j + (q + 1)<GOAL>φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (n + 1)<VAR>hj₁ : n + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬n < q<GOAL>φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (n + 1)<VAR>hj₁ : n + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬n < q<VAR>a : ℕ<VAR>ha : q + a = n<GOAL>φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (n + 1)<VAR>hj₁ : n + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬n < q<VAR>a : ℕ<VAR>ha : q + a = n<GOAL>φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>q a m : ℕ<VAR>φ : Y ⟶ X _[m + 1 + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (m + 1 + 1)<VAR>hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬m + 1 < q<VAR>ha : q + a = m + 1<VAR>hj₂ : ¬a = ↑j<GOAL>φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>q a m : ℕ<VAR>φ : Y ⟶ X _[m + 1 + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (m + 1 + 1)<VAR>hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬m + 1 < q<VAR>ha : q + a = m + 1<VAR>hj₂ : ¬a = ↑j<VAR>haj : a < ↑j<GOAL>φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>q a m : ℕ<VAR>φ : Y ⟶ X _[m + 1 + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (m + 1 + 1)<VAR>hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬m + 1 < q<VAR>ha : q + a = m + 1<VAR>hj₂ : ¬a = ↑j<VAR>haj : a < ↑j<VAR>ham : a ≤ m<GOAL>φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>q a m : ℕ<VAR>φ : Y ⟶ X _[m + 1 + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (m + 1 + 1)<VAR>hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬m + 1 < q<VAR>ha : q + a = m + 1<VAR>hj₂ : ¬a = ↑j<VAR>haj : a < ↑j<VAR>ham : a ≤ m<GOAL>φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>q a m : ℕ<VAR>φ : Y ⟶ X _[m + 1 + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (m + 1 + 1)<VAR>hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)<VAR>hqn : ¬m + 1 < q<VAR>ha : q + a = m + 1<VAR>hj₂ : ¬a = ↑j<VAR>haj : a < ↑j<VAR>ham : a ≤ m<GOAL>⟨a, ⋯⟩.succ < j.succ
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>q n : ℕ<GOAL>G.map ((Q q).f n) = (Q q).f n
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>q n : ℕ<GOAL>G.map (𝟙 (X _[n])) = 𝟙 (((whiskering C D).obj G).obj X _[n])
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ p f : Perm α<VAR>h : p ∈ f.cycleFactorsFinset<GOAL>p.support ≤ f.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ p f : Perm α<VAR>h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a<GOAL>p.support ≤ f.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ p f : Perm α<VAR>h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a<VAR>x : α<VAR>hx : x ∈ p.support<GOAL>x ∈ f.support
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V₁<VAR>inst✝¹⁰ : Module k V₁<VAR>inst✝⁹ : AffineSpace V₁ P₁<VAR>inst✝⁸ : AddCommGroup V₂<VAR>inst✝⁷ : Module k V₂<VAR>inst✝⁶ : AffineSpace V₂ P₂<VAR>inst✝⁵ : AddCommGroup V₃<VAR>inst✝⁴ : Module k V₃<VAR>inst✝³ : AffineSpace V₃ P₃<VAR>inst✝² : AddCommGroup V₄<VAR>inst✝¹ : Module k V₄<VAR>inst✝ : AffineSpace V₄ P₄<VAR>e : P₁ ≃ P₂<VAR>el : V₁ ≃ₗ[k] V₂<VAR>h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p<VAR>e' : P₁ ≃ P₂<VAR>el' : V₁ ≃ₗ[k] V₂<VAR>h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p<VAR>H : ↑{ toEquiv := e, linear := el, map_vadd' := h } = ↑{ toEquiv := e', linear := el', map_vadd' := h' }<GOAL>{ toEquiv := e, linear := el, map_vadd' := h } = { toEquiv := e', linear := el', map_vadd' := h' }
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V₁<VAR>inst✝¹⁰ : Module k V₁<VAR>inst✝⁹ : AffineSpace V₁ P₁<VAR>inst✝⁸ : AddCommGroup V₂<VAR>inst✝⁷ : Module k V₂<VAR>inst✝⁶ : AffineSpace V₂ P₂<VAR>inst✝⁵ : AddCommGroup V₃<VAR>inst✝⁴ : Module k V₃<VAR>inst✝³ : AffineSpace V₃ P₃<VAR>inst✝² : AddCommGroup V₄<VAR>inst✝¹ : Module k V₄<VAR>inst✝ : AffineSpace V₄ P₄<VAR>e : P₁ ≃ P₂<VAR>el : V₁ ≃ₗ[k] V₂<VAR>h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p<VAR>e' : P₁ ≃ P₂<VAR>el' : V₁ ≃ₗ[k] V₂<VAR>h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p<VAR>H : e = e' ∧ el = el'<GOAL>{ toEquiv := e, linear := el, map_vadd' := h } = { toEquiv := e', linear := el', map_vadd' := h' }
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V₁<VAR>inst✝¹⁰ : Module k V₁<VAR>inst✝⁹ : AffineSpace V₁ P₁<VAR>inst✝⁸ : AddCommGroup V₂<VAR>inst✝⁷ : Module k V₂<VAR>inst✝⁶ : AffineSpace V₂ P₂<VAR>inst✝⁵ : AddCommGroup V₃<VAR>inst✝⁴ : Module k V₃<VAR>inst✝³ : AffineSpace V₃ P₃<VAR>inst✝² : AddCommGroup V₄<VAR>inst✝¹ : Module k V₄<VAR>inst✝ : AffineSpace V₄ P₄<VAR>e : P₁ ≃ P₂<VAR>el : V₁ ≃ₗ[k] V₂<VAR>h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p<VAR>e' : P₁ ≃ P₂<VAR>el' : V₁ ≃ₗ[k] V₂<VAR>h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p<VAR>H : e = e' ∧ el = el'<GOAL>e = e'
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V₁<VAR>inst✝¹⁰ : Module k V₁<VAR>inst✝⁹ : AffineSpace V₁ P₁<VAR>inst✝⁸ : AddCommGroup V₂<VAR>inst✝⁷ : Module k V₂<VAR>inst✝⁶ : AffineSpace V₂ P₂<VAR>inst✝⁵ : AddCommGroup V₃<VAR>inst✝⁴ : Module k V₃<VAR>inst✝³ : AffineSpace V₃ P₃<VAR>inst✝² : AddCommGroup V₄<VAR>inst✝¹ : Module k V₄<VAR>inst✝ : AffineSpace V₄ P₄<VAR>e : P₁ ≃ P₂<VAR>el : V₁ ≃ₗ[k] V₂<VAR>h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p<VAR>e' : P₁ ≃ P₂<VAR>el' : V₁ ≃ₗ[k] V₂<VAR>h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p<VAR>H : e = e' ∧ el = el'<GOAL>el = el'
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p q P : α → Prop<GOAL>(∃ a, P a) ∨ ∀ (a : α), ¬P a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p q P : α → Prop<GOAL>(∃ a, P a) ∨ ¬∃ x, P x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Ring α<VAR>inst✝¹ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x✝ y✝ : α<VAR>hf : IsRingHom f<VAR>γ : Type u_1<VAR>inst✝ : Ring γ<VAR>g : β → γ<VAR>hg : IsRingHom g<VAR>x y : α<GOAL>(g ∘ f) (x + y) = (g ∘ f) x + (g ∘ f) y
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Ring α<VAR>inst✝¹ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x✝ y✝ : α<VAR>hf : IsRingHom f<VAR>γ : Type u_1<VAR>inst✝ : Ring γ<VAR>g : β → γ<VAR>hg : IsRingHom g<VAR>x y : α<GOAL>(g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Ring α<VAR>inst✝¹ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x y : α<VAR>hf : IsRingHom f<VAR>γ : Type u_1<VAR>inst✝ : Ring γ<VAR>g : β → γ<VAR>hg : IsRingHom g<GOAL>(g ∘ f) 1 = 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : r.size = 0 → l.size ≤ 1<VAR>H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size<VAR>H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3<GOAL>Valid' o₁ (l.balanceR x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : r.size = 0 → l.size ≤ 1<VAR>H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size<VAR>H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3<GOAL>Valid' o₂ (r.dual.balanceL x l.dual) o₁
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : r.size = 0 → l.size ≤ 1<VAR>H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size<VAR>H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3<VAR>this : (r.dual.size = 0 → l.dual.size ≤ 1) → (1 ≤ r.dual.size → 1 ≤ l.dual.size → l.dual.size ≤ delta * r.dual.size) → 2 * r.dual.size ≤ 9 * l.dual.size + 5 ∨ r.dual.size ≤ 3 → Valid' o₂ (r.dual.balanceL x l.dual) o₁<GOAL>Valid' o₂ (r.dual.balanceL x l.dual) o₁
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : r.size = 0 → l.size ≤ 1<VAR>H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size<VAR>H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3<VAR>this : (r.size = 0 → l.size ≤ 1) → (1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size) → 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3 → Valid' o₂ (r.dual.balanceL x l.dual) o₁<GOAL>Valid' o₂ (r.dual.balanceL x l.dual) o₁
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n m : ℕ<VAR>f : R⟦X⟧<VAR>h : n < m<GOAL>(coeff R n) ↑(trunc m f) = (coeff R n) f
<VAR>X : Type u_1<VAR>a : FreeAbelianGroup X<GOAL>(-a).support = a.support
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝² : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>f : (i : I) → A ⥤ C i<VAR>i : I<GOAL>pi' f ⋙ Pi.eval C i = f i
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝² : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>f : (i : I) → A ⥤ C i<VAR>i : I<GOAL>autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), (pi' f ⋙ Pi.eval C i).map f_1 = eqToHom ⋯ ≫ (f i).map f_1 ≫ eqToHom ⋯) _auto✝
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝² : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>f : (i : I) → A ⥤ C i<VAR>i : I<GOAL>∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<GOAL>yn a1 n ∣ yn a1 (n * (k + 1))
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<GOAL>yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<GOAL>Injective f ↔ (Injective fun x => f (some x)) ∧ ∀ (x : α), ¬f (some x) = f none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<GOAL>((Injective fun x => f (some x)) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<VAR>h_some : Injective fun x => f (some x)<VAR>h_none : ∀ (x : α), ¬f (some x) = f none<VAR>hab : f none = f none<GOAL>none = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<VAR>h_some : Injective fun x => f (some x)<VAR>h_none : ∀ (x : α), ¬f (some x) = f none<VAR>b : α<VAR>hab : f none = f (some b)<GOAL>none = some b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<VAR>h_some : Injective fun x => f (some x)<VAR>h_none : ∀ (x : α), ¬f (some x) = f none<VAR>a : α<VAR>hab : f (some a) = f none<GOAL>some a = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α → β<VAR>h_some : Injective fun x => f (some x)<VAR>h_none : ∀ (x : α), ¬f (some x) = f none<VAR>a b : α<VAR>hab : f (some a) = f (some b)<GOAL>some a = some b