ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<VAR>hkl : (p.toLin.flip (coroot l)) (root k) = 2<VAR>_i : NoZeroSMulDivisors ℤ M<VAR>this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.toLin.flip ∘ ⇑coroot))<GOAL>MapsTo (⇑(preReflection (root k) ((⇑p.toLin.flip ∘ ⇑coroot) l))) (range ⇑root) (range ⇑root)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<VAR>hkl : (p.toLin.flip (coroot l)) (root k) = 2<VAR>_i : NoZeroSMulDivisors ℤ M<VAR>this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.toLin.flip ∘ ⇑coroot))<GOAL>MapsTo (⇑(sα ∘ₗ sβ ∘ₗ sα)) (range ⇑root) (range ⇑root)
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddCommGroup β<VAR>f g : α → β<VAR>hf : IsAddGroupHom f<VAR>hg : IsAddGroupHom g<GOAL>IsAddGroupHom fun a => f a - g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (a : α), f a ≠ ⊤<GOAL>(∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal
<VAR>α : Type<VAR>n : ℕ<VAR>xs : Vector α n<VAR>β σ₁ γ σ₂ : Type<VAR>ys : Vector β n<VAR>f₁ : α → β → σ₁ → σ₁ × γ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>R : σ₁ → σ₂ → Prop<VAR>h₀ : R s₁ s₂<VAR>hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2<GOAL>(mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
<VAR>C✝ : Type u<VAR>inst✝³ : Category.{v, u} C✝<VAR>D✝ : Type u'<VAR>inst✝² : Category.{v', u'} D✝<VAR>J : Type w<VAR>C : J → Type u<VAR>D : J → Type u'<VAR>inst✝¹ : (j : J) → Category.{v, u} (C j)<VAR>inst✝ : (j : J) → Category.{v', u'} (D j)<VAR>W : (j : J) → MorphismProperty (C j)<VAR>F : (j : J) → C j ⥤ D j<VAR>hF : ∀ (j : J), (W j).IsInvertedBy (F j)<VAR>X✝ Y✝ : (j : J) → C j<VAR>f : X✝ ⟶ Y✝<VAR>hf : MorphismProperty.pi W f<GOAL>IsIso ((Functor.pi F).map f)
<VAR>C✝ : Type u<VAR>inst✝³ : Category.{v, u} C✝<VAR>D✝ : Type u'<VAR>inst✝² : Category.{v', u'} D✝<VAR>J : Type w<VAR>C : J → Type u<VAR>D : J → Type u'<VAR>inst✝¹ : (j : J) → Category.{v, u} (C j)<VAR>inst✝ : (j : J) → Category.{v', u'} (D j)<VAR>W : (j : J) → MorphismProperty (C j)<VAR>F : (j : J) → C j ⥤ D j<VAR>hF : ∀ (j : J), (W j).IsInvertedBy (F j)<VAR>X✝ Y✝ : (j : J) → C j<VAR>f : X✝ ⟶ Y✝<VAR>hf : MorphismProperty.pi W f<GOAL>∀ (i : J), IsIso ((Functor.pi F).map f i)
<VAR>u : XgcdType<VAR>wp x y zp ap bp : ℕ<GOAL>{ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp + { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp + { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp * { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp = { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x * { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y ↔ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w * { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z = ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x * { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat
<VAR>u : XgcdType<VAR>wp x y zp ap bp : ℕ<VAR>h : wp + zp + wp * zp = x * y<GOAL>(wp + 1) * (zp + 1) = x * y + 1
<VAR>u : XgcdType<VAR>wp x y zp ap bp : ℕ<VAR>h : (wp + 1) * (zp + 1) = x * y + 1<GOAL>wp + zp + wp * zp = x * y
<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>s : Finset α<VAR>e : α ↪ γ<VAR>f : γ → β<GOAL>∏ x ∈ map e s, f x = ∏ x ∈ s, f (e x)
<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>s : Finset α<VAR>e : α ↪ γ<VAR>f : γ → β<GOAL>(Multiset.map ((fun x => f x) ∘ ⇑e) s.val).prod = ∏ x ∈ s, f (e x)
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hu : m = 0<GOAL>m + n = n
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hu : m = 0<GOAL>append u v = v ∘ cast ⋯
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hu : m = 0<VAR>l : Fin m<GOAL>append u v (castAdd n l) = (v ∘ cast ⋯) (castAdd n l)
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hu : m = 0<VAR>r : Fin n<GOAL>append u v (natAdd m r) = (v ∘ cast ⋯) (natAdd m r)
<VAR>C : Type ?u.31337<VAR>inst✝⁵ : Category.{?u.31341, ?u.31337} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>S₁.f ≫ φ.τ₂ = 0
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<VAR>H : RightHomologyMapData φ (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ (CokernelCofork.ofπ S₁.pOpcycles ⋯) S₁.opcyclesIsCokernel) (RightHomologyData.ofZeros S₂ hf₂ hg₂) := { φQ := S₁.descOpcycles φ.τ₂ ⋯, φH := S₁.descOpcycles φ.τ₂ ⋯, commp := ⋯, commg' := ⋯, commι := ⋯ }<GOAL>QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>s.einfsep ≠ ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>X Y : Set α<VAR>hX : X ⊆ S<VAR>hY : Y ⊆ S<GOAL>sSup X ≤ sSup Y ↔ X ⊆ Y
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>X Y : Set α<VAR>hX : X ⊆ S<VAR>hY : Y ⊆ S<GOAL>sSup X ≤ sSup Y → X ⊆ Y
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>X Y : Set α<VAR>hX : X ⊆ S<VAR>hY : Y ⊆ S<VAR>h : sSup X ≤ sSup Y<VAR>a : α<VAR>ha : a ∈ X<GOAL>a ∈ Y
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>X Y : Set α<VAR>hX : X ⊆ S<VAR>hY : Y ⊆ S<VAR>h : sSup X ≤ sSup Y<VAR>a : α<VAR>ha : a ∈ X<GOAL>IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SupSet α<VAR>inst✝ : Inhabited ↑s<VAR>t : Set ↑s<VAR>h' : t.Nonempty<VAR>h'' : BddAbove t<VAR>h : sSup (Subtype.val '' t) ∈ s<GOAL>sSup (Subtype.val '' t) = ↑(sSup t)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s * t).IsPWO
<VAR>α : Type u_1<VAR>s t : Set α<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>((fun x => x.1 * x.2) '' s ×ˢ t).IsPWO
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>x : Localization I.primeCompl<GOAL>IsNilpotent x ↔ x ∈ nonunits (Localization I.primeCompl)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>h : R ≃+* P<GOAL>IsLocalization (nonZeroDivisors R) S ↔ IsLocalization (nonZeroDivisors P) S
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>h : R ≃+* P<GOAL>nonZeroDivisors P = Submonoid.map h.toMonoidHom (nonZeroDivisors R)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>h : R ≃+* P<VAR>x : P<GOAL>x ∈ nonZeroDivisors P ↔ x ∈ Submonoid.map h.toMonoidHom (nonZeroDivisors R)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>h : R ≃+* P<VAR>x : P<GOAL>x ∈ nonZeroDivisors P ↔ x ∈ Submonoid.comap h.toMulEquiv.symm.toMonoidHom (nonZeroDivisors R)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>h : R ≃+* P<VAR>x : P<GOAL>x ∈ nonZeroDivisors P ↔ (↑h).symm x ∈ nonZeroDivisors R
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>n : α →₀ ℕ<VAR>f : (α →₀ ℕ) → (α →₀ ℕ) → M<GOAL>∀ (i : (α →₀ ℕ) × (α →₀ ℕ)), i ∈ antidiagonal n ↔ (Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i ∈ antidiagonal n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeInf γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>IsLUB (Ico a b) b
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.29822<VAR>α : ι → Type u_1<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<GOAL>∅ ∈ measurableCylinders α
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.29822<VAR>α : ι → Type u_1<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<GOAL>∃ i i_1, ∃ (_ : MeasurableSet i_1), ∅ = cylinder i i_1
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<GOAL>evalEval (C X) Y (baseChange W R[X][Y]).toAffine.polynomial = W.polynomial
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : α → R<GOAL>(Finsupp.total α M R v) ((linearEquivFunOnFinite R R α).symm x) = ((Fintype.total R S) v) x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : α → R<GOAL>((linearEquivFunOnFinite R R α).symm x).support ⊆ Finset.univ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : α → R<GOAL>∀ x_1 ∈ Finset.univ, x_1 ∉ ((linearEquivFunOnFinite R R α).symm x).support → (fun i => ⇑((fun i => LinearMap.id.smulRight (v i)) i)) x_1 (((linearEquivFunOnFinite R R α).symm x) x_1) = 0
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<VAR>s : Stream'.Seq (Pair K)<VAR>gcf_v_eq : of ↑q = { h := ↑⌊↑q⌋, s := s }<GOAL>{ h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := ↑⌊↑q⌋, s := s }
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β✝ : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝¹ : UniformSpace β✝<VAR>β : Type u_4<VAR>inst✝ : UniformSpace β<VAR>f : β → (i : ι) → α i<GOAL>UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i
<VAR>x✝ y✝ z x y : ℝ<VAR>hx_nonneg : 0 ≤ x<GOAL>|x ^ y| = |x| ^ y
<VAR>x✝ y✝ z x y : ℝ<VAR>hx_nonneg : 0 ≤ x<VAR>h_rpow_nonneg : 0 ≤ x ^ y<GOAL>|x ^ y| = |x| ^ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>hg : Monotone g<GOAL>⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<GOAL>descSet hc Set.univ = Set.univ
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α✝<VAR>γ : Type w<VAR>inst✝¹ : MetricSpace γ<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε<GOAL>SecondCountableTopology α
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α✝<VAR>γ : Type w<VAR>inst✝¹ : MetricSpace γ<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α✝<VAR>γ : Type w<VAR>inst✝¹ : MetricSpace γ<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u_3<VAR>fβ : Encodable β<VAR>F : α → β<VAR>hF : ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>Finv : ↑(range F) → α := rangeSplitting F<GOAL>∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α✝<VAR>γ : Type w<VAR>inst✝¹ : MetricSpace γ<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u_3<VAR>fβ : Encodable β<VAR>F : α → β<VAR>hF : ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>Finv : ↑(range F) → α := rangeSplitting F<VAR>x : α<GOAL>∃ y ∈ range Finv, dist x y ≤ ε
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α✝<VAR>γ : Type w<VAR>inst✝¹ : MetricSpace γ<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u_3<VAR>fβ : Encodable β<VAR>F : α → β<VAR>hF : ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>Finv : ↑(range F) → α := rangeSplitting F<VAR>x : α<VAR>x' : α := Finv ⟨F x, ⋯⟩<GOAL>∃ y ∈ range Finv, dist x y ≤ ε
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α✝<VAR>γ : Type w<VAR>inst✝¹ : MetricSpace γ<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u_3<VAR>fβ : Encodable β<VAR>F : α → β<VAR>hF : ∀ (x y : α), F x = F y → dist x y ≤ ε<VAR>Finv : ↑(range F) → α := rangeSplitting F<VAR>x : α<VAR>x' : α := Finv ⟨F x, ⋯⟩<VAR>this : F x' = F x<GOAL>∃ y ∈ range Finv, dist x y ≤ ε
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>r : R<GOAL>‖inl r‖₊ = ‖r‖₊
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>S : Set G<VAR>hS : S ∈ 𝓝 1<GOAL>S⁻¹ ∈ 𝓝 1
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c : α<VAR>h : IsUnit b<VAR>a : α<GOAL>b / (a * b) = a⁻¹
<VAR>R : Type u_1<VAR>inst✝¹⁵ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v : ι → M<VAR>v' : ι → M'<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>m : M<GOAL>update (update v i m) j m i = update (update v i m) j m j
<VAR>s : Finset ℕ<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>hp : m.primeFactors ⊆ s<GOAL>m ∈ factoredNumbers s
<VAR>s : Finset ℕ<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>hp : m.primeFactors ⊆ s<GOAL>m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>hnm : n ≤ m<GOAL>(∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>hnm : n ≤ m<GOAL>(∀ i ∈ Ico n n, r i (succ i)) → ReflTransGen r n n
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>hnm : n ≤ m<GOAL>∀ (n_1 : α), n ≤ n_1 → ((∀ i ∈ Ico n n_1, r i (succ i)) → ReflTransGen r n n_1) → (∀ i ∈ Ico n (succ n_1), r i (succ i)) → ReflTransGen r n (succ n_1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>h : s.Countable<VAR>inhabited_h : Inhabited α<GOAL>∃ f, s ⊆ range f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → DecidableEq (α i)<VAR>inst✝¹ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>f : Π₀ (i : ι), α i<GOAL>(Iic f).card = ∏ i ∈ f.support, (Iic (f i)).card
<VAR>R✝ : Type u<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>inst✝² : StarMul R<VAR>r : R<VAR>inst✝¹ : Invertible r<VAR>inst✝ : Invertible (star r)<GOAL>star ⅟r = ⅟(star r)
<VAR>R✝ : Type u<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>inst✝² : StarMul R<VAR>r : R<VAR>inst✝¹ : Invertible r<VAR>inst✝ : Invertible (star r)<VAR>this : star ⅟r = star ⅟r * (star r * ⅟(star r))<GOAL>star ⅟r = ⅟(star r)
<VAR>R✝ : Type u<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>inst✝² : StarMul R<VAR>r : R<VAR>inst✝¹ : Invertible r<VAR>inst✝ : Invertible (star r)<VAR>this : star ⅟r = star ⅟r * (star r * ⅟(star r))<GOAL>star ⅟r * star r * ⅟(star r) = ⅟(star r)
<VAR>R✝ : Type u<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>inst✝² : StarMul R<VAR>r : R<VAR>inst✝¹ : Invertible r<VAR>inst✝ : Invertible (star r)<VAR>this✝ : star ⅟r = star ⅟r * (star r * ⅟(star r))<VAR>this : star ⅟r * star r = star 1<GOAL>star ⅟r * star r * ⅟(star r) = ⅟(star r)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>i j : n<VAR>i_ne_j : i ≠ j<VAR>hij : ∀ (k : n), M k i = M k j<GOAL>M.det = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>i j : n<VAR>i_ne_j : i ≠ j<VAR>hij : ∀ (k : n), M k i = M k j<GOAL>Mᵀ i = Mᵀ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u_4<VAR>f : ι → Ordinal.{max u_5 u_4}<VAR>a : Ordinal.{max u_4 u_5}<VAR>ha : a < mex f<GOAL>∃ i, f i = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u_4<VAR>f : ι → Ordinal.{max u_5 u_4}<VAR>a : Ordinal.{max u_4 u_5}<VAR>ha : a < mex f<VAR>ha' : ∀ (i : ι), f i ≠ a<GOAL>False
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<VAR>i : Fin (minpoly K x).natDegree<GOAL>(powerBasisAux hx) i = AdjoinSimple.gen K x ^ ↑i