ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>val✝ : Fintype η<VAR>ι : Type<VAR>w✝ : Fintype ι<VAR>hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l<VAR>C : (ι × Shrink.{0, u_7} η → α) → κ<VAR>l : Line (Shrink.{0, u_7} η → α) ι<VAR>hl : Line.IsMono (fun x => C fun x_1 => match x_1 with | (i, e) => x i e) l<GOAL>IsMono C (l.toSubspace.reindex (equivShrink η).symm (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>val✝ : Fintype η<VAR>ι : Type<VAR>w✝ : Fintype ι<VAR>hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l<VAR>C : (ι × Shrink.{0, u_7} η → α) → κ<VAR>l : Line (Shrink.{0, u_7} η → α) ι<VAR>hl : Line.IsMono (fun x => C fun x_1 => match x_1 with | (i, e) => x i e) l<VAR>x✝ : ι × Shrink.{0, u_7} η → α<GOAL>x✝ = ⇑(Equiv.refl α).symm ∘ x✝ ∘ ⇑(Equiv.refl (ι × Shrink.{0, u_7} η))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂⁺ 𝒜 ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>(∃ s ∈ 𝒜, ∃ a ∈ t, t.erase a = s) ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = (bind₁ fun i => (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n)) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>p✝ : α → Prop<VAR>x y z : α<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>n : ℤ<GOAL>(g.extendDomain f ^ n) ↑(f x) = ↑(f y) ↔ (g ^ n) x = y
<VAR>o : Ordinal.{u_1}<VAR>l : o.IsLimit<VAR>a : Ordinal.{u_1}<GOAL>(ord ∘ aleph') o ≤ a ↔ ∀ b < o, (ord ∘ aleph') b ≤ a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<GOAL>⨅ a, ker (lapply a) ≤ ⊥
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<GOAL>∀ ⦃x : α →₀ M⦄, (∀ (i : α), x i = 0) → x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>x✝ : R<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : R<GOAL>eval x p = ∑ i ∈ range n, p.coeff i * x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>x✝ : R<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : R<GOAL>∀ (n : ℕ), 0 * x ^ n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder γ t<VAR>e : r ≃r s<VAR>f : r ≺i t<VAR>g : s ≺i t<GOAL>f.top = g.top
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder γ t<VAR>e : r ≃r s<VAR>f : r ≺i t<VAR>g : s ≺i t<GOAL>(equivLT e g).top = g.top
<VAR>α : Type u<VAR>β : Type v<VAR>f✝ f : α → β<VAR>hf : Bijective f<VAR>s : Set α<VAR>t : Set β<GOAL>s = f ⁻¹' t ↔ f '' s = t
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<GOAL>span R ↑∅ = ⊥
<VAR>β : Type u_1<VAR>o : Ordinal.{u_1}<VAR>c : Cardinal.{u_1}<VAR>ho : o.card ≤ c<VAR>hc : ℵ₀ ≤ c<VAR>A : Ordinal.{u_1} → Set β<VAR>hA : ∀ j < o, #↑(A j) ≤ c<GOAL>#↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c
<VAR>β : Type u_1<VAR>o : Ordinal.{u_1}<VAR>c : Cardinal.{u_1}<VAR>ho : o.card ≤ c<VAR>hc : ℵ₀ ≤ c<VAR>A : Ordinal.{u_1} → Set β<VAR>hA : ∀ j < o, #↑(A j) ≤ c<GOAL>#↑(sSup (range ((fun x => A ↑x) ∘ ⇑o.enumIsoOut.symm))) ≤ c
<VAR>β : Type u_1<VAR>o : Ordinal.{u_1}<VAR>c : Cardinal.{u_1}<VAR>ho : o.card ≤ c<VAR>hc : ℵ₀ ≤ c<VAR>A : Ordinal.{u_1} → Set β<VAR>hA : ∀ j < o, #↑(A j) ≤ c<GOAL>#(Quotient.out o).α * ⨆ i, #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoOut.symm) i) ≤ c * c
<VAR>β : Type u_1<VAR>o : Ordinal.{u_1}<VAR>c : Cardinal.{u_1}<VAR>ho : o.card ≤ c<VAR>hc : ℵ₀ ≤ c<VAR>A : Ordinal.{u_1} → Set β<VAR>hA : ∀ j < o, #↑(A j) ≤ c<GOAL>o.card * ⨆ i, #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoOut.symm) i) ≤ c * c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Finset S<VAR>f : S → R<GOAL>trop (s.inf f) = ∑ i ∈ s, trop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Finset S<VAR>f : S → R<GOAL>∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Finset S<VAR>f : S → R<GOAL>∑ i ∈ s, trop (f i) = (Multiset.map (fun i => trop (f i)) s.val).sum
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<GOAL>CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<GOAL>Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α) ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<GOAL>(∀ (ib : γ), p ib → ∃ ia, True ∧ ∀ x ∈ Ici ia ×ˢ Ici ia, Prod.map u u x ∈ s ib) ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>i✝ i : ℕ<VAR>f g : E → F<VAR>hf : ContDiff 𝕜 (↑i) f<VAR>hg : ContDiff 𝕜 (↑i) g<GOAL>iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>i✝ i : ℕ<VAR>f g : E → F<VAR>hf : ContDiffOn 𝕜 (↑i) f univ<VAR>hg : ContDiffOn 𝕜 (↑i) g univ<GOAL>iteratedFDerivWithin 𝕜 i (f + g) univ x = iteratedFDerivWithin 𝕜 i f univ x + iteratedFDerivWithin 𝕜 i g univ x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>inst✝ : Finite ι<VAR>F : ι → X → α<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ ∀ (i : ι), ContinuousOn (F i) S
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<GOAL>r < ↑b ^ (log b r + 1)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : r ≤ 0<GOAL>r < ↑b ^ (log b r + 1)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : 0 < r<GOAL>r < ↑b ^ (log b r + 1)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : 0 < r<VAR>hr1 : 1 ≤ r<GOAL>r < ↑b ^ (log b r + 1)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : 0 < r<VAR>hr1 : r < 1<GOAL>r < ↑b ^ (log b r + 1)
<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>p✝ m : ℕ<VAR>p : MvPolynomial σ R<GOAL>p ∈ restrictTotalDegree σ R m ↔ p.totalDegree ≤ m
<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>p✝ m : ℕ<VAR>p : MvPolynomial σ R<GOAL>p ∈ restrictTotalDegree σ R m ↔ ∀ b ∈ p.support, (b.sum fun x e => e) ≤ m
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>R' : Type v<VAR>inst✝ : CommRing R'<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>hp : IsUnit ↑p<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<GOAL>gaussSum χ ψ ^ p = χ ↑p * gaussSum χ ψ
<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>L' : Type w₁<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>x y : ⨁ (i : ι), L i<VAR>f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)<GOAL>{ toFun := ⇑(toModule R ι L' fun i => ↑(f i)), map_add' := ⋯, map_smul' := ⋯ }.toFun ⁅x, y⁆ = ⁅{ toFun := ⇑(toModule R ι L' fun i => ↑(f i)), map_add' := ⋯, map_smul' := ⋯ }.toFun x, { toFun := ⇑(toModule R ι L' fun i => ↑(f i)), 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>L' : Type w₁<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>x y : ⨁ (i : ι), L i<VAR>f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)<GOAL>∀ (i : ι) (y : L i), (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) 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>L' : Type w₁<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>x y : ⨁ (i : ι), L i<VAR>f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)<GOAL>∀ (i j : ι) (y : L i) (x : L j), (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ = ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) 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>L' : Type w₁<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>x✝ y✝ : ⨁ (i : ι), L i<VAR>f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)<VAR>i j : ι<VAR>y : L i<VAR>x : L j<GOAL>(toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ = ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) 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>L' : Type w₁<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>x✝ y✝ : ⨁ (i : ι), L i<VAR>f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)<VAR>i j : ι<VAR>y : L i<VAR>x : L j<GOAL>(toAddMonoid fun i => (↑(f i)).toAddMonoidHom) ⁅(of L j) x, (of L i) y⁆ = ⁅(↑(f j)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom 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>L' : Type w₁<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>x✝ y✝ : ⨁ (i : ι), L i<VAR>f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)<VAR>i : ι<VAR>y x : L i<GOAL>(toAddMonoid fun i => (↑(f i)).toAddMonoidHom) ⁅(of L i) x, (of L i) y⁆ = ⁅(↑(f i)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom 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>L' : Type w₁<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : (i : ι) → L i →ₗ⁅R⁆ L'<VAR>hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0<VAR>x✝ y✝ : ⨁ (i : ι), L i<VAR>f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)<VAR>i j : ι<VAR>y : L i<VAR>x : L j<VAR>hij : i ≠ j<GOAL>(toAddMonoid fun i => (↑(f i)).toAddMonoidHom) ⁅(of L j) x, (of L i) y⁆ = ⁅(↑(f j)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆
<VAR>q✝ a b c q : ℚ<VAR>hq : q.num = 0<GOAL>q = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>P : LieSubmodule R L M → Prop := fun N => IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<GOAL>IsCompl (weightSpace M 0) (posFittingComp R L M)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>P : LieSubmodule R L M → Prop := fun N => IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<GOAL>P ⊤
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>P : LieSubmodule R L M → Prop := fun N => IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<VAR>N : LieSubmodule R L M<VAR>hN : ∀ y < N, P y<GOAL>P N
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>P : LieSubmodule R L M → Prop := fun N => IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<VAR>N : LieSubmodule R L M<VAR>hN : ∀ y < N, P y<VAR>N' : LieSubmodule R L ↥↑N<VAR>hN' : N' < ⊤<GOAL>IsCompl (weightSpace (↥↑N') 0) (posFittingComp R L ↥↑N')
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>P : LieSubmodule R L M → Prop := fun N => IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<VAR>N : LieSubmodule R L M<VAR>hN : ∀ y < N, P y<VAR>N' : LieSubmodule R L ↥↑N<VAR>hN' : N' < ⊤<GOAL>IsCompl (weightSpace (↥↑(LieSubmodule.map N.incl N')) 0) (posFittingComp R L ↥↑(LieSubmodule.map N.incl N'))
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : Nat.Prime (Fintype.card α)<VAR>h2 : orderOf σ = Fintype.card α<GOAL>Fintype.card α < 2 * orderOf σ
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : Nat.Prime (Fintype.card α)<VAR>h2 : orderOf σ = Fintype.card α<GOAL>1 < 2
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M<GOAL>trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose = trace R M
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M<VAR>h : Function.Surjective ⇑↑e<GOAL>trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose = trace R M
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M<VAR>h : Function.Surjective ⇑↑e<GOAL>(trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose) ∘ₗ ↑e = trace R M ∘ₗ ↑e
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : (forget C).PreservesEpimorphisms<GOAL>MorphismProperty.surjective C = epimorphisms C
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : (forget C).PreservesEpimorphisms<GOAL>(forget C).PreservesEpimorphisms
<VAR>r p : ℝ<GOAL>r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0
<VAR>p q : ℚ≥0<VAR>n₁✝ n₂✝ d₁✝ d₂✝ d n₁ n₂ d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<GOAL>Rat.divInt ↑n₁ ↑d₁ * Rat.divInt ↑n₂ ↑d₂ = Rat.divInt (↑n₁ * ↑n₂) (↑d₁ * ↑d₂)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra K E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<VAR>x : L<GOAL>(algebraMap K L) ((norm K) x) = ∏ σ : L ≃ₐ[K] L, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra K E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<VAR>x : L<GOAL>(algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = (algebraMap L (AlgebraicClosure L)) (∏ σ : L ≃ₐ[K] L, σ x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra K E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<VAR>x : L<GOAL>(algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x_1 : L ≃ₐ[K] L, (algebraMap L (AlgebraicClosure L)) (x_1 x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra K E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<VAR>x : L<GOAL>(algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x : L →ₐ[K] AlgebraicClosure L, ?a.f✝ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra K E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<VAR>x : L<GOAL>(L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra K E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<VAR>x : L<GOAL>∀ (x_1 : L →ₐ[K] AlgebraicClosure L), ?a.f✝ x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹⁻¹ = 1 * A⁻¹⁻¹
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>1 * A⁻¹⁻¹ = A * A⁻¹ * A⁻¹⁻¹
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A * A⁻¹ * A⁻¹⁻¹ = A
<VAR>n : Type u_1<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n (ZMod p)<GOAL>(M ^ p).charpoly = M.charpoly