ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Nonempty F.M<VAR>bisim : IsBisimulation R<VAR>inhabited_h : Inhabited F.M<VAR>s₁ s₂ : F.M<VAR>Hr : R s₁ s₂<GOAL>s₁ = s₂
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Nonempty F.M<VAR>bisim : IsBisimulation R<VAR>inhabited_h : Inhabited F.M<VAR>s₁ s₂ : F.M<VAR>Hr : R s₁ s₂<GOAL>∀ (ps : Path F), iselect ps s₁ = iselect ps s₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(imageUnopOp g).inv ≫ (factorThruImage g.unop).op = image.ι g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<GOAL>(d n A) f g = (diagonalHomEquiv (n + 1) A) ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<GOAL>(d n A) f g = ((diagonalHomEquiv n A).symm f).hom ((resolution.d k G (n + 1)) (Finsupp.single (Fin.partialProd g) 1))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<GOAL>(d n A) f g = ((diagonalHomEquiv n A).symm f).hom (∑ p : Fin (n + 1 + 1), Finsupp.single (Fin.partialProd g ∘ p.succAbove) ((-1) ^ ↑p))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<GOAL>(d n A) f g = ∑ x : Fin (n + 1 + 1), ((diagonalHomEquiv n A).symm f).hom ((-1) ^ ↑x • Finsupp.single (Fin.partialProd g ∘ x.succAbove) 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<GOAL>(A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g) = (A.ρ ((Fin.partialProd g ∘ Fin.succ) 0)) (f fun i => ((Fin.partialProd g ∘ Fin.succ) i.castSucc)⁻¹ * (Fin.partialProd g ∘ Fin.succ) i.succ) + ∑ i : Fin (n + 1), ((diagonalHomEquiv n A).symm f).hom ((-1) ^ ↑i.succ • Finsupp.single (Fin.partialProd g ∘ i.succ.succAbove) 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<GOAL>(A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g) = (A.ρ (g 0)) (f fun i => (Fin.partialProd g i.castSucc.castSucc * g i.castSucc)⁻¹ * (Fin.partialProd g i.succ.castSucc * g i.succ)) + ∑ i : Fin (n + 1), ((diagonalHomEquiv n A).symm f).hom ((-1) ^ ↑i.succ • Finsupp.single (Fin.partialProd g ∘ i.succ.succAbove) 1)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<GOAL>wrepr ((P F).wMk a f' f) = (P F).wMk' (repr (abs ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<GOAL>((P F).wMk' ∘ repr) (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, splitFun f' f⟩)) = (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : Absorbent ℝ s<VAR>ha : 0 ≤ a<VAR>x : E<GOAL>x ∈ {x | gauge s x ≤ a} ↔ x ∈ ⋂ r, ⋂ (_ : a < r), r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : Absorbent ℝ s<VAR>ha : 0 ≤ a<VAR>x : E<GOAL>gauge s x ≤ a ↔ ∀ (i : ℝ), a < i → x ∈ i • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : Absorbent ℝ s<VAR>ha : 0 ≤ a<VAR>x : E<VAR>h : gauge s x ≤ a<VAR>r : ℝ<VAR>hr : a < r<GOAL>x ∈ r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : Absorbent ℝ s<VAR>ha : 0 ≤ a<VAR>x : E<VAR>h : ∀ (i : ℝ), a < i → x ∈ i • s<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>gauge s x < a + ε
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a b - b = -toIcoDiv hp a b • p
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>hd : DiffContOnCl ℂ f (ball z (dist w z))<VAR>hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z<GOAL>‖f w‖ = ‖f z‖
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>w : ℂ<VAR>hd : DiffContOnCl ℂ f (ball w (dist w w))<VAR>hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w<GOAL>‖f w‖ = ‖f w‖
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>hd : DiffContOnCl ℂ f (ball z (dist w z))<VAR>hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z<VAR>hne : w ≠ z<GOAL>‖f w‖ = ‖f z‖
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>hd : DiffContOnCl ℂ f (ball z (dist w z))<VAR>hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z<VAR>hne : dist w z ≠ 0<GOAL>‖f w‖ = ‖f z‖
<VAR>α✝ : Type u_1<VAR>σ : Type u_2<VAR>inst✝³ : Primcodable α✝<VAR>inst✝² : Primcodable σ<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>n : ℕ<GOAL>Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => (Nat.unpair (Nat.pair z y)).2.succ) (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1)))) (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) = encode (Option.map Prod.snd (decode n))
<VAR>α✝ : Type u_1<VAR>σ : Type u_2<VAR>inst✝³ : Primcodable α✝<VAR>inst✝² : Primcodable σ<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>n : ℕ<GOAL>Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => n.succ) (encode (decode (Nat.unpair n).2))) (encode (decode (Nat.unpair n).1)) = encode (Option.map Prod.snd ((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝³ : AddCommMonoid α<VAR>inst✝² : Neg β<VAR>inst✝¹ : DivisionSemiring γ<VAR>inst✝ : Module γ α<VAR>h : Antiperiodic f c<VAR>a : γ<VAR>ha : a ≠ 0<VAR>x : α<GOAL>(fun x => f (a • x)) (x + a⁻¹ • c) = -(fun x => f (a • x)) x
<VAR>R✝ : Type u<VAR>S : Type v<VAR>A✝ : Type w<VAR>B : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Semiring A✝<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R✝ B<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝ : Semiring A<VAR>P Q : Algebra R A<VAR>h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r<GOAL>P = Q
<VAR>R✝ : Type u<VAR>S : Type v<VAR>A✝ : Type w<VAR>B : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Semiring A✝<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R✝ B<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝ : Semiring A<VAR>P Q : Algebra R A<VAR>h : toRingHom = toRingHom<GOAL>P = Q
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x + y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity (↑p) (x ^ n + y ^ n) = multiplicity (↑p) (x + y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - -y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity (↑p) (x ^ n + y ^ n) = multiplicity (↑p) (x + y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - -y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity (↑p) (x ^ n - (-y) ^ n) = multiplicity (↑p) (x - -y) + multiplicity p n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>x✝ : E<GOAL>x✝ ∈ parallelepiped v ↔ x✝ ∈ ∑ i : ι, segment ℝ 0 (v i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>x✝ : E<GOAL>(∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i : ι, t i • v i) ↔ ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = x✝
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁵ : CommRing R₂<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v✝ : ι' → M<VAR>i✝ : ι<VAR>j : ι'<VAR>S : Type u_9<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>v : ι' → S<VAR>i : ι'<GOAL>(⇑b ᵥ* (b.toMatrix v).map ⇑(algebraMap R S)) i = v i
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n : ℕ<GOAL>↑(↑(n + 1))⁻¹ = (↑(n + 1))⁻¹
<VAR>D : GlueData<VAR>i : D.J<GOAL>D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫ ((PresheafedSpace.forget CommRingCat).mapIso (SheafedSpace.forgetToPresheafedSpace.mapIso (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫ D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace) ≪≫ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso (PresheafedSpace.forget CommRingCat)).inv = (D.ι i).val.base
<VAR>D : GlueData<VAR>i : D.J<GOAL>(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i ≫ D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫ (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).base = (D.ι i).val.base
<VAR>D : GlueData<VAR>i : D.J<GOAL>((D.toLocallyRingedSpaceGlueData.ι i).val ≫ (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).base = (D.ι i).val.base
<VAR>D : GlueData<VAR>i : D.J<GOAL>(D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).val.base = (D.ι i).val.base
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (oddKernel a) (Ioi 0)
<VAR>a : ℝ<GOAL>ContinuousOn (oddKernel ↑a) (Ioi 0)
<VAR>a : ℝ<GOAL>ContinuousOn (fun x => ↑(oddKernel (↑a) x)) (Ioi 0)
<VAR>a : ℝ<GOAL>ContinuousOn (fun x => cexp (-↑π * ↑a ^ 2 * ↑x) * (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))) (Ioi 0)
<VAR>a x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>Continuous fun x => cexp (-↑π * ↑a ^ 2 * ↑x)
<VAR>a x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>ContinuousAt (fun x => jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)) x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>e : M₁ ≃ₗ[R] M<VAR>f : Module.End R M<GOAL>B.IsPairSelfAdjoint F f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>e : M₁ ≃ₗ[R] M<VAR>f : Module.End R M<VAR>hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e<GOAL>B.IsPairSelfAdjoint F f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>e : M₁ ≃ₗ[R] M<VAR>f : Module.End R M<VAR>hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e<VAR>hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e<GOAL>B.IsPairSelfAdjoint F f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>e : M₁ ≃ₗ[R] M<VAR>f : Module.End R M<VAR>hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e<VAR>hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e<VAR>he : Function.Surjective ⇑↑e<GOAL>B.IsPairSelfAdjoint F f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) (e.symm.conj f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>toIocMod hp a (a + p) = a + p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>a < a + p ∧ ∃ z, a + p = a + p + z • p
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>(range ENNReal.toEReal).OrdConnected
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>(Ici 0).OrdConnected
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>f✝ g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>f : X ≅ Y<GOAL>inv f.inv = f.hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>f✝ g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>f : X ≅ Y<GOAL>f.inv ≫ f.hom = 𝟙 Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>a : M<GOAL>a ^ (n - 1) * a = a ^ n
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>x : (a : ι) → π a<VAR>hi : i.Finite<VAR>hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)<GOAL>i.pi s ∈ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>x : (a : ι) → π a<VAR>hi : i.Finite<VAR>hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)<GOAL>∀ i_1 ∈ i, eval i_1 ⁻¹' s i_1 ∈ 𝓝 x
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>s t : SetSemiring A<GOAL>span R (SetSemiring.down (s * t)) = span R (SetSemiring.down s) * span R (SetSemiring.down t)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>inst✝ : DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<VAR>a✝ : ι<GOAL>a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>inst✝ : DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<VAR>a✝ : ι<GOAL>¬f a✝ ⊓ g a✝ = 0 ↔ ¬f a✝ = 0 ∧ ¬g a✝ = 0
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<GOAL>map f ⁅I₁, I₂⁆ ≤ ⁅map f I₁, map f I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<GOAL>⁅I₁, I₂⁆ ≤ comap f ⁅map f I₁, map f I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑(comap f ⁅map f I₁, map f I₂⁆)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>x y₁ : L<VAR>hy₁ : y₁ ∈ I₁<VAR>y₂ : L<VAR>hy₂ : y₂ ∈ I₂<VAR>hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x<GOAL>⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>x y₁ : L<VAR>hy₁ : y₁ ∈ I₁<VAR>y₂ : L<VAR>hy₂ : y₂ ∈ I₂<VAR>hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x<VAR>fy₁ : ↥(map f I₁) := ⟨f y₁, ⋯⟩<GOAL>⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>x y₁ : L<VAR>hy₁ : y₁ ∈ I₁<VAR>y₂ : L<VAR>hy₂ : y₂ ∈ I₂<VAR>hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x<VAR>fy₁ : ↥(map f I₁) := ⟨f y₁, ⋯⟩<VAR>fy₂ : ↥(map f I₂) := ⟨f y₂, ⋯⟩<GOAL>⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>x y₁ : L<VAR>hy₁ : y₁ ∈ I₁<VAR>y₂ : L<VAR>hy₂ : y₂ ∈ I₂<VAR>hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x<VAR>fy₁ : ↥(map f I₁) := ⟨f y₁, ⋯⟩<VAR>fy₂ : ↥(map f I₂) := ⟨f y₂, ⋯⟩<GOAL>⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ comap f ⁅map f I₁, map f I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>x y₁ : L<VAR>hy₁ : y₁ ∈ I₁<VAR>y₂ : L<VAR>hy₂ : y₂ ∈ I₂<VAR>hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x<VAR>fy₁ : ↥(map f I₁) := ⟨f y₁, ⋯⟩<VAR>fy₂ : ↥(map f I₂) := ⟨f y₂, ⋯⟩<GOAL>⁅f y₁, f y₂⁆ ∈ ⁅map f I₁, map f I₂⁆
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α<VAR>s : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : Countable α<VAR>h : MeasurableSingletonClass α<GOAL>(Measure.dirac a).toPMF = pure a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.reverse.coeff 0 = f.leadingCoeff
<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>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y'<VAR>h : F.obj X' ⟶ Y<VAR>k : Y ⟶ Y'<VAR>w : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k<GOAL>F.map f ≫ g = h ≫ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>this✝ : Fintype α<VAR>this : Fintype β<GOAL>Nat.card β ≤ Nat.card α
<VAR>n m : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ last n<GOAL>j ≤ i.castPred hi ↔ j.castSucc ≤ i
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(gammaCDFReal a r) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<VAR>this : IsProbabilityMeasure (gammaMeasure a r)<GOAL>↑(gammaCDFReal a r) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<VAR>this : IsProbabilityMeasure (gammaMeasure a r)<GOAL>((gammaMeasure a r) (Iic x)).toReal = (∫⁻ (x : ℝ) in Iic x, ENNReal.ofReal (gammaPDFReal a r x)).toReal
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : AddGroupWithOne R<VAR>inst✝ : Fintype R<GOAL>↑(card R) = 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ : Multiset α<VAR>β : Type u_2<VAR>m : Multiset α<VAR>f : α → β<GOAL>map (fun x => f x.fst) Finset.univ.val = map f m
<VAR>α ι : Type u<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<GOAL>#↑t ≤ a
<VAR>α ι : Type u<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<VAR>ha : a < ℵ₀<GOAL>#↑t ≤ a
<VAR>α ι : Type u<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<VAR>ha : ℵ₀ ≤ a<GOAL>#↑t ≤ a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : Submodule R M<VAR>h : p < ⊤<GOAL>Nontrivial (M ⧸ p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x✝ y : M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : Submodule R M<VAR>h : p < ⊤<VAR>x : M<VAR>left✝ : x ∈ ⊤<VAR>not_mem_s : x ∉ p<GOAL>Nontrivial (M ⧸ p)