ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<VAR>h : n ≠ 0<GOAL>|a ^ n| = |a| ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<VAR>h : n ≠ 0<GOAL>1 = 1 ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>z : A<GOAL>(algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ofBaseChangeAux A Q) 1 = (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<GOAL>(id n % 2 == 1) = n.bodd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>a : α<VAR>x✝ : List α<GOAL>count a (dedup (Quot.mk Setoid.r x✝)) = if a ∈ Quot.mk Setoid.r x✝ then 1 else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>a : α<VAR>x✝ : List α<GOAL>List.count a x✝.dedup = if a ∈ x✝ then 1 else 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>s : Set F<VAR>hs : MeasurableSet s<GOAL>(∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this : FiniteDimensional 𝕜 E<GOAL>(∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : AEMeasurable (⇑L) μ<GOAL>(∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : AEMeasurable (⇑L) μ<GOAL>(∀ᵐ (y : F) ∂map (⇑L) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : AEMeasurable (⇑L) μ<VAR>c : ℝ≥0∞<VAR>c_pos : 0 < c<VAR>hc : map (⇑L) μ = c • ν<GOAL>(∀ᵐ (y : F) ∂map (⇑L) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : AEMeasurable (⇑L) μ<VAR>c : ℝ≥0∞<VAR>c_pos : 0 < c<VAR>hc : map (⇑L) μ = c • ν<GOAL>(∀ᵐ (y : F) ∂c • ν, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q✝ : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>inst✝ : ∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>w : α<VAR>hp : p w<VAR>hq : q w hp<VAR>H : ∀ (y : α) (hy : p y), q y hy → y = w<GOAL>∃! x, ∃! hx, q x hx
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q✝ : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>inst✝ : ∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>w : α<VAR>hp : p w<VAR>hq : q w hp<VAR>H : ∀ (y : α) (hy : p y), q y hy → y = w<GOAL>∃! x, ∃ hx, q x hx
<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>v v₁ v₂ : α →₀ M<VAR>inst✝ : CommMonoid N<VAR>f : α → β<VAR>s : α →₀ M<VAR>h : β → M → N<VAR>hf : Injective f<GOAL>(mapDomain f s).prod h = s.prod fun a b => h (f a) b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.40895, u_1} C<VAR>inst✝³ : Category.{?u.40899, u_2} D<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X✝ Y✝ : ShortComplex C<VAR>φ : X✝ ⟶ Y✝<GOAL>F.map φ.τ₁ ≫ F.map Y✝.f = F.map X✝.f ≫ F.map φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.40895, u_1} C<VAR>inst✝³ : Category.{?u.40899, u_2} D<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X✝ Y✝ : ShortComplex C<VAR>φ : X✝ ⟶ Y✝<GOAL>F.map φ.τ₂ ≫ F.map Y✝.g = F.map X✝.g ≫ F.map φ.τ₃
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>a : n<VAR>c : R<VAR>M : Matrix n n R<GOAL>(M * transvection i j c) a j = M a j + c * M a i
<VAR>m n✝ n : ℤ<GOAL>Xor' (Even n) (Odd n)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type w<VAR>inst✝ : Fintype ι<VAR>h : Basis ι R M<GOAL>Module.rank R M = ↑(Fintype.card ι)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>inst✝¹¹ : Category.{u_8, u_1} C₁<VAR>inst✝¹⁰ : Category.{u_9, u_2} C₂<VAR>inst✝⁹ : Category.{u_7, u_3} D<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>inst✝⁶ : Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝⁵ : F.Additive<VAR>inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>inst✝³ : DecidableEq J<VAR>inst✝² : TotalComplexShape c₁ c₂ c<VAR>inst✝¹ : K₁.HasMapBifunctor K₂ F c<VAR>inst✝ : L₁.HasMapBifunctor L₂ F c<VAR>j j' : J<VAR>h : ¬c.Rel j' j<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h' : c₁.π c₂ c (i₁, i₂) = j<GOAL>((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h' ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalDesc fun i₁ i₂ x => c₁.ε₁ c₂ c (c₁.prev i₁, i₂) • (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫ (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h' ≫ 0
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>inst✝¹¹ : Category.{u_8, u_1} C₁<VAR>inst✝¹⁰ : Category.{u_9, u_2} C₂<VAR>inst✝⁹ : Category.{u_7, u_3} D<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>inst✝⁶ : Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝⁵ : F.Additive<VAR>inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>inst✝³ : DecidableEq J<VAR>inst✝² : TotalComplexShape c₁ c₂ c<VAR>inst✝¹ : K₁.HasMapBifunctor K₂ F c<VAR>inst✝ : L₁.HasMapBifunctor L₂ F c<VAR>j j' : J<VAR>h : ¬c.Rel j' j<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h' : c₁.π c₂ c (i₁, i₂) = j<GOAL>c₁.ε₁ c₂ c (c₁.prev i₁, i₂) • (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫ (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j' = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>w : σ → M<VAR>hφ : IsWeightedHomogeneous w φ n<VAR>d : σ →₀ ℕ<VAR>hd : (weight w) d ≠ n<GOAL>coeff d φ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>w : σ → M<VAR>hφ : IsWeightedHomogeneous w φ n<VAR>d : σ →₀ ℕ<VAR>hd : (weight w) d ≠ n<VAR>aux : ¬coeff d φ ≠ 0<GOAL>coeff d φ = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>(T • z).re = z.re + 1
<VAR>C : Type u'<VAR>inst✝³ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R : Sheaf J RingCat<VAR>inst✝² : HasWeakSheafify J AddCommGrp<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>I : Type u<VAR>s : I → M.sections<VAR>p : M ⟶ N<VAR>x✝ : I<VAR>X✝ : Cᵒᵖ<GOAL>↑(N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) x✝) X✝ = ↑(N.freeHomEquiv (N.freeHomEquiv.symm fun i => sectionsMap p (s i)) x✝) X✝
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d + c * x) = c⁻¹ • ∫ (x : ℝ) in d + c * a..d + c * b, f x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜 : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (filter (fun x => a ∉ x) 𝒜) → p (filter (fun x => a ∈ x) 𝒜) → p 𝒜<GOAL>p 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ : α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜✝ : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (filter (fun x => a ∉ x) 𝒜) → p (filter (fun x => a ∈ x) 𝒜) → p 𝒜<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜₀ : p (nonMemberSubfamily a 𝒜)<VAR>h𝒜₁ : p (memberSubfamily a 𝒜)<GOAL>p (filter (fun x => a ∈ x) 𝒜)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ : α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜✝ : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (filter (fun x => a ∉ x) 𝒜) → p (filter (fun x => a ∈ x) 𝒜) → p 𝒜<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜₀ : p (nonMemberSubfamily a 𝒜)<VAR>h𝒜₁ : p (memberSubfamily a 𝒜)<GOAL>p (image (insert a) (memberSubfamily a 𝒜))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hu : (p * q).IsPrimitive<VAR>hpm : p.natDegree = 0<GOAL>IsUnit p
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hu : (p * q).IsPrimitive<VAR>hpm : p.natDegree = 0<GOAL>IsUnit (p.coeff 0)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hu : (p * q).IsPrimitive<VAR>hpm : p.natDegree = 0<GOAL>C (p.coeff 0) ∣ p * q
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hu : (p * q).IsPrimitive<VAR>hpm : p.natDegree = 0<GOAL>p ∣ p * q
<VAR>α : Sort u_1<VAR>a✝ b : α<VAR>h : a✝ = b<VAR>a : α<GOAL>a✝ = a ↔ b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>hxy : x ≠ y<VAR>hyz : y ≠ z<VAR>hxz : x ≠ z<GOAL>{x, y, z}.einfsep = edist x y ⊓ edist x z ⊓ edist y z
<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>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s (comap f μ)<GOAL>NullMeasurableSet (f '' s) μ
<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>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s (comap f μ)<GOAL>f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)
<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>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s (comap f μ)<GOAL>f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
<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>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s (comap f μ)<GOAL>NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ
<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>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s (comap f μ)<VAR>h : toMeasurable (comap f μ) s =ᶠ[ae (comap f μ)] s<GOAL>f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
<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>inst✝ : DecidableEq E<VAR>s : Set E<GOAL>Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫_𝕜 = if v = w then 1 else 0
<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>inst✝ : DecidableEq E<VAR>s : Set E<GOAL>(∀ (i j : { x // x ∈ s }), ⟪↑i, ↑j⟫_𝕜 = if i = j then 1 else 0) ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫_𝕜 = if v = w then 1 else 0
<VAR>X₁ : Type u₁<VAR>inst✝⁹ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : NormalSpace X<VAR>s✝ : Set X<VAR>hs✝ : IsClosed s✝<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝⁶ : TopologicalSpace Y✝<VAR>inst✝⁵ : TietzeExtension Y✝<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TietzeExtension Z<VAR>ι : C(Y, Z)<VAR>r : C(Z, Y)<VAR>h : r.comp ι = ContinuousMap.id Y<VAR>X✝ : Type u<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : NormalSpace X✝<VAR>s : Set X✝<VAR>hs : IsClosed s<VAR>f : C(↑s, Y)<GOAL>∃ g, ContinuousMap.restrict s g = f
<VAR>X₁ : Type u₁<VAR>inst✝⁹ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : NormalSpace X<VAR>s✝ : Set X<VAR>hs✝ : IsClosed s✝<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝⁶ : TopologicalSpace Y✝<VAR>inst✝⁵ : TietzeExtension Y✝<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TietzeExtension Z<VAR>ι : C(Y, Z)<VAR>r : C(Z, Y)<VAR>h : r.comp ι = ContinuousMap.id Y<VAR>X✝ : Type u<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : NormalSpace X✝<VAR>s : Set X✝<VAR>hs : IsClosed s<VAR>f : C(↑s, Y)<VAR>g : C(X✝, Z)<VAR>hg : ContinuousMap.restrict s g = ι.comp f<GOAL>∃ g, ContinuousMap.restrict s g = f
<VAR>X₁ : Type u₁<VAR>inst✝⁹ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : NormalSpace X<VAR>s✝ : Set X<VAR>hs✝ : IsClosed s✝<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝⁶ : TopologicalSpace Y✝<VAR>inst✝⁵ : TietzeExtension Y✝<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TietzeExtension Z<VAR>ι : C(Y, Z)<VAR>r : C(Z, Y)<VAR>h : r.comp ι = ContinuousMap.id Y<VAR>X✝ : Type u<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : NormalSpace X✝<VAR>s : Set X✝<VAR>hs : IsClosed s<VAR>f : C(↑s, Y)<VAR>g : C(X✝, Z)<VAR>hg : ContinuousMap.restrict s g = ι.comp f<GOAL>ContinuousMap.restrict s (r.comp g) = f
<VAR>X₁ : Type u₁<VAR>inst✝⁹ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : NormalSpace X<VAR>s✝ : Set X<VAR>hs✝ : IsClosed s✝<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝⁶ : TopologicalSpace Y✝<VAR>inst✝⁵ : TietzeExtension Y✝<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TietzeExtension Z<VAR>ι : C(Y, Z)<VAR>r : C(Z, Y)<VAR>h : r.comp ι = ContinuousMap.id Y<VAR>X✝ : Type u<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : NormalSpace X✝<VAR>s : Set X✝<VAR>hs : IsClosed s<VAR>f : C(↑s, Y)<VAR>g : C(X✝, Z)<VAR>hg : ContinuousMap.restrict s g = ι.comp f<VAR>x : ↑s<VAR>this : r.comp (ContinuousMap.restrict s g) = r.comp (ι.comp f)<GOAL>(ContinuousMap.restrict s (r.comp g)) x = f x
<VAR>X₁ : Type u₁<VAR>inst✝⁹ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : NormalSpace X<VAR>s✝ : Set X<VAR>hs✝ : IsClosed s✝<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝⁶ : TopologicalSpace Y✝<VAR>inst✝⁵ : TietzeExtension Y✝<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TietzeExtension Z<VAR>ι : C(Y, Z)<VAR>r : C(Z, Y)<VAR>h : r.comp ι = ContinuousMap.id Y<VAR>X✝ : Type u<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : NormalSpace X✝<VAR>s : Set X✝<VAR>hs : IsClosed s<VAR>f : C(↑s, Y)<VAR>g : C(X✝, Z)<VAR>hg : ContinuousMap.restrict s g = ι.comp f<VAR>x : ↑s<VAR>this : r.comp (ContinuousMap.restrict s g) = f<GOAL>(ContinuousMap.restrict s (r.comp g)) x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>n : ℕ<VAR>hn : n + 1 < xs.length<GOAL>xs.formPerm (xs.get ⟨n, ⋯⟩) = xs.get ⟨n + 1, hn⟩
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>f g : Arrow C<VAR>inst✝⁵ : HasImage f.hom<VAR>inst✝⁴ : HasImage g.hom<VAR>sq : f ⟶ g<VAR>inst✝³ : HasImageMap sq<VAR>h : Arrow C<VAR>inst✝² : HasImage h.hom<VAR>sq' : g ⟶ h<VAR>inst✝¹ : HasImageMap sq'<VAR>inst✝ : HasImageMap (sq ≫ sq')<GOAL>HasImageMap.imageMap (sq ≫ sq') = imageMapComp sq sq'
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>v₃ : Valuation R Γ''₀<VAR>h : v₁.IsEquiv v₂<VAR>r s : R<GOAL>v₁ r = v₁ s ↔ v₂ r = v₂ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>vectorSpan k (p '' s) = Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Submodule.span k (insert (p i -ᵥ p i) ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))) = Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>a * b ∈ ball a r ↔ ‖b‖ < r
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝ : CommSemiring S'<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<GOAL>zariskiTopology = TopologicalSpace.induced (⇑(comap f)) zariskiTopology
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X✝ : C<VAR>p✝¹ : X✝ ⟶ X✝<VAR>idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹<VAR>p✝ : X✝ ⟶ X✝<VAR>idem✝ : p✝ ≫ p✝ = p✝<VAR>h_p : p✝¹ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p✝<GOAL>{ X := X✝, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }
<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>p₁ p₂ : P<VAR>h : ¬Collinear k {p₁, p₂, p₂}<GOAL>False
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V : Set (β × β)<VAR>hV : SymmetricRel V<VAR>x y : β<GOAL>y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}