ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>ι : Sort u_1<VAR>S : ι → NonUnitalStarSubalgebra R A<GOAL>(⨅ i, S i).toNonUnitalSubalgebra = ⨅ i, (S i).toNonUnitalSubalgebra
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>x : A<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>⊥.toNonUnitalSubalgebra = ⊥
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>↑⊥ = {0}
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>S = ⊤ ↔ ∀ (x : A), x ∈ S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<GOAL>NonUnitalStarAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>NonUnitalStarAlgHom.range (NonUnitalStarAlgHom.id R A) = ⊤
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<GOAL>NonUnitalStarSubalgebra.map f ⊤ = NonUnitalStarAlgHom.range f
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<GOAL>NonUnitalStarSubalgebra.map f ⊥ = ⊥
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<GOAL>NonUnitalStarSubalgebra.comap f ⊤ = ⊤
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>s : Set A<GOAL>NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R s) = NonUnitalStarAlgebra.adjoin R (⇑f '' s)
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>x : A<GOAL>NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R {x}) = NonUnitalStarAlgebra.adjoin R {f x}
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype S) = S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>h : S ≤ T<GOAL>Function.Injective ⇑(NonUnitalStarSubalgebra.inclusion h)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>NonUnitalAlgHomClass.toNonUnitalAlgHom (NonUnitalStarSubalgebra.inclusion ⋯) = NonUnitalAlgHom.id R ↥S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>h : S ≤ T<VAR>x : A<VAR>hx : x ∈ S<GOAL>(NonUnitalStarSubalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>h : S ≤ T<VAR>x : ↥T<VAR>m : ↑x ∈ S<GOAL>(NonUnitalStarSubalgebra.inclusion h) ⟨↑x, m⟩ = x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T U : NonUnitalStarSubalgebra R A<VAR>hst : S ≤ T<VAR>htu : T ≤ U<VAR>x : ↥S<GOAL>(NonUnitalStarSubalgebra.inclusion htu) ((NonUnitalStarSubalgebra.inclusion hst) x) = (NonUnitalStarSubalgebra.inclusion ⋯) x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>h : S ≤ T<VAR>s : ↥S<GOAL>↑((NonUnitalStarSubalgebra.inclusion h) s) = ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>S : NonUnitalStarSubalgebra R A<VAR>S₁ : NonUnitalStarSubalgebra R B<GOAL>↑(S.prod S₁) = ↑S ×ˢ ↑S₁
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>S : NonUnitalStarSubalgebra R A<VAR>S₁ : NonUnitalStarSubalgebra R B<GOAL>(S.prod S₁).toNonUnitalSubalgebra = S.prod S₁.toNonUnitalSubalgebra
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>S : NonUnitalStarSubalgebra R A<VAR>S₁ : NonUnitalStarSubalgebra R B<VAR>x : A × B<GOAL>x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>S T : NonUnitalStarSubalgebra R A<VAR>S₁ T₁ : NonUnitalStarSubalgebra R B<GOAL>S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>S T : NonUnitalStarSubalgebra R A<VAR>S₁ T₁ : NonUnitalStarSubalgebra R B<GOAL>S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>S : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(iSup S) = ⋃ i, ↑(S i)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)<VAR>T : NonUnitalStarSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ T<GOAL>(NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalStarSubalgebra.inclusion h) x) = (f i) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)<VAR>T : NonUnitalStarSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>h : K i ≤ T<GOAL>(NonUnitalStarSubalgebra.iSupLift K dir f hf T hT).comp (NonUnitalStarSubalgebra.inclusion h) = f i
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)<VAR>T : NonUnitalStarSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>hx : ↑x ∈ T<GOAL>(NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)<VAR>T : NonUnitalStarSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥T<VAR>hx : ↑x ∈ K i<GOAL>(NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>↑(NonUnitalStarSubalgebra.center R A) = Set.center A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>(NonUnitalStarSubalgebra.center R A).toNonUnitalSubalgebra = NonUnitalSubalgebra.center R A
<VAR>R : Type u<VAR>CommSemiring R<VAR>StarRing R<VAR>A : Type u_1<VAR>NonUnitalCommSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>NonUnitalStarSubalgebra.center R A = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>a : A<GOAL>a ∈ NonUnitalStarSubalgebra.center R A ↔ ∀ (b : A), b * a = a * b
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<GOAL>↑(NonUnitalStarSubalgebra.centralizer R s) = (s ∪ star s).centralizer
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<VAR>z : A<GOAL>z ∈ NonUnitalStarSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s t : Set A<VAR>h : s ⊆ t<GOAL>NonUnitalStarSubalgebra.centralizer R t ≤ NonUnitalStarSubalgebra.centralizer R s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>NonUnitalStarSubalgebra.centralizer R Set.univ = NonUnitalStarSubalgebra.center R A
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).re = TrivSqZeroExt.fst q.re
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imI = TrivSqZeroExt.fst q.imI
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imJ = TrivSqZeroExt.fst q.imJ
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imK = TrivSqZeroExt.fst q.imK
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).re = TrivSqZeroExt.snd q.re
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imI = TrivSqZeroExt.snd q.imI
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imJ = TrivSqZeroExt.snd q.imJ
<VAR>R : Type u_1<VAR>CommRing R<VAR>q : Quaternion (DualNumber R)<GOAL>(TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imK = TrivSqZeroExt.snd q.imK
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).re = (TrivSqZeroExt.fst d).re
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).imI = (TrivSqZeroExt.fst d).imI
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).imJ = (TrivSqZeroExt.fst d).imJ
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).imK = (TrivSqZeroExt.fst d).imK
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).re = (TrivSqZeroExt.snd d).re
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).imI = (TrivSqZeroExt.snd d).imI
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).imJ = (TrivSqZeroExt.snd d).imJ
<VAR>R : Type u_1<VAR>CommRing R<VAR>d : DualNumber (Quaternion R)<GOAL>TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).imK = (TrivSqZeroExt.snd d).imK
<VAR>R : Type u<VAR>Ring R<VAR>X Y : Type u<VAR>f : X ⟶ Y<GOAL>(ModuleCat.free R).map f = Finsupp.lmapDomain R R f
<VAR>R : Type u<VAR>Ring R<VAR>X : Type u<GOAL>(ModuleCat.free R).obj X = ModuleCat.of R (X →₀ R)
<VAR>R : Type u<VAR>CommRing R<VAR>r : R<GOAL>(ModuleCat.Free.ε R) r = Finsupp.single PUnit.unit r
<VAR>R : Type u<VAR>CommRing R<VAR>X Y X' Y' : Type u<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>CategoryTheory.MonoidalCategory.tensorHom ((ModuleCat.free R).map f) ((ModuleCat.free R).map g) ≫ (ModuleCat.Free.μ R Y Y').hom = (ModuleCat.Free.μ R X X').hom ≫ (ModuleCat.free R).map (CategoryTheory.MonoidalCategory.tensorHom f g)
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type u<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor ((ModuleCat.free R).obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom (ModuleCat.Free.ε R) (𝟙 ((ModuleCat.free R).obj X)) ≫ (ModuleCat.Free.μ R (𝟙_ (Type u)) X).hom ≫ CategoryTheory.map (ModuleCat.free R).obj (CategoryTheory.MonoidalCategory.leftUnitor X).hom
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type u<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor ((ModuleCat.free R).obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom (𝟙 ((ModuleCat.free R).obj X)) (ModuleCat.Free.ε R) ≫ (ModuleCat.Free.μ R X (𝟙_ (Type u))).hom ≫ CategoryTheory.map (ModuleCat.free R).obj (CategoryTheory.MonoidalCategory.rightUnitor X).hom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : Type u<GOAL>CategoryTheory.MonoidalCategory.tensorHom (ModuleCat.Free.μ R X Y).hom (𝟙 ((ModuleCat.free R).obj Z)) ≫ (ModuleCat.Free.μ R (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom ≫ CategoryTheory.map (ModuleCat.free R).obj (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator ((ModuleCat.free R).obj X) ((ModuleCat.free R).obj Y) ((ModuleCat.free R).obj Z)).hom ≫ CategoryTheory.MonoidalCategory.tensorHom (𝟙 ((ModuleCat.free R).obj X)) (ModuleCat.Free.μ R Y Z).hom ≫ (ModuleCat.Free.μ R X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom
<VAR>R : Type u<VAR>CommRing R<GOAL>CategoryTheory.LaxMonoidal.ε = ModuleCat.Free.ε R
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type u<GOAL>CategoryTheory.LaxMonoidal.μ X Y = (ModuleCat.Free.μ R X Y).hom
<VAR>R : Type u_1<VAR>CommRing R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>r s : R<GOAL>Finsupp.single f r ≫ Finsupp.single g s = Finsupp.single (f ≫ g) (r * s)
<VAR>R : Type u_1<VAR>CommRing R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Free.embedding R C).map f = Finsupp.single f 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.Free.embedding R C).obj X = X
<VAR>R : Type u_1<VAR>CommRing R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R D<VAR>F : C ⥤ D<VAR>X : CategoryTheory.Free R C<GOAL>(CategoryTheory.Free.lift R F).obj X = F.obj X
<VAR>R : Type u_1<VAR>CommRing R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R D<VAR>F : C ⥤ D<VAR>X Y : CategoryTheory.Free R C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Free.lift R F).map f = Finsupp.sum f fun f' r => r • F.map f'
<VAR>R : Type u_1<VAR>CommRing R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>r : R<GOAL>(CategoryTheory.Free.lift R F).map (Finsupp.single f r) = r • F.map f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Abelian C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i : ι<VAR>x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i))<VAR>j : ι<VAR>hj : c.next i = j<VAR>hx : ((CategoryTheory.forget₂ C Ab).map (K.d i j)) x = 0<GOAL>((CategoryTheory.forget₂ C Ab).map (K.iCycles i)) (K.cyclesMk x j hj hx) = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Abelian C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₃.homology i))<VAR>x₂ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₂.opcycles i))<VAR>x₁ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₁.cycles j))<VAR>h₂ : ((CategoryTheory.forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i)) x₂ = ((CategoryTheory.forget₂ C Ab).map (S.X₃.homologyι i)) x₃<VAR>h₁ : ((CategoryTheory.forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j)) x₁ = ((CategoryTheory.forget₂ C Ab).map (S.X₂.opcyclesToCycles i j)) x₂<GOAL>((CategoryTheory.forget₂ C Ab).map (hS.δ i j hij)) x₃ = ((CategoryTheory.forget₂ C Ab).map (S.X₁.homologyπ j)) x₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.HasForget₂ C Ab<VAR>CategoryTheory.Abelian C<VAR>(CategoryTheory.forget₂ C Ab).Additive<VAR>(CategoryTheory.forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₃.X i))<VAR>hx₃ : ((CategoryTheory.forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0<VAR>x₂ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₂.X i))<VAR>hx₂ : ((CategoryTheory.forget₂ C Ab).map (S.g.f i)) x₂ = x₃<VAR>x₁ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₁.X j))<VAR>hx₁ : ((CategoryTheory.forget₂ C Ab).map (S.f.f j)) x₁ = ((CategoryTheory.forget₂ C Ab).map (S.X₂.d i j)) x₂<VAR>k : ι<VAR>hk : c.next j = k<GOAL>((CategoryTheory.forget₂ C Ab).map (hS.δ i j hij)) (((CategoryTheory.forget₂ C Ab).map (S.X₃.homologyπ i)) (S.X₃.cyclesMk x₃ j ⋯ hx₃)) = ((CategoryTheory.forget₂ C Ab).map (S.X₁.homologyπ j)) (S.X₁.cyclesMk x₁ k hk ⋯)
<VAR>R : Type u<VAR>CommRing R<VAR>UnivLE.{v, w}<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{t, v, w, max (w + 1) u} (AlgebraCat R)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : V<GOAL>((HomologicalComplex.single V c j).obj A).X j = A
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : V<VAR>i : ι<VAR>hi : i ≠ j<GOAL>CategoryTheory.Limits.IsZero (((HomologicalComplex.single V c j).obj A).X i)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : V<VAR>k l : ι<GOAL>((HomologicalComplex.single V c j).obj A).d k l = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : V<VAR>f : A ⟶ B<GOAL>((HomologicalComplex.single V c j).map f).f j = (HomologicalComplex.singleObjXSelf c j A).hom ≫ f ≫ (HomologicalComplex.singleObjXSelf c j B).inv
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>X : V<GOAL>(HomologicalComplex.singleCompEvalIsoSelf V c j).inv.app X = (HomologicalComplex.singleObjXSelf c j X).inv