ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix p p 𝕜<VAR>e : p ≃ n<VAR>L₀ L₀' : List (TransvectionStruct n 𝕜)<VAR>D₀ : n → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)<GOAL>(reindex e.symm e.symm) (List.map toMatrix L₀).prod * (reindex e.symm e.symm) ((reindex e e) M) * (reindex e.symm e.symm) (List.map toMatrix L₀').prod = diagonal (D₀ ∘ ⇑e)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix p p 𝕜<VAR>e : p ≃ n<VAR>L₀ L₀' : List (TransvectionStruct n 𝕜)<VAR>D₀ : n → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)<GOAL>(reindexAlgEquiv 𝕜 𝕜 e.symm) (diagonal D₀) = diagonal (D₀ ∘ ⇑e)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝¹ : Semiring k<VAR>inst✝ : MulOneClass G<VAR>f : MonoidAlgebra k G<GOAL>f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>h : ∀ (A B : C), ∃ c x, Mono c.inl<VAR>A B : C<VAR>c' : BinaryCofan A B<VAR>hc' : IsColimit c'<VAR>c : BinaryCofan A B<VAR>hc₁ : IsColimit c<VAR>hc₂ : Mono c.inl<GOAL>Mono c'.inl
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>e : A ≅ B<GOAL>e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃
<VAR>x : ℝ<GOAL>sign ↑x = sign x
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁷ : Category.{v₁, u₁} A<VAR>inst✝⁶ : Category.{v₂, u₂} B<VAR>inst✝⁵ : HasEqualizers A<VAR>inst✝⁴ : HasImages A<VAR>inst✝³ : StrongEpiCategory B<VAR>inst✝² : HasImages B<VAR>L : A ⥤ B<VAR>inst✝¹ : {X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PreservesLimit (cospan f g) L<VAR>inst✝ : {X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → PreservesColimit (span f g) L<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>(iso L f).hom ≫ L.map (image.ι f) = image.ι (L.map f)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>hψ : ψ.Odd<GOAL>(toUnitHom ψ) (-1) = -1
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>hψ : ψ.Odd<GOAL>ψ ↑(-1) = ↑(-1)
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hca : c ∣ b<GOAL>(a + b) / c = a / c + b / c
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ α : E<VAR>q : F[X]<VAR>q_irred : Irreducible q<VAR>q_aeval : (aeval α) q = 0<VAR>hα : IsSolvableByRad F α<GOAL>IsSolvable q.Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ α : E<VAR>q : F[X]<VAR>q_irred : Irreducible q<VAR>q_aeval : (aeval α) q = 0<VAR>hα : IsSolvableByRad F α<VAR>this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal<GOAL>IsSolvable q.Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ α : E<VAR>q : F[X]<VAR>q_irred : Irreducible q<VAR>q_aeval : (aeval α) q = 0<VAR>hα : IsSolvableByRad F α<VAR>this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal<GOAL>q * C q.leadingCoeff⁻¹ ≠ 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ α : E<VAR>q : F[X]<VAR>q_irred : Irreducible q<VAR>q_aeval : (aeval α) q = 0<VAR>hα : IsSolvableByRad F α<VAR>this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal<GOAL>¬q = 0 ∧ ¬q.leadingCoeff = 0
<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✝¹² : Semiring R₂✝<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R₂✝ M₂<VAR>τ₁₂✝ : R✝ →+* R₂✝<VAR>inst✝⁷ : RingHomSurjective τ₁₂✝<VAR>F : Type u_8<VAR>inst✝⁶ : FunLike F M M₂<VAR>inst✝⁵ : SemilinearMapClass F τ₁₂✝ M M₂<VAR>R : Type u_9<VAR>R₂ : Type u_10<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring R₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R₂ M₂<VAR>ι : Type u_11<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>p : ι → Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>hf : LinearMap.range f = ⨆ i ∈ s, p i<GOAL>⨆ i ∈ s, comap f (p i) = ⊤
<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✝¹² : Semiring R₂✝<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R₂✝ M₂<VAR>τ₁₂✝ : R✝ →+* R₂✝<VAR>inst✝⁷ : RingHomSurjective τ₁₂✝<VAR>F : Type u_8<VAR>inst✝⁶ : FunLike F M M₂<VAR>inst✝⁵ : SemilinearMapClass F τ₁₂✝ M M₂<VAR>R : Type u_9<VAR>R₂ : Type u_10<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring R₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R₂ M₂<VAR>ι : Type u_11<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>p : ι → Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>hf : LinearMap.range f = ⨆ i ∈ s, p i<GOAL>⨆ i ∈ s, comap (LinearMap.range f).subtype (p i) = ⊤
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>s : σ<VAR>f : σ →₀ ℕ<GOAL>f s ≤ f.degree
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>s : σ<VAR>f : σ →₀ ℕ<GOAL>f s ≤ (weight 1) f
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>s : σ<VAR>f : σ →₀ ℕ<GOAL>1 s ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y : α<VAR>l : List α<VAR>a b : α<GOAL>(x :: y :: l ++ [a, b]).formPerm = (x :: y :: l ++ [a]).formPerm * swap a b
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>LinearIndependent ℤ (eval (π C fun x => ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(smaller C o)) => ↑p
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>LinearIndependent (ι := ↑(range (π C fun x => ord I x < o))) ℤ ((fun p => ↑p) ∘ (range_equiv_smaller C o).toFun) ↔ LinearIndependent ℤ fun (p : ↑(smaller C o)) => ↑p
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Vector α n<VAR>σ₁ : Type<VAR>β : Type u_1<VAR>σ₂ : Type<VAR>f₁ : α → σ₁ → σ₁ × β<VAR>f₂ : α → σ₂ → σ₂ × β<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>R : σ₁ → σ₂ → Prop<VAR>h₀ : R s₁ s₂<VAR>hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2<GOAL>(mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>x z : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>x z : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>x z : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>x z : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) (1 • z) = a * dist x z
<VAR>m : ℕ<GOAL>(2 * m + 1).choose (m + 1) = (2 * m + 1).choose m
<VAR>m : ℕ<GOAL>2 * m + 1 = m + 1 + m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>r : α → α → Prop<VAR>S : Set (Set α)<VAR>hd : DirectedOn (fun x x_1 => x ⊆ x_1) S<VAR>h : ∀ x ∈ S, DirectedOn r x<GOAL>DirectedOn r (⋃₀ S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>r : α → α → Prop<VAR>S : Set (Set α)<VAR>hd : DirectedOn (fun x x_1 => x ⊆ x_1) S<VAR>h : ∀ x ∈ S, DirectedOn r x<GOAL>DirectedOn r (⋃ i, ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs ys : List α<VAR>h : xs <+ ys<GOAL>xs.sym2 <+ ys.sym2
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>hM' : Module.IsTorsionBySet R M ↑⊤.annihilator<GOAL>DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>hM' : Module.IsTorsionBySet R M ↑⊤.annihilator<VAR>hI : ↑⊤.annihilator ∩ ↑(nonZeroDivisors R) ≠ ∅<GOAL>DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>hM' : Module.IsTorsionBySet R M ↑⊤.annihilator<VAR>hI : ↑⊤.annihilator ∩ ↑(nonZeroDivisors R) ≠ ∅<GOAL>⊤.annihilator ≠ ⊥
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>hM' : Module.IsTorsionBySet R M ↑⊤.annihilator<VAR>hI : (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty<GOAL>⊤.annihilator ≠ ⊥
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>hM' : Module.IsTorsionBySet R M ↑⊤.annihilator<VAR>hI : (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty<GOAL>∃ x ∈ ⊤.annihilator, x ≠ 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>hM' : Module.IsTorsionBySet R M ↑⊤.annihilator<VAR>x : R<VAR>H : x ∈ ↑⊤.annihilator<VAR>hx : x ∈ ↑(nonZeroDivisors R)<GOAL>∃ x ∈ ⊤.annihilator, x ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a b c d : G₀<VAR>h : b = 0 → a = 0<GOAL>b * (a / b) = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A C : Set E<VAR>X : Finset E<VAR>x✝ x : E<VAR>w✝ : E →L[𝕜] 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}<VAR>hx : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}<GOAL>x ∈ A
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i j : Discrete ι<VAR>h : i ≠ j<VAR>U : Opens ↑↑(F.obj i).toPresheafedSpace<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)<GOAL>x ∈ ↑((Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U))) ↔ x ∈ ↑⊥
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i j : Discrete ι<VAR>h : i ≠ j<VAR>U : Opens ↑↑(F.obj i).toPresheafedSpace<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)<GOAL>x ∉ ↑((Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i j : Discrete ι<VAR>h : i ≠ j<VAR>U : Opens ↑↑(F.obj i).toPresheafedSpace<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)<VAR>y : ↑↑(F.obj i).toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>eq : (colimit.ι F i).base y = (preservesColimitIso forgetToPresheafedSpace F).inv.base ((colimit.ι (F ⋙ forgetToPresheafedSpace) j).base x)<GOAL>False
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i j : Discrete ι<VAR>h : i ≠ j<VAR>U : Opens ↑↑(F.obj i).toPresheafedSpace<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)<VAR>y : ↑↑(F.obj i).toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>eq : (preservesColimitIso (forget C) F ≪≫ HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom ((colimit.ι F i).base y) = (preservesColimitIso (forget C) F ≪≫ HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom ((preservesColimitIso forgetToPresheafedSpace F).inv.base ((colimit.ι (F ⋙ forgetToPresheafedSpace) j).base x))<GOAL>False
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i j : Discrete ι<VAR>h : i ≠ j<VAR>U : Opens ↑↑(F.obj i).toPresheafedSpace<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)<VAR>y : ↑↑(F.obj i).toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>eq : ((preservesColimitIso (forget C) F).hom ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) ((colimit.ι F i).base y) = ((preservesColimitIso (forget C) F).hom ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) ((colimit.ι (F ⋙ forgetToPresheafedSpace) j ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base x)<GOAL>False
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i j : Discrete ι<VAR>h : i ≠ j<VAR>U : Opens ↑↑(F.obj i).toPresheafedSpace<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)<VAR>y : ↑↑(F.obj i).toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>eq : ((preservesColimitIso (forget C) F).hom ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) ((colimit.ι F i).base y) = ((preservesColimitIso (forget C) F).hom ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) ((forgetToPresheafedSpace.map (colimit.ι F j)).base x)<GOAL>False
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>as✝¹ : ι<VAR>U : Opens ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace<VAR>y : ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>as✝ : ι<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj { as := as✝ })<VAR>h : { as := as✝¹ } ≠ { as := as✝ }<VAR>eq : ((forget C).map (colimit.ι F { as := as✝¹ }) ≫ (preservesColimitIso (forget C) F).hom ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) y = ((forget C).map (colimit.ι F { as := as✝ }) ≫ (preservesColimitIso (forget C) F).hom ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) x<GOAL>False
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>as✝¹ : ι<VAR>U : Opens ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace<VAR>y : ↑↑(F.obj { as := as✝¹ }).toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>as✝ : ι<VAR>x : ↑↑((F ⋙ forgetToPresheafedSpace).obj { as := as✝ })<VAR>h : { as := as✝¹ } ≠ { as := as✝ }<VAR>eq : (Discrete.natIsoFunctor.hom.app { as := as✝¹ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝¹) y = (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝) x<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : TangentBundle I H<GOAL>↑(chartAt (ModelProd H E) p).symm = ⇑(TotalSpace.toProd H E).symm
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : TangentBundle I H<GOAL>↑(TotalSpace.toProd H E).toPartialEquiv.symm = ⇑(TotalSpace.toProd H E).symm
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>m : List I<VAR>hm : List.Chain' (fun x x_1 => x > x_1) m<VAR>h : ⟨m, hm⟩ ∈ {m | m < nil}<GOAL>⟨m, hm⟩ ∈ ∅
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<VAR>r : ℝ<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc✝ : Cospherical ps<VAR>r : ℝ<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r<VAR>c : P<VAR>hc : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<GOAL>HasStrictDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<VAR>this : HasStrictDerivAt (fun y => (c y).comp (d y)) ((((compL 𝕜 E F G) (c x)).comp (smulRight 1 d') + ((compL 𝕜 E F G).flip (d x)).comp (smulRight 1 c')) 1) x<GOAL>HasStrictDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>h : b ≤ a<GOAL>a - b = c ↔ a = c + b
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ : Weight R L M<GOAL>∃ x ∈ weightSpace M ⇑χ, x ≠ 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>x : ZMod p<GOAL>x ^ p = x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>x : ZMod p<VAR>h : x ^ Fintype.card (ZMod p) = x<GOAL>x ^ p = x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : NonUnitalNonAssocSemiring β<VAR>inst✝ : NonUnitalNonAssocSemiring γ<VAR>g✝ : β →ₙ+* γ<VAR>f : α →ₙ+* β<VAR>g : β →ₙ+* γ<VAR>f₁ f₂ : α →ₙ+* β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>x : α<GOAL>g (f₁ x) = g (f₂ x)
<VAR>z : ℂ<VAR>hz : z ≠ 0<VAR>w : ℂ<GOAL>abs (z ^ w) = abs z ^ w.re / rexp (z.arg * w.im)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<GOAL>LpAddConst 0 = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<GOAL>0 ∉ Set.Ioo 0 1