ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z v : ι → E<GOAL>(convexHull R) (Set.range v) = {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z v : ι → E<GOAL>Set.range v ⊆ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z v : ι → E<GOAL>Convex R {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z v : ι → E<GOAL>{x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x} ⊆ (convexHull R) (Set.range v)
<GOAL>↑(0 / 0) = ↑0 / ↑0
<VAR>n d : PosNum<GOAL>↑(n.div' d) = ↑(pos n) / ↑(pos d)
<VAR>n d : PosNum<GOAL>↑↑(n.div' d) = ↑(pos n) / ↑(pos d)
<VAR>n d : PosNum<GOAL>-↑(n.div' d) = ↑(pos n) / ↑(neg d)
<VAR>n d : PosNum<GOAL>-↑↑(n.div' d) = ↑(pos n) / ↑(neg d)
<VAR>n d : PosNum<GOAL>-↑(n.pred' / Num.pos d).succ' = -↑n / ↑d
<VAR>n d : PosNum<GOAL>-↑(↑n.pred' / ↑(Num.pos d) + 1) = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)
<VAR>n d : PosNum<GOAL>-[↑n.pred' / ↑d+1] = -[↑n.pred' / (↑d.pred' + 1)+1]
<VAR>n d : PosNum<GOAL>↑(n.pred' / Num.pos d).succ' = -↑n / -↑d
<VAR>n d : PosNum<GOAL>↑(↑n.pred' / ↑(Num.pos d) + 1) = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)
<VAR>n d : PosNum<GOAL>↑(↑n.pred' / ↑d).succ = ↑(↑n.pred' / (↑d.pred' + 1)).succ
<VAR>f : ℂ →ₐ[ℝ] ℂ<GOAL>f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe
<VAR>f : ℂ →ₐ[ℝ] ℂ<VAR>h : f I = I<GOAL>f I = (AlgHom.id ℝ ℂ) I
<VAR>f : ℂ →ₐ[ℝ] ℂ<VAR>h : f I = -I<GOAL>f I = ↑conjAe I
<VAR>q a✝ b✝ c✝ : ℚ<VAR>a b c : ℤ<VAR>h : ¬c = 0<GOAL>(a + b) /. c = a /. c + b /. c
<VAR>q a✝ b✝ c✝ : ℚ<VAR>a b c : ℤ<VAR>h : ¬c = 0<GOAL>(a + b) * (c * c) = (a * c + b * c) * c
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l ≤ Henstock<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>H₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>A : l.bHenstock = true<GOAL>∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : Submodule R M<VAR>t : ι → Submodule R N<GOAL>map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i)
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : Submodule R M<VAR>t : ι → Submodule R N<GOAL>map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, map₂ f (span R ↑s) (span R ↑(t i))
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<GOAL>Submodule.map (Submodule.subtype I) (LinearMap.ker I.toCotangent) = I ^ 2
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ∣ Nat.card G<GOAL>↑P ≠ ⊥
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ∣ Nat.card G<VAR>h : ↑P = ⊥<GOAL>p ∣ 1
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ∣ Nat.card G<VAR>h : ↑P = ⊥<VAR>key : p ∣ Nat.card ↥↑P<GOAL>p ∣ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : Semiring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : StarModule R A<VAR>s : NonUnitalStarSubalgebra R A<GOAL>Subalgebra.toSubmodule (adjoin R ↑s).toSubalgebra = span R {1} ⊔ s.toSubmodule
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (0 < ↑n / ↑d) = true<VAR>h₂ : decide (↑n / ↑d < 1) = true<GOAL>Real.log e ≠ 0
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (0 < ↑n / ↑d) = true<VAR>h₂ : decide (↑n / ↑d < 1) = true<GOAL>Real.log (↑n / ↑d) ≠ 0
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (0 < ↑n / ↑d) = true<VAR>h₂ : decide (↑n / ↑d < 1) = true<VAR>h₁' : 0 < ↑n / ↑d<GOAL>Real.log (↑n / ↑d) ≠ 0
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (0 < ↑n / ↑d) = true<VAR>h₂ : decide (↑n / ↑d < 1) = true<VAR>h₁' : 0 < ↑n / ↑d<VAR>h₂' : ↑n / ↑d < 1<GOAL>Real.log (↑n / ↑d) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>f : α →+* β<VAR>a b : AsBoolAlg α<GOAL>toBoolAlg (f (ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b)) = toBoolAlg (f (ofBoolAlg a)) ⊔ toBoolAlg (f (ofBoolAlg b))
<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 k : ι<VAR>hjk : c.Rel j k<GOAL>(desc φ α hα).f j = fstX φ j k hjk ≫ hα.hom k j + sndX φ j ≫ α.f 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>(desc φ α hα).f j = fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>1 < a⁻¹ ↔ a < 1
<VAR>ξ : ℝ<GOAL>{q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite ↔ Irrational ξ
<VAR>ξ : ℝ<VAR>h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite<VAR>a b : ℤ<VAR>H : ξ = ↑a / ↑b<GOAL>{q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
<VAR>ξ : ℝ<VAR>h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite<VAR>a b : ℤ<VAR>H : ξ = ↑a / ↑b<VAR>q : ℚ<GOAL>|ξ - ↑q| < 1 / ↑q.den ^ 2 ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2
<VAR>ξ : ℝ<VAR>h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite<VAR>a b : ℤ<VAR>H : ξ = ↑a / ↑b<VAR>q : ℚ<GOAL>|↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (x - y) = (equivShrink α).symm x - (equivShrink α).symm y
<VAR>α : Type u_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x - (equivShrink α).symm y)) = (equivShrink α).symm x - (equivShrink α).symm y
<VAR>num : Int<VAR>den : Nat<VAR>nz : den ≠ 0<VAR>c : num.natAbs.Coprime den<GOAL>{ num := num, den := den, den_nz := nz, reduced := c } = normalize num den nz
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<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✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I, N⁆ ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<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✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<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✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>m : M<VAR>x : ↥I<VAR>n : ↥N<VAR>hn : ⁅↑x, ↑n⁆ = m<GOAL>⁅↑x, ↑n⁆ ∈ ↑N
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>r : R<GOAL>nthRoots 0 r = 0
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)<GOAL>s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)<VAR>this : (s + 1).Gammaℝ ≠ 0<GOAL>s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : ℝ<VAR>h : y ∈ uIcc x z<GOAL>dist y z ≤ dist x z
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime x y<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>hx : IsPrimal x<GOAL>x * y ∣ z
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime x y<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>hx : IsPrimal x<GOAL>y * x ∣ z
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>h : ∀ x ∈ [[a, b]], f x ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<GOAL>IntervalIntegrable (fun x => (f x)⁻¹) μ a b
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>h : b ≤ 1<GOAL>a * b ≤ a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>S : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : Module S A<VAR>inst✝² : IsScalarTower S A A<VAR>inst✝¹ : SMulCommClass S A A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<VAR>f : S → R<GOAL>QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G.op ⊣ F.op<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<GOAL>((h.homEquiv (Opposite.op Y) (Opposite.op X')) (g.op ≫ f.op)).unop = F.map f ≫ ((h.homEquiv (Opposite.op Y) (Opposite.op X)) g.op).unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G.op ⊣ F.op<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<GOAL>(h.unit.app (Opposite.op Y) ≫ F.op.map (g.op ≫ f.op)).unop = F.map f ≫ (h.unit.app (Opposite.op Y) ≫ F.op.map g.op).unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G.op ⊣ F.op<VAR>X : C<VAR>Y Y' : D<VAR>f : F.obj X ⟶ Y<VAR>g : Y ⟶ Y'<GOAL>((h.homEquiv (Opposite.op Y') (Opposite.op X)).symm (g.op ≫ f.op)).unop = ((h.homEquiv (Opposite.op Y) (Opposite.op X)).symm f.op).unop ≫ G.map g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G.op ⊣ F.op<VAR>X : C<VAR>Y Y' : D<VAR>f : F.obj X ⟶ Y<VAR>g : Y ⟶ Y'<GOAL>(G.op.map (g.op ≫ f.op) ≫ h.counit.app (Opposite.op X)).unop = (G.op.map f.op ≫ h.counit.app (Opposite.op X)).unop ≫ G.map g
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<GOAL>ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt 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 (Fin 2) (Fin 2) α<VAR>i j : Fin 2<GOAL>A.adjugate i j = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
<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 (Fin 2) (Fin 2) α<VAR>i j : Fin 2<GOAL>(-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(((TensorProduct.mk R M N).compr₂ (lTensor M (g ∘ₗ f))) m) n = (((TensorProduct.mk R M N).compr₂ (lTensor M g ∘ₗ lTensor M f)) m) n
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>A : Type v<VAR>inst✝ : CommGroup A<VAR>f : G →* A<GOAL>commutator G ≤ f.ker
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>A : Type v<VAR>inst✝ : CommGroup A<VAR>f : G →* A<GOAL>commutatorSet G ⊆ ↑f.ker
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>A : Type v<VAR>inst✝ : CommGroup A<VAR>f : G →* A<VAR>p q : G<GOAL>⁅p, q⁆ ∈ ↑f.ker
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<GOAL>∃ g, orderOf g = exponent G
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<GOAL>∃ g, orderOf g = exponent G
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<GOAL>∃ g, orderOf g = exponent G
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<GOAL>∃ g, orderOf g = exponent G
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<GOAL>orderOf t = exponent G
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<GOAL>exponent G ∣ orderOf t
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<GOAL>(exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<GOAL>∀ x ∈ (exponent G).primeFactorsList, List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>h : ∃ x ∈ (exponent G).primeFactorsList, List.count x (orderOf t).primeFactorsList < List.count x (exponent G).primeFactorsList<GOAL>False
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : p ∈ (exponent G).primeFactorsList<VAR>hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList<GOAL>False
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList<VAR>hp : Nat.Prime p<GOAL>False
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpe : (orderOf t).factorization p < (exponent G).factorization p<GOAL>False
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<GOAL>False
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<GOAL>False
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<GOAL>orderOf t < orderOf (t ^ p ^ k * g)
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<VAR>hpk : p ^ k ∣ orderOf t<GOAL>orderOf t < orderOf (t ^ p ^ k * g)
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<VAR>hpk : p ^ k ∣ orderOf t<VAR>hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k<GOAL>orderOf t < orderOf (t ^ p ^ k * g)
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<VAR>hpk : p ^ k ∣ orderOf t<VAR>hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k<VAR>a : ℕ<VAR>ha : (exponent G).factorization p = k + a + 1<GOAL>orderOf t < orderOf (t ^ p ^ k * g)
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<VAR>hpk : p ^ k ∣ orderOf t<VAR>hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k<VAR>a : ℕ<VAR>ha : (exponent G).factorization p = k + a + 1<VAR>hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)<GOAL>orderOf t < orderOf (t ^ p ^ k * g)
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<VAR>hpk : p ^ k ∣ orderOf t<VAR>hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k<VAR>a : ℕ<VAR>ha : (exponent G).factorization p = k + a + 1<VAR>hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)<GOAL>1 < p ^ (a + 1)