ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this : PreservesFiniteLimits (forget₂ C Ab)<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (forget C).map (D.φ₁ ≫ D.v₂₃.τ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (forget C).map (D.φ₁ ≫ D.v₂₃.τ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)<VAR>eq₁ : (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (forget C).map (D.φ₁ ≫ D.v₂₃.τ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)<VAR>eq₁ : (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (forget C).map (D.φ₁ ≫ D.v₂₃.τ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map D.δ ((forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)) = (forget C).map D.v₂₃.τ₁ ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map D.δ x₃ = (forget C).map D.v₂₃.τ₁ ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>D.δ x₃ = D.v₂₃.τ₁ x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map D.δ x₃ = (forget C).map D.v₂₃.τ₁ ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>(forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map D.δ x₃ = (forget C).map D.v₂₃.τ₁ ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>(forget C).map D.L₂.f ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)) = (forget C).map D.L₂.f x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map D.δ x₃ = (forget C).map D.v₂₃.τ₁ ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>(forget C).map D.φ₂ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (forget C).map D.L₂.f x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map D.δ x₃ = (forget C).map D.v₂₃.τ₁ ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>(forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃ ≫ D.v₁₂.τ₂) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (forget C).map D.L₂.f x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : (forget C).obj D.L₀.X₃<VAR>x₂ : (forget C).obj D.L₁.X₂<VAR>x₁ : (forget C).obj D.L₂.X₁<VAR>h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃<VAR>h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂<VAR>this✝ : PreservesFiniteLimits (forget₂ C Ab)<VAR>this : PreservesFiniteLimits (forget C)<VAR>eq : (forget C).map D.δ x₃ = (forget C).map D.v₂₃.τ₁ ((forget C).map D.φ₁ (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))<VAR>eq₁ : (forget C).map (pullback.fst D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂<VAR>eq₂ : (forget C).map (pullback.snd D.L₁.g D.v₀₁.τ₃) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃<GOAL>(forget C).map D.v₁₂.τ₂ x₂ = (forget C).map D.L₂.f x₁
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>hf : IsOpenMap ⇑f<VAR>U : Opens ↑X<VAR>S : Sieve U<VAR>hU : S ∈ (Opens.grothendieckTopology ↑X).sieves U<VAR>x : ↑X<VAR>hx : x ∈ ↑U<VAR>V : Opens ↑X<VAR>i : V ⟶ U<VAR>hV : S.arrows i<VAR>hxV : x ∈ V<GOAL>∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ f x ∈ U_1
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasStrictDerivAt log x⁻¹ x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : x < 0<GOAL>HasStrictDerivAt log x⁻¹ x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : 0 < x<GOAL>HasStrictDerivAt log x⁻¹ x
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>-[n+1].toNat = 0 ↔ -[n+1] ≤ 0
<VAR>x : ℂ<GOAL>HasStrictDerivAt cosh (sinh x) x
<VAR>x : ℂ<GOAL>HasStrictDerivAt cosh ((cexp x - cexp (-x)) * 2⁻¹) x
<VAR>x : ℂ<GOAL>(cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>inst✝ : Nontrivial n<VAR>i j : n<GOAL>adjugate 0 i j = 0 i j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>inst✝ : Nontrivial n<VAR>i j j' : n<VAR>hj' : j' ≠ j<GOAL>adjugate 0 i j = 0 i j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>inst✝ : Nontrivial n<VAR>i j j' : n<VAR>hj' : j' ≠ j<GOAL>∀ (i_1 : n), 0ᵀ.updateColumn j (Pi.single i 1) i_1 j' = 0
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>inst✝ : Nontrivial n<VAR>i j j' : n<VAR>hj' : j' ≠ j<VAR>j'' : n<GOAL>0ᵀ.updateColumn j (Pi.single i 1) j'' j' = 0
<VAR>x✝ y x : ℝ<GOAL>π / 4 ≤ arcsin x ↔ √2 / 2 ≤ x
<VAR>x✝ y x : ℝ<GOAL>π / 4 ∈ Ioc (-(π / 2)) (π / 2)
<VAR>x✝ y x : ℝ<VAR>this : 0 < π<GOAL>π / 4 ∈ Ioc (-(π / 2)) (π / 2)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>M : Λ → Stmt₁<VAR>S : Finset Λ<VAR>q₁ q₂ : Stmt₁<VAR>h₁ : q₁ ∈ stmts₁ q₂<GOAL>some q₂ ∈ stmts M S → some q₁ ∈ stmts M S
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>M : Λ → Stmt₁<VAR>S : Finset Λ<VAR>q₁ q₂ : Stmt₁<VAR>h₁ : q₁ ∈ stmts₁ q₂<GOAL>∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Set α<GOAL>IsCompact s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Set α<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set α<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hs : s ⊆ ⋃ i, U i<GOAL>∃ t, s ⊆ ⋃ i ∈ t, U i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Set α<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set α<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hs : s ⊆ ⋃ i, U i<VAR>t : Finset ι✝<VAR>ht : ↑{ carrier := ⋃ i, U i, is_open' := ⋯ } ⊆ ⋃ i ∈ t, U i<GOAL>∃ t, s ⊆ ⋃ i ∈ t, U i
<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>h : Filter γ<VAR>k : Filter δ<GOAL>map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
<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>h : Filter γ<VAR>k : Filter δ<GOAL>comap ((Prod.fst ∘ Prod.fst) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f ⊓ comap ((Prod.snd ∘ Prod.fst) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) g ⊓ (comap ((Prod.fst ∘ Prod.snd) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) h ⊓ comap ((Prod.snd ∘ Prod.snd) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) k) = comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓ (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommRing R<VAR>p q a : MvPolynomial σ R<GOAL>(-a).totalDegree = a.totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h2 : p * q ≠ 0<GOAL>p.degree ≤ (p * q).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h2 : p ≠ 0 ∧ q ≠ 0<GOAL>p.degree ≤ (p * q).degree
<VAR>k m n : ℕ+<VAR>h : m.Coprime n<GOAL>k.gcd (m * n) = k.gcd m * k.gcd n
<VAR>k m n : ℕ+<VAR>h : (↑m).Coprime ↑n<GOAL>k.gcd (m * n) = k.gcd m * k.gcd n
<VAR>k m n : ℕ+<VAR>h : (↑m).Coprime ↑n<GOAL>↑(k.gcd (m * n)) = ↑(k.gcd m * k.gcd n)
<VAR>k m n : ℕ+<VAR>h : (↑m).Coprime ↑n<GOAL>(↑k).gcd (↑m * ↑n) = (↑k).gcd ↑m * (↑k).gcd ↑n
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : eval₂ i b (X ^ n - C a) = 0<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = C (i (X ^ n - C a).leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<VAR>hs' : Multiset.card s = n<GOAL>Splits i (X ^ n - 1)
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<VAR>hs' : Multiset.card s = n<GOAL>Polynomial.map i (X ^ n - 1) = C (i (X ^ n - 1).leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.map (fun c => c / b) s)).prod
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<VAR>hs' : Multiset.card s = n<GOAL>Polynomial.map i (X ^ n - 1) = (Multiset.map ((fun a => X - C a) ∘ fun c => c / b) s).prod
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<VAR>hs' : Multiset.card s = n<VAR>C_mul_C : C (i a⁻¹) * C (i a) = 1<GOAL>Polynomial.map i (X ^ n - 1) = (Multiset.map ((fun a => X - C a) ∘ fun c => c / b) s).prod
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<VAR>hs' : Multiset.card s = n<VAR>C_mul_C : C (i a⁻¹) * C (i a) = 1<VAR>key1 : Polynomial.map i (X ^ n - 1) = C (i a⁻¹) * (Polynomial.map i (X ^ n - C a)).comp (C b * X)<GOAL>Polynomial.map i (X ^ n - 1) = (Multiset.map ((fun a => X - C a) ∘ fun c => c / b) s).prod