ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>x : α<GOAL>f (x - c) = -f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddCommGroup α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<GOAL>f (c - x) = -f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<GOAL>Function.Antiperiodic f (-c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<GOAL>f (-c) = -f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Semiring α<VAR>NegZeroClass β<VAR>h : Function.Antiperiodic f c<VAR>hi : f 0 = 0<VAR>n : ℕ<GOAL>f (↑n * c) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Ring α<VAR>SubtractionMonoid β<VAR>h : Function.Antiperiodic f c<VAR>hi : f 0 = 0<VAR>n : ℤ<GOAL>f (↑n * c) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddGroup α<VAR>AddGroup β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>f (x + n • c) = ↑n.negOnePow • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddGroup α<VAR>AddGroup β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>f (x - n • c) = ↑n.negOnePow • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddCommGroup α<VAR>AddGroup β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>f (n • c - x) = ↑n.negOnePow • f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>Ring β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>f (x + ↑n * c) = ↑↑n.negOnePow * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>Ring β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>f (x - ↑n * c) = ↑↑n.negOnePow * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>Ring β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>f (↑n * c - x) = ↑↑n.negOnePow * f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddMonoid α<VAR>AddGroup β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>f (x + n • c) = (-1) ^ n • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddGroup α<VAR>AddGroup β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>f (x - n • c) = (-1) ^ n • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddCommGroup α<VAR>AddGroup β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>f (n • c - x) = (-1) ^ n • f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Semiring α<VAR>Ring β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>f (x + ↑n * c) = (-1) ^ n * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>Ring β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>f (x - ↑n * c) = (-1) ^ n * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>Ring β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>f (↑n * c - x) = (-1) ^ n * f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddSemigroup α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<GOAL>Function.Antiperiodic (fun x => f (a + x)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommSemigroup α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<GOAL>Function.Antiperiodic (fun x => f (x + a)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommGroup α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<GOAL>Function.Antiperiodic (fun x => f (a - x)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommGroup α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<GOAL>Function.Antiperiodic (fun x => f (x - a)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>Monoid γ<VAR>AddGroup β<VAR>DistribMulAction γ β<VAR>h : Function.Antiperiodic f c<VAR>a : γ<GOAL>Function.Antiperiodic (a • f) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>Neg β<VAR>Group γ<VAR>DistribMulAction γ α<VAR>h : Function.Antiperiodic f c<VAR>a : γ<GOAL>Function.Antiperiodic (fun x => f (a • x)) (a⁻¹ • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddCommMonoid α<VAR>Neg β<VAR>DivisionSemiring γ<VAR>Module γ α<VAR>h : Function.Antiperiodic f c<VAR>a : γ<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (a • x)) (a⁻¹ • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (a * x)) (a⁻¹ * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>Neg β<VAR>Group γ<VAR>DistribMulAction γ α<VAR>h : Function.Antiperiodic f c<VAR>a : γ<GOAL>Function.Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddCommMonoid α<VAR>Neg β<VAR>DivisionSemiring γ<VAR>Module γ α<VAR>h : Function.Antiperiodic f c<VAR>a : γ<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (a⁻¹ * x)) (a * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (x * a)) (c * a⁻¹)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (x * a)) (c / a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (x * a⁻¹)) (c * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Antiperiodic (fun x => f (x / a)) (c * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h1 : Function.Antiperiodic f c₁<VAR>h2 : Function.Antiperiodic f c₂<GOAL>Function.Periodic f (c₁ + c₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h1 : Function.Antiperiodic f c₁<VAR>h2 : Function.Antiperiodic f c₂<GOAL>Function.Periodic f (c₁ - c₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddGroup α<VAR>Neg β<VAR>h1 : Function.Periodic f c₁<VAR>h2 : Function.Antiperiodic f c₂<GOAL>Function.Antiperiodic f (c₁ + c₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h1 : Function.Periodic f c₁<VAR>h2 : Function.Antiperiodic f c₂<GOAL>Function.Antiperiodic f (c₁ - c₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddGroup α<VAR>Neg β<VAR>h1 : Function.Periodic f c₁<VAR>h2 : Function.Antiperiodic f c₂<GOAL>f (c₁ + c₂) = -f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h1 : Function.Periodic f c₁<VAR>h2 : Function.Antiperiodic f c₂<GOAL>f (c₁ - c₂) = -f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>c : α<VAR>Add α<VAR>Mul β<VAR>HasDistribNeg β<VAR>hf : Function.Antiperiodic f c<VAR>hg : Function.Antiperiodic g c<GOAL>Function.Periodic (f * g) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>c : α<VAR>Add α<VAR>DivisionMonoid β<VAR>HasDistribNeg β<VAR>hf : Function.Antiperiodic f c<VAR>hg : Function.Antiperiodic g c<GOAL>Function.Periodic (f / g) c
<VAR>α : Type u_4<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Function.Periodic Int.fract 1
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>V : Submodule R M<GOAL>↑(Submodule.restrictScalars S V) = ↑V
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>V : Submodule R M<GOAL>(Submodule.restrictScalars S V).toAddSubmonoid = V.toAddSubmonoid
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>V : Submodule R M<VAR>m : M<GOAL>m ∈ Submodule.restrictScalars S V ↔ m ∈ V
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>V : Submodule R M<GOAL>Submodule.restrictScalars R V = V
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<GOAL>Function.Injective (Submodule.restrictScalars S)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>V₁ V₂ : Submodule R M<GOAL>Submodule.restrictScalars S V₁ = Submodule.restrictScalars S V₂ ↔ V₁ = V₂
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>V : Submodule R M<GOAL>(Submodule.restrictScalarsEmbedding S R M) V = Submodule.restrictScalars S V
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>p : Submodule R M<GOAL>∀ (a : ↥p), (Submodule.restrictScalarsEquiv S R M p) a = a
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>p : Submodule R M<GOAL>∀ (a : ↥p), (Submodule.restrictScalarsEquiv S R M p).symm a = a
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<GOAL>Submodule.restrictScalars S ⊥ = ⊥
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>p : Submodule R M<GOAL>Submodule.restrictScalars S p = ⊥ ↔ p = ⊥
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<GOAL>Submodule.restrictScalars S ⊤ = ⊤
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Semiring S<VAR>Module S M<VAR>Module R M<VAR>SMul S R<VAR>IsScalarTower S R M<VAR>p : Submodule R M<GOAL>Submodule.restrictScalars S p = ⊤ ↔ p = ⊤
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Type u_2<VAR>AddCommMonoid P<VAR>Module R P<VAR>self : Module.Projective R P<GOAL>∃ s, Function.LeftInverse ⇑(Finsupp.total P P R id) ⇑s
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Type u_2<VAR>AddCommMonoid P<VAR>Module R P<GOAL>Module.Projective R P ↔ ∃ s, Function.LeftInverse ⇑(Finsupp.total P P R id) ⇑s
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Type u_2<VAR>AddCommMonoid P<VAR>Module R P<GOAL>Module.Projective R P ↔ ∃ s, Finsupp.total P P R id ∘ₗ s = LinearMap.id
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Type u_2<VAR>AddCommMonoid P<VAR>Module R P<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>Module R N<VAR>h : Module.Projective R P<VAR>f : M →ₗ[R] N<VAR>g : P →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<GOAL>∃ h, f ∘ₗ h = g
<VAR>R : Type u<VAR>Semiring R<VAR>P : Type v<VAR>AddCommMonoid P<VAR>Module R P<VAR>huniv : ∀ (f : (P →₀ R) →ₗ[R] P), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = LinearMap.id<GOAL>Module.Projective R P
<VAR>R : Type u<VAR>Ring R<VAR>P : Type v<VAR>AddCommGroup P<VAR>Module R P<VAR>ι : Type u_1<VAR>b : Basis ι R P<GOAL>Module.Projective R P
<VAR>R : Type u<VAR>Ring R<VAR>P : Type v<VAR>AddCommGroup P<VAR>Module R P<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Projective R M<VAR>i : P →ₗ[R] M<VAR>s : M →ₗ[R] P<VAR>H : s ∘ₗ i = LinearMap.id<GOAL>Module.Projective R P
<VAR>R : Type u<VAR>Ring R<VAR>P : Type v<VAR>AddCommGroup P<VAR>Module R P<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Projective R M<VAR>e : M ≃ₗ[R] P<GOAL>Module.Projective R P
<VAR>R : Type u<VAR>Ring R<VAR>P : Type v<VAR>AddCommGroup P<VAR>Module R P<GOAL>Module.Projective R P ↔ ∃ M x x_1, ∃ (_ : Module.Free R M), ∃ i s, s ∘ₗ i = LinearMap.id
<VAR>R : Type u<VAR>Ring R<VAR>P : Type v<VAR>AddCommGroup P<VAR>Module R P<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Projective R M<VAR>s : M →ₗ[R] P<VAR>hs : Function.Surjective ⇑s<GOAL>Module.Projective R P ↔ ∃ i, s ∘ₗ i = LinearMap.id
<VAR>R : Type u<VAR>Semiring R<VAR>P : Type (max u v)<VAR>AddCommMonoid P<VAR>Module R P<VAR>huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Module R M] [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g<GOAL>Module.Projective R P
<VAR>R : Type u<VAR>Ring R<VAR>P : Type (max u v)<VAR>AddCommGroup P<VAR>Module R P<VAR>huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g<GOAL>Module.Projective R P
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid M<VAR>Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>h : Submodule.map f K ≤ Submodule.map i K<VAR>n : ℕ<GOAL>f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid M<VAR>Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>m : ℕ<VAR>heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K<VAR>hf : Function.Surjective ⇑f<VAR>hi : Function.Injective ⇑i<VAR>n : ℕ<GOAL>f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid M<VAR>Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>m : ℕ<VAR>heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K<VAR>hf : Function.Surjective ⇑f<VAR>hi : Function.Injective ⇑i<GOAL>LinearMap.ker f ≤ K
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>f : M → N<VAR>g : N → P<VAR>Zero P<VAR>h : Function.Exact f g<VAR>x : M<GOAL>g (f x) = 0
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>f : M → N<VAR>g : N → P<VAR>Zero P<VAR>h : Function.Exact f g<GOAL>g ∘ f = 0
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>f : M → N<VAR>g : N → P<VAR>Zero P<VAR>h1 : g ∘ f = 0<VAR>h2 : ∀ (x : N), g x = 0 → x ∈ Set.range f<GOAL>Function.Exact f g
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>f : M → N<VAR>g : N → P<VAR>g' : P → P'<VAR>Zero P<VAR>Zero P'<VAR>exact : Function.Exact f g<VAR>inj : Function.Injective g'<VAR>h0 : g' 0 = 0<GOAL>Function.Exact f (g' ∘ g)
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>f : M → N<VAR>g : N → P<VAR>Zero P<VAR>hc : g ∘ f = 0<VAR>hr : ∀ (y : N), g y = 0 → y ∈ Set.range f<GOAL>Function.Exact f g
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>AddGroup M<VAR>AddGroup N<VAR>AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<GOAL>Function.Exact ⇑f ⇑g ↔ g.ker = f.range
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>AddGroup M<VAR>AddGroup N<VAR>AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>h1 : g.comp f = 0<VAR>h2 : g.ker ≤ f.range<GOAL>Function.Exact ⇑f ⇑g
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>AddGroup M<VAR>AddGroup N<VAR>AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>h1 : g.comp f = 0<VAR>h2 : ∀ (x : N), g x = 0 → x ∈ f.range<GOAL>Function.Exact ⇑f ⇑g
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>AddGroup M<VAR>AddGroup N<VAR>AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>hfg : Function.Exact ⇑f ⇑g<GOAL>g.ker = f.range
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>AddGroup M<VAR>AddGroup N<VAR>AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>h : Function.Exact ⇑f ⇑g<GOAL>g.comp f = 0
<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>AddCommMonoid X₁<VAR>AddCommMonoid X₂<VAR>AddCommMonoid X₃<VAR>AddCommMonoid Y₁<VAR>AddCommMonoid Y₂<VAR>AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Function.Exact ⇑f₁₂ ⇑f₂₃<GOAL>Function.Exact ⇑g₁₂ ⇑g₂₃
<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>AddCommMonoid X₁<VAR>AddCommMonoid X₂<VAR>AddCommMonoid X₃<VAR>AddCommMonoid Y₁<VAR>AddCommMonoid Y₂<VAR>AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Function.Exact ⇑g₁₂ ⇑g₂₃<GOAL>Function.Exact ⇑f₁₂ ⇑f₂₃
<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>AddCommMonoid X₁<VAR>AddCommMonoid X₂<VAR>AddCommMonoid X₃<VAR>AddCommMonoid Y₁<VAR>AddCommMonoid Y₂<VAR>AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<GOAL>Function.Exact ⇑g₁₂ ⇑g₂₃ ↔ Function.Exact ⇑f₁₂ ⇑f₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<GOAL>Function.Exact ⇑f ⇑g ↔ LinearMap.ker g = LinearMap.range f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h1 : g ∘ₗ f = 0<VAR>h2 : LinearMap.ker g ≤ LinearMap.range f<GOAL>Function.Exact ⇑f ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h1 : g ∘ₗ f = 0<VAR>h2 : ∀ (x : N), g x = 0 → x ∈ LinearMap.range f<GOAL>Function.Exact ⇑f ⇑g
<VAR>R : Type u_8<VAR>N : Type u_10<VAR>CommRing R<VAR>AddCommGroup N<VAR>Module R N<VAR>Q : Submodule R N<GOAL>Function.Exact ⇑Q.subtype ⇑Q.mkQ
<VAR>R : Type u_8<VAR>M : Type u_9<VAR>N : Type u_10<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>Function.Exact ⇑f ⇑(LinearMap.range f).mkQ
<VAR>R : Type u_8<VAR>N : Type u_10<VAR>P : Type u_11<VAR>CommRing R<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R N<VAR>Module R P<VAR>g : N →ₗ[R] P<GOAL>Function.Exact ⇑(LinearMap.ker g).subtype ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid N'<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R N'<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>e : N ≃ₗ[R] N'<GOAL>Function.Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Function.Exact ⇑f ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hfg : Function.Exact ⇑f ⇑g<GOAL>LinearMap.ker g = LinearMap.range f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<GOAL>g ∘ₗ f = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R M'<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>p : M' →ₗ[R] M<VAR>h : Function.Surjective ⇑p<GOAL>Function.Exact ⇑(f ∘ₗ p) ⇑g ↔ Function.Exact ⇑f ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid P'<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R P'<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>i : P →ₗ[R] P'<VAR>h : Function.Injective ⇑i<GOAL>Function.Exact ⇑f ⇑(i ∘ₗ g) ↔ Function.Exact ⇑f ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>AddCommMonoid N<VAR>AddCommMonoid N'<VAR>AddCommMonoid P<VAR>AddCommMonoid P'<VAR>Module R M<VAR>Module R M'<VAR>Module R N<VAR>Module R N'<VAR>Module R P<VAR>Module R P'<VAR>f₁₂ : M →ₗ[R] N<VAR>f₂₃ : N →ₗ[R] P<VAR>g₁₂ : M' →ₗ[R] N'<VAR>g₂₃ : N' →ₗ[R] P'<VAR>e₁ : M ≃ₗ[R] M'<VAR>e₂ : N ≃ₗ[R] N'<VAR>e₃ : P ≃ₗ[R] P'<VAR>h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂<VAR>h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃<GOAL>Function.Exact ⇑g₁₂ ⇑g₂₃ ↔ Function.Exact ⇑f₁₂ ⇑f₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>AddCommMonoid N<VAR>AddCommMonoid N'<VAR>AddCommMonoid P<VAR>AddCommMonoid P'<VAR>Module R M<VAR>Module R M'<VAR>Module R N<VAR>Module R N'<VAR>Module R P<VAR>Module R P'<VAR>f₁₂ : M →ₗ[R] N<VAR>f₂₃ : N →ₗ[R] P<VAR>g₁₂ : M' →ₗ[R] N'<VAR>g₂₃ : N' →ₗ[R] P'<VAR>e₁ : M ≃ₗ[R] M'<VAR>e₂ : N ≃ₗ[R] N'<VAR>e₃ : P ≃ₗ[R] P'<VAR>h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂<VAR>h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃<VAR>H : Function.Exact ⇑f₁₂ ⇑f₂₃<GOAL>Function.Exact ⇑g₁₂ ⇑g₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Semiring R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<GOAL>[Function.Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Function.Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id, ∃ e, f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE
<VAR>R : Type u_8<VAR>M : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>Semiring R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>[∃ l, g ∘ₗ l = LinearMap.id, ∃ l, l ∘ₗ f = LinearMap.id, ∃ e, f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>Function.Exact ⇑(LinearMap.inr R M N) ⇑(LinearMap.fst R M N)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>Function.Exact ⇑(LinearMap.inl R M N) ⇑(LinearMap.snd R M N)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>P : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>r : Submodule R P<VAR>hpq : p ≤ Submodule.comap f q<VAR>hqr : q ≤ Submodule.comap g r<GOAL>Function.Exact ⇑(p.mapQ q f hpq) ⇑(q.mapQ r g hqr) ↔ LinearMap.range g ⊓ r ≤ Submodule.map g q