ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>o₁ o₂ : ONote<VAR>inst✝¹ : o₁.NF<VAR>inst✝ : o₂.NF<VAR>a : ONote<VAR>m : ℕ<VAR>e₁ : o₁.split = (a, m)<VAR>N₁ : a.NF<VAR>r₁ : o₁.repr = a.repr + ↑m<GOAL>(o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>inst✝¹ : CommMonoid β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι ≃ κ<VAR>hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t<VAR>hfg : ∀ i ∈ s, f i = g (e i)<GOAL>∏ i ∈ s, f i = ∏ i ∈ t, g i
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPushout b.fst b.snd 0 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPushout (b.inl ≫ b.fst) 0 0 (0 ≫ 0)
<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>U : Set (G ⧸ N)<VAR>g : ↥N.op<VAR>x : G<GOAL>x ∈ g • ⇑(mk' N) ⁻¹' U ↔ x ∈ ⇑(mk' N) ⁻¹' U
<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>U : Set (G ⧸ N)<VAR>g : ↥N.op<VAR>x : G<GOAL>(mk' N) (g⁻¹ • x) ∈ U ↔ (mk' N) x ∈ U
<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>U : Set (G ⧸ N)<VAR>g : ↥N.op<VAR>x : G<GOAL>(mk' N) (g⁻¹ • x) = (mk' N) x
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f g : End F<GOAL>(endEquivAutGalois F) (g ≫ f) = (endEquivAutGalois F) g * (endEquivAutGalois F) f
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f g : End F<VAR>A : PointedGaloisObject F<GOAL>(fun f => F.map f.hom A.pt) ((AutGalois.π F A) ((endEquivAutGalois F) (g ≫ f))) = (fun f => F.map f.hom A.pt) ((AutGalois.π F A) ((endEquivAutGalois F) g * (endEquivAutGalois F) f))
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f g : End F<VAR>A : PointedGaloisObject F<GOAL>(g.app A.obj ≫ f.app A.obj) A.pt = F.map (((AutGalois.π F A) ((endEquivAutGalois F) f)).hom ≫ ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f g : End F<VAR>A : PointedGaloisObject F<GOAL>f.app A.obj (g.app A.obj A.pt) = F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom (f.app A.obj A.pt)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f g : End F<VAR>A : PointedGaloisObject F<GOAL>f.app A.obj (g.app A.obj A.pt) = (f.app A.obj ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<GOAL>p.natDegree ∣ Fintype.card p.Gal
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<GOAL>p.natDegree ∣ finrank F p.SplittingField
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>hp : p.degree ≠ 0<GOAL>p.natDegree ∣ finrank F p.SplittingField
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>hp : p.degree ≠ 0<VAR>α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp<GOAL>p.natDegree ∣ finrank F p.SplittingField
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>hp : p.degree ≠ 0<VAR>α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp<VAR>hα : IsIntegral F α<GOAL>p.natDegree ∣ finrank F p.SplittingField
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>hp : p.degree ≠ 0<VAR>α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp<VAR>hα : IsIntegral F α<GOAL>finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>hp : p.degree ≠ 0<VAR>α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp<VAR>hα : IsIntegral F α<GOAL>(minpoly F α).natDegree = p.natDegree
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>hp : p.degree ≠ 0<VAR>α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp<VAR>hα : IsIntegral F α<GOAL>minpoly F α ∣ p
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>hp : p.degree ≠ 0<VAR>α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp<VAR>hα : IsIntegral F α<GOAL>(aeval α) p = 0
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<GOAL>σ 1 = σ (↑ₐ 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<GOAL>DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>x y : R<VAR>h : Commute x y<GOAL>(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>x y : R<VAR>h : Commute x y<VAR>r : R<VAR>hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r<GOAL>(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s✝ t✝ : Set α<VAR>l : List α<VAR>a : α<VAR>s : Set α<VAR>t : Set β<VAR>n m : ℕ<GOAL>s.chainHeight + ↑n ≤ t.chainHeight + ↑m ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s✝ t✝ : Set α<VAR>l : List α<VAR>a : α<VAR>s : Set α<VAR>t : Set β<VAR>n m : ℕ<VAR>H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m<GOAL>s.chainHeight + ↑n ≤ t.chainHeight + ↑m
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : Group G✝<VAR>inst✝¹ : Fintype G✝<VAR>x : G✝<VAR>n : ℕ<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<VAR>key : g ^ ↑((Nat.card G).gcd n) = g ^ (↑(Nat.card G) * (Nat.card G).gcdA n + ↑n * (Nat.card G).gcdB n)<GOAL>(fun g => g ^ (Nat.card G).gcdB n) ((fun g => g ^ n) g) = g
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : Group G✝<VAR>inst✝¹ : Fintype G✝<VAR>x : G✝<VAR>n : ℕ<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<VAR>key : g ^ ↑((Nat.card G).gcd n) = g ^ (↑(Nat.card G) * (Nat.card G).gcdA n + ↑n * (Nat.card G).gcdB n)<GOAL>(fun g => g ^ n) ((fun g => g ^ (Nat.card G).gcdB n) g) = g
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN<GOAL>∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN<VAR>f : Ω →ᵇ ℝ≥0<GOAL>∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : μ.toWeakDualBCNN f = ν.toWeakDualBCNN f<GOAL>∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : μ.toWeakDualBCNN f = ν.toWeakDualBCNN f<GOAL>∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≠ ⊤
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : μ.toWeakDualBCNN f = ν.toWeakDualBCNN f<GOAL>∫⁻ (ω : Ω), ↑(f ω) ∂↑ν ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>c₀ : Chain α<VAR>c₁ : Chain β<GOAL>ωSup (c₀.zip c₁) = (ωSup c₀, ωSup c₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>c₀ : Chain α<VAR>c₁ : Chain β<GOAL>∀ (c : α × β), ωSup (c₀.zip c₁) ≤ c ↔ (ωSup c₀, ωSup c₁) ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>c₀ : Chain α<VAR>c₁ : Chain β<VAR>z₁ : α<VAR>z₂ : β<GOAL>ωSup (c₀.zip c₁) ≤ (z₁, z₂) ↔ (ωSup c₀, ωSup c₁) ≤ (z₁, z₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>G✝ : Type u_6<VAR>H✝ : Type u_7<VAR>F : Type u_8<VAR>inst✝⁵ : Group G✝<VAR>inst✝⁴ : CommGroup H✝<VAR>G : Type u_9<VAR>H : Type u_10<VAR>inst✝³ : Group G<VAR>inst✝² : MulOneClass H<VAR>inst✝¹ : FunLike F G H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>h : ∀ (a : G), f a = 1 → a = 1<VAR>x y : G<VAR>hxy : f x = f y<GOAL>f (x * y⁻¹) = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree = 3
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>↑3 = 3
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Sort u_4<VAR>p : ι → Submodule R M<GOAL>↑(⨅ i, p i) = ⋂ i, ↑(p i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Sort u_4<VAR>p : ι → Submodule R M<GOAL>⋂ p_1 ∈ Set.range fun i => p i, ↑p_1 = ⋂ i, ↑(p i)
<VAR>k : ℕ<GOAL>(k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>im ⟪x, y⟫_𝕜 = -im ⟪y, x⟫_𝕜
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hx : 0 < x + 1<VAR>n : ℕ<VAR>hn : n + 1 + 1 ≠ 0<GOAL>0 < ∑ i ∈ range (n + 1 + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hx : 0 < x + 1<VAR>n : ℕ<VAR>hn : n + 1 + 1 ≠ 0<VAR>hx' : x < 0<GOAL>0 < ∑ i ∈ range (n + 1 + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hx : 0 < x + 1<VAR>n : ℕ<VAR>hn : n + 1 + 1 ≠ 0<VAR>hx' : 0 ≤ x<GOAL>0 < ∑ i ∈ range (n + 1 + 1), x ^ i
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<GOAL>f^[n] a ≤ nfp f a
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<GOAL>f^[n] a ≤ (fun a => sup fun n => f^[n] a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic x) ∂ν a = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → ι<VAR>hs : s.SupIndep (f ∘ g)<VAR>t : Finset ι<VAR>ht : t ⊆ Finset.image g s<VAR>i : ι<VAR>hi : i ∈ Finset.image g s<VAR>hit : i ∉ t<GOAL>Disjoint (f i) (t.sup f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → ι<VAR>hs : s.SupIndep (f ∘ g)<VAR>t : Finset ι<VAR>ht : t ⊆ Finset.image g s<VAR>i : ι<VAR>hi : ∃ a ∈ s, g a = i<VAR>hit : i ∉ t<GOAL>Disjoint (f i) (t.sup f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → ι<VAR>hs : s.SupIndep (f ∘ g)<VAR>t : Finset ι<VAR>ht : t ⊆ Finset.image g s<VAR>i : ι'<VAR>hi : i ∈ s<VAR>hit : g i ∉ t<VAR>this : DecidableEq ι'<GOAL>Disjoint (f (g i)) (t.sup f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → ι<VAR>hs : s.SupIndep (f ∘ g)<VAR>t : Finset ι<VAR>ht : t ⊆ Finset.image g s<VAR>i : ι'<VAR>hi : i ∈ s<VAR>hit : g i ∉ t<VAR>this : DecidableEq ι'<GOAL>t ⊆ Finset.image g (s.erase i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → ι<VAR>hs : s.SupIndep (f ∘ g)<VAR>t : Finset ι<VAR>ht : t ⊆ Finset.image g s<VAR>i : ι'<VAR>hi : i ∈ s<VAR>hit : g i ∉ t<VAR>this : DecidableEq ι'<VAR>j : ι<VAR>hjt : j ∈ t<GOAL>j ∈ Finset.image g (s.erase i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → ι<VAR>hs : s.SupIndep (f ∘ g)<VAR>t : Finset ι<VAR>ht : t ⊆ Finset.image g s<VAR>i : ι'<VAR>hi : i ∈ s<VAR>hit : g i ∉ t<VAR>this : DecidableEq ι'<VAR>j : ι'<VAR>hj : j ∈ s<VAR>hjt : g j ∈ t<GOAL>g j ∈ Finset.image g (s.erase i)
<VAR>x y z : ℝ<VAR>n✝ : ℕ<VAR>hx : 0 ≤ x<VAR>n : ℤ<VAR>h : y - ↑n ≠ 0<GOAL>x ^ (y - ↑n) = x ^ y / x ^ n
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι✝ : Type u_6<VAR>inst✝⁴ : SeminormedRing 𝕜<VAR>inst✝³ : SMul 𝕜 E<VAR>inst✝² : Zero E<VAR>inst✝¹ : TopologicalSpace E<VAR>ι : Sort u_7<VAR>inst✝ : Finite ι<VAR>s : ι → Set E<GOAL>IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ (i : ι), IsVonNBounded 𝕜 (s i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>s : Set β<GOAL>map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>N✝ : Type w<VAR>inst✝⁸ : AddCommGroup N✝<VAR>inst✝⁷ : Module R N✝<VAR>inst✝⁶ : Small.{v, u} R<VAR>flat : Flat R M<VAR>N N' N'' : Type v<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup N''<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<VAR>π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ<GOAL>Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>N✝ : Type w<VAR>inst✝⁸ : AddCommGroup N✝<VAR>inst✝⁷ : Module R N✝<VAR>inst✝⁶ : Small.{v, u} R<VAR>flat : Flat R M<VAR>N N' N'' : Type v<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup N''<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<VAR>π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ<VAR>ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)<GOAL>Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>N✝ : Type w<VAR>inst✝⁸ : AddCommGroup N✝<VAR>inst✝⁷ : Module R N✝<VAR>inst✝⁶ : Small.{v, u} R<VAR>flat : Flat R M<VAR>N N' N'' : Type v<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup N''<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<VAR>π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ<VAR>ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)<GOAL>Function.Exact ⇑(rTensor M f) ⇑(rTensor M π)
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<GOAL>∃ θ, f = o.rotation θ
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this : Nontrivial V<GOAL>∃ θ, f = o.rotation θ
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>∃ θ, f = o.rotation θ
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>f = o.rotation (o.oangle x (f x))
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>f.toLinearEquiv = (o.rotation (o.oangle x (f x))).toLinearEquiv
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>↑f.toLinearEquiv = ↑(o.rotation (o.oangle x (f x))).toLinearEquiv
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>∀ (i : Fin 2), ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) i) = ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) i)
<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>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ⟨1, ⋯⟩) = ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ⟨1, ⋯⟩)