ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) s x
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ₀<VAR>v✝ : Valuation R Γ₀<VAR>J : Ideal R<VAR>v : Valuation (R ⧸ J) Γ₀<GOAL>J ≤ (comap (Ideal.Quotient.mk J) v).supp
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ₀<VAR>v✝ : Valuation R Γ₀<VAR>J : Ideal R<VAR>v : Valuation (R ⧸ J) Γ₀<GOAL>Ideal.map (Ideal.Quotient.mk J) J ≤ v.supp
<VAR>o e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>h : o.split = (e.oadd n a, m)<GOAL>a.repr + ↑m < ω ^ e.repr
<VAR>o e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>h : o.split = (e.oadd n a, m)<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.repr = (e.oadd n a).repr + ↑m<GOAL>a.repr + ↑m < ω ^ e.repr
<VAR>o e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>h : o.split = (e.oadd n a, m)<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.repr = (e.oadd n a).repr + ↑m<VAR>e0 : e.repr ≠ 0<VAR>d : ω ∣ a.repr<GOAL>a.repr + ↑m < ω ^ e.repr
<VAR>o e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>h : o.split = (e.oadd n a, m)<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.repr = (e.oadd n a).repr + ↑m<VAR>e0 : e.repr ≠ 0<VAR>d : ω ∣ a.repr<GOAL>ω ≤ ω ^ e.repr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DistribLattice α<VAR>a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α<VAR>h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c<GOAL>b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DistribLattice α<VAR>a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α<VAR>h : ∀ (x : α), x ∈ (fun b => [[b, a]]) b ↔ x ∈ (fun b => [[b, a]]) c<GOAL>b = c
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.75332<VAR>inst✝ : MulAction R X<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<VAR>r' : R<VAR>s' : ↥S<VAR>huv : ↑s' * r₁ = r' * ↑s₂<GOAL>r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : 0 ≤ f'<VAR>x : ℝ<GOAL>0 ≤ deriv f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : 0 ≤ f'<VAR>x : ℝ<GOAL>0 ≤ f' x
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² inst✝¹ : NoZeroSMulDivisors R M<VAR>h : Module.rank R M = 0<VAR>inst✝ : Nontrivial R<GOAL>⊥ = ⊤
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² inst✝¹ : NoZeroSMulDivisors R M<VAR>h : Subsingleton M<VAR>inst✝ : Nontrivial R<GOAL>⊥ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>hc : t.ncard < s.ncard<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : autoParam t.Finite _auto✝<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>hc : t.ncard < s.ncard<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : autoParam t.Finite _auto✝<VAR>h' : ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>hc : t.ncard < s.ncard<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : autoParam t.Finite _auto✝<VAR>h' : ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1 → x = x_1<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<GOAL>minpoly A 1 = X - 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>head✝ : M<VAR>tail✝ : List M<VAR>tail_ih✝ : (∀ x ∈ tail✝, 1 ≤ x) → ∀ x ∈ tail✝, x ≤ tail✝.prod<VAR>hl₁ : ∀ x ∈ head✝ :: tail✝, 1 ≤ x<GOAL>∀ x ∈ head✝ :: tail✝, x ≤ (head✝ :: tail✝).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>head✝ : M<VAR>tail✝ : List M<VAR>tail_ih✝ : (∀ x ∈ tail✝, 1 ≤ x) → ∀ x ∈ tail✝, x ≤ tail✝.prod<VAR>hl₁ : 1 ≤ head✝ ∧ ∀ x ∈ tail✝, 1 ≤ x<GOAL>head✝ ≤ head✝ * tail✝.prod ∧ ∀ x ∈ tail✝, x ≤ head✝ * tail✝.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>head✝ : M<VAR>tail✝ : List M<VAR>tail_ih✝ : (∀ x ∈ tail✝, 1 ≤ x) → ∀ x ∈ tail✝, x ≤ tail✝.prod<VAR>hl₁ : 1 ≤ head✝ ∧ ∀ x ∈ tail✝, 1 ≤ x<GOAL>head✝ ≤ head✝ * tail✝.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>head✝ : M<VAR>tail✝ : List M<VAR>tail_ih✝ : (∀ x ∈ tail✝, 1 ≤ x) → ∀ x ∈ tail✝, x ≤ tail✝.prod<VAR>hl₁ : 1 ≤ head✝ ∧ ∀ x ∈ tail✝, 1 ≤ x<GOAL>∀ x ∈ tail✝, x ≤ head✝ * tail✝.prod
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<GOAL>(f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s) ↔ f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>h : SurjOn f s t<GOAL>InvOn (invFunOn f s) f (invFunOn f s '' t) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>h : SurjOn f s t<GOAL>LeftInvOn (invFunOn f s) f (invFunOn f s '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>h : SurjOn f s t<VAR>y : β<VAR>hy : y ∈ t<GOAL>invFunOn f s (f (invFunOn f s y)) = invFunOn f s y
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>i j : ι<VAR>hjk : c.Rel j i<GOAL>inlX φ i j hjk ≫ (desc φ α hα).f j = hα.hom i j
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>j : ι<VAR>hjk : c.Rel j (c.next j)<GOAL>inlX φ (c.next j) j hjk ≫ (desc φ α hα).f j = hα.hom (c.next j) j
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>j : ι<VAR>hjk : c.Rel j (c.next j)<GOAL>(inlX φ (c.next j) j hjk ≫ if hj : c.Rel j (c.next j) then fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j else sndX φ j ≫ α.f j) = hα.hom (c.next j) j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>j : ℕ<GOAL>f j ((ComplexShape.down ℕ).prev j) ≫ Q.d ((ComplexShape.down ℕ).prev j) j = f j (j + 1) ≫ Q.d (j + 1) j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>j : ℕ<VAR>this : (ComplexShape.down ℕ).prev j = j + 1<GOAL>f j ((ComplexShape.down ℕ).prev j) ≫ Q.d ((ComplexShape.down ℕ).prev j) j = f j (j + 1) ≫ Q.d (j + 1) j
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>K₀ : PositiveCompacts G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>((haarContent K₀).measure ↑K₀)⁻¹ * (haarContent K₀).measure s = (haarContent K₀).outerMeasure s / (haarContent K₀).measure ↑K₀
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : PartialOrder R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : StarOrderedRing R<VAR>inst✝⁸ : NonUnitalRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : PartialOrder A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : StarModule R A<VAR>inst✝² : NoZeroSMulDivisors R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a b : A<VAR>c : R<VAR>hab : a < b<VAR>hc : 0 < c<GOAL>c • a < c • b
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : PartialOrder R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : StarOrderedRing R<VAR>inst✝⁸ : NonUnitalRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : PartialOrder A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : StarModule R A<VAR>inst✝² : NoZeroSMulDivisors R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a b : A<VAR>c : R<VAR>hab : 0 < b - a<VAR>hc : 0 < c<GOAL>0 < c • b - c • a
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : PartialOrder R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : StarOrderedRing R<VAR>inst✝⁸ : NonUnitalRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : PartialOrder A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : StarModule R A<VAR>inst✝² : NoZeroSMulDivisors R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a b : A<VAR>c : R<VAR>hab : 0 < b - a<VAR>hc : 0 < c<GOAL>0 < c • (b - a)
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : PartialOrder R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : StarOrderedRing R<VAR>inst✝⁸ : NonUnitalRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : PartialOrder A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : StarModule R A<VAR>inst✝² : NoZeroSMulDivisors R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a b : A<VAR>c : R<VAR>hab : 0 < b - a<VAR>hc : 0 < c<GOAL>0 ≤ c • (b - a)
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : PartialOrder R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : StarOrderedRing R<VAR>inst✝⁸ : NonUnitalRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : PartialOrder A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : StarModule R A<VAR>inst✝² : NoZeroSMulDivisors R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a b : A<VAR>c : R<VAR>hab : 0 < b - a<VAR>hc : 0 < c<GOAL>0 ≠ c • (b - a)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<VAR>r : R<GOAL>(X ^ n - C r).natDegree = n
<VAR>p q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>q r : ℚ≥0<GOAL>↑(q + r) = ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace (G i)<VAR>hVortho : OrthogonalFamily 𝕜 G V<VAR>hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure<GOAL>Function.Surjective ⇑hVortho.linearIsometry
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace (G i)<VAR>hVortho : OrthogonalFamily 𝕜 G V<VAR>hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure<GOAL>Function.Surjective ⇑hVortho.linearIsometry.toLinearMap
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>X : Type u_2<VAR>inst✝¹ : MulAction G X<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>a : X<GOAL>IsBlock G (orbit (↥N) a)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>X : Type u_2<VAR>inst✝¹ : MulAction G X<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>a : X<GOAL>∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>X : Type u_2<VAR>inst✝¹ : MulAction G X<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>a : X<VAR>g : G<GOAL>g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>X : Type u_2<VAR>inst✝¹ : MulAction G X<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>a : X<VAR>g : G<GOAL>orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) a)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>p.coeff n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>p.degree < ↑n
<VAR>r s : ℝ<GOAL>(↑r).IsSt s ↔ (↑s).IsSt r
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>x : α<GOAL>f ((ofInjective f hf).symm ⟨f x, ⋯⟩) = f (rangeSplitting f ⟨f x, ⋯⟩)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<GOAL>M.Base B ↔ M.Indep B ∧ M.closure B = M.E
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<GOAL>M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r
<VAR>l r : Type u<VAR>L : l → PGame<VAR>R : r → PGame<VAR>x✝ : (mk l r L R).Impartial<GOAL>(mk l r L R).grundyValue = mex fun i => ((mk l r L R).moveRight i).grundyValue
<VAR>l r : Type u<VAR>L : l → PGame<VAR>R : r → PGame<VAR>x✝ : (mk l r L R).Impartial<GOAL>(mex fun i => ((-mk l r L R).moveLeft i).grundyValue) = mex fun i => ((mk l r L R).moveRight i).grundyValue
<VAR>l r : Type u<VAR>L : l → PGame<VAR>R : r → PGame<VAR>x✝ : (mk l r L R).Impartial<VAR>i : (-mk l r L R).LeftMoves<VAR>this : (R i).Impartial<GOAL>((-mk l r L R).moveLeft i).grundyValue = ((mk l r L R).moveRight i).grundyValue
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁸ : FunLike F α β<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Preorder β<VAR>inst✝⁵ : Preorder γ<VAR>inst✝⁴ : Preorder δ<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : BoundedOrder γ<VAR>inst✝ : BoundedOrder δ<VAR>g : BoundedOrderHom β γ<VAR>f₁ f₂ : BoundedOrderHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.209062, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 2<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<GOAL>g.map' 0 1 ⋯ ⋯ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.209062, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 2<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<GOAL>g.map' 1 2 ⋯ ⋯ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 ⋯ ⋯
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s✝ s s' : Set V<GOAL>(G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>h₁ : IsSolvable R L'<VAR>h₂ : Surjective ⇑f<VAR>k : ℕ<VAR>hk : derivedSeries R L' k = ⊥<GOAL>IsSolvable R L
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>h₁ : IsSolvable R L'<VAR>h₂ : Surjective ⇑f<VAR>k : ℕ<VAR>hk : derivedSeries R L' k = ⊥<GOAL>derivedSeries R L k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>h₁ : IsSolvable R L'<VAR>h₂ : Surjective ⇑f<VAR>k : ℕ<VAR>hk : derivedSeries R L' k = ⊥<GOAL>LieIdeal.map f ⊥ = ⊥
<VAR>q : ℚ≥0<GOAL>↑q⁻¹ = ↑(divNat q.den q.num)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hp : p ≠ 0<VAR>hq : 0 < q.degree<VAR>hq0 : q ≠ 0<GOAL>(p / q).degree < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hp : p ≠ 0<VAR>hq : 0 < q.degree<VAR>hq0 : q ≠ 0<GOAL>(p /ₘ (q * C q.leadingCoeff⁻¹)).degree < p.degree
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>inst✝¹¹ : Category.{u_8, u_1} C₁<VAR>inst✝¹⁰ : Category.{u_9, u_2} C₂<VAR>inst✝⁹ : Category.{u_7, u_3} D<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>inst✝⁶ : Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝⁵ : F.Additive<VAR>inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>inst✝³ : DecidableEq J<VAR>inst✝² : TotalComplexShape c₁ c₂ c<VAR>inst✝¹ : K₁.HasMapBifunctor K₂ F c<VAR>inst✝ : L₁.HasMapBifunctor L₂ F c<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h ≫ (mapBifunctorMap f₁ f₂ F c).f j = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h ≫ ((K₁.mapBifunctor K₂ F c).d j (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j + hom₁ h₁ f₂ F c j (c.prev j) ≫ (L₁.mapBifunctor L₂ F c).d (c.prev j) j + (mapBifunctorMap f₁' f₂ F c).f j)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>inst✝¹¹ : Category.{u_8, u_1} C₁<VAR>inst✝¹⁰ : Category.{u_9, u_2} C₂<VAR>inst✝⁹ : Category.{u_7, u_3} D<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>inst✝⁶ : Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝⁵ : F.Additive<VAR>inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>inst✝³ : DecidableEq J<VAR>inst✝² : TotalComplexShape c₁ c₂ c<VAR>inst✝¹ : K₁.HasMapBifunctor K₂ F c<VAR>inst✝ : L₁.HasMapBifunctor L₂ F c<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>(F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫ (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h + (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫ (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₁ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j + (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j + ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h ≫ hom₁ h₁ f₂ F c j (c.prev j) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₁ c (c.prev j) j + (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h ≫ hom₁ h₁ f₂ F c j (c.prev j) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₂ c (c.prev j) j)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>nodalWeight s v i ≠ 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>∀ a ∈ s.erase i, (v i - v a)⁻¹ ≠ 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s.erase i<GOAL>(v i - v j)⁻¹ ≠ 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj✝ : j ∈ s.erase i<VAR>hij : j ≠ i<VAR>hj : j ∈ s<GOAL>(v i - v j)⁻¹ ≠ 0