ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>g : M →* N<VAR>h₀ : (s ∩ mulSupport f).Finite<GOAL>g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>g : M →* N<VAR>h₀ : (s ∩ mulSupport f).Finite<GOAL>∏ᶠ (i : α), g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>g : M →* N<VAR>h₀ : (s ∩ mulSupport f).Finite<GOAL>(mulSupport fun j => ∏ᶠ (_ : j ∈ s), f j).Finite
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P (f ∣_ U i)<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P (f ∣_ U i)<VAR>i : ((Y.openCoverOfISupEqTop Subtype.val ⋯).pullbackCover f).J<GOAL>P ((Y.openCoverOfISupEqTop Subtype.val ⋯).pullbackHom f i)
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P (f ∣_ U i)<VAR>i : ι<GOAL>P ((Y.openCoverOfISupEqTop Subtype.val ⋯).pullbackHom f ⟨U i, ⋯⟩)
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P (f ∣_ U i)<VAR>i : ι<GOAL>P (f ∣_ Scheme.Hom.opensRange ((Y.openCoverOfISupEqTop Subtype.val ⋯).map ⟨U i, ⋯⟩))
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P (f ∣_ U i)<VAR>i : ι<GOAL>P (f ∣_ Scheme.Hom.opensRange (U i).ι)
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P (f ∣_ U i)<VAR>i : ι<GOAL>P (f ∣_ U i)
<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>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>m : List α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<GOAL>m.prod = ∏ i ∈ s, i ^ count i m
<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>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>m : List α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<GOAL>∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m = ∏ i ∈ s, i ^ count i m
<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>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>m : List α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<VAR>x : α<VAR>x✝ : x ∈ s<VAR>hx : x ∉ m.toFinset<GOAL>x ^ count x m = 1
<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>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>m : List α<VAR>s : Finset α<VAR>hs : m.toFinset ⊆ s<VAR>x : α<VAR>x✝ : x ∈ s<VAR>hx : x ∉ m<GOAL>x ^ count x m = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : CommMonoid α<VAR>f : α →₀ ℕ<GOAL>(toMultiset f).prod = f.prod fun a n => a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : CommMonoid α<VAR>f : α →₀ ℕ<GOAL>(toMultiset 0).prod = prod 0 fun a n => a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : CommMonoid α<VAR>f : α →₀ ℕ<GOAL>∀ (a : α) (b : ℕ) (f : α →₀ ℕ), a ∉ f.support → b ≠ 0 → ((toMultiset f).prod = f.prod fun a n => a ^ n) → (toMultiset (single a b + f)).prod = (single a b + f).prod fun a n => a ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<VAR>hmp : p.Monic<VAR>hq : q ≠ 0<VAR>zn0 : 0 ≠ 1<VAR>x✝ : p ^ (q.natDegree + 1) ∣ q<VAR>r : R[X]<VAR>hr : q = p ^ (q.natDegree + 1) * r<VAR>hp0 : p ≠ 0<VAR>hr0 : r ≠ 0<VAR>hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<VAR>hmp : p.Monic<VAR>hq : q ≠ 0<VAR>zn0 : 0 ≠ 1<VAR>x✝ : p ^ (q.natDegree + 1) ∣ q<VAR>r : R[X]<VAR>hr : q = p ^ (q.natDegree + 1) * r<VAR>hp0 : p ≠ 0<VAR>hr0 : r ≠ 0<VAR>hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1<VAR>hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<VAR>hmp : p.Monic<VAR>hq : q ≠ 0<VAR>zn0 : 0 ≠ 1<VAR>x✝ : p ^ (q.natDegree + 1) ∣ q<VAR>r : R[X]<VAR>hr : q = p ^ (q.natDegree + 1) * r<VAR>hp0 : p ≠ 0<VAR>hr0 : r ≠ 0<VAR>hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1<VAR>hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0<VAR>hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<VAR>hmp : p.Monic<VAR>hq : q ≠ 0<VAR>zn0 : 0 ≠ 1<VAR>x✝ : p ^ (q.natDegree + 1) ∣ q<VAR>r : R[X]<VAR>hr : q = p ^ (q.natDegree + 1) * r<VAR>hp0 : p ≠ 0<VAR>hr0 : r ≠ 0<VAR>hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1<VAR>hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0<VAR>hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0<VAR>hnp : 0 < p.natDegree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<VAR>hmp : p.Monic<VAR>hq : q ≠ 0<VAR>zn0 : 0 ≠ 1<VAR>x✝ : p ^ (q.natDegree + 1) ∣ q<VAR>r : R[X]<VAR>hr : q = p ^ (q.natDegree + 1) * r<VAR>hp0 : p ≠ 0<VAR>hr0 : r ≠ 0<VAR>hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1<VAR>hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0<VAR>hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0<VAR>hnp : 0 < p.natDegree<VAR>this : q.natDegree = (p ^ (q.natDegree + 1) * r).natDegree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<VAR>hmp : p.Monic<VAR>hq : q ≠ 0<VAR>zn0 : 0 ≠ 1<VAR>x✝ : p ^ (q.natDegree + 1) ∣ q<VAR>r : R[X]<VAR>hr : q = p ^ (q.natDegree + 1) * r<VAR>hp0 : p ≠ 0<VAR>hr0 : r ≠ 0<VAR>hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1<VAR>hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0<VAR>hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0<VAR>hnp : 0 < p.natDegree<VAR>this : q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ k, ↑p ^ (-↑k) < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>k : ℕ<VAR>hk : ε⁻¹ < ↑k<GOAL>∃ k, ↑p ^ (-↑k) < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>k : ℕ<VAR>hk : ε⁻¹ < ↑k<GOAL>↑p ^ (-↑k) < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>k : ℕ<VAR>hk : ε⁻¹ < ↑k<GOAL>ε⁻¹ < (↑p ^ (-↑k))⁻¹
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>k : ℕ<VAR>hk : ε⁻¹ < ↑k<GOAL>0 < ↑p
<VAR>m n : ℤ<GOAL>Odd (m - n) ↔ (Odd m ↔ Even n)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s : Stream' α<GOAL>(take n s).length = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α<VAR>s t : Finset α<VAR>inst✝² : Fintype α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : Fintype { a // p a }<GOAL>map (Embedding.subtype p) univ = filter p univ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>(p * (X + ↑n)).comp q = p.comp q * (q + ↑n)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g : G<VAR>x✝ : α<GOAL>x✝ ∈ fixedBy α g⁻¹ ↔ x✝ ∈ fixedBy α g
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeInf ι<VAR>inst✝¹ : NoMinOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s μ<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>μ t = 0 ∨ μ t = 1
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>inst✝⁴ : HasBinaryCoproduct A B<VAR>inst✝³ : HasBinaryCoproduct A' B'<VAR>inst✝² : HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>inst✝¹ : HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>inst✝ : IsIso (coprodComparison F A B)<GOAL>F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>f : (fun x x_1 => x > x_1) ↪r r<GOAL>¬WellFounded r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>f : (fun x x_1 => x > x_1) ↪r r<GOAL>Nonempty ((fun x x_1 => x > x_1) ↪r r)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle x (x + y)).sign = (o.oangle x y).sign
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>F' : Type u_4<VAR>inst✝² : EquivLike F' R S<VAR>inst✝¹ : RingEquivClass F' R S<VAR>f : F'<VAR>I : Ideal R<VAR>inst✝ : I.IsPrime<VAR>h : map f I = map (↑↑f) I<GOAL>(map f I).IsPrime
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>F' : Type u_4<VAR>inst✝² : EquivLike F' R S<VAR>inst✝¹ : RingEquivClass F' R S<VAR>f : F'<VAR>I : Ideal R<VAR>inst✝ : I.IsPrime<VAR>h : map f I = map (↑↑f) I<GOAL>(comap (↑f).symm I).IsPrime
<VAR>α : Type u_1<VAR>m n : ZNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>m n : ZNum<GOAL>¬↑n < ↑m ↔ m ≤ n
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>R : Type<VAR>inst✝ : Ring R<VAR>X : Mat_ (SingleObj Rᵐᵒᵖ)<VAR>i✝ j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X)<GOAL>{ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map (𝟙 X) i✝ j✝ = 𝟙 ({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X) i✝ j✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>R : Type<VAR>inst✝ : Ring R<VAR>X : Mat_ (SingleObj Rᵐᵒᵖ)<VAR>i✝ j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X)<GOAL>MulOpposite.unop (if h : i✝ = j✝ then eqToHom ⋯ else 0) = if i✝ = j✝ then 1 else 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>R : Type<VAR>inst✝ : Ring R<VAR>X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>i✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X✝)<VAR>j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj Z✝)<GOAL>{ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map (f ≫ g) i✝ j✝ = ({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map f ≫ { obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.map g) i✝ j✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>R : Type<VAR>inst✝ : Ring R<VAR>X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>i✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj X✝)<VAR>j✝ : ↑({ obj := fun X => FintypeCat.of X.ι, map := fun {X Y} f i j => MulOpposite.unop (f i j) }.obj Z✝)<GOAL>MulOpposite.unop (∑ j : Y✝.ι, f i✝ j ≫ g j j✝) = ∑ j : ↑(FintypeCat.of Y✝.ι), MulOpposite.unop (f i✝ j) * MulOpposite.unop (g j j✝)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : x ∈ p ⊔ p'<GOAL>∃ y ∈ p, ∃ z ∈ p', y + z = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : x ∈ span R (↑p ∪ ↑p')<GOAL>∃ y ∈ p, ∃ z ∈ p', y + z = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : x ∈ span R (↑p ∪ ↑p')<GOAL>∀ x ∈ ↑p ∪ ↑p', ∃ y ∈ p, ∃ z ∈ p', y + z = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : x ∈ span R (↑p ∪ ↑p')<GOAL>∃ y ∈ p, ∃ z ∈ p', y + z = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : x ∈ span R (↑p ∪ ↑p')<GOAL>∀ (x y : M), (∃ y ∈ p, ∃ z ∈ p', y + z = x) → (∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y) → ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = x + y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : x ∈ span R (↑p ∪ ↑p')<GOAL>∀ (a : R) (x : M), (∃ y ∈ p, ∃ z ∈ p', y + z = x) → ∃ y ∈ p, ∃ z ∈ p', y + z = a • x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ p<VAR>z : M<VAR>hz : z ∈ p'<GOAL>y + z ∈ p ⊔ p'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>inst✝ : Nonempty ι<VAR>f : Filter α<VAR>g : ι → Filter β<GOAL>f.prod (⨅ i, g i) = ⨅ i, f.prod (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>inst✝ : Nonempty ι<VAR>f : Filter α<VAR>g : ι → Filter β<GOAL>⨅ x, comap Prod.fst f ⊓ comap Prod.snd (g x) = ⨅ i, f.prod (g i)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>p : ℕ<VAR>φ : MvPolynomial σ R<GOAL>(map f) ((expand p) φ) = (expand p) ((map f) φ)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f ∈ (insert a s).finsuppAntidiag n ↔ ∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s ↔ ∃ a_1 b, a_1 + b = n ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ Grp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : Types.FilteredColimit.Rel (F ⋙ forget Grp) x y<GOAL>colimitInvAux F x = colimitInvAux F y
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ Grp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : Types.FilteredColimit.Rel (F ⋙ forget Grp) x y<GOAL>∃ k f g, (F.map f) ⟨x.fst, x.snd⁻¹⟩.snd = (F.map g) ⟨y.fst, y.snd⁻¹⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ Grp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<VAR>hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd<GOAL>∃ k f g, (F.map f) ⟨x.fst, x.snd⁻¹⟩.snd = (F.map g) ⟨y.fst, y.snd⁻¹⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ Grp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<VAR>hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd<GOAL>(F.map f) ⟨x.fst, x.snd⁻¹⟩.snd = (F.map g) ⟨y.fst, y.snd⁻¹⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ Grp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<VAR>hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd<GOAL>(F.map f) x.snd = (F.map g) y.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, a ≤ b → b = a<GOAL>s.erase a ⊔ Iic a = s
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<GOAL>(graph f).card = n
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<GOAL>Finset.univ.card = n
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<GOAL>Function.Injective fun i => (f i, i)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.10116, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex (Karoubi C) c<VAR>i j k : ι<VAR>x✝¹ : c.Rel i j<VAR>x✝ : c.Rel j k<GOAL>(fun i j => (K.d i j).f) i j ≫ (fun i j => (K.d i j).f) j k = 0
<VAR>θ : ℂ<GOAL>sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π
<VAR>θ : ℂ<GOAL>(∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) ↔ ∃ k, θ = ↑k * ↑π
<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>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : Module.Finite R M'<VAR>ι : Type v<VAR>inst✝ : Fintype ι<GOAL>finrank R (ι →₀ M) = card ι * finrank R M
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>A : C<VAR>inst✝¹ : HasBinaryProduct A A<VAR>inst✝ : IsIso (diag A)<VAR>Z : C<VAR>f g : Z ⟶ A<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>A : C<VAR>inst✝¹ : HasBinaryProduct A A<VAR>inst✝ : IsIso (diag A)<VAR>Z : C<VAR>f g : Z ⟶ A<VAR>this : prod.fst = prod.snd<GOAL>f = g
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>s : Set ↑(X.presheaf.obj (op U))<GOAL>IsClosed (X.zeroLocus s)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>s : Set ↑(X.presheaf.obj (op U))<GOAL>∀ i ∈ s, IsClosed (↑(X.basicOpen i))ᶜ
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>s : Set ↑(X.presheaf.obj (op U))<VAR>i : ↑(X.presheaf.obj (op U))<VAR>a✝ : i ∈ s<GOAL>IsClosed (↑(X.basicOpen i))ᶜ
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>s : Set ↑(X.presheaf.obj (op U))<VAR>i : ↑(X.presheaf.obj (op U))<VAR>a✝ : i ∈ s<GOAL>IsOpen ↑(X.basicOpen i)
<VAR>a b c d✝ m n : ℤ<VAR>hcb : c ∣ b<VAR>h : a ∣ b / c<VAR>d : ℤ<VAR>hd : b / c = a * d<GOAL>b = c * a * d
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>1 < star x ↔ 1 < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<GOAL>(M.map f hf)✶ = M✶.map f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<GOAL>∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.Base B ↔ (M✶.map f hf).Base B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<GOAL>∀ a ⊆ M.E, ((M.map f hf).Base (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).Base (f '' a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : B ⊆ M.E<GOAL>((M.map f hf).Base (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).Base (f '' B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : B ⊆ M.E<GOAL>M.Base (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>h : G.Adj u v<VAR>x✝ : V<GOAL>x✝ ∈ (G.subgraphOfAdj h).support ↔ x✝ ∈ {u, v}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>h : G.Adj u v<VAR>x✝ : V<GOAL>(∃ w, (G.subgraphOfAdj h).Adj x✝ w) ↔ x✝ ∈ {u, v}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>h : G.Adj u v<VAR>x✝ : V<GOAL>(∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) ↔ x✝ ∈ {u, v}