ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>t : ↑(Icc v.tMin v.tMax)<GOAL>f.vComp ↑t = v.toFun (↑t) (f.toFun t)
<VAR>α : Type u_1<VAR>inst✝¹ : OrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>t : β<VAR>ht : t ∈ Icc 0 1<GOAL>1 - t ∈ Icc 0 1
<VAR>α : Type u_1<VAR>inst✝¹ : OrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>t : β<VAR>ht : 0 ≤ t ∧ t ≤ 1<GOAL>0 ≤ 1 - t ∧ 1 - t ≤ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>s : Set α<GOAL>f (sSup s) = ⨆ x ∈ s, f x
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ S.a + ↑η ^ 2 * S.b<GOAL>Associated p λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ S.a + ↑η ^ 2 * S.b<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ S.a + ↑η ^ 2 * S.b<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b<VAR>this : p ∣ (1 * ↑η ^ 2 - ↑η * 1) * gcd S.a S.b<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b<VAR>this : p ∣ ↑η ^ 2 - ↑η<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b<VAR>this : p ∣ ↑η ^ 2 - ↑η<GOAL>λ = (↑η ^ 2 - ↑η) * ↑η * ↑η
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<VAR>hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b<VAR>this : p ∣ ↑η ^ 2 - ↑η<GOAL>(↑η ^ 2 - ↑η) * ↑η * ↑η = λ
<VAR>a : ℤ<GOAL>|a| < 1 ↔ a = 0
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>this : Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop (𝓝 (∑' (n : ℕ), f n))<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>this : Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop (𝓝 (∑' (n : ℕ), f n))<VAR>H : ∀ (n : ℕ), ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => (1 - f p)⁻¹) p = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>this : Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop (𝓝 (∑' (n : ℕ), f n))<VAR>H : ∀ (n : ℕ), ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => (1 - f p)⁻¹) p = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹<VAR>H' : ({p | Nat.Prime p}.mulIndicator fun p => (1 - f p)⁻¹) = {p | Nat.Prime p}.mulIndicator fun p => ∑' (e : ℕ), f (p ^ e)<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>t : α → Finset β<VAR>h : s₁ ⊆ s₂<VAR>x : β<GOAL>x ∈ s₁.biUnion t → x ∈ s₂.biUnion t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>t : α → Finset β<VAR>h : s₁ ⊆ s₂<VAR>x : β<GOAL>(∃ a ∈ s₁, x ∈ t a) → ∃ a ∈ s₂, x ∈ t a
<VAR>p✝ p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<GOAL>↑(p.maxPowDiv n) = multiplicity p n
<VAR>p✝ p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<GOAL>¬p ^ (p.maxPowDiv n + 1) ∣ n
<VAR>p✝ p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : p ^ (p.maxPowDiv n + 1) ∣ n<GOAL>False
<VAR>p✝ p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : p ^ (p.maxPowDiv n + 1) ∣ n<GOAL>p.maxPowDiv n < p.maxPowDiv n + 1
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>R.mul ▷ X P Q ≫ actLeft P Q = (α_ R.X R.X (X P Q)).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(tensorLeft (R.X ⊗ R.X)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ R.mul ▷ X P Q ≫ actLeft P Q = (tensorLeft (R.X ⊗ R.X)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ (α_ R.X R.X (X P Q)).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ R.mul ▷ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q = (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(R.mul ▷ (P.X ⊗ Q.X) ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ actLeft P Q = (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>R.mul ▷ (P.X ⊗ Q.X) ≫ (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(((α_ (R.X ⊗ R.X) P.X Q.X).inv ≫ R.mul ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(α_ (R.X ⊗ R.X) P.X Q.X).inv ≫ ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(α_ (R.X ⊗ R.X) P.X Q.X).inv ≫ ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (((α_ R.X R.X (P.X ⊗ Q.X)).hom ≫ R.X ◁ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ R.X ◁ actLeft P Q) ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(α_ (R.X ⊗ R.X) P.X Q.X).inv ≫ ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (α_ R.X R.X (P.X ⊗ Q.X)).hom ≫ (R.X ◁ (α_ R.X P.X Q.X).inv ≫ R.X ◁ P.actLeft ▷ Q.X ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ actLeft P Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(α_ (R.X ⊗ R.X) P.X Q.X).inv ≫ ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (α_ R.X R.X (P.X ⊗ Q.X)).hom ≫ R.X ◁ (α_ R.X P.X Q.X).inv ≫ R.X ◁ P.actLeft ▷ Q.X ≫ (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(α_ (R.X ⊗ R.X) P.X Q.X).inv ≫ ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (α_ R.X R.X (P.X ⊗ Q.X)).hom ≫ R.X ◁ (α_ R.X P.X Q.X).inv ≫ (((α_ R.X (R.X ⊗ P.X) Q.X).inv ≫ (R.X ◁ P.actLeft) ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>R' : Type v<VAR>inst✝ : CommMonoid R'<VAR>φ : AddChar R R'<VAR>a : R<VAR>h : 0 < ringChar R<GOAL>⋯.unit ∈ rootsOfUnity (ringChar R).toPNat' R'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (SuccOrder.succ #α).ord)<GOAL>∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_ninj : ∃ a b, (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧ a ≠ b<GOAL>∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_ninj : ∃ a b, (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧ a ≠ b<VAR>a b : ↑(Set.Iio (SuccOrder.succ #α).ord)<VAR>h_fab : (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b<VAR>h_nab : a ≠ b<GOAL>∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_ninj : ∃ a b, (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧ a ≠ b<VAR>a b : ↑(Set.Iio (SuccOrder.succ #α).ord)<VAR>h_fab : (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b<VAR>h_nab : a ≠ b<GOAL>↑a < (succ #α).ord ∧ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_ninj : ∃ a b, (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧ a ≠ b<VAR>a b : ↑(Set.Iio (SuccOrder.succ #α).ord)<VAR>h_fab : (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b<VAR>h_nab : a ≠ b<GOAL>∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_ninj : ∃ a b, (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧ a ≠ b<VAR>a b : ↑(Set.Iio (SuccOrder.succ #α).ord)<VAR>h_fab : (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b<VAR>h_nab : a ≠ b<GOAL>↑b < (succ #α).ord ∧ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_ninj : ∃ a b, (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧ a ≠ b<VAR>a b : ↑(Set.Iio (SuccOrder.succ #α).ord)<VAR>h_fab : (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a = (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b<VAR>h_nab : a ≠ b<GOAL>↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<GOAL>∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>∃ c, ‖c‖ = 1 ∧ ↑‖0‖ = c * 0
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<VAR>hx : x ≠ 0<GOAL>∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>i✝ : κ<GOAL>(comapDomain h hh 0) i✝ = 0 i✝
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>(μ.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) s = ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>(⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ) s = ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>(μ.toFinite.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ ⊤ * (μ.toFinite.restrict μ.sigmaFiniteSetᶜ) s = ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>μ.toFinite (s ∩ μ.sigmaFiniteSetᶜ) = 0 ∨ ⊤ * μ.toFinite (s ∩ μ.sigmaFiniteSetᶜ) = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Injective (image f) ↔ Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Injective (image f)<VAR>x x' : α<VAR>hx : f x = f x'<GOAL>x = x'
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Injective (image f)<VAR>x x' : α<VAR>hx : f x = f x'<GOAL>{x} = {x'}
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Injective (image f)<VAR>x x' : α<VAR>hx : f x = f x'<GOAL>f '' {x} = f '' {x'}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>𝔸 : Type u_3<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝔸<VAR>inst✝³ : NormedCommRing 𝔸'<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>inst✝¹ : NormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : E → 𝔸<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => f x ^ 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>𝔸 : Type u_3<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝔸<VAR>inst✝³ : NormedCommRing 𝔸'<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>inst✝¹ : NormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : E → 𝔸<VAR>hf : ContDiff 𝕜 n f<VAR>m : ℕ<GOAL>ContDiff 𝕜 n fun x => f x ^ (m + 1)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>(Lagrange.basis s v i).degree = ↑(s.card - 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(↑p).valuation = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : 1 < ↑p<GOAL>(↑p).valuation = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : 1 < ↑p<GOAL>↑p ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : 1 < ↑p<GOAL>‖↑p‖ = ↑p ^ (-1)
<VAR>a b k m n p : ℕ<GOAL>p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>P Q : C → Prop<VAR>inst✝ : ClosedUnderIsomorphisms P<GOAL>isoClosure P = P
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>P Q : C → Prop<VAR>inst✝ : ClosedUnderIsomorphisms P<GOAL>isoClosure P ≤ P
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>P Q : C → Prop<VAR>inst✝ : ClosedUnderIsomorphisms P<GOAL>P ≤ isoClosure P
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u✝ v : Finset α<VAR>a b : α<VAR>s t u : Finset α<VAR>x : α<GOAL>x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>f : α →* β<VAR>hf : Function.Surjective ⇑f<VAR>b : ConjClasses β<GOAL>∃ a, map f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>f : α →* β<VAR>hf : Function.Surjective ⇑f<VAR>b : β<GOAL>∃ a, map f a = ConjClasses.mk b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : LinearOrder E<VAR>inst✝¹ : Zero E<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ ℝ<VAR>a : α<GOAL>↑(map (fun b => max b 0) f - map (fun b => max b 0) (-f)) a = ↑f a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : LinearOrder E<VAR>inst✝¹ : Zero E<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ ℝ<VAR>a : α<GOAL>(↑(map (fun b => max b 0) f) - ↑(map (fun b => max b 0) (-f))) a = ↑f a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>S R : Sieve X<GOAL>pullback (𝟙 X) S = S
<VAR>n : ℕ<VAR>x : ℕ × ℕ<VAR>h : x ∈ n.divisorsAntidiagonal<GOAL>x.1 ∈ n.divisors
<VAR>n : ℕ<VAR>x : ℕ × ℕ<VAR>h : x.1 * x.2 = n ∧ n ≠ 0<GOAL>x.1 ∈ n.divisors
<VAR>n x : ℕ<VAR>hx : x < n + 2<GOAL>(finRotate (n + 2) ^ ↑↑⟨x, hx⟩) 0 = ⟨x, hx⟩
<VAR>n x : ℕ<VAR>hx : x < n + 2<GOAL>↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
<VAR>n x : ℕ<VAR>ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩<VAR>hx : x + 1 < n + 2<GOAL>↑((finRotate (n + 2) ^ ↑⟨x + 1, hx⟩) 0) = ↑⟨x + 1, hx⟩
<VAR>n x : ℕ<VAR>ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩<VAR>hx : x + 1 < n + 2<GOAL>(finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)
<VAR>n x : ℕ<VAR>ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩<VAR>hx : x + 1 < n + 2<GOAL>¬↑⟨x, ⋯⟩ = n + 1
<VAR>X : Type u_1<VAR>x y : X<GOAL>(((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x)) 1) y = (((AddMonoidHom.id (X →₀ ℤ)).comp (singleAddHom x)) 1) y
<VAR>X : Type u_1<VAR>x y : X<GOAL>(((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x)) 1) y = ((singleAddHom x) 1) y
<VAR>X : Type u_1<VAR>x y : X<GOAL>((toFinsupp.comp ((smulAddHom ℤ (FreeAbelianGroup X)).flip (of x))) 1) y = ((singleAddHom x) 1) y