ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<GOAL>finrank K ↥V = (charpoly φ).natTrailingDegree
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<GOAL>finrank K ↥V = (charpoly φ).natTrailingDegree
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<GOAL>finrank K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<GOAL>finrank K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<GOAL>F.charpoly.natTrailingDegree = finrank K ↥V
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<GOAL>∀ (m : ↥V), ∃ n, (F ^ n) m = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<GOAL>∀ (a : M) (b : ∃ k, (φ ^ k) a = 0), ∃ n, (restrict φ hφV ^ n) ⟨a, ⋯⟩ = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<VAR>x : M<VAR>n : ℕ<VAR>hx : (φ ^ n) x = 0<GOAL>∃ n_1, (restrict φ hφV ^ n_1) ⟨x, ⋯⟩ = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<VAR>x : M<VAR>n : ℕ<VAR>hx : (φ ^ n) x = 0<GOAL>(restrict φ hφV ^ n) ⟨x, ⋯⟩ = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<VAR>x : M<VAR>n : ℕ<VAR>hx : (φ ^ n) x = 0<GOAL>↑((restrict φ hφV ^ n) ⟨x, ⋯⟩) = ↑0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<VAR>x : M<VAR>n : ℕ<VAR>hx : (φ ^ n) x = 0<GOAL>↑((restrict φ hφV ^ n) ⟨x, ⋯⟩) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<VAR>x : M<VAR>n : ℕ<VAR>hx : (φ ^ n) x = 0<GOAL>↑((restrict φ hφV ^ n) ⟨x, ⋯⟩) = (φ ^ n) x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<VAR>F : ↥V →ₗ[K] ↥V := restrict φ hφV<VAR>G : ↥W →ₗ[K] ↥W := restrict φ hφW<VAR>ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G<VAR>e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW<VAR>bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V<VAR>bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W<VAR>b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW<VAR>hψ : ψ = e.symm.conj φ<VAR>hG : G.charpoly.natTrailingDegree = 0<VAR>x : M<VAR>n : ℕ<VAR>h' : x ∈ φ.maxGenEigenspace 0<GOAL>↑((restrict φ hφV ^ n) ⟨x, h'⟩) = (φ ^ n) x
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x = y ^ z⁻¹ ↔ x ^ z = y
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : ι → Submodule R M<VAR>t : Submodule R N<GOAL>map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : ι → Submodule R M<VAR>t : Submodule R N<GOAL>map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x y : α<VAR>S U Z : Set α<VAR>h : IsGenericPoint x S<VAR>hZ : IsClosed Z<GOAL>x ∈ Z ↔ S ⊆ Z
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ a ∈ s, f a ≠ ⊤<GOAL>(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ a ∈ s, f a ≠ ⊤<GOAL>∀ x ∈ s, f x = ↑(f x).toNNReal
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ a ∈ s, f a ≠ ⊤<GOAL>∑ a ∈ s, f a ≠ ⊤
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f₁ f₂ : X' ⟶ Y'<GOAL>f₁ + f₂ = add W eX eY f₁ f₂
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : AddCommGroup V1<VAR>inst✝³ : AffineSpace V1 P1<VAR>inst✝² : AddCommGroup V2<VAR>inst✝¹ : Module k V1<VAR>inst✝ : Module k V2<VAR>c : P1<VAR>r₁ r₂ : k<GOAL>homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>v : ExteriorAlgebra R M<GOAL>(liftAlternating (ιMulti R)) v = v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>r : R<GOAL>(liftAlternating (ιMulti R)) ((algebraMap R (CliffordAlgebra 0)) r) = (algebraMap R (CliffordAlgebra 0)) r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>x y : CliffordAlgebra 0<VAR>hx : (liftAlternating (ιMulti R)) x = x<VAR>hy : (liftAlternating (ιMulti R)) y = y<GOAL>(liftAlternating (ιMulti R)) (x + y) = x + y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>x : CliffordAlgebra 0<VAR>m : M<VAR>hx : (liftAlternating (ιMulti R)) x = x<GOAL>(liftAlternating (ιMulti R)) ((CliffordAlgebra.ι 0) m * x) = (CliffordAlgebra.ι 0) m * x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝² : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : (i : ι) → MetricSpace (α i)<VAR>x : (i : ι) → α i<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(Measure.pi μ) (Metric.closedBall x r) = ∏ i : ι, (μ i) (Metric.closedBall (x i) r)
<VAR>𝕜 : Type u_1<VAR>inst✝ : NormedLinearOrderedField 𝕜<VAR>α : Type u_2<VAR>u v : α → 𝕜<VAR>l : Filter α<VAR>huv : u =O[l] v<VAR>hu : Tendsto (fun x => ‖u x‖) l atTop<GOAL>Tendsto (fun x => ‖v x‖) l atTop
<VAR>𝕜 : Type u_1<VAR>inst✝ : NormedLinearOrderedField 𝕜<VAR>α : Type u_2<VAR>u v : α → 𝕜<VAR>l : Filter α<VAR>huv : u =O[l] v<VAR>hu : Tendsto (fun x => ‖u x‖) l atTop<VAR>c : ℝ<VAR>hc : c > 0<VAR>hcuv : IsBigOWith c l u v<GOAL>Tendsto (fun x => ‖v x‖) l atTop
<VAR>𝕜 : Type u_1<VAR>inst✝ : NormedLinearOrderedField 𝕜<VAR>α : Type u_2<VAR>u v : α → 𝕜<VAR>l : Filter α<VAR>huv : u =O[l] v<VAR>hu : Tendsto (fun x => ‖u x‖) l atTop<VAR>c : ℝ<VAR>hc : c > 0<VAR>hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖<GOAL>Tendsto (fun x => ‖v x‖) l atTop
<VAR>𝕜 : Type u_1<VAR>inst✝ : NormedLinearOrderedField 𝕜<VAR>α : Type u_2<VAR>u v : α → 𝕜<VAR>l : Filter α<VAR>huv : u =O[l] v<VAR>hu : Tendsto (fun x => ‖u x‖) l atTop<VAR>c : ℝ<VAR>hc : c > 0<VAR>hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖<VAR>x✝ : α<GOAL>‖v x✝‖ = c * ‖v x✝‖ / c
<VAR>x y : ℂ<GOAL>((starRingEnd ℂ) x).cot = (starRingEnd ℂ) x.cot
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<GOAL>sSup {a | CompleteLattice.IsCompactElement a} = ⊤
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ {a | CompleteLattice.IsCompactElement a} ↔ x ∈ {c | CompleteLattice.IsCompactElement c ∧ c ≤ ⊤}
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x ⧏ y ↔ (∃ i, (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧ ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧ ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j'
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>((∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y) ↔ (∃ i, (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧ ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧ ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j'
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>v : Option ι → V<GOAL>LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ span K (range (v ∘ some))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>G : D ⥤ C<VAR>inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)<VAR>A : C<VAR>B : D<VAR>f : A ⟶ G.obj B<VAR>B' : StructuredArrow A G := StructuredArrow.mk f<GOAL>(fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f => (initial.to (StructuredArrow.mk f)).right) f) = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x✝ y✝ : α<VAR>r : ℝ≥0∞<VAR>Kf Kg : ℝ≥0<VAR>f : β → γ<VAR>g : α → β<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>x y : α<GOAL>↑Kf * (↑Kg * edist x y) = ↑(Kf * Kg) * edist x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<GOAL>x < y ↔ TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>h : TransGen (fun x x_1 => x ⋖ x_1) x y<GOAL>x < y
<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>bernoulliFourierCoeff 0 n = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s<GOAL>s ∈ maximals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s<GOAL>P s → ((∀ ⦃y : Finset α⦄, P y → s ⊆ y → s = y) ↔ ∀ x ∉ s, ¬P (insert x s))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s<VAR>x✝ : P s<VAR>h : ∀ x ∉ s, ¬P (insert x s)<VAR>t : Finset α<VAR>ht : P t<VAR>hst : s ⊆ t<VAR>x : α<VAR>hxt : x ∈ t<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<GOAL>P.toPoly.natDegree ≤ 1
<VAR>θ ψ : Angle<VAR>h : 2 • θ = 2 • ψ<GOAL>|θ.cos| = |ψ.cos|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m], M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det<GOAL>M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m], M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det<VAR>h✝ : IsEmpty m<GOAL>M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det