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<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<VAR>ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • 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))
<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<VAR>ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0<VAR>n' : ℕ<VAR>bN' : Basis (Fin n') R ↥N'<VAR>m' : ℕ<VAR>hn'm' : n' ≤ m'<VAR>bM' : Basis (Fin m') R ↥M'<GOAL>∃ (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)), ↑((Basis.mkFinConsOfLE y yN bN' N'_le_N ⋯ ⋯) 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<VAR>ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0<VAR>n' : ℕ<VAR>bN' : Basis (Fin n') R ↥N'<VAR>m' : ℕ<VAR>hn'm' : n' ≤ m'<VAR>bM' : Basis (Fin m') R ↥M'<GOAL>Basis (Fin (m' + 1)) R ↥M
<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<VAR>ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0<VAR>n' : ℕ<VAR>bN' : Basis (Fin n') R ↥N'<VAR>m' : ℕ<VAR>hn'm' : n' ≤ m'<VAR>bM' : Basis (Fin m') R ↥M'<GOAL>∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑((Basis.mkFinConsOfLE y yN bN' N'_le_N ⋯ ⋯) i) = as' i • ↑(?neg.intro.intro.intro.refine_2.refine_1✝ (Fin.castLE ⋯ 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<VAR>ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0<VAR>n' : ℕ<VAR>bN' : Basis (Fin n') R ↥N'<VAR>m' : ℕ<VAR>hn'm' : n' ≤ m'<VAR>bM' : Basis (Fin m') R ↥M'<VAR>as : Fin n' → R<VAR>h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))<VAR>i : Fin (n' + 1)<GOAL>↑((Basis.mkFinConsOfLE y yN bN' N'_le_N ⋯ ⋯) i) = Fin.cons a as i • ↑((Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ⋯) (Fin.castLE ⋯ 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<VAR>ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0<VAR>n' : ℕ<VAR>bN' : Basis (Fin n') R ↥N'<VAR>m' : ℕ<VAR>hn'm' : n' ≤ m'<VAR>bM' : Basis (Fin m') R ↥M'<VAR>as : Fin n' → R<VAR>h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))<VAR>i : Fin (n' + 1)<GOAL>↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i) = Fin.cons a as i • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ i))
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>j : ι<VAR>x y : L j<GOAL>{ toFun := ⇑(of L j), map_add' := ⋯, map_smul' := ⋯ }.toFun ⁅x, y⁆ = ⁅{ toFun := ⇑(of L j), map_add' := ⋯, map_smul' := ⋯ }.toFun x, { toFun := ⇑(of L j), map_add' := ⋯, map_smul' := ⋯ }.toFun y⁆
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>j : ι<VAR>x y : L j<VAR>i : ι<GOAL>({ toFun := ⇑(of L j), map_add' := ⋯, map_smul' := ⋯ }.toFun ⁅x, y⁆) i = ⁅{ toFun := ⇑(of L j), map_add' := ⋯, map_smul' := ⋯ }.toFun x, { toFun := ⇑(of L j), map_add' := ⋯, map_smul' := ⋯ }.toFun y⁆ i
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>j : J<VAR>x : F.obj j<GOAL>(colimitEquivQuot F) (colimit.ι F j x) = Quot.mk (Quot.Rel F) ⟨j, x⟩
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>j : J<VAR>x : F.obj j<GOAL>(colimitEquivQuot F).symm ((colimitEquivQuot F) (colimit.ι F j x)) = (colimitEquivQuot F).symm (Quot.mk (Quot.Rel F) ⟨j, x⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>r : ℝ≥0<GOAL>HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
<VAR>x✝ y x : ℝ<VAR>hx : x ≤ -1<GOAL>arccos x = π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝ : IsEmpty β<GOAL>HasProd f 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y)) = (x ⊔ y \ x) ⊓ (x \ y ⊔ y)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(x ⊔ y \ x) ⊓ (x \ y ⊔ y) = x ⊔ y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<GOAL>(CoordinateRing.basis W) ⟨0, ⋯⟩ = ![1, (mk W) Y] ⟨0, ⋯⟩
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<GOAL>(CoordinateRing.basis W) ⟨1, ⋯⟩ = ![1, (mk W) Y] ⟨1, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f✝ : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((κ.map (fun x => (f x, g x)) ⋯).fst x) s = ((κ.map f hf) x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f✝ : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(κ x) ((fun x => (f x, g x)) ⁻¹' {p | p.1 ∈ s}) = (κ x) (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f✝ : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : Ω → β<VAR>g : Ω → γ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>CondIndepFun m' hm' f g μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>f✝ : B' → B<VAR>inst✝¹ : TopologicalSpace B'<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>f : B' → B<GOAL>Continuous TotalSpace.proj
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>f✝ : B' → B<VAR>inst✝¹ : TopologicalSpace B'<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>f : B' → B<GOAL>induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced TotalSpace.proj inst✝¹
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : PointsWithCircumcenterIndex n<VAR>a✝ : j ∈ univ<GOAL>pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>1 = if pointIndex i ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i) else 0
<VAR>α β : Type u<VAR>s : Set Cardinal.{u}<VAR>ι : Type u<VAR>e : ↑s ≃ ι<GOAL>BddAbove s
<VAR>α β : Type u<VAR>s : Set Cardinal.{u}<VAR>ι : Type u<VAR>e : ↑s ≃ ι<GOAL>(range fun x => ↑(e.symm x)) = s
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>x : α<GOAL>∀ᶠ (a : Set α) in v.filterAt x, MeasurableSet a
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s : (i : ι) → i ∈ S → Set α<GOAL>⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s : (i : ι) → i ∈ S → Set α<GOAL>⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s : (i : ι) → i ∈ S → Set α<VAR>this : Encodable ↑S<GOAL>⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
<VAR>B X : TopCat<VAR>π : X ⟶ B<VAR>x✝ : EffectiveEpi π<VAR>hπ : RegularEpi π<VAR>F : WalkingParallelPair ⥤ TopCat := parallelPair RegularEpi.left RegularEpi.right<VAR>i : B ≅ colimit F := RegularEpi.isColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair RegularEpi.left RegularEpi.right))<GOAL>QuotientMap ⇑π
<VAR>B X : TopCat<VAR>π : X ⟶ B<VAR>x✝ : EffectiveEpi π<VAR>hπ : RegularEpi π<VAR>F : WalkingParallelPair ⥤ TopCat := parallelPair RegularEpi.left RegularEpi.right<VAR>i : B ≅ colimit F := RegularEpi.isColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair RegularEpi.left RegularEpi.right))<GOAL>QuotientMap (⇑(homeoOfIso i) ∘ ⇑π)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>0 < ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>0 < μ (support ↑f)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>0 < μ (ball c f.rOut)
<VAR>I : MulticospanIndex (Type u)<VAR>c : Multifork I<GOAL>Nonempty (IsLimit c) ↔ Function.Bijective c.toSections
<VAR>x a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>hx : 0 < x<GOAL>0 < gammaPDFReal a r x
<VAR>x a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>hx : 0 < x<GOAL>0 < r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.base<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.base<VAR>this : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.base<VAR>this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)<VAR>this : IsIso f.c<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.base<VAR>this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)<VAR>this : IsIso f.c<GOAL>IsIso f.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.base<VAR>this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)<VAR>this : IsIso f.c<VAR>t : ↑↑X ≃ₜ ↑↑Y := (Homeomorph.ofEmbedding ⇑f.base ⋯).trans { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>IsIso f.base
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>x✝ : Invertible b<GOAL>a * b * ⅟b = a
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>R : Type w<VAR>inst✝ : CommRing R<VAR>a b : R<VAR>ha : a ∈ R⁰<VAR>x : R ⧸ Submodule.span R {a * b}<GOAL>x ∈ torsionBy R (R ⧸ Submodule.span R {a * b}) a ↔ x ∈ Submodule.span R {(mk (Submodule.span R {a * b})) b}
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>R : Type w<VAR>inst✝ : CommRing R<VAR>a b : R<VAR>ha : a ∈ R⁰<VAR>x : R ⧸ Submodule.span R {a * b}<GOAL>a • x = 0 ↔ ∃ a_1, a_1 • (mk (Submodule.span R {a * b})) b = x
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>R : Type w<VAR>inst✝ : CommRing R<VAR>a b : R<VAR>ha : a ∈ R⁰<VAR>x : R<GOAL>a • (mk (Submodule.span R {a * b})) x = 0 ↔ ∃ a_1, a_1 • (mk (Submodule.span R {a * b})) b = (mk (Submodule.span R {a * b})) x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>opcyclesMap φ = opcyclesMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ S₂.rightHomologyData
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>opcyclesMap φ = opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>r : k<VAR>φ : MvPowerSeries σ k<GOAL>(r • φ)⁻¹ = r⁻¹ • φ⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<GOAL>∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>n : ℕ<VAR>hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a<GOAL>∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>n : ℕ<VAR>hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a<GOAL>range s ⊆ ⋃ y ∈ s '' {k | k ≤ n}, {x | (x, y) ∈ a}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>n : ℕ<VAR>hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a<GOAL>∀ (y : ℕ), s y ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>n : ℕ<VAR>hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a<VAR>m : ℕ<GOAL>s m ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>n : ℕ<VAR>hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a<VAR>m : ℕ<GOAL>∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>n : ℕ<VAR>hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a<VAR>m : ℕ<VAR>hm : m ≤ n<GOAL>∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>n : ℕ<VAR>hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<VAR>H : IsSuccLimit o<GOAL>(beth o).IsStrongLimit
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>H : IsSuccLimit 0<GOAL>(beth 0).IsStrongLimit
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<VAR>H : IsSuccLimit o<VAR>h : o ≠ 0<GOAL>(beth o).IsStrongLimit