ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0<VAR>h2 : (aeval z) (trinomial 0 (n - 1 + 0) n ↑1 ↑(-1) ↑(-1)) = 0<GOAL>z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0<VAR>h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0<GOAL>z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0<VAR>h1 : z ^ n = z + 1<GOAL>z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h1 : z ^ n = z + 1<VAR>h2 : (1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n) * z = 0<GOAL>z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h1 : z ^ n = z + 1<VAR>h2 : 1 * z ^ 0 * z + -1 * z ^ n + -1 * z ^ n * z = 0<GOAL>z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h1 : z ^ n = z + 1<VAR>h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0<GOAL>z + 1 = z + 1 ∧ z + 1 + z ^ 2 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊓ B.orthogonal (Submodule.span K {x}) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x}) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>y : V<VAR>h : y ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})<GOAL>y ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V → K<VAR>h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})<GOAL>∑ i ∈ {x}, μ i • i ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V → K<VAR>h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})<VAR>this : B.IsOrtho x (∑ i ∈ {x}, μ i • i)<GOAL>∑ i ∈ {x}, μ i • i ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V → K<VAR>h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})<GOAL>x ∈ Submodule.span K ↑{x}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp2 : p = 2<VAR>x✝ : Irreducible ↑p<VAR>not_unit✝ : ¬IsUnit ↑p<VAR>h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp2 : p = 2<VAR>x✝ : Irreducible ↑p<VAR>not_unit✝ : ¬IsUnit ↑p<VAR>h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b<VAR>this : IsUnit { re := 1, im := 1 } ∨ IsUnit { re := 1, im := -1 }<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp2 : p = 2<VAR>x✝ : Irreducible ↑p<VAR>not_unit✝ : ¬IsUnit ↑p<VAR>h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b<VAR>this : { re := 1, im := 1 }.norm.natAbs = 1 ∨ { re := 1, im := -1 }.norm.natAbs = 1<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ZMod p<VAR>hk : -1 = k * k<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<VAR>hpk : p ∣ k ^ 2 + 1<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<VAR>hpk : p ∣ k ^ 2 + 1<VAR>hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<VAR>hpk : p ∣ k ^ 2 + 1<VAR>hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }<VAR>hkltp : 1 + k * k < p * p<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<VAR>hpk : p ∣ k ^ 2 + 1<VAR>hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }<VAR>hkltp : 1 + k * k < p * p<VAR>hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<VAR>hpk : p ∣ k ^ 2 + 1<VAR>hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }<VAR>hkltp : 1 + k * k < p * p<VAR>hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }<VAR>hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<VAR>hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }<VAR>hkltp : 1 + k * k < p * p<VAR>hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }<VAR>hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }<VAR>y : ℕ<VAR>hy : k ^ 2 + 1 = p * y<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : Prime ↑p<VAR>hp1 : p % 2 = 1<VAR>hp3 : p % 4 ≠ 3<VAR>hp41 : p % 4 = 1<VAR>k : ℕ<VAR>k_lt_p : k < p<VAR>hk : -1 = ↑k * ↑k<VAR>hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }<VAR>hkltp : 1 + k * k < p * p<VAR>hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }<VAR>hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }<VAR>y : ℕ<VAR>hy : k ^ 2 + 1 = p * y<VAR>this : ↑p ∣ { re := ↑k, im := 1 } ∨ ↑p ∣ { re := ↑k, im := -1 }<GOAL>False
<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 : α<GOAL>toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>X : Cᵒᵖ<GOAL>(shiftFunctorZero Cᵒᵖ ℤ).inv.app X = ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H K : Subgroup G<VAR>hK : H ≤ K<VAR>hN : (H.subgroupOf K).Normal<VAR>a b : G<VAR>hb : b ∈ K<VAR>h : a * b ∈ H<GOAL>b * a ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H K : Subgroup G<VAR>hK : H ≤ K<VAR>hN : (H.subgroupOf K).Normal<VAR>a b : G<VAR>hb : b ∈ K<VAR>h : a * b ∈ H<VAR>this : b * (a * b) * b⁻¹ ∈ H<GOAL>b * a ∈ H
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>f : E → F<VAR>fa : AnalyticOn 𝕜 f univ<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>f : E → F<VAR>fa : AnalyticOn 𝕜 f univ<GOAL>ContinuousOn f univ
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁸ : Ring R✝<VAR>inst✝⁷ : AddCommGroup M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : NoZeroSMulDivisors R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : CharZero R<VAR>z : ℤ<VAR>x : M<VAR>h : z • x = 0<GOAL>z = 0 ∨ x = 0
<VAR>I : Type u<VAR>inst✝⁵ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : MonoidalCategory C<VAR>X₁ X₂ Y₁ Y₂ : GradedObject I C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<VAR>inst✝² : X₁.HasTensor Y₁<VAR>inst✝¹ : X₂.HasTensor Y₂<VAR>inst✝ : X₂.HasTensor Y₁<GOAL>tensorHom f g = whiskerRight f Y₁ ≫ whiskerLeft X₂ g
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>φ : MvPowerSeries σ R<VAR>s : σ<GOAL>(coeff R 0) (X s * φ) = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>α : Type u_11<GOAL>⋃ x, {x} = univ
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>r : R<GOAL>(((taylor r) f).sum fun i a => C a * (X - C r) ^ i) = f
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{max u_2 u_3}<VAR>f : (a : Ordinal.{max u_2 u_3}) → a < o → Ordinal.{max u_2 u_3}<VAR>c : Cardinal.{max u_2 u_3}<VAR>hc : c.IsRegular<VAR>hι : o.card < c<GOAL>o.card < c.ord.cof
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<GOAL>(p.append q connect).toFun (Fin.last (p.append q connect).length) = q.toFun (Fin.last q.length)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<GOAL>Fin.last (p.append q connect).length = ↑↑(Fin.natAdd p.length (Fin.last q.length)) + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<GOAL>↑(Fin.last (p.append q connect).length) = (↑(Fin.natAdd p.length (Fin.last q.length)) % ((p.append q connect).length + 1) + 1 % ((p.append q connect).length + 1)) % ((p.append q connect).length + 1)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : DivisionMonoid G<VAR>a b c d : G<VAR>h : Commute a b<VAR>n : ℕ<GOAL>(a * b) ^ ↑n = a ^ ↑n * b ^ ↑n
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : DivisionMonoid G<VAR>a b c d : G<VAR>h : Commute a b<VAR>n : ℕ<GOAL>(a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y : ℝ<VAR>hy : 0 < y<GOAL>ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>U✝ V : OpenSubgroup G<VAR>g : G<VAR>inst✝ : ContinuousMul G<VAR>U : OpenSubgroup G<GOAL>IsClosed ↑U
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>U✝ V : OpenSubgroup G<VAR>g : G<VAR>inst✝ : ContinuousMul G<VAR>U : OpenSubgroup G<GOAL>IsOpen (↑U)ᶜ
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>U✝ V : OpenSubgroup G<VAR>g : G<VAR>inst✝ : ContinuousMul G<VAR>U : OpenSubgroup G<VAR>x : G<VAR>hx : x ∈ (↑U)ᶜ<GOAL>(fun y => y * x⁻¹) ⁻¹' ↑U ⊆ (↑U)ᶜ
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>U✝ V : OpenSubgroup G<VAR>g : G<VAR>inst✝ : ContinuousMul G<VAR>U : OpenSubgroup G<VAR>x : G<VAR>hx : x ∈ (↑U)ᶜ<GOAL>IsOpen ((fun y => y * x⁻¹) ⁻¹' ↑U)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>U✝ V : OpenSubgroup G<VAR>g : G<VAR>inst✝ : ContinuousMul G<VAR>U : OpenSubgroup G<VAR>x : G<VAR>hx : x ∈ (↑U)ᶜ<GOAL>x ∈ (fun y => y * x⁻¹) ⁻¹' ↑U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ᵐ (a : α) ∂μ, f a ≤ g a<GOAL>∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ᵐ (a : α) ∂μ, f a ≤ g a<VAR>t : Set α<VAR>hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t<VAR>ht : MeasurableSet t<VAR>ht0 : μ t = 0<GOAL>∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ᵐ (a : α) ∂μ, f a ≤ g a<VAR>t : Set α<VAR>hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t<VAR>ht : MeasurableSet t<VAR>ht0 : μ t = 0<VAR>this : ∀ᵐ (x : α) ∂μ, x ∉ t<GOAL>∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ᵐ (a : α) ∂μ, f a ≤ g a<VAR>t : Set α<VAR>hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t<VAR>ht : MeasurableSet t<VAR>ht0 : μ t = 0<VAR>this : ∀ᵐ (x : α) ∂μ, x ∉ t<GOAL>⨆ g, ⨆ (_ : ↑g ≤ fun a => f a), g.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => g a), g_1.lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ᵐ (a : α) ∂μ, f a ≤ g a<VAR>t : Set α<VAR>hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t<VAR>ht : MeasurableSet t<VAR>ht0 : μ t = 0<VAR>this : ∀ᵐ (x : α) ∂μ, x ∉ t<VAR>s : α →ₛ ℝ≥0∞<VAR>hfs : ↑s ≤ fun a => f a<GOAL>↑(s.restrict tᶜ) ≤ fun a => g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ᵐ (a : α) ∂μ, f a ≤ g a<VAR>t : Set α<VAR>hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t<VAR>ht : MeasurableSet t<VAR>ht0 : μ t = 0<VAR>this : ∀ᵐ (x : α) ∂μ, x ∉ t<VAR>s : α →ₛ ℝ≥0∞<VAR>hfs : ↑s ≤ fun a => f a<GOAL>s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>M : n × n → S<VAR>i : ℕ<GOAL>(MvPolynomial.eval₂Hom f M) ((univ R n).coeff i) = (of (Function.curry M)).charpoly.coeff i
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>a b : α<VAR>s : Set α<VAR>f g : ι → α<GOAL>(⨆ i, f i) ∆ ⨆ i, g i ≤ ⨆ i, f i ∆ g i
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>a b : α<VAR>s : Set α<VAR>f g : ι → α<GOAL>⨆ i, f i ≤ ⨆ x, g x ⊔ f x ∆ g x ∧ ⨆ i, g i ≤ ⨆ x, f x ⊔ f x ∆ g x
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>K₀ : Set G<VAR>f : Compacts G → ℝ<GOAL>f ∈ haarProduct K₀ ↔ ∀ (K : Compacts G), f K ∈ Icc 0 ↑(index (↑K) K₀)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 0 = 0
<VAR>ι : Sort u_1<VAR>α : ι → Sort u_2<VAR>ne : ∀ (i : ι), Nonempty (α i)<VAR>p : ι → Prop<VAR>f : (i : Subtype p) → α i.val<VAR>this : DecidablePred p<GOAL>∃ g, (fun i => g i.val) = f
<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝³ : Group H<VAR>M : Type x<VAR>inst✝² : Monoid M<VAR>φ : G →* H<VAR>H₁ : Subgroup G<VAR>inst✝¹ : H₁.Normal<VAR>H₂ : Subgroup (G ⧸ H₁)<VAR>inst✝ : H₂.Normal<VAR>x : G<GOAL>x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔ x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
<VAR>α : Type u_1<VAR>s : Multiset ℕ<VAR>h : ∀ x ∈ s, Irreducible x<GOAL>normalizedFactors s.prod = s
<VAR>α : Type u_1<VAR>s : Multiset ℕ<VAR>h : ∀ x ∈ s, Irreducible x<GOAL>Multiset.Rel (fun x x_1 => x ~ᵤ x_1) (normalizedFactors s.prod) s
<VAR>α : Type u_1<VAR>s : Multiset ℕ<VAR>h : ∀ x ∈ s, Irreducible x<GOAL>s.prod ≠ 0
<VAR>α : Type u_1<VAR>s : Multiset ℕ<VAR>h : ∀ x ∈ s, Irreducible x<GOAL>0 ∉ s
<GOAL>closure (range fun x => x * x) = nonneg ℚ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>x ∈ closure s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>finrank K ↥↑(rootSpace H ⇑α) = 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>¬1 < finrank K ↥↑(rootSpace H ⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>F : ↥↑(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>F : ↥↑(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype<VAR>hF : LinearMap.ker F ≠ ⊥<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>F : ↥↑(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype<VAR>hF : LinearMap.ker F ≠ ⊥<VAR>y : L<VAR>hyα : y ∈ ↑(rootSpace H ⇑α)<VAR>hy : ⟨y, hyα⟩ ∈ LinearMap.ker F<VAR>hy₀ : ⟨y, hyα⟩ ≠ 0<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>F : ↥↑(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype<VAR>hF : LinearMap.ker F ≠ ⊥<VAR>y : L<VAR>hyα : y ∈ ↑(rootSpace H ⇑α)<VAR>hy₀ : ⟨y, hyα⟩ ≠ 0<VAR>hy : ⁅y, f⁆ = 0<GOAL>False