ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>this : Nontrivial K<GOAL>Module.rank K V = 1 ↔ ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>this : Nontrivial K<VAR>h : Module.rank K V = 1<GOAL>∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>this : Nontrivial K<VAR>x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v<VAR>v₀ : V<VAR>h : v₀ ≠ 0<VAR>hv : ∀ (v : V), ∃ r, r • v₀ = v<GOAL>1 ≤ Module.rank K V
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>I : ProjectiveSpectrum 𝒜<GOAL>I ∈ (zeroLocus 𝒜 {f})ᶜ ↔ f ∉ I.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>I : ProjectiveSpectrum 𝒜<GOAL>f ∉ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<GOAL>(opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<GOAL>((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop = (hc.coconePointUniqueUpToIso hc').op.inv.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<GOAL>∀ (j : Discrete α), c'.ι.app j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop = c'.ι.app j ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<VAR>j : α<GOAL>c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop = c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<VAR>j : α<GOAL>c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop = c.ι.app { as := j }
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<VAR>j : α<GOAL>(c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op = (c.ι.app { as := j }).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<VAR>j : α<GOAL>(opCoproductIsoProduct' hc hf).hom ≫ f.proj j = (c.ι.app { as := j }).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hc' : IsColimit c'<VAR>hf : IsLimit f<VAR>j : α<GOAL>(opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op = (c.ι.app { as := j }).op
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(if hf : const (padicNorm p) 1 ≈ 0 then 0 else padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : ¬const (padicNorm p) 1 ≈ 0<GOAL>(if hf : const (padicNorm p) 1 ≈ 0 then 0 else padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : ¬const (padicNorm p) 1 ≈ 0<GOAL>padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint h)) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>H0 : C ∅<VAR>H1 : ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → C s → C (insert a s)<VAR>s : Finset α<GOAL>C ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>H0 : C ∅<VAR>H1 : ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → C s → C (insert a s)<GOAL>C ↑∅
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>H0 : C ∅<VAR>H1 : ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → C s → C (insert a s)<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hs : C ↑s<GOAL>C ↑(Finset.cons a s ha)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<GOAL>multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hyx : y ≤ x<GOAL>multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hyx : x ≤ y<GOAL>multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : DivisionSemiring R<VAR>inst✝ : StarRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>n : ℤ<GOAL>IsSelfAdjoint (x ^ n)
<VAR>f : CauSeq ℂ ⇑abs'<GOAL>(cauSeqConj f).lim.re = ((starRingEnd ℂ) f.lim).re
<VAR>f : CauSeq ℂ ⇑abs'<GOAL>(cauSeqConj f).lim.im = ((starRingEnd ℂ) f.lim).im
<VAR>f : CauSeq ℂ ⇑abs'<GOAL>CauSeq.lim ⟨fun n => -(↑f n).im, ⋯⟩ = (-⟨fun n => (↑f n).im, ⋯⟩).lim
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>(∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ (x : α), ¬∃ b, x ∈ s ∧ b ∈ s ∧ x ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f g : α →ₘ[μ] β<GOAL>f ⊓ g ≤ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f g : α →ₘ[μ] β<GOAL>↑(f ⊓ g) ≤ᶠ[ae μ] ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f g : α →ₘ[μ] β<VAR>a✝ : α<VAR>ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝<GOAL>↑(f ⊓ g) a✝ ≤ ↑g a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f g : α →ₘ[μ] β<VAR>a✝ : α<VAR>ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝<GOAL>↑f a✝ ⊓ ↑g a✝ ≤ ↑g a✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I J : Ideal R<GOAL>RingHom.ker (quotLeftToQuotSup I J) = map (Ideal.Quotient.mk I) J
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.123075, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>opcyclesMap e.hom ≫ opcyclesMap e.inv = 𝟙 S₁.opcycles
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.123075, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>opcyclesMap e.inv ≫ opcyclesMap e.hom = 𝟙 S₂.opcycles
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<VAR>h : Inducing f<GOAL>Inducing (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<VAR>h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))<GOAL>∀ (x : ↑(f ⁻¹' s)), 𝓝 x = comap Subtype.val (comap f (𝓝 (f ↑x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<VAR>h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))<VAR>a : ↑(f ⁻¹' s)<GOAL>𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<GOAL>Setoid.r s t ↔ h.finpartition.part s = h.finpartition.part t
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<GOAL>t ∈ (Finpartition.ofSetoid h.setoid).part s ↔ h.finpartition.part s = h.finpartition.part t
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<GOAL>t ∈ fp.part s ↔ fp.part s = fp.part t
<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>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<GOAL>map f ↑n = ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>s : Set R<VAR>x : R<GOAL>x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<GOAL>x ∈ closure s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<VAR>H : NonUnitalSubsemiring R<VAR>J : H ∈ {S | s ⊆ ↑S}<GOAL>x ∈ (fun h => ↑H) J
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<VAR>H : NonUnitalSubsemiring R<VAR>J : H ∈ {S | s ⊆ ↑S}<VAR>y : R<VAR>hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))<GOAL>y ∈ ↑H.toAddSubmonoid
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<VAR>H : NonUnitalSubsemiring R<VAR>J : H ∈ {S | s ⊆ ↑S}<VAR>y : R<VAR>hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))<VAR>z : R<VAR>hz : z ∈ ↑(AddSubmonoid.closure s)<GOAL>z ∈ ↑H.toSubsemigroup
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), -f x) = -∯ (x : Fin n → ℂ) in T(c, R), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : M ≃+ N<VAR>x : α →₀ M<GOAL>mapRange ⇑f.symm ⋯ (mapRange ⇑f ⋯ x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : M ≃+ N<VAR>x : α →₀ M<GOAL>mapRange id ⋯ x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : M ≃+ N<VAR>x : α →₀ M<GOAL>id 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : M ≃+ N<VAR>x : α →₀ N<GOAL>mapRange ⇑f ⋯ (mapRange ⇑f.symm ⋯ x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : M ≃+ N<VAR>x : α →₀ N<GOAL>mapRange id ⋯ x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : M ≃+ N<VAR>x : α →₀ N<GOAL>id 0 = 0
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.mulOption y i j⟧ < ⟦x * y⟧ ↔ P3 (x.moveLeft i) x (y.moveLeft j) y
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft j⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ < ⟦x * y⟧ ↔ P3 (x.moveLeft i) x (y.moveLeft j) y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>0 < P.pairing i j ↔ 0 < P.pairing j i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x : M<VAR>S : Type u_10<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M'<VAR>inst✝ : SMulCommClass R S M'<VAR>f : ι → M'<VAR>i : ι<GOAL>((b.constr S) f) (b i) = f i
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H : Subgroup G<VAR>K : Subgroup N<GOAL>H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ t : Set α<VAR>p : α → Prop<VAR>ht : ∀ᵐ (x : α) ∂μ.restrict t, p x<VAR>htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x<GOAL>(μ.restrict t) {x | ¬p x} + (μ.restrict tᶜ) {x | ¬p x} = 0
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x : ℝ<VAR>h : x ∈ Ioo (I.lower i) (I.upper i)<VAR>h' : optParam (∀ (j : ι), I.lower j < update I.upper i x j) ⋯<GOAL>I.splitLower i x = ↑{ lower := I.lower, upper := update I.upper i x, lower_lt_upper := h' }
<VAR>n : Type u_1<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>Q : QuadraticForm ℝ (n → ℝ)<VAR>hQ : PosDef Q<GOAL>(toMatrix' Q).PosDef
<VAR>n : Type u_1<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>Q : QuadraticForm ℝ (n → ℝ)<VAR>hQ : (LinearMap.BilinMap.toQuadraticMap ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((associatedHom ℝ) Q)))).PosDef<GOAL>(toMatrix' Q).PosDef
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasBinaryCoproducts C<VAR>inst✝ : HasInitial C<VAR>P : C<GOAL>desc (initial.to P) (𝟙 P) ≫ inr = 𝟙 ((⊥_ C) ⨿ P)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : ModuleCat R<VAR>f : Y ⟶ Z<GOAL>X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : ModuleCat R<VAR>f : Y ⟶ Z<GOAL>(𝟙 X ⊗ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>J : Type w<VAR>inst✝² : Category.{r, w} J<VAR>F : J ⥤ C<VAR>inst✝¹ : PreservesColimit F (forget C)<VAR>inst✝ : IsFiltered J<VAR>D : Cocone F<VAR>i j : J<VAR>hD : IsColimit D<VAR>x : (forget C).obj (F.obj i)<VAR>y : (forget C).obj (F.obj j)<VAR>h : (D.ι.app i) x = (D.ι.app j) y<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>hE : IsColimit E := isColimitOfPreserves (forget C) hD<GOAL>∃ k f g, (F.map f) x = (F.map g) y
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f✝ : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>h : ContDiff ℝ 1 f<GOAL>dimH (range f) = dimH (f '' univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>h1 : μ₁ ≪ ν<VAR>h2 : μ₂ ≪ ν'<VAR>s : Set α<VAR>hs : (ν + ν') s = 0<GOAL>(μ₁ + μ₂) s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>h1 : μ₁ ≪ ν<VAR>h2 : μ₂ ≪ ν'<VAR>s : Set α<VAR>hs : ν s = 0 ∧ ν' s = 0<GOAL>μ₁ s = 0 ∧ μ₂ s = 0
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>ContDiff 𝕜 (↑(n + 1)) f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ↑n fun y => fderiv 𝕜 f y
<VAR>n : ℕ<GOAL>(n + 1)‼ ≤ (n + 1)!
<VAR>n : ℕ<GOAL>(n + 1)‼ ≤ (n + 1)‼ * n‼
<VAR>a b✝ c d m n : ℤ<VAR>ha : a ≠ 0<VAR>b : ℤ<VAR>hb : a * n = a * m * b<GOAL>m ∣ n
<VAR>a b✝ c d m n : ℤ<VAR>ha : a ≠ 0<VAR>b : ℤ<VAR>hb : n = m * b<GOAL>m ∣ n
<VAR>n : ℕ<VAR>hn : Odd n<VAR>u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯<VAR>hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0<VAR>i j : ZMod n<VAR>h : Commute (r i, sr j).1 (r i, sr j).2<GOAL>(fun x => match x with | Sum.inl i => ⟨(sr i, r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩) ((fun x => match x with | ⟨(sr i, r a), property⟩ => Sum.inl i | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))) ⟨(r i, sr j), h⟩) = ⟨(r i, sr j), h⟩
<VAR>n : ℕ<VAR>hn : Odd n<VAR>u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯<VAR>hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0<VAR>i j : ZMod n<VAR>h : Commute (sr i, r j).1 (sr i, r j).2<GOAL>(fun x => match x with | Sum.inl i => ⟨(sr i, r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩) ((fun x => match x with | ⟨(sr i, r a), property⟩ => Sum.inl i | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))) ⟨(sr i, r j), h⟩) = ⟨(sr i, r j), h⟩
<VAR>n : ℕ<VAR>hn : Odd n<VAR>u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯<VAR>hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0<VAR>i j : ZMod n<VAR>h✝ : Commute (sr i, sr j).1 (sr i, sr j).2<VAR>h : j - i = i - j<GOAL>(fun x => match x with | Sum.inl i => ⟨(sr i, r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩) ((fun x => match x with | ⟨(sr i, r a), property⟩ => Sum.inl i | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))) ⟨(sr i, sr j), h✝⟩) = ⟨(sr i, sr j), h✝⟩
<VAR>n : ℕ<VAR>hn : Odd n<VAR>u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯<VAR>hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0<VAR>i j : ZMod n<VAR>h✝ : Commute (sr i, sr j).1 (sr i, sr j).2<VAR>h : i = j<GOAL>(fun x => match x with | Sum.inl i => ⟨(sr i, r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩) ((fun x => match x with | ⟨(sr i, r a), property⟩ => Sum.inl i | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))) ⟨(sr i, sr j), h✝⟩) = ⟨(sr i, sr j), h✝⟩