ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>IsClosed (diagonal (Quotient R))
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>IsClosed (Prod.map π π ⁻¹' diagonal (Quotient R))
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>Prod.map π π ⁻¹' diagonal (Quotient R) = range fun gx => (gx.1 • gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>Type ?u.23430
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>TopologicalSpace ?convert_1
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>Group ?convert_1
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>MulAction ?convert_1 X
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<VAR>this : QuotientMap (Prod.map π π)<GOAL>ProperSMul ?convert_1 X
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<VAR>f : ι → M<GOAL>(Matrix.det fun i j => ((e.unitsSMul w).repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => (e.repr (f j)) i
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<VAR>f : ι → M<GOAL>(Matrix.det fun i j => (w i)⁻¹ • (e.repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => (e.repr (f j)) i
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<VAR>f : ι → M<GOAL>↑(∏ i : ι, w i)⁻¹ = ∏ i : ι, ↑(w i)⁻¹
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<VAR>f : ι → M<GOAL>↑(∏ x : ι, (w x)⁻¹) = ∏ i : ι, ↑(w i)⁻¹
<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<GOAL>LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.total ι M R v) l = 0 → l = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<VAR>h2 : a < b<GOAL>a - c < b - c
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<VAR>h2 : a < b<GOAL>c + (a - c) < b
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty<VAR>E : Set α<GOAL>cthickening δ E = ⋂ ε ∈ s, cthickening ε E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty<VAR>E : Set α<GOAL>cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty<VAR>E : Set α<GOAL>⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s : β → α<GOAL>R (m (⨆ b, s b)) (∏' (b : β), m (s b))
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s : β → α<VAR>val✝ : Encodable β<GOAL>R (m (⨆ b, s b)) (∏' (b : β), m (s b))
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s : β → α<VAR>val✝ : Encodable β<GOAL>R (m (⨆ i, ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))
<VAR>a b : UnitAddCircle<VAR>z : ℂ<GOAL>DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) z
<VAR>a b : UnitAddCircle<VAR>z : ℂ<VAR>hz : z ≠ 1<GOAL>DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) z
<VAR>a b : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - hurwitzZetaEven b s) 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>h₃ : S₃.LeftHomologyData<VAR>γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂<VAR>γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃<GOAL>leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝⁶ : Category.{u_4, u_3} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroObject C<VAR>K L M : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>e : c.Embedding c'<VAR>inst✝³ : e.IsTruncGE<VAR>inst✝² : ∀ (i' : ι'), K.HasHomology i'<VAR>inst✝¹ : ∀ (i' : ι'), L.HasHomology i'<VAR>inst✝ : ∀ (i' : ι'), M.HasHomology i'<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>i' j' : ι'<VAR>hi' : e.f i = i'<VAR>hj' : e.f j = j'<VAR>hi : ¬e.BoundaryGE i<GOAL>(if hij : c.Rel i j then if hi : e.BoundaryGE i then (truncGE'.XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv else (truncGE'.XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv else 0) = (K.truncGE'XIso e hi' hi).hom ≫ K.d i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝⁶ : Category.{u_4, u_3} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroObject C<VAR>K L M : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>e : c.Embedding c'<VAR>inst✝³ : e.IsTruncGE<VAR>inst✝² : ∀ (i' : ι'), K.HasHomology i'<VAR>inst✝¹ : ∀ (i' : ι'), L.HasHomology i'<VAR>inst✝ : ∀ (i' : ι'), M.HasHomology i'<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>i' j' : ι'<VAR>hi' : e.f i = i'<VAR>hj' : e.f j = j'<VAR>hi : ¬e.BoundaryGE i<GOAL>(truncGE'.XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv = (K.truncGE'XIso e hi' hi).hom ≫ K.d i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>LinearIndependent Rₛ (⇑f ∘ v)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<GOAL>∀ (s : Finset ι) (g : ι → Rₛ), ∑ i ∈ s, g i • (⇑f ∘ v) i = 0 → ∀ i ∈ s, g i = 0
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>t : Finset ι<VAR>g : ι → Rₛ<VAR>hg : ∑ i ∈ t, g i • (⇑f ∘ v) i = 0<VAR>i : ι<VAR>hi : i ∈ t<GOAL>g i = 0
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>t : Finset ι<VAR>g : ι → Rₛ<VAR>hg : ∑ i ∈ t, g i • (⇑f ∘ v) i = 0<VAR>i : ι<VAR>hi : i ∈ t<VAR>a : ↥S<VAR>g' : ι → R<VAR>hg' : ∀ i ∈ t, (algebraMap R Rₛ) (g' i) = ↑a • g i<GOAL>g i = 0
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>t : Finset ι<VAR>g : ι → Rₛ<VAR>hg : ∑ i ∈ t, g i • (⇑f ∘ v) i = 0<VAR>i : ι<VAR>hi : i ∈ t<VAR>a : ↥S<VAR>g' : ι → R<VAR>hg' : ∀ i ∈ t, (algebraMap R Rₛ) (g' i) = ↑a • g i<VAR>h0 : f (∑ i ∈ t, g' i • v i) = 0<GOAL>g i = 0
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>t : Finset ι<VAR>g : ι → Rₛ<VAR>hg : ∑ i ∈ t, g i • (⇑f ∘ v) i = 0<VAR>i : ι<VAR>hi : i ∈ t<VAR>a : ↥S<VAR>g' : ι → R<VAR>hg' : ∀ i ∈ t, (algebraMap R Rₛ) (g' i) = ↑a • g i<VAR>h0 : f (∑ i ∈ t, g' i • v i) = 0<VAR>s : ↥S<VAR>hs : s • ∑ i ∈ t, g' i • v i = 0<GOAL>g i = 0
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>t : Finset ι<VAR>g : ι → Rₛ<VAR>hg : ∑ i ∈ t, g i • (⇑f ∘ v) i = 0<VAR>i : ι<VAR>hi : i ∈ t<VAR>a : ↥S<VAR>g' : ι → R<VAR>hg' : ∀ i ∈ t, (algebraMap R Rₛ) (g' i) = ↑a • g i<VAR>h0 : f (∑ i ∈ t, g' i • v i) = 0<VAR>s : ↥S<VAR>hs : ∑ x ∈ t, (↑s * g' x) • v x = 0<GOAL>g i = 0
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>t : Finset ι<VAR>g : ι → Rₛ<VAR>hg : ∑ i ∈ t, g i • (⇑f ∘ v) i = 0<VAR>i : ι<VAR>hi : i ∈ t<VAR>a : ↥S<VAR>g' : ι → R<VAR>hg' : ∀ i ∈ t, (algebraMap R Rₛ) (g' i) = ↑a • g i<VAR>h0 : f (∑ i ∈ t, g' i • v i) = 0<VAR>s : ↥S<VAR>hs : ∑ x ∈ t, (↑s * g' x) • v x = 0<VAR>hv : ↑s * g' i = 0<GOAL>g i = 0
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>t : Finset ι<VAR>g : ι → Rₛ<VAR>hg : ∑ i ∈ t, g i • (⇑f ∘ v) i = 0<VAR>i : ι<VAR>hi : i ∈ t<VAR>a : ↥S<VAR>g' : ι → R<VAR>hg' : ∀ i ∈ t, (algebraMap R Rₛ) (g' i) = ↑a • g i<VAR>h0 : f (∑ i ∈ t, g' i • v i) = 0<VAR>s : ↥S<VAR>hs : ∑ x ∈ t, (↑s * g' x) • v x = 0<VAR>hv : ↑s * g' i = 0<GOAL>(algebraMap R Rₛ) (g' i) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace E<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<GOAL>SigmaFinite (μ.trim ?m.540668)
<VAR>R : Type u_1<VAR>inst✝ : Semigroup R<VAR>a b : R<VAR>ab : IsRightRegular (b * a)<VAR>x y : R<VAR>xy : (fun x => x * b) x = (fun x => x * b) y<GOAL>x * (b * a) = y * (b * a)
<VAR>R : Type u_1<VAR>inst✝ : Semigroup R<VAR>a b : R<VAR>ab : IsRightRegular (b * a)<VAR>x y : R<VAR>xy : (fun x => x * b) x = (fun x => x * b) y<GOAL>x * b * a = y * b * a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>t✝ : (i : ι) → Finset (α i)<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>t : Π₀ (i : ι), Finset (α i)<VAR>ht : t.support ⊆ s<GOAL>f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>t✝ : (i : ι) → Finset (α i)<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>t : Π₀ (i : ι), Finset (α i)<VAR>ht : t.support ⊆ s<VAR>i : ι<VAR>h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)<GOAL>f i ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>t✝ : (i : ι) → Finset (α i)<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>t : Π₀ (i : ι), Finset (α i)<VAR>ht : t.support ⊆ s<VAR>i : ι<VAR>h : f i ∈ t i<VAR>hi : i ∈ f.support<VAR>H : t i = 0<GOAL>f i = 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>a : M<VAR>b : CliffordAlgebra Q<GOAL>(contractLeft d) ((ι Q) a * b) = d a • b - (ι Q) a * (contractLeft d) b
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>a : M<VAR>b : CliffordAlgebra Q<GOAL>∀ (m : M) (x fx : CliffordAlgebra Q), ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>n✝ n' m : ℕ<VAR>s✝ : Sym α✝ n✝<VAR>a b : α✝<VAR>α : Type u_3<VAR>n : ℕ<VAR>s : Sym α n<GOAL>↑(map id s) = ↑s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>n : ℕ<VAR>hc : s.card = n + 1<GOAL>finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z : P<VAR>x y : V<GOAL>midpoint R x y = ⅟2 • (x + y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a a✝ : α<GOAL>a✝ ∈ (s.erase a)ᶜ ↔ a✝ ∈ insert a sᶜ
<VAR>a b m n : ℕ+<VAR>cop : m.Coprime n<VAR>am : a ∣ m<VAR>bn : b ∣ n<GOAL>a = m.gcd (b * a)
<VAR>a b m n : ℕ+<VAR>cop : m.Coprime n<VAR>am : a ∣ m<VAR>bn : b ∣ n<GOAL>a = (b * a).gcd m
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ha : a ≠ 0<GOAL>((monomial n) a).natTrailingDegree = n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ha : a ≠ 0<GOAL>(↑n).toNat = n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι₁ : Type u_4<VAR>s₁ : Finset ι₁<VAR>w₁ : ι₁ → ℝ<VAR>v₁ : ι₁ → F<VAR>h₁ : ∑ i ∈ s₁, w₁ i = 0<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w₂ : ι₂ → ℝ<VAR>v₂ : ι₂ → F<VAR>h₂ : ∑ i ∈ s₂, w₂ i = 0<GOAL>⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
<VAR>x y : ℝ<VAR>hp : 0 < y<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (x, y)
<VAR>x y : ℝ<VAR>hp : 0 < y<VAR>hx : x ≠ 0<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (x, y)
<VAR>y : ℝ<VAR>hp : 0 < y<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (0, y)
<VAR>y : ℝ<VAR>hp : 0 < y<VAR>A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (0, y)
<VAR>y : ℝ<VAR>hp : 0 < y<VAR>A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)<VAR>B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (0, y)
<VAR>y : ℝ<VAR>hp : 0 < y<VAR>A : Tendsto (fun p => rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)<VAR>B : Tendsto (fun p => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)<VAR>C : Tendsto (fun p => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (0, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>a : M<VAR>h : m ≤ n<GOAL>a ^ (n - m) * a ^ m = a ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>b + m • p - (toIcoDiv hp a b + m) • p ∈ Set.Ico a (a + p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sFiniteSeq 0 n) s = 0 s