ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : q.degree < p.degree<GOAL>(p - q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : (-q).degree < p.degree<GOAL>(p - q).leadingCoeff = p.leadingCoeff
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>T : E →L[𝕜] E<VAR>x : E<VAR>c : 𝕜<GOAL>T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x
<VAR>a b c d m n : ℤ<VAR>this : 1 ≠ -1<GOAL>∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign
<VAR>a b c d m✝ n✝ : ℤ<VAR>this : 1 ≠ -1<VAR>m n : ℕ<GOAL>(↑m + 1 + (↑n + 1)).sign = 1
<VAR>a b c d m✝ n✝ : ℤ<VAR>this : 1 ≠ -1<VAR>m n : ℕ<GOAL>0 < ↑m + 1 + (↑n + 1)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : Preadditive C<VAR>σ τ : Type<VAR>inst✝³ : Finite τ<VAR>S : σ → C<VAR>inst✝² : HasBiproduct S<VAR>T : τ → C<VAR>inst✝¹ : HasBiproduct T<VAR>s : σ<VAR>f : ⨁ S ⟶ ⨁ T<VAR>inst✝ : IsIso f<GOAL>(∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : Preadditive C<VAR>σ τ : Type<VAR>inst✝³ : Finite τ<VAR>S : σ → C<VAR>inst✝² : HasBiproduct S<VAR>T : τ → C<VAR>inst✝¹ : HasBiproduct T<VAR>s : σ<VAR>f : ⨁ S ⟶ ⨁ T<VAR>inst✝ : IsIso f<VAR>val✝ : Fintype τ<GOAL>(∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : Preadditive C<VAR>σ τ : Type<VAR>inst✝³ : Finite τ<VAR>S : σ → C<VAR>inst✝² : HasBiproduct S<VAR>T : τ → C<VAR>inst✝¹ : HasBiproduct T<VAR>s : σ<VAR>f : ⨁ S ⟶ ⨁ T<VAR>inst✝ : IsIso f<VAR>val✝ : Fintype τ<VAR>z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0<GOAL>𝟙 (S s) = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : Preadditive C<VAR>σ τ : Type<VAR>inst✝³ : Finite τ<VAR>S : σ → C<VAR>inst✝² : HasBiproduct S<VAR>T : τ → C<VAR>inst✝¹ : HasBiproduct T<VAR>s : σ<VAR>f : ⨁ S ⟶ ⨁ T<VAR>inst✝ : IsIso f<VAR>val✝ : Fintype τ<VAR>z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0<VAR>reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h<GOAL>𝟙 (S s) = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : Preadditive C<VAR>σ τ : Type<VAR>inst✝³ : Finite τ<VAR>S : σ → C<VAR>inst✝² : HasBiproduct S<VAR>T : τ → C<VAR>inst✝¹ : HasBiproduct T<VAR>s : σ<VAR>f : ⨁ S ⟶ ⨁ T<VAR>inst✝ : IsIso f<VAR>val✝ : Fintype τ<VAR>z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0<VAR>reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h<VAR>x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s<VAR>h₁ : x = 𝟙 (S s)<GOAL>𝟙 (S s) = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : Preadditive C<VAR>σ τ : Type<VAR>inst✝³ : Finite τ<VAR>S : σ → C<VAR>inst✝² : HasBiproduct S<VAR>T : τ → C<VAR>inst✝¹ : HasBiproduct T<VAR>s : σ<VAR>f : ⨁ S ⟶ ⨁ T<VAR>inst✝ : IsIso f<VAR>val✝ : Fintype τ<VAR>z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0<VAR>reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h<VAR>x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s<VAR>h₁ : x = 𝟙 (S s)<VAR>h₀ : x = 0<GOAL>𝟙 (S s) = 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.φ 4 = C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * C W.Ψ₃ ^ 3) * C W.Ψ₃ = C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>↑((skewAdjointPart R) x) = ↑0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pm : p.natDegree ≤ m<VAR>qn : q.natDegree ≤ n<GOAL>(p * q).coeff (m + n) = p.coeff m * q.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pm : p.natDegree ≤ m<VAR>qn : q.natDegree ≤ n<GOAL>(p.toFinsupp * q.toFinsupp) (m + n) = p.toFinsupp m * q.toFinsupp n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pm : p.natDegree ≤ m<VAR>qn : q.natDegree ≤ n<GOAL>∀ (a1 a2 : ℕ), id (a1 + a2) = id a1 + id a2
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pm : p.natDegree ≤ m<VAR>qn : q.natDegree ≤ n<GOAL>AddMonoidAlgebra.supDegree id p.toFinsupp ≤ id m
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pm : p.natDegree ≤ m<VAR>qn : q.natDegree ≤ n<GOAL>AddMonoidAlgebra.supDegree id q.toFinsupp ≤ id n
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<GOAL>⨆ i, p i = span R (⋃ i, ↑(p i))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.38840, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>b : β<GOAL>noncommFoldr f (↑l) comm b = List.foldr f b l
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>b : β<GOAL>List.foldr (fun x => f ↑x) b (List.pmap Subtype.mk l ⋯) = List.foldr f b l
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>b : β<GOAL>List.foldr f b (List.map Subtype.val (List.pmap Subtype.mk l ⋯)) = List.foldr f b l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>x y : α<VAR>s t : Seq α<VAR>h : cons x s = cons y t<GOAL>x = y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>x y : α<VAR>s t : Seq α<VAR>h : cons x s = cons y t<VAR>n : ℕ<GOAL>s.get? n = t.get? n
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<GOAL>IsConnected (f ⁻¹' connectedComponent t)
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<GOAL>IsConnected (f ⁻¹' connectedComponent t)
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<GOAL>IsPreconnected (f ⁻¹' connectedComponent t)
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<GOAL>IsPreconnected (f ⁻¹' connectedComponent t)
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<GOAL>∀ (u v : Set α), IsClosed u → IsClosed v → f ⁻¹' connectedComponent t ⊆ u ∪ v → Disjoint u v → f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>huv : f ⁻¹' connectedComponent t ⊆ u ∪ v<VAR>uv_disj : Disjoint u v<VAR>T₁ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ u}<VAR>T₂ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ v}<VAR>fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v<VAR>T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u<VAR>T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v<GOAL>f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>huv : f ⁻¹' connectedComponent t ⊆ u ∪ v<VAR>uv_disj : Disjoint u v<VAR>T₁ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ u}<VAR>T₂ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ v}<VAR>fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v<VAR>T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u<VAR>T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v<VAR>hT₁ : IsClosed T₁<GOAL>f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>huv : f ⁻¹' connectedComponent t ⊆ u ∪ v<VAR>uv_disj : Disjoint u v<VAR>T₁ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ u}<VAR>T₂ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ v}<VAR>fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v<VAR>T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u<VAR>T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v<VAR>hT₁ : IsClosed T₁<VAR>hT₂ : IsClosed T₂<GOAL>f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>huv : f ⁻¹' connectedComponent t ⊆ u ∪ v<VAR>uv_disj : Disjoint u v<VAR>T₁ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ u}<VAR>T₂ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ v}<VAR>fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v<VAR>T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u<VAR>T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v<VAR>hT₁ : IsClosed T₁<VAR>hT₂ : IsClosed T₂<VAR>T_decomp : connectedComponent t ⊆ T₁ ∪ T₂<GOAL>f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>huv : f ⁻¹' connectedComponent t ⊆ u ∪ v<VAR>uv_disj : Disjoint u v<VAR>T₁ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ u}<VAR>T₂ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ v}<VAR>fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v<VAR>T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u<VAR>T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v<VAR>hT₁ : IsClosed T₁<VAR>hT₂ : IsClosed T₂<VAR>T_decomp : connectedComponent t ⊆ T₁ ∪ T₂<VAR>T_disjoint : Disjoint T₁ T₂<GOAL>f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>huv : f ⁻¹' connectedComponent t ⊆ u ∪ v<VAR>uv_disj : Disjoint u v<VAR>T₁ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ u}<VAR>T₂ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ v}<VAR>fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v<VAR>T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u<VAR>T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v<VAR>hT₁ : IsClosed T₁<VAR>hT₂ : IsClosed T₂<VAR>T_decomp : connectedComponent t ⊆ T₁ ∪ T₂<VAR>T_disjoint : Disjoint T₁ T₂<VAR>h : connectedComponent t ⊆ T₁<GOAL>f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<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>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<VAR>hf : Surjective f<VAR>hT : IsClosed (f ⁻¹' connectedComponent t)<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>huv : f ⁻¹' connectedComponent t ⊆ u ∪ v<VAR>uv_disj : Disjoint u v<VAR>T₁ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ u}<VAR>T₂ : Set β := {t' | t' ∈ connectedComponent t ∧ f ⁻¹' {t'} ⊆ v}<VAR>fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v<VAR>T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u<VAR>T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v<VAR>hT₁ : IsClosed T₁<VAR>hT₂ : IsClosed T₂<VAR>T_decomp : connectedComponent t ⊆ T₁ ∪ T₂<VAR>T_disjoint : Disjoint T₁ T₂<VAR>h : connectedComponent t ⊆ T₂<GOAL>f ⁻¹' connectedComponent t ⊆ u ∨ f ⁻¹' connectedComponent t ⊆ v
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>C a * (monomial n) b = (monomial n) (a * b)
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝² : Quiver U<VAR>inst✝¹ : Quiver V<VAR>inst✝ : Quiver W<VAR>h : HasInvolutiveReverse V<VAR>a b : V<VAR>f : a ⟶ b<VAR>g : b ⟶ a<GOAL>f = reverse g ↔ reverse f = g
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<GOAL>∀ {x y : L}, x ∈ __src✝.carrier → y ∈ __src✝.carrier → ⁅x, y⁆ ∈ __src✝.carrier
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<GOAL>∀ {x_1 y : L} (x_2 : ℕ), ((ad R L) x ^ x_2) x_1 = 0 → ∀ (x_3 : ℕ), ((ad R L) x ^ x_3) y = 0 → ∃ k, ((ad R L) x ^ k) ⁅x_1, y⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y z : L<VAR>m : ℕ<VAR>hm : ((ad R L) x ^ m) y = 0<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) z = 0<GOAL>((ad R L) x ^ (m + n)) ⁅y, z⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y z : L<VAR>m : ℕ<VAR>hm : ((ad R L) x ^ m) y = 0<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) z = 0<GOAL>∑ ij ∈ Finset.antidiagonal (m + n), (m + n).choose ij.1 • ⁅((ad R L) x ^ ij.1) y, ((ad R L) x ^ ij.2) z⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y z : L<VAR>m : ℕ<VAR>hm : ((ad R L) x ^ m) y = 0<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) z = 0<GOAL>∀ x_1 ∈ Finset.antidiagonal (m + n), (m + n).choose x_1.1 • ⁅((ad R L) x ^ x_1.1) y, ((ad R L) x ^ x_1.2) z⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y z : L<VAR>m : ℕ<VAR>hm : ((ad R L) x ^ m) y = 0<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) z = 0<VAR>ij : ℕ × ℕ<VAR>hij : ij ∈ Finset.antidiagonal (m + n)<GOAL>(m + n).choose ij.1 • ⁅((ad R L) x ^ ij.1) y, ((ad R L) x ^ ij.2) z⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y z : L<VAR>m : ℕ<VAR>hm : ((ad R L) x ^ m) y = 0<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) z = 0<VAR>ij : ℕ × ℕ<VAR>hij : ij ∈ Finset.antidiagonal (m + n)<VAR>h : m ≤ ij.1<GOAL>(m + n).choose ij.1 • ⁅((ad R L) x ^ ij.1) y, ((ad R L) x ^ ij.2) z⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y z : L<VAR>m : ℕ<VAR>hm : ((ad R L) x ^ m) y = 0<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) z = 0<VAR>ij : ℕ × ℕ<VAR>hij : ij ∈ Finset.antidiagonal (m + n)<VAR>h : n ≤ ij.2<GOAL>(m + n).choose ij.1 • ⁅((ad R L) x ^ ij.1) y, ((ad R L) x ^ ij.2) z⁆ = 0
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i✝ : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∈ s<GOAL>∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s.erase i, fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i ∂μ
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>i : ℕ<GOAL>(p.update n a).coeff i = if i = n then a else p.coeff i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>s✝ t : Set β<VAR>a✝ a : α<VAR>s : Set α<GOAL>(op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>s✝ t : Set β<VAR>a : α<VAR>s : Set α<GOAL>(op 0 • s)⁻¹ = 0⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>s✝ t : Set β<VAR>a✝ a : α<VAR>s : Set α<VAR>ha : a ≠ 0<GOAL>(op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set A<VAR>zero_mem : 0 ∈ s<VAR>sub_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a - b ∈ s<VAR>x y : A<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x + -y ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁶ : FunLike F α β<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Preorder β<VAR>inst✝² : Zero β<VAR>inst✝¹ : OrderHomClass F α β<VAR>inst✝ : ZeroHomClass F α β<VAR>f : F<VAR>a : α<VAR>ha : a ≤ 0<GOAL>f a ≤ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁶ : FunLike F α β<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Preorder β<VAR>inst✝² : Zero β<VAR>inst✝¹ : OrderHomClass F α β<VAR>inst✝ : ZeroHomClass F α β<VAR>f : F<VAR>a : α<VAR>ha : a ≤ 0<GOAL>f a ≤ f 0
<VAR>a x z✝ z : ℂ<GOAL>-(π / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<GOAL>(0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<GOAL>(0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : z.re = 0<GOAL>(0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : 0 < z.re<GOAL>(0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<GOAL>powersetCard 1 ⟦l⟧ = map singleton ⟦l⟧
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.138915 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.144366 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄ = pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.138915 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.144366 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄ = pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫ pullback.fst f₃ f₄
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.138915 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.144366 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫ pullback.fst f₃ f₄ = pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>h : a.primeFactorsList <+~ b.primeFactorsList<GOAL>a ∣ b