ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>(α_ (P.X ⊗ Q.X) L.X U.X).hom ≫ (((α_ P.X Q.X (L.X ⊗ U.X)).hom ≫ P.X ◁ Q.X ◁ L.actRight) ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫ coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫ P.X ◁ TensorBimod.actLeft Q L) = (α_ P.X Q.X L.X).hom ▷ U.X ≫ (((α_ P.X (Q.X ⊗ L.X) U.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ▷ U.X) ≫ P.X ◁ (Q.tensorBimod L).actRight) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>(α_ (P.X ⊗ Q.X) L.X U.X).hom ≫ (((α_ P.X Q.X (L.X ⊗ U.X)).hom ≫ P.X ◁ Q.X ◁ L.actRight) ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫ coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫ P.X ◁ TensorBimod.actLeft Q L) = (α_ P.X Q.X L.X).hom ▷ U.X ≫ (((α_ P.X (Q.X ⊗ L.X) U.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ▷ U.X) ≫ P.X ◁ TensorBimod.actRight Q L) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>(α_ (P.X ⊗ Q.X) L.X U.X).hom ≫ (((α_ P.X Q.X (L.X ⊗ U.X)).hom ≫ P.X ◁ Q.X ◁ L.actRight) ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫ coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫ P.X ◁ TensorBimod.actLeft Q L) = (α_ P.X Q.X L.X).hom ▷ U.X ≫ (α_ P.X (Q.X ⊗ L.X) U.X).hom ≫ (P.X ◁ (α_ Q.X L.X U.X).hom ≫ P.X ◁ Q.X ◁ L.actRight ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Algebra A B<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A S<VAR>inst✝ : Nontrivial A<VAR>pb : PowerBasis A S<GOAL>(X ^ pb.dim - ∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree = ↑pb.dim
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Algebra A B<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A S<VAR>inst✝ : Nontrivial A<VAR>pb : PowerBasis A S<GOAL>(∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < ↑pb.dim
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>#↑s ≤ ↑n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>∀ (s_1 : Finset ↑s), s_1.card ≤ n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<GOAL>t.card ≤ n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<GOAL>(Finset.map (Embedding.subtype s) t).card ≤ n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<GOAL>LinearIndependent R fun i => ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>p : ι → Prop<VAR>q : ι → ι' → Prop<VAR>s : (x : ι) → (y : ι') → p x ∧ q x y → Set α<GOAL>⋃ x, ⋃ y, ⋃ (h : p x ∧ q x y), s x y h = ⋃ x, ⋃ (hx : p x), ⋃ y, ⋃ (hy : q x y), s x y ⋯
<VAR>A : Class<VAR>x : ZFSet<VAR>x✝ : A.ToSet ↑x<VAR>y : ZFSet<VAR>yx : ↑y = ↑x<VAR>py : A y<GOAL>A x
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m✝ : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>β : ι → Type u_6<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (x : ι) → Ω → β x<VAR>μ : Measure Ω<GOAL>iIndepFun m f μ ↔ ∀ (s : Finset ι) {f' : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitLower i x = ⊥ ↔ x ≤ I.lower i
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>i : ι<VAR>x : ℝ<GOAL>(min x (I.upper i) ≤ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i
<VAR>a c b_n : ℕ<VAR>b_ih : a.choose c ≤ (a + b_n).choose c<GOAL>a.choose c ≤ (a + (b_n + 1)).choose c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ affineSpan ℝ (Set.range s.points)<GOAL>dist p1 p2 * dist p1 p2 = dist p1 ↑(s.orthogonalProjectionSpan p2) * dist p1 ↑(s.orthogonalProjectionSpan p2) + dist p2 ↑(s.orthogonalProjectionSpan p2) * dist p2 ↑(s.orthogonalProjectionSpan p2)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ affineSpan ℝ (Set.range s.points)<GOAL>⟪p1 -ᵥ ↑(s.orthogonalProjectionSpan p2), ↑(s.orthogonalProjectionSpan p2) -ᵥ p2⟫_ℝ = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype m<VAR>A : Matrix m n α<VAR>x y : m → α<VAR>x✝ : n<GOAL>((x - y) ᵥ* A) x✝ = (x ᵥ* A - y ᵥ* A) x✝
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∠ p₃ p₂ p₁ = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∠ p₁ p₂ p₃ = π / 2
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<VAR>ha0 : a ≠ 0<VAR>ha1 : ¬IsUnit a<VAR>this✝¹ : DecidableEq R := Classical.decEq R<VAR>i j : ℕ<VAR>hij : (fun x => a ^ x) i = (fun x => a ^ x) j<VAR>this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }<VAR>this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid<GOAL>i = j
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<VAR>ha0 : a ≠ 0<VAR>ha1 : ¬IsUnit a<VAR>this✝¹ : DecidableEq R := Classical.decEq R<VAR>i j : ℕ<VAR>hij : (fun x => a ^ x) i = (fun x => a ^ x) j<VAR>this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }<VAR>this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid<VAR>p' : R<VAR>hp' : Irreducible p'<VAR>dvd' : p' ∣ a<GOAL>i = j
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<VAR>ha0 : a ≠ 0<VAR>ha1 : ¬IsUnit a<VAR>this✝¹ : DecidableEq R := Classical.decEq R<VAR>i j : ℕ<VAR>hij : (fun x => a ^ x) i = (fun x => a ^ x) j<VAR>this✝ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }<VAR>this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid<VAR>p' : R<VAR>hp' : Irreducible p'<VAR>dvd' : p' ∣ a<VAR>p : R<VAR>mem : p ∈ normalizedFactors a<VAR>right✝ : p' ~ᵤ p<GOAL>i = j
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<VAR>ha0 : a ≠ 0<VAR>ha1 : ¬IsUnit a<VAR>this✝² : DecidableEq R := Classical.decEq R<VAR>i j : ℕ<VAR>hij : (fun x => a ^ x) i = (fun x => a ^ x) j<VAR>this✝¹ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }<VAR>this✝ : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid<VAR>p' : R<VAR>hp' : Irreducible p'<VAR>dvd' : p' ∣ a<VAR>p : R<VAR>mem : p ∈ normalizedFactors a<VAR>right✝ : p' ~ᵤ p<VAR>this : (fun x => Multiset.count p (normalizedFactors x)) ((fun x => a ^ x) i) = (fun x => Multiset.count p (normalizedFactors x)) ((fun x => a ^ x) j)<GOAL>i = j
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<VAR>ha0 : a ≠ 0<VAR>ha1 : ¬IsUnit a<VAR>this✝² : DecidableEq R := Classical.decEq R<VAR>i j : ℕ<VAR>hij : (fun x => a ^ x) i = (fun x => a ^ x) j<VAR>this✝¹ : Nontrivial R := { exists_pair_ne := Exists.intro a (Exists.intro 0 ha0) }<VAR>this✝ : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid<VAR>p' : R<VAR>hp' : Irreducible p'<VAR>dvd' : p' ∣ a<VAR>p : R<VAR>mem : p ∈ normalizedFactors a<VAR>right✝ : p' ~ᵤ p<VAR>this : i * Multiset.count p (normalizedFactors a) = j * Multiset.count p (normalizedFactors a)<GOAL>i = j
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : Mul M<VAR>inst✝² : Mul N<VAR>a x y : M<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>h : SemiconjBy (f a) (f x) (f y)<GOAL>f (a * x) = f (y * a)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>inst✝¹ : IsIso f<VAR>inst✝ : IsIso g<VAR>p : inv f = inv g<GOAL>f = g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>inst✝¹ : IsIso f<VAR>inst✝ : IsIso g<VAR>p : inv f = inv g<GOAL>inv f ≫ f = inv f ≫ g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f✝ g✝ : β → α<VAR>a : α<VAR>inst✝¹ : SemilatticeSup γ<VAR>inst✝ : OrderBot γ<VAR>s : Finset β<VAR>f : β → α<VAR>g : α → γ<VAR>g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y<VAR>bot : g ⊥ = ⊥<VAR>c : β<VAR>t : Finset β<VAR>hc : c ∉ t<VAR>ih : g (t.sup f) = t.sup (g ∘ f)<GOAL>g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⟶ Y ⊗ ⨁ f<VAR>w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⟶ Y ⊗ ⨁ f<VAR>w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j<GOAL>g ≫ (leftDistributor Y f).hom = h ≫ (leftDistributor Y f).hom
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⟶ Y ⊗ ⨁ f<VAR>w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j<VAR>j✝ : J<GOAL>(g ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝ = (h ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⟶ Y ⊗ ⨁ f<VAR>w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j<VAR>j✝ : J<GOAL>g ≫ Y ◁ biproduct.π f j✝ = h ≫ Y ◁ biproduct.π f j✝
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hf : Memℒp f p μ<GOAL>eLpNorm (-f) p μ < ⊤
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹² : NormedAddCommGroup D<VAR>inst✝¹¹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup X<VAR>inst✝³ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝² : NormedRing R<VAR>inst✝¹ : NormedAlgebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>ContDiffAt 𝕜 n Ring.inverse ↑x
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹² : NormedAddCommGroup D<VAR>inst✝¹¹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup X<VAR>inst✝³ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝² : NormedRing R<VAR>inst✝¹ : NormedAlgebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>ContDiffAt 𝕜 0 Ring.inverse ↑x
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹² : NormedAddCommGroup D<VAR>inst✝¹¹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup X<VAR>inst✝³ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝² : NormedRing R<VAR>inst✝¹ : NormedAlgebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>n : ℕ<VAR>IH : ContDiffAt 𝕜 (↑n) Ring.inverse ↑x<GOAL>ContDiffAt 𝕜 (↑n.succ) Ring.inverse ↑x
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹² : NormedAddCommGroup D<VAR>inst✝¹¹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup X<VAR>inst✝³ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝² : NormedRing R<VAR>inst✝¹ : NormedAlgebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) Ring.inverse ↑x<GOAL>ContDiffAt 𝕜 ⊤ Ring.inverse ↑x
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>map_eq : Polynomial.map f p = 1<VAR>a✝ : Nontrivial R<VAR>hdeg : p.degree = 0<GOAL>p = 1
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>map_eq : Polynomial.map f p = 1<VAR>a✝ : Nontrivial R<VAR>hdeg : p.degree = 0<VAR>hndeg : p.natDegree = 0<GOAL>p = 1
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>map_eq : Polynomial.map f p = 1<VAR>a✝ : Nontrivial R<VAR>hdeg : p.degree = 0<VAR>hndeg : p.natDegree = 0<GOAL>1 = C (p.coeff 0)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hm : LinearIndependent R m<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hm : LinearIndependent R m<VAR>this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hm : LinearIndependent R m<VAR>this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup<VAR>n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hm : LinearIndependent R m<VAR>this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup<VAR>n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<VAR>hn : (mulLeftMap N m) n = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hm : LinearIndependent R m<VAR>this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup<VAR>n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<VAR>hn : n = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<VAR>h : LinearIndependent R ![a, b]<VAR>m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]<VAR>hm : LinearIndependent R m<VAR>this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup<VAR>n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩<VAR>hn : b = 0 ∧ a = 0<GOAL>False
<VAR>i j : ℕ<GOAL>i ! * j ! ∣ (i + j)!
<VAR>i j : ℕ<GOAL>i ! * (i + j - i)! ∣ (i + j)!
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set β<GOAL>⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ