ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>hdvd : ∀ (i : ι), a ∣ (b'M.coord i) ⟨y, ⋯⟩<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<GOAL>∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<VAR>ϕy'_eq : ϕ ⟨y', y'M⟩ = 1<GOAL>∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<VAR>ϕy'_eq : ϕ ⟨y', y'M⟩ = 1<VAR>ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0<GOAL>∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<VAR>ϕy'_eq : ϕ ⟨y', y'M⟩ = 1<VAR>ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0<VAR>M' : Submodule R O := map M.subtype (LinearMap.ker ϕ)<VAR>N' : Submodule R O := map N.subtype (LinearMap.ker (ϕ ∘ₗ inclusion N_le_M))<GOAL>∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<VAR>ϕy'_eq : ϕ ⟨y', y'M⟩ = 1<VAR>ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0<VAR>M' : Submodule R O := map M.subtype (LinearMap.ker ϕ)<VAR>N' : Submodule R O := map N.subtype (LinearMap.ker (ϕ ∘ₗ inclusion N_le_M))<VAR>M'_le_M : M' ≤ M<GOAL>∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<VAR>ϕy'_eq : ϕ ⟨y', y'M⟩ = 1<VAR>ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0<VAR>M' : Submodule R O := map M.subtype (LinearMap.ker ϕ)<VAR>N' : Submodule R O := map N.subtype (LinearMap.ker (ϕ ∘ₗ inclusion N_le_M))<VAR>M'_le_M : M' ≤ M<VAR>N'_le_M' : N' ≤ M'<GOAL>∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<VAR>ϕy'_eq : ϕ ⟨y', y'M⟩ = 1<VAR>ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0<VAR>M' : Submodule R O := map M.subtype (LinearMap.ker ϕ)<VAR>N' : Submodule R O := map N.subtype (LinearMap.ker (ϕ ∘ₗ inclusion N_le_M))<VAR>M'_le_M : M' ≤ M<VAR>N'_le_M' : N' ≤ M'<VAR>N'_le_N : N' ≤ N<GOAL>∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<VAR>y : O<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = a<VAR>_ϕy_ne_zero : ϕ ⟨y, ⋯⟩ ≠ 0<VAR>c : ι → R<VAR>hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i<VAR>val✝ : Fintype ι<VAR>y' : O := ∑ i : ι, c i • ↑(b'M i)<VAR>y'M : y' ∈ M<VAR>mk_y' : ⟨y', y'M⟩ = ∑ i : ι, c i • b'M i<VAR>a_smul_y' : a • y' = y<VAR>ϕy'_eq : ϕ ⟨y', y'M⟩ = 1<VAR>ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0<VAR>M' : Submodule R O := map M.subtype (LinearMap.ker ϕ)<VAR>N' : Submodule R O := map N.subtype (LinearMap.ker (ϕ ∘ₗ inclusion N_le_M))<VAR>M'_le_M : M' ≤ M<VAR>N'_le_M' : N' ≤ M'<VAR>N'_le_N : N' ≤ N<VAR>y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0<GOAL>(∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))