ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>f : (i : α) → E i<VAR>c : 𝕜<VAR>hf : Memℓp f ⊤<GOAL>Memℓp (c • f) ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<VAR>c : 𝕜<VAR>hp : 0 < p.toReal<GOAL>Memℓp (c • f) p
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>y z : ℕ<GOAL>y = y - z + z ∨ y ≤ z ∧ y - z = 0
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>y z : ℕ<VAR>yz : y ≤ z<GOAL>y = y - z + z ∨ y ≤ z ∧ y - z = 0
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>y z : ℕ<VAR>zy : z ≤ y<GOAL>y = y - z + z ∨ y ≤ z ∧ y - z = 0
<VAR>R : Type u_1<VAR>K : 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✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆<VAR>m₀ m₁ : M<VAR>hm₀ : m₀ ∈ weightSpace M 0<VAR>hm₁ : m₁ ∈ posFittingComp R L M<GOAL>(B m₀) m₁ = 0
<VAR>R : Type u_1<VAR>K : 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✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>m₀ m₁ : M<VAR>hm₀ : m₀ ∈ weightSpace M 0<VAR>hm₁ : m₁ ∈ posFittingComp R L M<VAR>hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n<GOAL>(B m₀) m₁ = 0
<VAR>R : Type u_1<VAR>K : 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✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>m₀ m₁ : M<VAR>hm₀ : m₀ ∈ weightSpace M 0<VAR>hm₁ : m₁ ∈ posFittingComp R L M<VAR>hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n<GOAL>∀ (x : L), ∀ m ∈ posFittingCompOf R M x, (B m₀) m = 0
<VAR>R : Type u_1<VAR>K : 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✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>m₀ : M<VAR>hm₀ : m₀ ∈ weightSpace M 0<VAR>hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n<VAR>x : L<VAR>m₁ : M<VAR>hm₁ : m₁ ∈ posFittingCompOf R M x<GOAL>(B m₀) m₁ = 0
<VAR>R : Type u_1<VAR>K : 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✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>m₀ : M<VAR>hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n<VAR>x : L<VAR>m₁ : M<VAR>hm₁ : m₁ ∈ posFittingCompOf R M x<VAR>hm₀ : ∀ (x : L), ∃ k, (φ x ^ k) m₀ = 0<GOAL>(B m₀) m₁ = 0
<VAR>R : Type u_1<VAR>K : 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✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>m₀ : M<VAR>hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n<VAR>x : L<VAR>m₁ : M<VAR>hm₁ : m₁ ∈ posFittingCompOf R M x<VAR>hm₀ : ∀ (x : L), ∃ k, (φ x ^ k) m₀ = 0<VAR>k : ℕ<VAR>hk : (φ x ^ k) m₀ = 0<GOAL>(B m₀) m₁ = 0
<VAR>R : Type u_1<VAR>K : 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✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>B : LinearMap.BilinForm R M<VAR>m₀ : M<VAR>hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n<VAR>x : L<VAR>hm₀ : ∀ (x : L), ∃ k, (φ x ^ k) m₀ = 0<VAR>k : ℕ<VAR>hk : (φ x ^ k) m₀ = 0<VAR>m : M<VAR>hm₁ : (φ x ^ k) m ∈ posFittingCompOf R M x<GOAL>(B m₀) ((φ x ^ k) m) = 0
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y z : R<VAR>hxz : x ∣ z<VAR>hyz : y ∣ z<VAR>hxy : ¬gcd x y = 0<GOAL>x * y / gcd x y ∣ z
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y z : R<VAR>hxz : x ∣ z<VAR>hyz : y ∣ z<VAR>hxy : ¬gcd x y = 0<VAR>r : R<VAR>hr : x = gcd x y * r<VAR>s : R<VAR>hs : y = gcd x y * s<GOAL>x * y / gcd x y ∣ z
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y z : R<VAR>hxz : x ∣ z<VAR>hyz : y ∣ z<VAR>hxy : ¬gcd x y = 0<VAR>r : R<VAR>hr : x = gcd x y * r<VAR>s : R<VAR>hs : y = gcd x y * s<GOAL>x * y ∣ z * gcd x y
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y z : R<VAR>hxz : x ∣ z<VAR>hyz : y ∣ z<VAR>hxy : ¬gcd x y = 0<VAR>r : R<VAR>hr : x = gcd x y * r<VAR>s : R<VAR>hs : y = gcd x y * s<GOAL>x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y z : R<VAR>hxz : x ∣ z<VAR>hyz : y ∣ z<VAR>hxy : ¬gcd x y = 0<VAR>r : R<VAR>hr : x = gcd x y * r<VAR>s : R<VAR>hs : y = gcd x y * s<GOAL>x * y ∣ z * (x * gcdA x y)
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y z : R<VAR>hxz : x ∣ z<VAR>hyz : y ∣ z<VAR>hxy : ¬gcd x y = 0<VAR>r : R<VAR>hr : x = gcd x y * r<VAR>s : R<VAR>hs : y = gcd x y * s<GOAL>x * y ∣ z * (y * gcdB x y)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (c * x - d) = c⁻¹ • ∫ (x : ℝ) in c * a - d..c * b - d, f x
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n ≠ 1<VAR>n✝ : ℕ<VAR>h_card : Fintype.card n = n✝ + 1 + 1<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<GOAL>A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n ≠ 1<VAR>n✝ : ℕ<VAR>h_card : Fintype.card n = n✝ + 1 + 1<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<GOAL>A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n ≠ 1<VAR>n✝ : ℕ<VAR>h_card : Fintype.card n = n✝ + 1 + 1<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<VAR>h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1<GOAL>A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n ≠ 1<VAR>n✝ : ℕ<VAR>h_card : Fintype.card n = n✝ + 1 + 1<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<VAR>h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1<VAR>is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det<GOAL>A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n ≠ 1<VAR>n✝ : ℕ<VAR>h_card : Fintype.card n = n✝ + 1 + 1<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<VAR>h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1<VAR>is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det<GOAL>(fun x => A'.det • x) A'.adjugate.adjugate = (fun x => A'.det • x) (A'.det ^ (Fintype.card n - 2) • A')
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h : Fintype.card n ≠ 1<VAR>n✝ : ℕ<VAR>h_card : Fintype.card n = n✝ + 1 + 1<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<VAR>h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1<VAR>is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det<GOAL>A'.det • A'.adjugate.adjugate = A'.det • A'.det ^ (Fintype.card n - 2) • 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>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>P₁ P₂ : D<VAR>f : P₁ ⟶ P₂<GOAL>W (fun x => x ∈ Set.range F.obj) f ↔ (MorphismProperty.isomorphisms C).inverseImage G f
<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>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>P₁ P₂ : D<VAR>f : P₁ ⟶ P₂<GOAL>IsIso (G.map f) ↔ (MorphismProperty.isomorphisms C).inverseImage G f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hf : IsMulFreimanIso 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<GOAL>f a * f b = f c * f d ↔ a * b = c * d
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hf : IsMulFreimanIso 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<GOAL>{f a, f b}.prod = {f c, f d}.prod ↔ {a, b}.prod = {c, d}.prod
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : AddCommMonoid B<VAR>inst✝¹ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝ : AddCommMonoid M<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<GOAL>indicator s f = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : AddCommMonoid B<VAR>inst✝¹ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝ : AddCommMonoid M<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<GOAL>∑ x ∈ s.attach, single (↑x) ((indicator s f) ↑x) = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : AddCommMonoid B<VAR>inst✝¹ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝ : AddCommMonoid M<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<GOAL>∀ x ∈ s, x ∉ (indicator s f).support → single x ((indicator s f) x) = 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : IsNoetherian R M<VAR>f : End R M<VAR>μ : R<VAR>h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)) ⋯<GOAL>IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ) h)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : IsNoetherian R M<VAR>f : End R M<VAR>μ : R<VAR>h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)) ⋯<VAR>l : ℕ<VAR>hl : ⨆ k, (f.genEigenspace μ) k = (f.genEigenspace μ) l<GOAL>IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ) h)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : IsNoetherian R M<VAR>f : End R M<VAR>μ : R<VAR>h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)) ⋯<VAR>l : ℕ<VAR>hl : ⨆ k, (f.genEigenspace μ) k = (f.genEigenspace μ) l<GOAL>LinearMap.restrict (f - (algebraMap R (End R M)) μ) h ^ l = 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : IsNoetherian R M<VAR>f : End R M<VAR>μ : R<VAR>h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)) ⋯<VAR>l : ℕ<VAR>hl : ⨆ k, (f.genEigenspace μ) k = (f.genEigenspace μ) l<VAR>x : M<VAR>hx : x ∈ ⨆ k, (f.genEigenspace μ) k<GOAL>↑((LinearMap.restrict (f - (algebraMap R (End R M)) μ) h ^ l) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝² : s.HaveLebesgueDecomposition μ<VAR>inst✝¹ : t.HaveLebesgueDecomposition μ<VAR>inst✝ : (s + t).HaveLebesgueDecomposition μ<GOAL>(s + t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + t.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝² : s.HaveLebesgueDecomposition μ<VAR>inst✝¹ : t.HaveLebesgueDecomposition μ<VAR>inst✝ : (s + t).HaveLebesgueDecomposition μ<GOAL>μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A✝ A : C<VAR>i : ι<VAR>hi : i ≠ j<GOAL>IsZero (((single C c j).obj A).homology i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>rk : α → ℕ<VAR>s : Set α<VAR>f0 : ℕ → α<VAR>hf0 : IsBadSeq r s f0<VAR>fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } := fun t => Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t<VAR>h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m<GOAL>∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>rk : α → ℕ<VAR>s : Set α<VAR>f0 : ℕ → α<VAR>hf0 : IsBadSeq r s f0<VAR>fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } := fun t => Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t<VAR>h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m<VAR>m n : ℕ<VAR>mn : m < n<GOAL>¬r ((fun n => ↑(fs n) n) m) ((fun n => ↑(fs n) n) n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>rk : α → ℕ<VAR>s : Set α<VAR>f0 : ℕ → α<VAR>hf0 : IsBadSeq r s f0<VAR>fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } := fun t => Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t<VAR>h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m<VAR>n : ℕ<VAR>g : ℕ → α<VAR>hg1 : ∀ m < n, (fun n => ↑(fs n) n) m = g m<VAR>hg2 : rk (g n) < rk ((fun n => ↑(fs n) n) n)<GOAL>¬IsBadSeq r s g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>K : Type u_3<VAR>inst✝² : Add G<VAR>inst✝¹ : AddZeroClass H<VAR>a : G<VAR>b : H<VAR>inst✝ : DistribSMul K H<VAR>c : K<VAR>f : G →+c[a, b] H<VAR>x : G<GOAL>(c • ⇑f) (x + a) = (c • ⇑f) x + c • b
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : Profinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget Profinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>a z = b z
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : Profinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget Profinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>↑(a z) = ↑(b z)
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : Profinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget Profinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).1 = (↑(b z)).1
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : Profinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget Profinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).2 = (↑(b z)).2
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<GOAL>p.degree ≤ 0 ↔ p = 1
<VAR>𝕜 : Type u<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>𝔸' : Type u_3<VAR>inst✝¹ : NormedCommRing 𝔸'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>f' : ι → 𝔸'<VAR>hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x<GOAL>HasStrictDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<GOAL>∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<GOAL>(fun a => μ {a_1 | a ≤ f a_1}) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => μ {a_1 | a < f a_1}
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>t : ℝ<VAR>ht : μ {a | t ≤ f a} = μ {a | t < f a}<GOAL>μ {a | t ≤ f a} = μ {a | t < f a}
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : IsPRadical i p<VAR>inst✝ : IsPRadical f p<VAR>x : M<GOAL>∃ n y, (f.comp i) y = x ^ p ^ n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : IsPRadical i p<VAR>inst✝ : IsPRadical f p<VAR>x : M<VAR>n : ℕ<VAR>y : L<VAR>hy : f y = x ^ p ^ n<GOAL>∃ n y, (f.comp i) y = x ^ p ^ n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : IsPRadical i p<VAR>inst✝ : IsPRadical f p<VAR>x : M<VAR>n : ℕ<VAR>y : L<VAR>hy : f y = x ^ p ^ n<VAR>m : ℕ<VAR>z : K<VAR>hz : i z = y ^ p ^ m<GOAL>∃ n y, (f.comp i) y = x ^ p ^ n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : IsPRadical i p<VAR>inst✝ : IsPRadical f p<VAR>x : K<VAR>h : x ∈ RingHom.ker (f.comp i)<GOAL>x ∈ pNilradical K p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : IsPRadical i p<VAR>inst✝ : IsPRadical f p<VAR>x : K<VAR>h : i x ∈ RingHom.ker f<GOAL>x ∈ pNilradical K p
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>h : I = ∅<GOAL>M.Basis I ∅
<VAR>n : ℕ<VAR>b : Multiset ℕ<VAR>hb₁ : ∀ {i : ℕ}, i ∈ b → 0 < i<VAR>hb₂ : b.sum = n<GOAL>∃ a, ofComposition n a = { parts := b, parts_pos := hb₁, parts_sum := hb₂ }
<VAR>n : ℕ<VAR>b : List ℕ<VAR>hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i<VAR>hb₂ : sum ⟦b⟧ = n<GOAL>∃ a, ofComposition n a = { parts := ⟦b⟧, parts_pos := hb₁, parts_sum := hb₂ }