ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>(LinearMap.inl R M M₂).coprod (LinearMap.inr R M M₂) = LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>g : M₂ →ₗ[R] M₃<GOAL>LinearMap.coprod 0 g = g ∘ₗ LinearMap.snd R M M₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<GOAL>f.coprod 0 = f ∘ₗ LinearMap.fst R M M₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f : M₃ →ₗ[R] M₄<VAR>g₁ : M →ₗ[R] M₃<VAR>g₂ : M₂ →ₗ[R] M₃<GOAL>f ∘ₗ g₁.coprod g₂ = (f ∘ₗ g₁).coprod (f ∘ₗ g₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.fst R M M₂ = LinearMap.id.coprod 0
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.snd R M M₂ = LinearMap.coprod 0 LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f : M₂ →ₗ[R] M₄<VAR>g : M₃ →ₗ[R] M₄<VAR>f' : M →ₗ[R] M₂<VAR>g' : M →ₗ[R] M₃<GOAL>f.coprod g ∘ₗ f'.prod g' = f ∘ₗ f' + g ∘ₗ g'
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>S : Submodule R M<VAR>S' : Submodule R M₂<GOAL>Submodule.map (f.coprod g) (S.prod S') = Submodule.map f S ⊔ Submodule.map g S'
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module S M₃<VAR>SMulCommClass R S M₃<VAR>f : M × M₂ →ₗ[R] M₃<GOAL>(LinearMap.coprodEquiv S).symm f = (f ∘ₗ LinearMap.inl R M M₂, f ∘ₗ LinearMap.inr R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module S M₃<VAR>SMulCommClass R S M₃<VAR>f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)<GOAL>(LinearMap.coprodEquiv S) f = f.1.coprod f.2
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f g : M × M₂ →ₗ[R] M₃<GOAL>f = g ↔ f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂ ∧ f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f g : M × M₂ →ₗ[R] M₃<VAR>hl : f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂<VAR>hr : f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂<GOAL>f = g
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₄<GOAL>⇑(f.prodMap g) = Prod.map ⇑f ⇑g
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₄<VAR>x : M × M₂<GOAL>(f.prodMap g) x = (f x.1, g x.2)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f : M →ₗ[R] M₂<VAR>g : M₃ →ₗ[R] M₄<VAR>S : Submodule R M₂<VAR>S' : Submodule R M₄<GOAL>Submodule.comap (f.prodMap g) (S.prod S') = (Submodule.comap f S).prod (Submodule.comap g S')
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f : M →ₗ[R] M₂<VAR>g : M₃ →ₗ[R] M₄<GOAL>LinearMap.ker (f.prodMap g) = (LinearMap.ker f).prod (LinearMap.ker g)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.id.prodMap LinearMap.id = LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.prodMap 1 1 = 1
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>AddCommMonoid M₅<VAR>AddCommMonoid M₆<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>Module R M₅<VAR>Module R M₆<VAR>f₁₂ : M →ₗ[R] M₂<VAR>f₂₃ : M₂ →ₗ[R] M₃<VAR>g₁₂ : M₄ →ₗ[R] M₅<VAR>g₂₃ : M₅ →ₗ[R] M₆<GOAL>f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f₁₂ f₂₃ : M →ₗ[R] M<VAR>g₁₂ g₂₃ : M₂ →ₗ[R] M₂<GOAL>f₂₃.prodMap g₂₃ * f₁₂.prodMap g₁₂ = (f₂₃ * f₁₂).prodMap (g₂₃ * g₁₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f₁ f₂ : M →ₗ[R] M₃<VAR>g₁ g₂ : M₂ →ₗ[R] M₄<GOAL>(f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap g₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<GOAL>LinearMap.prodMap 0 0 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>Module S M₃<VAR>Module S M₄<VAR>SMulCommClass R S M₃<VAR>SMulCommClass R S M₄<VAR>s : S<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₄<GOAL>(s • f).prodMap (s • g) = s • f.prodMap g
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>Module S M₃<VAR>Module S M₄<VAR>SMulCommClass R S M₃<VAR>SMulCommClass R S M₄<VAR>f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄)<GOAL>(LinearMap.prodMapLinear R M M₂ M₃ M₄ S) f = f.1.prodMap f.2
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)<GOAL>(LinearMap.prodMapRingHom R M M₂) f = f.1.prodMap f.2
<VAR>R : Type u<VAR>Semiring R<VAR>A : Type u_4<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>B : Type u_5<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>a₁ a₂ : A<GOAL>(LinearMap.inl R A B) (a₁ * a₂) = (LinearMap.inl R A B) a₁ * (LinearMap.inl R A B) a₂
<VAR>R : Type u<VAR>Semiring R<VAR>A : Type u_4<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>B : Type u_5<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>b₁ b₂ : B<GOAL>(LinearMap.inr R A B) (b₁ * b₂) = (LinearMap.inr R A B) b₁ * (LinearMap.inr R A B) b₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)<VAR>i : M × M₂<GOAL>((LinearMap.prodMapAlgHom R M M₂) f) i = (f.1 i.1, f.2 i.2)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<GOAL>LinearMap.range (f.coprod g) = LinearMap.range f ⊔ LinearMap.range g
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>IsCompl (LinearMap.range (LinearMap.inl R M M₂)) (LinearMap.range (LinearMap.inr R M M₂))
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.range (LinearMap.inl R M M₂) ⊔ LinearMap.range (LinearMap.inr R M M₂) = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Disjoint (LinearMap.range (LinearMap.inl R M M₂)) (LinearMap.range (LinearMap.inr R M M₂))
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>Submodule.map (f.coprod g) (p.prod q) = Submodule.map f p ⊔ Submodule.map g q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>p : Submodule R M₂<VAR>q : Submodule R M₃<GOAL>Submodule.comap (f.prod g) (p.prod q) = Submodule.comap f p ⊓ Submodule.comap g q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>p.prod q = Submodule.comap (LinearMap.fst R M M₂) p ⊓ Submodule.comap (LinearMap.snd R M M₂) q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>p.prod q = Submodule.map (LinearMap.inl R M M₂) p ⊔ Submodule.map (LinearMap.inr R M M₂) q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>s : Set M<VAR>t : Set M₂<GOAL>Submodule.span R (⇑(LinearMap.inl R M M₂) '' s ∪ ⇑(LinearMap.inr R M M₂) '' t) = (Submodule.span R s).prod (Submodule.span R t)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>LinearMap.ker (f.prod g) = LinearMap.ker f ⊓ LinearMap.ker g
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>LinearMap.range (f.prod g) ≤ (LinearMap.range f).prod (LinearMap.range g)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M₂ : Type u_3<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>M₃ : Type u_4<VAR>AddCommGroup M₃<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<GOAL>(LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker (f.coprod g)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M₂ : Type u_3<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>M₃ : Type u_4<VAR>AddCommGroup M₃<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>hd : Disjoint (LinearMap.range f) (LinearMap.range g)<GOAL>LinearMap.ker (f.coprod g) = (LinearMap.ker f).prod (LinearMap.ker g)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>p ⊔ q = LinearMap.range (p.subtype.coprod q.subtype)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<GOAL>Submodule.map (LinearMap.inl R M M₂) p = p.prod ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>q : Submodule R M₂<GOAL>Submodule.map (LinearMap.inr R M M₂) q = ⊥.prod q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<GOAL>Submodule.comap (LinearMap.fst R M M₂) p = p.prod ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>q : Submodule R M₂<GOAL>Submodule.comap (LinearMap.snd R M M₂) q = ⊤.prod q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>Submodule.comap (LinearMap.inl R M M₂) (p.prod q) = p
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>Submodule.comap (LinearMap.inr R M M₂) (p.prod q) = q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>Submodule.map (LinearMap.fst R M M₂) (p.prod q) = p
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>Submodule.map (LinearMap.snd R M M₂) (p.prod q) = q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.ker (LinearMap.inl R M M₂) = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.ker (LinearMap.inr R M M₂) = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.range (LinearMap.fst R M M₂) = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.range (LinearMap.snd R M M₂) = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>m : M<GOAL>↑((Submodule.fstEquiv R M M₂).symm m) = (m, 0)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>x : ↥(Submodule.fst R M M₂)<GOAL>(Submodule.fstEquiv R M M₂) x = (↑x).1
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Submodule.map (LinearMap.fst R M M₂) (Submodule.fst R M M₂) = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Submodule.map (LinearMap.snd R M M₂) (Submodule.fst R M M₂) = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>n : M₂<GOAL>↑((Submodule.sndEquiv R M M₂).symm n) = (0, n)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>x : ↥(Submodule.snd R M M₂)<GOAL>(Submodule.sndEquiv R M M₂) x = (↑x).2
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Submodule.map (LinearMap.fst R M M₂) (Submodule.snd R M M₂) = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Submodule.map (LinearMap.snd R M M₂) (Submodule.snd R M M₂) = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂ = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Submodule.fst R M M₂ ⊓ Submodule.snd R M M₂ = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p₁ : Submodule R M<VAR>p₂ : Submodule R M₂<VAR>q : Submodule R (M × M₂)<GOAL>q ≤ p₁.prod p₂ ↔ Submodule.map (LinearMap.fst R M M₂) q ≤ p₁ ∧ Submodule.map (LinearMap.snd R M M₂) q ≤ p₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p₁ : Submodule R M<VAR>p₂ : Submodule R M₂<VAR>q : Submodule R (M × M₂)<GOAL>p₁.prod p₂ ≤ q ↔ Submodule.map (LinearMap.inl R M M₂) p₁ ≤ q ∧ Submodule.map (LinearMap.inr R M M₂) p₂ ≤ q
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p₁ : Submodule R M<VAR>p₂ : Submodule R M₂<GOAL>p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>p₁ : Submodule R M<VAR>p₂ : Submodule R M₂<GOAL>p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>∀ (a : M × N), (LinearEquiv.prodComm R M N) a = a.swap
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.fst R M₂ M ∘ₗ ↑(LinearEquiv.prodComm R M M₂) = LinearMap.snd R M M₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.snd R M₂ M ∘ₗ ↑(LinearEquiv.prodComm R M M₂) = LinearMap.fst R M M₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>mnmn : (M × M₂) × M₃ × M₄<GOAL>(LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<GOAL>(LinearEquiv.prodProdProdComm R M M₂ M₃ M₄).symm = LinearEquiv.prodProdProdComm R M M₃ M₂ M₄
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<GOAL>↑(LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) = AddEquiv.prodProdProdComm M M₂ M₃ M₄
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>module_M : Module R M<VAR>module_M₂ : Module R M₂<VAR>module_M₃ : Module R M₃<VAR>module_M₄ : Module R M₄<VAR>e₁ : M ≃ₗ[R] M₂<VAR>e₂ : M₃ ≃ₗ[R] M₄<GOAL>(e₁.prod e₂).symm = e₁.symm.prod e₂.symm
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>module_M : Module R M<VAR>module_M₂ : Module R M₂<VAR>module_M₃ : Module R M₃<VAR>module_M₄ : Module R M₄<VAR>e₁ : M ≃ₗ[R] M₂<VAR>e₂ : M₃ ≃ₗ[R] M₄<VAR>p : M × M₃<GOAL>(e₁.prod e₂) p = (e₁ p.1, e₂ p.2)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>module_M : Module R M<VAR>module_M₂ : Module R M₂<VAR>module_M₃ : Module R M₃<VAR>module_M₄ : Module R M₄<VAR>e₁ : M ≃ₗ[R] M₂<VAR>e₂ : M₃ ≃ₗ[R] M₄<GOAL>↑(e₁.prod e₂) = (↑e₁).prodMap ↑e₂
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommGroup M₄<VAR>module_M : Module R M<VAR>module_M₂ : Module R M₂<VAR>module_M₃ : Module R M₃<VAR>module_M₄ : Module R M₄<VAR>e₁ : M ≃ₗ[R] M₂<VAR>e₂ : M₃ ≃ₗ[R] M₄<VAR>f : M →ₗ[R] M₄<VAR>x : M × M₃<GOAL>(e₁.skewProd e₂ f) x = (e₁ x.1, e₂ x.2 + f x.1)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommGroup M₄<VAR>module_M : Module R M<VAR>module_M₂ : Module R M₂<VAR>module_M₃ : Module R M₃<VAR>module_M₄ : Module R M₄<VAR>e₁ : M ≃ₗ[R] M₂<VAR>e₂ : M₃ ≃ₗ[R] M₄<VAR>f : M →ₗ[R] M₄<VAR>x : M₂ × M₄<GOAL>(e₁.skewProd e₂ f).symm x = (e₁.symm x.1, e₂.symm (x.2 - f (e₁.symm x.1)))
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : LinearMap.ker f ⊔ LinearMap.ker g = ⊤<GOAL>LinearMap.range (f.prod g) = (LinearMap.range f).prod (LinearMap.range g)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<VAR>Kφ : (K : Submodule R M) × ↥K ≃ₗ[R] M<GOAL>Function.Injective ⇑(f.tunnelAux Kφ)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<VAR>n : ℕ<GOAL>f.tailing i n ≤ OrderDual.ofDual ((f.tunnel i) n)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<VAR>n : ℕ<GOAL>Disjoint (f.tailing i n) (OrderDual.ofDual ((f.tunnel i) (n + 1)))
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<VAR>n : ℕ<GOAL>f.tailing i n ⊔ OrderDual.ofDual ((f.tunnel i) (n + 1)) ≤ OrderDual.ofDual ((f.tunnel i) n)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<GOAL>f.tailings i 0 = f.tailing i 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<VAR>n : ℕ<GOAL>f.tailings i (n + 1) = f.tailings i n ⊔ f.tailing i (n + 1)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<VAR>n : ℕ<GOAL>Disjoint (f.tailings i n) (OrderDual.ofDual ((f.tunnel i) (n + 1)))
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<VAR>n : ℕ<GOAL>Disjoint (f.tailings i n) (f.tailing i (n + 1))
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M →ₗ[R] M₂<VAR>x : M × M₂<GOAL>x ∈ f.graph ↔ x.2 = f x.1