ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<GOAL>∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(M₂.presheaf.obj X)), (((Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN).symm ψ.hom).app X) (r • x) = r • (((Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN).symm ψ.hom).app X) x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : (Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN) φ = ψ.hom<GOAL>∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(M₂.presheaf.obj X)), (((Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN).symm ψ.hom).app X) (r • x) = r • (((Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN).symm ψ.hom).app X) x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : (Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN) φ = ψ.hom<GOAL>∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(M₂.presheaf.obj X)), (φ.app X) (r • x) = r • (φ.app X) x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : f.hom ≫ φ = ψ.hom<VAR>X : Cᵒᵖ<VAR>r : ↑(R.obj X)<VAR>y : ↑(M₂.presheaf.obj X)<GOAL>(φ.app X) (r • y) = r • (φ.app X) y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : f.hom ≫ φ = ψ.hom<VAR>X : Cᵒᵖ<VAR>r : ↑(R.obj X)<VAR>y : ↑(M₂.presheaf.obj X)<GOAL>∀ (Y : C) (f_1 : Y ⟶ Opposite.unop X), (Presheaf.imageSieve f.hom y).arrows f_1 → (N.presheaf.map f_1.op) ((φ.app X) (r • y)) = (N.presheaf.map f_1.op) (r • (φ.app X) y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : f.hom ≫ φ = ψ.hom<VAR>X : Cᵒᵖ<VAR>r : ↑(R.obj X)<VAR>y : ↑(M₂.presheaf.obj X)<VAR>Y : C<VAR>p : Y ⟶ Opposite.unop X<VAR>x : (forget AddCommGrp).obj (M₁.presheaf.obj (Opposite.op Y))<VAR>hx : (f.hom.app (Opposite.op Y)) x = (M₂.presheaf.map p.op) y<GOAL>(N.presheaf.map p.op) ((φ.app X) (r • y)) = (N.presheaf.map p.op) (r • (φ.app X) y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : f.hom ≫ φ = ψ.hom<VAR>X : Cᵒᵖ<VAR>r : ↑(R.obj X)<VAR>y : ↑(M₂.presheaf.obj X)<VAR>Y : C<VAR>p : Y ⟶ Opposite.unop X<VAR>x : (forget AddCommGrp).obj (M₁.presheaf.obj (Opposite.op Y))<VAR>hx : (f.hom.app (Opposite.op Y)) x = (M₂.presheaf.map p.op) y<VAR>eq : (ψ.hom.app (Opposite.op Y)) ((R.map p.op) r • x) = (R.map p.op) r • (ψ.hom.app (Opposite.op Y)) x<GOAL>(N.presheaf.map p.op) ((φ.app X) (r • y)) = (N.presheaf.map p.op) (r • (φ.app X) y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : f.hom ≫ φ = ψ.hom<VAR>X : Cᵒᵖ<VAR>r : ↑(R.obj X)<VAR>y : ↑(M₂.presheaf.obj X)<VAR>Y : C<VAR>p : Y ⟶ Opposite.unop X<VAR>x : (forget AddCommGrp).obj (M₁.presheaf.obj (Opposite.op Y))<VAR>hx : (f.hom.app (Opposite.op Y)) x = (M₂.presheaf.map p.op) y<VAR>eq : (φ.app (Opposite.op Y)) ((f.hom.app (Opposite.op Y)) ((R.map p.op) r • x)) = (R.map p.op) r • (φ.app (Opposite.op Y)) ((f.hom.app (Opposite.op Y)) x)<GOAL>(N.presheaf.map p.op) ((φ.app X) (r • y)) = (N.presheaf.map p.op) (r • (φ.app X) y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R✝ : Sheaf J RingCat<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : Presheaf.IsSheaf J N.presheaf<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : Presheaf.IsLocallySurjective J f.hom<VAR>inst✝ : Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<VAR>φ : M₂.presheaf ⟶ N.presheaf<VAR>hφ : f.hom ≫ φ = ψ.hom<VAR>X : Cᵒᵖ<VAR>r : ↑(R.obj X)<VAR>y : ↑(M₂.presheaf.obj X)<VAR>Y : C<VAR>p : Y ⟶ Opposite.unop X<VAR>x : (forget AddCommGrp).obj (M₁.presheaf.obj (Opposite.op Y))<VAR>hx : (f.hom.app (Opposite.op Y)) x = (M₂.presheaf.map p.op) y<VAR>eq : (φ.app (Opposite.op Y)) ((f.hom.app (Opposite.op Y)) ((R.map p.op) r • x)) = (R.map p.op) r • (φ.app (Opposite.op Y)) ((f.hom.app (Opposite.op Y)) x)<GOAL>(φ.app (Opposite.op Y)) ((R.map p.op) r • (f.hom.app (Opposite.op Y)) x) = (φ.app (Opposite.op Y)) ((R.map p.op) r • (f.hom.app (Opposite.op Y)) x)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : CompleteSpace F<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup P<VAR>inst✝² : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : μ.IsNegInvariant<VAR>n : ℕ∞<VAR>hcf : HasCompactSupport f<VAR>hf : ContDiff 𝕜 n f<VAR>hg : LocallyIntegrable g μ<GOAL>ContDiff 𝕜 n (f ⋆[L, μ] g)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : CompleteSpace F<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup P<VAR>inst✝² : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : μ.IsNegInvariant<VAR>n : ℕ∞<VAR>hcf : HasCompactSupport f<VAR>hf : ContDiff 𝕜 n f<VAR>hg : LocallyIntegrable g μ<GOAL>ContDiff 𝕜 n (g ⋆[L.flip, μ] f)
<VAR>θ : Angle<GOAL>2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Sup α<VAR>inst✝² : Sup β<VAR>inst✝¹ : Sup γ<VAR>inst✝ : Sup δ<VAR>g : SupHom β γ<VAR>f₁ f₂ : SupHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>x : W.CoordinateRing<GOAL>((Algebra.norm R[X]) x).degree ≠ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<GOAL>((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree ≠ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<GOAL>max (2 • p.degree) (2 • q.degree + 3) ≠ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>n✝ a✝ : ℕ<GOAL>max (2 • some (n✝ + 1 + 1)) (2 • ↑a✝ + 3) ≠ 1
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M₁<VAR>inst✝⁸ : Module R M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : AddCommMonoid N₂<VAR>inst✝⁴ : Module R N₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] N₂<VAR>i : n<VAR>j : m<GOAL>(toMatrix₂Aux R ⇑b₁ ⇑b₂) B i j = (toMatrix₂ b₁ b₂) B i j
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ : Path x y<VAR>χ : ι → Type u_4<VAR>inst✝ : (i : ι) → TopologicalSpace (χ i)<VAR>as bs cs : (i : ι) → χ i<VAR>γ₀ : (i : ι) → Path (as i) (bs i)<VAR>γ₁ : (i : ι) → Path (bs i) (cs i)<VAR>t : ↑I<VAR>i : ι<GOAL>{ toFun := (fun t => if t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * t) else (Path.pi γ₁).extend (2 * t - 1)) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } t i = (Path.pi fun i => { toFun := (fun t => if t ≤ 1 / 2 then (γ₀ i).extend (2 * t) else (γ₁ i).extend (2 * t - 1)) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }) t i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ : Path x y<VAR>χ : ι → Type u_4<VAR>inst✝ : (i : ι) → TopologicalSpace (χ i)<VAR>as bs cs : (i : ι) → χ i<VAR>γ₀ : (i : ι) → Path (as i) (bs i)<VAR>γ₁ : (i : ι) → Path (bs i) (cs i)<VAR>t : ↑I<VAR>i : ι<GOAL>(if ↑t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * ↑t) else (Path.pi γ₁).extend (2 * ↑t - 1)) i = if ↑t ≤ 1 / 2 then (γ₀ i).extend (2 * ↑t) else (γ₁ i).extend (2 * ↑t - 1)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>_l : List α<GOAL>countP p (Quot.mk Setoid.r _l) = card (Quot.mk Setoid.r _l) ↔ ∀ a ∈ Quot.mk Setoid.r _l, p a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<VAR>h : Injective fun n => x ^ n<GOAL>¬IsOfFinOrder x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<VAR>h : Injective fun n => x ^ n<GOAL>∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>h : Injective fun n => x ^ n<VAR>n : ℕ<VAR>hn_pos : 0 < n<VAR>hnx : x ^ n = 1<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>h : Injective fun n => x ^ n<VAR>n : ℕ<VAR>hn_pos : 0 < n<VAR>hnx : x ^ n = x ^ 0<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>h : Injective fun n => x ^ n<VAR>n : ℕ<VAR>hn_pos : 0 < 0<VAR>hnx : x ^ n = x ^ 0<GOAL>False
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>h : a ≠ 0<VAR>i : ℤ<GOAL>a ^ (1 + i) = a * a ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>x : R<GOAL>rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s✝ : Set α<VAR>hs✝ : MeasurableSet s✝<VAR>hμs : μ s✝ ≠ ⊤<VAR>c✝ : E<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>hsμ : μ s ≠ ⊤<VAR>ht : MeasurableSet t<VAR>htμ : μ t ≠ ⊤<VAR>c : E<VAR>hc : c ≠ 0<GOAL>indicatorConstLp p hs hsμ c = indicatorConstLp p ht htμ c ↔ s =ᶠ[ae μ] t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<GOAL>eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<VAR>h : x ≤ y<GOAL>eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<VAR>h : y ≤ x<GOAL>eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>val✝ : List α<VAR>property✝ : val✝.length = n<GOAL>(snoc ⟨val✝, property✝⟩ x).reverse = x ::ᵥ reverse ⟨val✝, property✝⟩
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>val✝ : List α<VAR>property✝ : val✝.length = n<GOAL>⟨(append ⟨val✝, property✝⟩ ⟨[x], ⋯⟩).toList.reverse, ⋯⟩ = ⟨x :: val✝.reverse, ⋯⟩
<VAR>a b : ℕ<VAR>ha : a % 4 = 3<VAR>hb : b % 4 = 3<GOAL>J(↑a | b) = -J(↑b | a)
<VAR>a b : ℕ<VAR>ha : a % 4 = 3<VAR>hb : b % 4 = 3<VAR>nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four<GOAL>J(↑a | b) = -J(↑b | a)
<VAR>θ₁ θ₂ : Angle<GOAL>(θ₁ + θ₂).expMapCircle = θ₁.expMapCircle * θ₂.expMapCircle
<VAR>θ₂ : Angle<VAR>x✝ : ℝ<GOAL>(↑x✝ + θ₂).expMapCircle = (↑x✝).expMapCircle * θ₂.expMapCircle
<VAR>x✝¹ x✝ : ℝ<GOAL>(↑x✝¹ + ↑x✝).expMapCircle = (↑x✝¹).expMapCircle * (↑x✝).expMapCircle
<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>κ : Type u_6<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>f : ι → β<GOAL>∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s ∩ t, f i
<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>κ : Type u_6<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>f : ι → β<GOAL>∏ i ∈ filter (fun i => i ∈ ↑t) s, f i = ∏ i ∈ filter (fun i => i ∈ t) s, f i
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<GOAL>Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x : X<VAR>r : R<VAR>h : ι R x = (algebraMap R (FreeAlgebra R X)) r<VAR>f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0<VAR>f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x : X<VAR>r : R<VAR>h : ι R x = (algebraMap R (FreeAlgebra R X)) r<VAR>f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0<VAR>f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1<VAR>hf0 : f0 (ι R x) = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x : X<VAR>r : R<VAR>h : ι R x = (algebraMap R (FreeAlgebra R X)) r<VAR>f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0<VAR>f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1<VAR>hf0 : f0 (ι R x) = 0<VAR>hf1 : f1 (ι R x) = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x : X<VAR>r : R<VAR>h : ι R x = (algebraMap R (FreeAlgebra R X)) r<VAR>f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0<VAR>f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1<VAR>hf0 : r = 0<VAR>hf1 : f1 (ι R x) = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x : X<VAR>r : R<VAR>h : ι R x = (algebraMap R (FreeAlgebra R X)) r<VAR>f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0<VAR>f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1<VAR>hf0 : r = 0<VAR>hf1 : r = 1<GOAL>False
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S : B<VAR>l : List ↥S<GOAL>(List.map Subtype.val l).prod ∈ S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S : B<VAR>l : List ↥S<GOAL>↑l.prod ∈ S
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝³ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝² : Module R P<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>i : ι<VAR>m : Mᵢ i<GOAL>(pi Q) (Pi.single i m) = (Q i) m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝³ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝² : Module R P<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>i : ι<VAR>m : Mᵢ i<VAR>j : ι<VAR>hj : j ≠ i<GOAL>(Q j) (Pi.single i m j) = 0
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>inst✝ : (a : α) → DecidableEq (δ a)<VAR>t : (a : α) → Finset (δ a)<VAR>a : α<VAR>x : δ a<VAR>hx : x ∉ t a<GOAL>filter (fun x_1 => x_1 a = x) (piFinset t) = ∅
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>inst✝ : (a : α) → DecidableEq (δ a)<VAR>t : (a : α) → Finset (δ a)<VAR>a : α<VAR>x : δ a<VAR>hx : x ∉ t a<GOAL>∀ ⦃x_1 : (a : α) → δ a⦄, (∀ (a : α), x_1 a ∈ t a) → ¬x_1 a = x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : HasBinaryCoproduct X Y<GOAL>coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr 0 0
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s t : Set Ω<VAR>S T : Set (Set Ω)<VAR>m0 : MeasurableSpace Ω<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h : IndepSets {s} {t} κ μ<VAR>u : Set Ω<VAR>hu : u ∈ {s}<GOAL>MeasurableSet u
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s t : Set Ω<VAR>S T : Set (Set Ω)<VAR>m0 : MeasurableSpace Ω<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h : IndepSets {s} {t} κ μ<VAR>u : Set Ω<VAR>hu : u ∈ {t}<GOAL>MeasurableSet u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>h : N.Basis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X<GOAL>(N.comap f).Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>h : N.Basis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X<GOAL>(N.comap f).Indep I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>h : N.Basis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X<VAR>e : α<VAR>x✝ : e ∈ X \ I<VAR>heX : e ∈ X<VAR>heI : e ∉ I<GOAL>(N.comap f).Dep (insert e I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>h : N.Basis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X<VAR>e : α<VAR>x✝ : e ∈ X \ I<VAR>heX : e ∈ X<VAR>heI : e ∉ I<VAR>hIE : insert e I ⊆ (N.comap f).E<GOAL>(N.comap f).Dep (insert e I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>h : N.Basis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X<VAR>e : α<VAR>x✝ : e ∈ X \ I<VAR>heX : e ∈ X<VAR>heI : e ∉ I<VAR>hIE : insert e I ⊆ (N.comap f).E<GOAL>N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
<VAR>n : Nat<GOAL>range n.succ = range n ++ [n]
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<GOAL>map Prod.fst l.revzip = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a c b : Ordinal.{u_4}<VAR>x✝ : a ∣ a * b + c<VAR>d : Ordinal.{u_4}<VAR>e : a * b + c = a * d<GOAL>c = a * (d - b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a c b : Ordinal.{u_4}<VAR>x✝ : a ∣ c<VAR>d : Ordinal.{u_4}<VAR>e : c = a * d<GOAL>a ∣ a * (b + d)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b✝ c d e : α<VAR>m n : ℤ<VAR>a : α<VAR>h : 0 < a<VAR>b : α<GOAL>∃ c, 0 < c ∧ b * c < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b✝ c d e : α<VAR>m n : ℤ<VAR>a : α<VAR>h : 0 < a<VAR>b : α<VAR>this : 0 < a / max (b + 1) 1<GOAL>∃ c, 0 < c ∧ b * c < a