ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<GOAL>generated X ≤ generatedNormal X
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<GOAL>{S | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal} ⊆ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>1 / a < b ↔ 1 / b < a
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : Dual R R<VAR>r : R<GOAL>f 1 * r = f r
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : Dual R R<VAR>r : R<GOAL>f 1 * r = f (r • 1)
<VAR>β : Sort ?u.114339<VAR>α : Sort ?u.114344<VAR>P : β → Sort w<VAR>e✝ : α ≃ β<VAR>ι'' : Sort u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>π : ι'' → Type u_1<VAR>e : ι ⊕ ι' ≃ ι''<VAR>f : (i : ι) → π (e (inl i))<VAR>g : (i : ι') → π (e (inr i))<VAR>j : ι'<GOAL>(piCongrLeft π e) ((sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (inr j)) = g j
<VAR>α β : FinBoolAlg<VAR>e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg<VAR>x✝ : (forget FinBoolAlg).obj α<GOAL>((let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : FinBoolAlg<VAR>e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg<VAR>x✝ : (forget FinBoolAlg).obj β<GOAL>((let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>x✝ : L ⧸ f.ker<VAR>x : L<VAR>y✝ : L ⧸ f.ker<VAR>y : L<GOAL>{ toFun := ⇑(↑f).quotKerEquivRange, map_add' := ⋯, map_smul' := ⋯ }.toFun ⁅Quot.mk Setoid.r x, Quot.mk Setoid.r y⁆ = ⁅{ toFun := ⇑(↑f).quotKerEquivRange, map_add' := ⋯, map_smul' := ⋯ }.toFun (Quot.mk Setoid.r x), { toFun := ⇑(↑f).quotKerEquivRange, map_add' := ⋯, map_smul' := ⋯ }.toFun (Quot.mk Setoid.r y)⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>x✝ : L ⧸ f.ker<VAR>x : L<VAR>y✝ : L ⧸ f.ker<VAR>y : L<GOAL>↑({ toFun := ⇑(↑f).quotKerEquivRange, map_add' := ⋯, map_smul' := ⋯ }.toFun ⁅Quot.mk Setoid.r x, Quot.mk Setoid.r y⁆) = ⁅↑({ toFun := ⇑(↑f).quotKerEquivRange, map_add' := ⋯, map_smul' := ⋯ }.toFun (Quot.mk Setoid.r x)), ↑({ toFun := ⇑(↑f).quotKerEquivRange, map_add' := ⋯, map_smul' := ⋯ }.toFun (Quot.mk Setoid.r y))⁆
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<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>F : Type u_2<VAR>E : Type u_3<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<GOAL>Module.rank F ↥⊤ = Module.rank F E
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>c : Chain α<VAR>f : α →o Part β<VAR>g : α →o β → Part γ<GOAL>ωSup (c.map (f.partBind g)) = ωSup (c.map f) >>= ωSup (c.map g)
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>c : Chain α<VAR>f : α →o Part β<VAR>g : α →o β → Part γ<GOAL>∀ (c_1 : Part γ), ωSup (c.map (f.partBind g)) ≤ c_1 ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ c_1
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>c : Chain α<VAR>f : α →o Part β<VAR>g : α →o β → Part γ<VAR>x : Part γ<GOAL>ωSup (c.map (f.partBind g)) ≤ x ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ x
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>c : Chain α<VAR>f : α →o Part β<VAR>g : α →o β → Part γ<VAR>x : Part γ<GOAL>(∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J✝ : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I J Js : Box ι<VAR>s : Finset (ι × ℝ)<VAR>H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s<VAR>HJs : Js ∈ splitMany I s<VAR>Hn : ¬Disjoint ↑J ↑Js<GOAL>Js ≤ J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J✝ : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I J Js : Box ι<VAR>s : Finset (ι × ℝ)<VAR>HJs : Js ∈ splitMany I s<VAR>Hn : ¬Disjoint ↑J ↑Js<VAR>H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s<GOAL>Js ≤ J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J✝ : Box ι<VAR>i : ι<VAR>x✝ : ℝ<VAR>I J Js : Box ι<VAR>s : Finset (ι × ℝ)<VAR>HJs : Js ∈ splitMany I s<VAR>Hn : ¬Disjoint ↑J ↑Js<VAR>H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s<VAR>x : ι → ℝ<VAR>hx : x ∈ ↑J<VAR>hxs : x ∈ ↑Js<GOAL>Js ≤ J
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r✝ p : R[X]<VAR>n d : ℕ<VAR>r : R<GOAL>((monomial n) r * p).coeff (d + n) = r * p.coeff d
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s₁ s₂ : Set α<VAR>hd : Disjoint s₁ s₂<VAR>h₁ : P s₁<VAR>h₂ : P s₂<GOAL>extend m (s₁ ∪ s₂) = extend m s₁ + extend m s₂
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s₁ s₂ : Set α<VAR>hd : Disjoint s₁ s₂<VAR>h₁ : P s₁<VAR>h₂ : P s₂<GOAL>∑ b : Bool, extend m (bif b then s₁ else s₂) = extend m s₁ + extend m s₂
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>logb b x < logb b y ↔ x < y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>log x < log y ↔ x < y
<VAR>z : ℂ<VAR>h : z ≠ 0<GOAL>z * z⁻¹ = 1
<VAR>a b c : ℕ<VAR>hb0 : 0 < b<VAR>hc : a / b ≤ c<VAR>x : ℕ<GOAL>x ∈ Ico 1 (a / b).succ ↔ x ∈ filter (fun x => x * b ≤ a) (Ico 1 c.succ)
<VAR>a b c : ℕ<VAR>hb0 : 0 < b<VAR>hc : a / b ≤ c<VAR>x : ℕ<VAR>this : x * b ≤ a → x ≤ c<GOAL>x ∈ Ico 1 (a / b).succ ↔ x ∈ filter (fun x => x * b ≤ a) (Ico 1 c.succ)
<VAR>a b c : ℕ<VAR>hb0 : 0 < b<VAR>hc : a / b ≤ c<VAR>x : ℕ<VAR>this : x * b ≤ a → x ≤ c<GOAL>x * b ≤ a → 1 ≤ x → x ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : SeminormedRing α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : Module α β<VAR>h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖<VAR>a : α<VAR>b₁ b₂ : β<GOAL>dist (a • b₁) (a • b₂) ≤ dist a 0 * dist b₁ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : SeminormedRing α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : Module α β<VAR>h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖<VAR>a₁ a₂ : α<VAR>b : β<GOAL>dist (a₁ • b) (a₂ • b) ≤ dist a₁ a₂ * dist b 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b : A<GOAL>D ((algebraMap R A) r) = 0
<VAR>P : ℝ → Prop<VAR>x₀ r : ℝ<VAR>hr : 1 < r<VAR>hx₀ : 0 < x₀<VAR>base : ∀ x ∈ Ico x₀ (r * x₀), P x<VAR>step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z<GOAL>∀ x ≥ x₀, P x
<VAR>P : ℝ → Prop<VAR>x₀ r : ℝ<VAR>hr : 1 < r<VAR>hx₀ : 0 < x₀<VAR>base : ∀ x ∈ Ico x₀ (r * x₀), P x<VAR>step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z<GOAL>∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
<VAR>P : ℝ → Prop<VAR>x₀ r : ℝ<VAR>hr : 1 < r<VAR>hx₀ : 0 < x₀<VAR>base : ∀ x ∈ Ico x₀ (r * x₀), P x<VAR>step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z<VAR>n : ℕ<GOAL>∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>b c : α<VAR>u : αˣ<GOAL>↑u * (↑u)⁻¹ = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hs : ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)<VAR>u : Set X<VAR>hu : IsOpen u<GOAL>f '' u = f '' interior u
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) ^ Group.rank ↥(closureCommutatorRepresentatives G)<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) ^ Group.rank ↥(closureCommutatorRepresentatives G)<VAR>h2 : Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣ (center ↥(closureCommutatorRepresentatives G)).index ^ ((center ↥(closureCommutatorRepresentatives G)).index * Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) + 1)<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank ↥(closureCommutatorRepresentatives G)<VAR>h2 : Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣ (center ↥(closureCommutatorRepresentatives G)).index ^ ((center ↥(closureCommutatorRepresentatives G)).index * Nat.card ↑(commutatorSet G) + 1)<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank ↥(closureCommutatorRepresentatives G)<VAR>h2 : Nat.card ↥(_root_.commutator G) ∣ (center ↥(closureCommutatorRepresentatives G)).index ^ ((center ↥(closureCommutatorRepresentatives G)).index * Nat.card ↑(commutatorSet G) + 1)<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h2 : Nat.card ↥(_root_.commutator G) ∣ (center ↥(closureCommutatorRepresentatives G)).index ^ ((center ↥(closureCommutatorRepresentatives G)).index * Nat.card ↑(commutatorSet G) + 1)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))<VAR>h2 : Nat.card ↥(_root_.commutator G) ∣ (center ↥(closureCommutatorRepresentatives G)).index ^ (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G)) * Nat.card ↑(commutatorSet G) + 1)<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))<VAR>h2 : Nat.card ↥(_root_.commutator G) ∣ (center ↥(closureCommutatorRepresentatives G)).index ^ (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)<GOAL>Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>h1 : (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))<VAR>h2 : Nat.card ↥(_root_.commutator G) ∣ (center ↥(closureCommutatorRepresentatives G)).index ^ (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)<GOAL>0 < (center ↥(closureCommutatorRepresentatives G)).index ^ (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>G : Karoubi C ⥤ Karoubi D<VAR>P : Karoubi C<GOAL>(G.map P.decompId_p).f = ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p ≫ (G.map P.decompId_p).f ≫ (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>G : Karoubi C ⥤ Karoubi D<VAR>P Q : Karoubi C<VAR>f : P ⟶ Q<GOAL>(((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f ≫ (fun P => { f := (G.map P.decompId_p).f, comm := ⋯ }) Q = (fun P => { f := (G.map P.decompId_p).f, comm := ⋯ }) P ≫ ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>G : Karoubi C ⥤ Karoubi D<VAR>P : Karoubi C<GOAL>(G.map P.decompId_i).f = (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p ≫ (G.map P.decompId_i).f ≫ ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>G : Karoubi C ⥤ Karoubi D<VAR>P Q : Karoubi C<VAR>f : P ⟶ Q<GOAL>((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f ≫ (fun P => { f := (G.map P.decompId_i).f, comm := ⋯ }) Q = (fun P => { f := (G.map P.decompId_i).f, comm := ⋯ }) P ≫ (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>G : Karoubi C ⥤ Karoubi D<VAR>P : Karoubi C<GOAL>(({ app := fun P => { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ } ≫ { app := fun P => { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }).app P).f = ((𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G)).app P).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>G : Karoubi C ⥤ Karoubi D<VAR>P : Karoubi C<GOAL>(({ app := fun P => { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } ≫ { app := fun P => { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ }).app P).f = ((𝟙 ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G)).app P).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>X Y : Karoubi C ⥤ Karoubi D<VAR>φ : X ⟶ Y<VAR>P : Karoubi C<GOAL>((X.map ((toKaroubi C).map P.p)).f ≫ (φ.app ((toKaroubi C).obj P.X)).f) ≫ (Y.map P.decompId_p).f = (X.map P.decompId_p).f ≫ (φ.app P).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>X Y : Karoubi C ⥤ Karoubi D<VAR>φ : X ⟶ Y<VAR>P : Karoubi C<GOAL>((X.map (P.decompId_p ≫ P.decompId_i)).f ≫ (φ.app ((toKaroubi C).obj P.X)).f) ≫ (Y.map P.decompId_p).f = (X.map P.decompId_p).f ≫ (X.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ Y.map P.decompId_p).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.48051, u_1} C<VAR>inst✝¹ : Category.{?u.48055, u_2} D<VAR>inst✝ : Category.{?u.48059, u_3} E<VAR>X Y : Karoubi C ⥤ Karoubi D<VAR>φ : X ⟶ Y<VAR>P : Karoubi C<GOAL>(X.map P.decompId_p).f ≫ (X.map P.decompId_i).f ≫ (φ.app ((toKaroubi C).obj P.X)).f ≫ (Y.map P.decompId_p).f = (X.map P.decompId_p).f ≫ (X.map P.decompId_i).f ≫ (φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ }).f ≫ (Y.map P.decompId_p).f
<VAR>x y : ℝ<GOAL>cos x ^ 2 ≤ 1
<VAR>x y : ℝ<GOAL>cos x ^ 2 ≤ sin x ^ 2 + cos x ^ 2
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.114018, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>rightHomologyMap' e.hom h₁ h₂ ≫ rightHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.114018, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>rightHomologyMap' e.inv h₂ h₁ ≫ rightHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s : Set (Set α)<VAR>hs : IsPiSystem s<GOAL>ofMeasurableSpace ((generate s).toMeasurableSpace ⋯) ≤ ofMeasurableSpace (generateFrom s)
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s : Set (Set α)<VAR>hs : IsPiSystem s<GOAL>generate s ≤ ofMeasurableSpace (generateFrom s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>x₀ : M<VAR>hf : ContMDiffAt I' I n f x₀<VAR>hg : ContMDiffAt I' I n g x₀<GOAL>ContMDiffAt I' I n (fun x => f x / g x) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>x₀ : M<VAR>hf : ContMDiffAt I' I n f x₀<VAR>hg : ContMDiffAt I' I n g x₀<GOAL>ContMDiffAt I' I n (fun x => f x * (g x)⁻¹) x₀
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁸ : CommRing A<VAR>inst✝³⁷ : CommRing B<VAR>inst✝³⁶ : Algebra A B<VAR>inst✝³⁵ : Field K<VAR>inst✝³⁴ : Field L<VAR>inst✝³³ : Algebra A K<VAR>inst✝³² : IsFractionRing A K<VAR>inst✝³¹ : Algebra B L<VAR>inst✝³⁰ : Algebra K L<VAR>inst✝²⁹ : Algebra A L<VAR>inst✝²⁸ : IsScalarTower A B L<VAR>inst✝²⁷ : IsScalarTower A K L<VAR>inst✝²⁶ : IsIntegralClosure B A L<VAR>inst✝²⁵ : FiniteDimensional K L<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²⁴ : CommRing Aₘ<VAR>inst✝²³ : CommRing Bₘ<VAR>inst✝²² : Algebra Aₘ Bₘ<VAR>inst✝²¹ : Algebra A Aₘ<VAR>inst✝²⁰ : Algebra B Bₘ<VAR>inst✝¹⁹ : Algebra A Bₘ<VAR>inst✝¹⁸ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁷ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁶ : IsLocalization M Aₘ<VAR>inst✝¹⁵ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹⁴ : IsIntegrallyClosed A<VAR>inst✝¹³ : IsDomain A<VAR>inst✝¹² : IsIntegrallyClosed A<VAR>inst✝¹¹ : IsDomain B<VAR>inst✝¹⁰ : IsIntegrallyClosed B<VAR>inst✝⁹ : Module.Finite A B<VAR>inst✝⁸ : NoZeroSMulDivisors A B<VAR>inst✝⁷ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : 0 ∉ M<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)