ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<VAR>x✝¹ : ℕ<VAR>x✝ : x✝¹ ∈ Ico 1 (p / 2).succ<GOAL>↑(↑a * ↑x✝¹).val = (if (↑a * ↑x✝¹).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x✝¹).valMinAbs.natAbs
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<VAR>x✝¹ : ℕ<VAR>x✝ : x✝¹ ∈ Ico 1 (p / 2).succ<GOAL>↑(↑a * ↑x✝¹).val = (if (↑a * ↑x✝¹).val ≤ p / 2 then 1 else -1) * if (↑a * ↑x✝¹).val ≤ p / 2 then ↑a * ↑x✝¹ else -(↑a * ↑x✝¹)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs = (-1) ^ (filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)).card * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<VAR>this : (∏ x ∈ Ico 1 (p / 2).succ, if (↑a * ↑x).val ≤ p / 2 then 1 else -1) = ∏ x ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ), -1<GOAL>∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs = (-1) ^ (filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)).card * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>(-1) ^ (filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)).card * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs = (-1) ^ (filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)).card * ↑(p / 2)!
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<GOAL>(PiToModule.fromMatrix R b) 0 = (PiToModule.fromEnd R b) 0
<VAR>n : ℕ<VAR>i : ZMod n<GOAL>orderOf (sr i) = 2
<VAR>n : ℕ<VAR>i : ZMod n<GOAL>sr i ^ 2 = 1
<VAR>n : ℕ<VAR>i : ZMod n<GOAL>sr i ≠ 1
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.castSucc ≠ 0<GOAL>a.castSucc.pred ha < b ↔ a ≤ b
<VAR>q : ℚ<GOAL>(-q)⁻¹ = -q⁻¹
<VAR>q : ℚ<GOAL>(-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g : G<VAR>a : α<GOAL>period g⁻¹ a = period g a
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g : G<VAR>a : α<GOAL>∀ (n : ℕ), g⁻¹ ^ n • a = a ↔ g ^ n • a = a
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g : G<VAR>a : α<VAR>n : ℕ<GOAL>g⁻¹ ^ n • a = a ↔ g ^ n • a = a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<GOAL>cgf X μ 0 = log (μ Set.univ).toReal
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>IsOpen (range Real.toEReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝¹ : Semiring α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<VAR>ha : Aᴴ.IsDiag<GOAL>A.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝¹ : Semiring α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<VAR>ha : Aᴴ.IsDiag<GOAL>A = Aᴴᴴ
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCancelCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>n : μ<VAR>f : ι → μ<GOAL>f ∈ (cons i s hi).piAntidiag n ↔ f ∈ (antidiagonal n).disjiUnion (fun p => map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCancelCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>n : μ<VAR>f : ι → μ<GOAL>(f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) ↔ ∃ a b, a + b = n ∧ ∃ a_1, (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t => if t = i then a else 0) a_1 = f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>hfm : AEStronglyMeasurable f μ<VAR>hf : f =O[⊤] g<VAR>hg : Integrable g μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>hfm : AEStronglyMeasurable f μ<VAR>hf : f =O[⊤] g<VAR>hg : IntegrableAtFilter g ⊤ μ<GOAL>IntegrableAtFilter f ⊤ μ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.45590, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0
<VAR>u v : ℤ<GOAL>u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>s ∩ ⋃ i, notConvergentSeq f g i (notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg i) ⊆ s
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.230696}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ f '' s<GOAL>lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.230696}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ range fun x => f ↑x<GOAL>lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.230696}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ range fun x => f ↑x<GOAL>lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t} = lift.{v, u} #↑((fun x => f ↑x) ⁻¹' t)
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.230696}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ range fun x => f ↑x<GOAL>lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x => f ↑x) ⁻¹' t)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>n k : ℕ<GOAL>(⇑derivative)^[k] (X ^ n) = C ↑(n.descFactorial k) * X ^ (n - k)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α✝<VAR>inst✝² : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_6<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0<VAR>μ : Measure α<VAR>h : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun x => ∑' (i : ι), f i x) μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α✝<VAR>inst✝² : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_6<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0<VAR>μ : Measure α<VAR>h : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun x => (∑' (b : ι), ↑(f b x)).toNNReal) μ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>WeierstrassCurve.expCoeff (2 * (m + 3)) = WeierstrassCurve.expCoeff (m + 2) ^ 2 * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 5) - WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 4) ^ 2 ∧ WeierstrassCurve.expCoeff (2 * (m + 2) + 1) = (WeierstrassCurve.expCoeff (m + 4) * WeierstrassCurve.expCoeff (m + 2) ^ 3 * if Even m then 4 ^ 2 else 1) - WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) ^ 3 * if Even m then 1 else 4 ^ 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>2 * (↑m + 3) / 2 = (((if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 2 * if Even m then ↑m + 3 else (↑m + 3) / 2) * if Even m then ↑m + 5 else (↑m + 5) / 2) - ((if Even m then ↑m + 1 else (↑m + 1) / 2) * if Even m then ↑m + 3 else (↑m + 3) / 2) * (if Even m then (↑m + 4) / 2 else ↑m + 4) ^ 2 ∧ 2 * (↑m + 2) + 1 = ((if Even m then (↑m + 4) / 2 else ↑m + 4) * (if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 3 * if Even m then 16 else 1) - (if Even m then ↑m + 1 else (↑m + 1) / 2) * (if Even m then ↑m + 3 else (↑m + 3) / 2) ^ 3 * if Even m then 1 else 16
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X X' Y Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>(f ⊗ g) ≫ (β_ Y Y').hom = (β_ X X').hom ≫ (g ⊗ f)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X X' Y Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>(X ◁ g ≫ f ▷ Y') ≫ (β_ Y Y').hom = (β_ X X').hom ≫ g ▷ X ≫ Y' ◁ f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrderBot α<VAR>inst✝ : DecidableEq α<VAR>b a✝ : α<GOAL>a✝ ∈ (Iic b).erase b ↔ a✝ ∈ Iio b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<GOAL>s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : 𝒜.Shatters s<GOAL>s ∈ 𝒜.biUnion powerset
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : 𝒜.Shatters s<GOAL>∃ a ∈ 𝒜, s ⊆ a
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n.bit0.size = (↑n.bit0).size
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>(↑n).size + 1 = (2 * ↑n).size
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>Nat.bit false ↑n ≠ 0
<VAR>α : Type u_1<VAR>n : PosNum<VAR>this : 0 < ↑n<GOAL>Nat.bit false ↑n ≠ 0
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n.bit1.size = (↑n.bit1).size
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>(↑n).size + 1 = (2 * ↑n + 1).size
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>Nat.bit true ↑n ≠ 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.217781, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝ : S.HasRightHomology<VAR>x : S.X₃ ⟶ A<VAR>hx : k = S.g ≫ x<GOAL>S.f ≫ k = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : GroupWithZero G₀<VAR>inst✝ : ContinuousMul G₀<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>map (fun x => a * x) (𝓝 1) = 𝓝 a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_6<VAR>K : Type u_7<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>r : S<VAR>x y : M<GOAL>(B x) (r • y) = r • (B x) y
<VAR>x✝ y z x : ℝ<GOAL>|0| ≤ |x|
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroOneClass M₀<VAR>s t : Set ι<VAR>i x✝ : ι<GOAL>(s ∩ t).indicator 1 x✝ = (s.indicator 1 * t.indicator 1) x✝
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroOneClass M₀<VAR>s t : Set ι<VAR>i x✝ : ι<GOAL>(s ∩ t).indicator 1 x✝ = (s ∩ t).indicator (fun j => 1) x✝
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u₁<VAR>inst✝² : Category.{v₁, u₁} D<VAR>inst✝¹ : Preadditive D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M : Mat_ C<VAR>i : M.ι<GOAL>(F.map (biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.lift (F.mapBicone (biproduct.bicone fun i => (embedding C).obj (M.X i))).π) ≫ biproduct.π (fun i => F.obj ((embedding C).obj (M.X i))) i = F.map ((biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u₁<VAR>inst✝² : Category.{v₁, u₁} D<VAR>inst✝¹ : Preadditive D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M : Mat_ C<VAR>i : M.ι<GOAL>F.map (biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.lift (F.mapBicone (biproduct.bicone fun i => (embedding C).obj (M.X i))).π ≫ biproduct.π (fun i => F.obj ((embedding C).obj (M.X i))) i = F.map fun j k => if h : j = i then eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u₁<VAR>inst✝² : Category.{v₁, u₁} D<VAR>inst✝¹ : Preadditive D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M : Mat_ C<VAR>i : M.ι<GOAL>F.map ((biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ (biproduct.bicone fun i => (embedding C).obj (M.X i)).π i) = F.map fun j k => if h : j = i then eqToHom ⋯ else 0
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a = none<GOAL>replaceF p l = l
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<GOAL>↑(stereoInvFun hv (stereoToFun v ↑x)) = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<GOAL>(‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x) + (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x‖ ^ 2 - 4) • v = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<VAR>a : ℝ := ((innerSL ℝ) v) ↑x<VAR>y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x<GOAL>(‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) + (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<VAR>a : ℝ := ((innerSL ℝ) v) ↑x<VAR>y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x<VAR>split : ↑x = a • v + ↑y<GOAL>(‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) + (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<VAR>a : ℝ := ((innerSL ℝ) v) ↑x<VAR>y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x<VAR>split : ↑x = a • v + ↑y<VAR>hvy : ⟪v, ↑y⟫_ℝ = 0<GOAL>(‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) + (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<VAR>a : ℝ := ((innerSL ℝ) v) ↑x<VAR>y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x<VAR>split : ↑x = a • v + ↑y<VAR>hvy : ⟪v, ↑y⟫_ℝ = 0<VAR>pythag : 1 = a ^ 2 + ‖y‖ ^ 2<GOAL>(‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) + (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<VAR>a : ℝ := ((innerSL ℝ) v) ↑x<VAR>y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x<VAR>split : ↑x = a • v + ↑y<VAR>hvy : ⟪v, ↑y⟫_ℝ = 0<VAR>pythag : 1 = a ^ 2 + ‖y‖ ^ 2<VAR>ha : 1 - a ≠ 0<GOAL>(‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) + (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(sphere 0 1)<VAR>hx : ↑x ≠ v<VAR>a : ℝ := ((innerSL ℝ) v) ↑x<VAR>y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x<VAR>split : ↑x = a • v + ↑y<VAR>hvy : ⟪v, ↑y⟫_ℝ = 0<VAR>pythag : 1 = a ^ 2 + ‖y‖ ^ 2<VAR>ha : 1 - a ≠ 0<VAR>h₁ : (2 ^ 2 / (1 - a) ^ 2 * ‖y‖ ^ 2 + 4)⁻¹ * 4 * (2 / (1 - a)) = 1<GOAL>(‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) + (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v = ↑x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cocone D<VAR>j : J<GOAL>T.map (c.ι.app j) ≫ T.map (t.desc (T.forget.mapCocone s)) ≫ s.pt.a = T.map (c.ι.app j) ≫ lambda c t ≫ t.desc (T.forget.mapCocone s)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cocone D<VAR>j : J<GOAL>T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = (D.obj j).a ≫ (T.forget.mapCocone s).ι.app j
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J✝ : Type u<VAR>inst✝² : Category.{v, u} J✝<VAR>D : J✝ ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cocone D<VAR>m : (liftedCocone c t).pt ⟶ s.pt<VAR>J : ∀ (j : J✝), (liftedCocone c t).ι.app j ≫ m = s.ι.app j<GOAL>m.f = ((fun s => { f := t.desc (T.forget.mapCocone s), h := ⋯ }) s).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J✝ : Type u<VAR>inst✝² : Category.{v, u} J✝<VAR>D : J✝ ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cocone D<VAR>m : (liftedCocone c t).pt ⟶ s.pt<VAR>J : ∀ (j : J✝), (liftedCocone c t).ι.app j ≫ m = s.ι.app j<GOAL>∀ (j : J✝), c.ι.app j ≫ m.f = c.ι.app j ≫ ((fun s => { f := t.desc (T.forget.mapCocone s), h := ⋯ }) s).f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝ : CommSemiring R<GOAL>DirectSum.Decomposition.decompose' = fun φ => (DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (Finset.image Finsupp.degree φ.support)) fun m => ⟨(homogeneousComponent ↑m) φ, ⋯⟩
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝ : CommSemiring R<GOAL>DirectSum.Decomposition.decompose' = fun φ => (DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑(weight 1)) φ.support)) fun m => ⟨(homogeneousComponent ↑m) φ, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : a < b * c<GOAL>a * c⁻¹ < b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : b ≤ a * c⁻¹<GOAL>b * c ≤ a
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod (2 * n)<GOAL>orderOf (a i) = 2 * n / (2 * n).gcd i.val
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod (2 * n)<GOAL>orderOf (a ↑i.val) = 2 * n / (2 * n).gcd i.val
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Semiring α<VAR>inst✝¹ : AddCommMonoid β<VAR>inst✝ : Module α β<VAR>a b : α<VAR>s : Set β<VAR>x : β<VAR>hx : x ∈ s<GOAL>(fun x => (a + b) • x) x ∈ a • s + b • s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = f.lift fun s => g.lift' fun t => s ×ˢ t
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>x : α<GOAL>span {x} = ⊤ ↔ IsUnit x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>x : α<VAR>y : β<VAR>hx : x ∈ e.source<VAR>hy : y ∈ e.target<VAR>h : x = ↑e.symm y<GOAL>↑e x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>x : α<VAR>y : β<VAR>hx : x ∈ e.source<VAR>hy : y ∈ e.target<VAR>h : ↑e x = y<GOAL>x = ↑e.symm y
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<GOAL>F.Final ↔ (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<VAR>hF : F.Final<GOAL>∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<VAR>hF : F.Final<GOAL>∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z✝ z₀ : ℂ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>h_z₀ : z₀ ∈ ball c R₁<VAR>g : ℂ → E := dslope f c<VAR>h_eq : ‖g z₀‖ = R₂ / R₁<VAR>z : ℂ<VAR>hz : z ∈ ball c R₁<VAR>h : ¬z = c<GOAL>f z = (fun z => f c + (z - c) • g z₀) z
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z✝ z₀ : ℂ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>h_z₀ : z₀ ∈ ball c R₁<VAR>g : ℂ → E := dslope f c<VAR>h_eq : ‖g z₀‖ = R₂ / R₁<VAR>z : ℂ<VAR>hz : z ∈ ball c R₁<VAR>h : ¬z = c<VAR>h_R₁ : 0 < R₁<GOAL>f z = (fun z => f c + (z - c) • g z₀) z
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z✝ z₀ : ℂ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>h_z₀ : z₀ ∈ ball c R₁<VAR>g : ℂ → E := dslope f c<VAR>h_eq : ‖g z₀‖ = R₂ / R₁<VAR>z : ℂ<VAR>hz : z ∈ ball c R₁<VAR>h : ¬z = c<VAR>h_R₁ : 0 < R₁<VAR>g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁<GOAL>f z = (fun z => f c + (z - c) • g z₀) z