ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<GOAL>((presheafToSheaf J B).map { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val).val = ((sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val))).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<GOAL>toSheafify J ((const Cᵒᵖ ⋙ (whiskeringRight Cᵒᵖ A B).obj U).obj (F.val.obj (op t))) ≫ ((presheafToSheaf J B).map { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val).val = toSheafify J ((const Cᵒᵖ ⋙ (whiskeringRight Cᵒᵖ A B).obj U).obj (F.val.obj (op t))) ≫ ((sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val))).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<GOAL>toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)) ⋙ U) ≫ ((presheafToSheaf J B).map { app := fun Y => U.map (F.val.map (ht.from (unop Y)).op), naturality := ⋯ }).val ≫ ((sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val).val = toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)) ⋙ U) ≫ ((sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t)))).val ≫ whiskerRight ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)).val U
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<GOAL>{ app := fun Y => U.map (F.val.map (ht.from (unop Y)).op), naturality := ⋯ } ≫ whiskerRight (toSheafify J F.val) U = whiskerRight (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))) U ≫ whiskerRight ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)).val U
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<VAR>x✝ : Cᵒᵖ<GOAL>({ app := fun Y => U.map (F.val.map (ht.from (unop Y)).op), naturality := ⋯ } ≫ whiskerRight (toSheafify J F.val) U).app x✝ = (whiskerRight (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))) U ≫ whiskerRight ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)).val U).app x✝
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<VAR>x✝ : Cᵒᵖ<GOAL>U.map (F.val.map (ht.from (unop x✝)).op ≫ (toSheafify J F.val).app x✝) = U.map ((toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))).app x✝ ≫ ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)).val.app x✝)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<VAR>x✝ : Cᵒᵖ<GOAL>F.val.map (ht.from (unop x✝)).op ≫ (toSheafify J F.val).app x✝ = (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))).app x✝ ≫ ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)).val.app x✝
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<VAR>x✝ : Cᵒᵖ<GOAL>(toSheafify J F.val).app (op t) ≫ (sheafify J F.val).map (ht.from (unop x✝)).op = (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))).app x✝ ≫ ((presheafToSheaf J A).map { app := fun x => F.val.map (ht.from (unop x)).op, naturality := ⋯ }).val.app x✝
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<VAR>x✝ : Cᵒᵖ<GOAL>(toSheafify J F.val).app (op t) ≫ (sheafify J F.val).map (ht.from (unop x✝)).op = ({ app := fun x => F.val.map (ht.from (unop x)).op, naturality := ⋯ } ≫ toSheafify J F.val).app x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae (μ.withDensity (ν.rnDeriv μ))] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<GOAL>2 + 1 = 3
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<GOAL>↑(1 + 1 + 1) = 3
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<GOAL>1 + 1 + 1 = 3
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x * cos x = (sin b ^ 2 - sin a ^ 2) / 2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>inst✝ : DecidableEq M<VAR>x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)<GOAL>(coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝ : (i : ι) → AddCommMonoid (β i)<VAR>κ : Type u_1<VAR>h : ι ≃ κ<VAR>f : ⨁ (i : ι), β i<VAR>k : κ<GOAL>((equivCongrLeft h) f) k = f (h.symm k)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hΦ₂ : span R Φ = ⊤<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hΦ₂ : span R Φ = ⊤<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁<VAR>hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hΦ₂ : span R Φ = ⊤<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁<VAR>hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hΦ₂ : span R Φ = ⊤<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁<VAR>hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x<GOAL>IsOfFinOrder u
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : K[X]<GOAL>factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<GOAL>factors (span {0}) = Multiset.map (fun q => span {q}) (factors 0)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : K[X]<VAR>hp : p ≠ 0<GOAL>factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : K[X]<VAR>hp : p ≠ 0<VAR>this : ∀ q ∈ Multiset.map (fun q => span {q}) (factors p), Prime q<GOAL>factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<GOAL>G.edgeSet = ∅ ↔ G = ⊥
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>x : ↥S.leftInv<GOAL>↑(S.fromLeftInv x) * ↑x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>image2 f s (⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, image2 f s (t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s✝ : Set α<VAR>f : ι → α<VAR>a✝ : α<VAR>s : ι → α<VAR>a : α<VAR>h : BddAbove (range s)<GOAL>a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>f : C(X, Y)<GOAL>𝓝 f = ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → List β<VAR>p : α → β → Bool<VAR>hf : Primrec f<VAR>hp : Primrec₂ p<VAR>a : α<GOAL>List.foldr (fun b s => bif p a b then 0 else s + 1) 0 (f a) = List.findIdx (p a) (f a)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff = 0<GOAL>f.eraseLead.natDegree ≤ f.natDegree - 2
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff = 0<GOAL>f.eraseLead.coeff (f.natDegree - 1) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : (∃ x, C x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0<GOAL>f.eraseLead.coeff (f.natDegree - 1) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>hf : 0 < f.natDegree<VAR>h : f.coeff (f.natDegree - 1) = 0<GOAL>f.eraseLead.coeff (f.natDegree - 1) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>hf : 0 < f.natDegree<VAR>h : f.coeff (f.natDegree - 1) = 0<GOAL>f.nextCoeff = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>mabs a * a = a⁺ᵐ ^ 2
<VAR>i : ℤ<GOAL>(natAbs 0).lcm i.natAbs = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℕ<VAR>ha : x - ↑a ∈ Ideal.span {↑p ^ n}<VAR>hb : x - ↑b ∈ Ideal.span {↑p ^ n}<GOAL>↑a = ↑b
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_1<VAR>β₂ : Type u_3<VAR>e : α₁ → β₁ ≃ β₂<VAR>a : α₁<VAR>b : β₁<GOAL>((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)) (a, b) = ((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm) (a, b)
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_1<VAR>β₂ : Type u_3<VAR>e : α₁ → β₁ ≃ β₂<VAR>a : α₁<VAR>b : β₁<GOAL>⟨((sigmaEquivProd α₁ β₁).symm (a, b)).fst, (e ((sigmaEquivProd α₁ β₁).symm (a, b)).fst) ((sigmaEquivProd α₁ β₁).symm (a, b)).snd⟩ = (sigmaEquivProd α₁ β₂).symm (a, (e a) b)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>hf : Function.Surjective ⇑f<VAR>h : affineSpan k s = ⊤<GOAL>affineSpan k (⇑f '' s) = ⊤
<VAR>α β : Type u<VAR>ι : Sort u_1<VAR>f : ι → Cardinal.{u_2}<GOAL>⨅ i, f i = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Ioc s t).card = 2 ^ (t.card - s.card) - 1
<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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ✝ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>s : Set β<GOAL>(Measure.map f μ) s = μ (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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ✝ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>s : Set β<GOAL>(Measure.map f μ) s ≤ μ (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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ✝ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>s : Set β<VAR>t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ<GOAL>(Measure.map f μ) s ≤ μ (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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ✝ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>s : Set β<VAR>t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ<VAR>htm : MeasurableSet t<GOAL>(Measure.map f μ) s ≤ μ (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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ✝ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>s : Set β<VAR>t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ<VAR>htm : MeasurableSet t<VAR>hst : s ⊆ t<GOAL>(Measure.map f μ) s ≤ μ (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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ✝ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>s : Set β<VAR>t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ<VAR>htm : MeasurableSet t<VAR>hst : s ⊆ t<VAR>hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)<GOAL>(Measure.map f μ) s ≤ μ (f ⁻¹' s)
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>logb b x < y ↔ x < b ^ y
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>a : R<VAR>hzero : p + q ≠ 0<GOAL>min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>a : R<VAR>hzero : p + q ≠ 0<GOAL>(X - C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : MulZeroOneClass β<VAR>inst✝ : Nontrivial β<VAR>s : ι → Set Ω<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<GOAL>filtrationOfSet hsm = natural (fun i => (s i).indicator fun x => 1) ⋯
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : MulZeroOneClass β<VAR>inst✝ : Nontrivial β<VAR>s : ι → Set Ω<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<GOAL>(fun i => MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) = fun i => MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : MulZeroOneClass β<VAR>inst✝ : Nontrivial β<VAR>s : ι → Set Ω<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>i : ι<GOAL>MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t} = MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}