mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.Γ_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ} (f : X ⟶ Y),
  AlgebraicGeometry.SheafedSpace.Γ.map f = f.unop.hom.c.app (Opposite.op ⊤)
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeFinset_replaceVertex_of_not_adj : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V] [inst_1 : Fintype V]
  [inst_2 : DecidableRel G.Adj],
  ¬G.Adj s t →
    (G.replaceVertex s t).edgeFinset =
      G.edgeFinset \ G.incidenceFinset t ∪ Finset.image (fun x => s(x, t)) (G.neighborFinset s)
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {A B : AlgCat R} {hom' hom'_1 : ↑A →ₐ[R] ↑B},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.justLoogleTacticImpl : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Constructions.SumProd
prod_generateFrom_generateFrom_eq : ∀ {X : Type u_5} {Y : Type u_6} {s : Set (Set X)} {t : Set (Set Y)},
  ⋃₀ s = Set.univ →
    ⋃₀ t = Set.univ → instTopologicalSpaceProd = TopologicalSpace.generateFrom (Set.image2 (fun x1 x2 => x1 ×ˢ x2) s t)
-- Init.Data.Vector.Lemmas
Vector.replicate_zero : ∀ {α : Type u_1} {a : α}, Vector.replicate 0 a = #v[]
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.instMembershipBox : {ι : Type u_1} → {I : BoxIntegral.Box ι} → Membership (BoxIntegral.Box ι) (BoxIntegral.Prepartition I)
-- Mathlib.Algebra.Order.GroupWithZero.Lex
/-- Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from
N to `WithZero (Mˣ ×ₗ Nˣ)`, which is the linearly ordered group with zero that can be identified
as their product.  -/
LinearOrderedCommGroupWithZero.inr : (α : Type u_1) →
  (β : Type u_2) →
    [inst : LinearOrderedCommGroupWithZero α] →
      [inst_1 : LinearOrderedCommGroupWithZero β] → β →*₀o WithZero (Lex (αˣ × βˣ))
-- Mathlib.Topology.Algebra.UniformConvergence
instPowUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [inst : Pow β M],
  instPowUniformOnFun = { pow := instPowUniformOnFun._aux_1 }
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin_apply : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁) (M : Matrix n n R₁)
  (x y : M₁), (((Matrix.toBilin b) M) x) y = ∑ i, ∑ j, (b.repr x) i * M i j * (b.repr y) j
-- Init.Conv
/-- `focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it.
Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred.
 -/
Lean.Parser.Tactic.Conv.focus : Lean.ParserDescr
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.iIndepSets : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {m : ι → MeasurableSpace Ω} {s : ι → Set (Set Ω)},
  (∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) →
    ProbabilityTheory.Kernel.iIndep m κ μ → ProbabilityTheory.Kernel.iIndepSets s κ μ
-- Mathlib.Tactic.Translate.Core
/-- if `f src = #[a_1, ..., a_n]` and `f tgt = #[b_1, ... b_n]` then `proceedFieldsAux src tgt f`
will insert translations from `a_i` to `b_i`.  -/
Mathlib.Tactic.Translate.proceedFieldsAux : Mathlib.Tactic.Translate.TranslateData →
  Lean.Name → Lean.Name → Mathlib.Tactic.Translate.Config → (Lean.Name → Array Lean.Name) → Lean.CoreM Unit
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {ga : α → α → α} {gb : β → β → β} {f' : β → γ}
  {gc : γ → γ → γ}, Function.Semiconj₂ f' gb gc → Function.Semiconj₂ f ga gb → Function.Semiconj₂ (f' ∘ f) ga gc
-- Mathlib.GroupTheory.PGroup
/-- **Alias** of the forward direction of `isPGroup_iff_orderOf_dvd_pow`. -/
IsPGroup.exists_orderOf_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → ∀ (g : G), ∃ k, orderOf g ∣ p ^ k
-- Mathlib.Data.Nat.ModEq
Nat.add_div_le_div_add_div_add_one : ∀ (a b c : ℕ), (a + b) / c ≤ a / c + b / c + 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, t.isEmpty = true → Std.DTreeMap.Raw.Const.getD t a fallback = fallback
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
/-- Unless a better candidate category is available, the full subcategory
of objects satisfying `t.heart` can be chosen as the heart of a t-structure `t`.  -/
CategoryTheory.Triangulated.TStructure.hasHeartFullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) → t.Heart t.heart.FullSubcategory
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α} {h_contains : (m₁.inter m₂).contains k = true},
  (m₁.inter m₂).get k h_contains = m₁.get k ⋯
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerRight_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H K : CategoryTheory.Functor C D} (α : G ⟶ H)
  (β : H ⟶ K) (F : CategoryTheory.Functor D E) {Z : CategoryTheory.Functor C E} (h : K.comp F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α F)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β F) h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_filter_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl = true ↔
    ∃ (h' : Std.DTreeMap.Internal.Impl.contains k t = true),
      f (t.getKey k h') (Std.DTreeMap.Internal.Impl.Const.get t k h') = true
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.transpose_adjMatrix : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Zero α] [inst_2 : One α],
  (SimpleGraph.adjMatrix α G).transpose = SimpleGraph.adjMatrix α G
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.f_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i j : self.J),
  CategoryTheory.Mono (self.f i j)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.functorToCore_obj_of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  (F : CategoryTheory.Functor G C) (X : G), ((CategoryTheory.Core.functorToCore F).obj X).of = F.obj X
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyFunctor_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C],
  (CategoryTheory.ShortComplex.leftHomologyFunctor C).Additive
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rcc_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n + 1 - m).toNat → (m...=n).toList[i]? = some (m + ↑i)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsLoop.eq_1 : ∀ {α : Type u_1} (H : Hypergraph α) (e : Set α), H.IsLoop e = (e ∈ H.edgeSet ∧ ∃ x, e = {x})
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleighQuotient_neg_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E), (-T).rayleighQuotient x = -T.rayleighQuotient x
-- Mathlib.GroupTheory.QuotientGroup.Finite
finite_iff_subgroup_quotient : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), Finite G ↔ Finite ↥H ∧ Finite (G ⧸ H)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- **Alias** of the reverse direction of `isUnit_cfc_iff`. -/
isUnit_cfc : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) isUnit_cfc_iff._auto_1 →
    autoParam (p a) isUnit_cfc_iff._auto_3 → (∀ x ∈ spectrum R a, f x ≠ 0) → IsUnit (cfc f a)
-- Mathlib.Algebra.Module.ZLattice.Summable
/-- If `L` is a `ℤ`-lattice with rank `d` in `E`, then `∑ z ∈ L, ‖z‖ʳ` converges when `r < -d`.  -/
ZLattice.summable_norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L], ∀ r < -↑(Module.finrank ℤ ↥L), Summable fun z => ‖z‖ ^ r
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_univ_inv_one_add_sq : ∫ (x : ℝ), (1 + x ^ 2)⁻¹ = Real.pi
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_min?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → t.min?.isSome = true
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.Bijective ⇑(AlgebraicGeometry.StructureSheaf.toOpenₗ R M ⊤)
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_le_ofNat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ} [inst_5 : n.AtLeastTwo], ↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.of_mulIndicator_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : One β] {s : Set α} {c : β},
  Filter.EventuallyConst (s.mulIndicator fun x => c) l → c ≠ 1 → Filter.EventuallyConst s l
-- Mathlib.Data.Finset.Sort
Finset.sort_cons : ∀ {α : Type u_1} {s : Finset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] {a : α},
  (∀ b ∈ s, r a b) → ∀ (h₂ : a ∉ s), (Finset.cons a s h₂).sort r = a :: s.sort r
-- Init.GrindInstances.Ring.UInt
UInt16.intCast_neg : ∀ (x : ℤ), ↑(-x) = -↑x
-- Lean.Declaration
Lean.ConstantInfo.recInfo.inj : ∀ {val val_1 : Lean.RecursorVal}, Lean.ConstantInfo.recInfo val = Lean.ConstantInfo.recInfo val_1 → val = val_1
-- Mathlib.Algebra.GCDMonoid.Basic
subsingleton_normalizedGCDMonoid_of_unique_units : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [Subsingleton αˣ], Subsingleton (NormalizedGCDMonoid α)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.Const.beqModel.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : BEq β] (l₁ l₂ : List ((_ : α) × β)),
  Std.Internal.List.Const.beqModel l₁ l₂ =
    if l₁.length ≠ l₂.length then false else l₁.all fun x => Std.Internal.List.getValue? x.fst l₂ == some x.snd
-- Mathlib.MeasureTheory.Integral.Pi
/-- A version of **Fubini's theorem** with the variables indexed by a general finite type.  -/
MeasureTheory.integral_fintype_prod_volume_eq_prod : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {E : ι → Type u_3} (f : (i : ι) → E i → 𝕜)
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (E i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume],
  ∫ (x : (i : ι) → E i), ∏ i, f i (x i) = ∏ i, ∫ (x : E i), f i x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_eq_zero_iff_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 3] [IsReduced R],
  W.j = 0 ↔ W.b₂ = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.cpow_inv_two_im_eq_neg_sqrt : ∀ {x : ℂ}, x.im < 0 → (x ^ 2⁻¹).im = -√((‖x‖ - x.re) / 2)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSeparatedFor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w))
  (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.IsSeparatedFor P R =
    ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R) (t₁ t₂ : P.obj (Opposite.op X)),
      x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoPushout_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) h.isoPushout.inv = inr
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.matrixOfPolynomials_blockTriangular : ∀ {R : Type u_9} [inst : Semiring R] {n : ℕ} (p : Fin n → Polynomial R),
  (∀ (i : Fin n), (p i).natDegree ≤ ↑i) → (Matrix.of fun i j => (p j).coeff ↑i).BlockTriangular id
-- Mathlib.Algebra.Field.Defs
/-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

Do not use this lemma directly. Use `NNRat.smul_def` instead.  -/
DivisionSemiring.nnqsmul_def : ∀ {K : Type u_2} [self : DivisionSemiring K] (q : ℚ≥0) (a : K), DivisionSemiring.nnqsmul q a = ↑q * a
-- Mathlib.Probability.Martingale.Convergence
/-- If a martingale `f` strongly adapted to `ℱ` converges in L¹ to `g`, then for all `n`, `f n` is
almost everywhere equal to `𝔼[g | ℱ n]`.  -/
MeasureTheory.Martingale.eq_condExp_of_tendsto_eLpNorm : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {g : Ω → ℝ}
  {μ : MeasureTheory.Measure Ω},
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.Integrable g μ →
      Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0) →
        ∀ (n : ℕ), f n =ᵐ[μ] μ[g | ↑ℱ n]
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_lt_toNNReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toNNReal < b.toNNReal ↔ a < b)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Neg
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastNeg : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Add several complete matches.  -/
Aesop.ForwardRuleMatches.insertMany : Array Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatches → Aesop.ForwardRuleMatches
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The induction step for the existence and uniqueness of the
circumcenter.  Given a nonempty set of points in a nonempty affine
subspace whose direction is complete, such that there is a unique
(circumcenter, circumradius) pair for those points in that subspace,
and a point `p` not in that subspace, there is a unique (circumcenter,
circumradius) pair for the set with `p` added, in the span of the
subspace with `p` added.  -/
EuclideanGeometry.existsUnique_dist_eq_of_insert : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [s.direction.HasOrthogonalProjection] {ps : Set P},
  ps.Nonempty →
    ∀ {p : P},
      ps ⊆ ↑s →
        p ∉ s →
          (∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius) →
            ∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.four_nsmul_coPolarization_compl_polarization_apply_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (i : ι),
  (4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
    ((P.RootForm (P.root i)) (P.root i) * (P.CorootForm (P.coroot i)) (P.coroot i)) • P.root i
-- Mathlib.Topology.Category.Compactum
/-- The forgetful functor to TypeCat  -/
Compactum.forget : CategoryTheory.Functor Compactum (Type u_1)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.writes.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Fintype Γ] (a : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.writes (Turing.TM1.Stmt.branch a q₁ q₂) = Turing.TM1to1.writes q₁ ∪ Turing.TM1to1.writes q₂
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.parentDeclCtx.injEq : ∀ (parentDecl parentDecl_1 : Lean.Name),
  (Lean.Elab.PartialContextInfo.parentDeclCtx parentDecl = Lean.Elab.PartialContextInfo.parentDeclCtx parentDecl_1) =
    (parentDecl = parentDecl_1)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.off : Lean.Lsp.Trace
-- Std.Data.TreeMap.Raw.Basic
/-- Returns the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.TreeMap.Raw.keyAtIdx? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → ℕ → Option α
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.mk.sizeOf_spec : ∀ {aig : Std.Sat.AIG ℕ} (cnf : Std.Sat.CNF ℕ) (cache : Std.Sat.AIG.toCNF.Cache✝ aig cnf)
  (inv : Std.Sat.AIG.toCNF.State.Inv✝ aig cnf),
  sizeOf { cnf := cnf, cache := cache, inv := inv } = 1 + sizeOf cnf + sizeOf cache
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_mul_X_pow_eq_monomial : ∀ {R : Type u_1} [inst : Semiring R] {a : R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R] ⦃n : ℕ⦄,
  SkewPolynomial.C a * SkewPolynomial.X ^ n = (SkewPolynomial.monomial n) a
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.op_comp_isSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {A : Type u} [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K]
  (G : CategoryTheory.Sheaf K A), CategoryTheory.Presheaf.IsSheaf J (F.op.comp G.obj)
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- The tensor product of two coalgebra morphisms as a coalgebra morphism.  -/
Coalgebra.TensorProduct.map : {R : Type u_5} →
  {S : Type u_6} →
    {M : Type u_7} →
      {N : Type u_8} →
        {P : Type u_9} →
          {Q : Type u_10} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring S] →
                [inst_2 : Algebra R S] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : AddCommMonoid N] →
                      [inst_5 : AddCommMonoid P] →
                        [inst_6 : AddCommMonoid Q] →
                          [inst_7 : Module R M] →
                            [inst_8 : Module R N] →
                              [inst_9 : Module R P] →
                                [inst_10 : Module R Q] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : IsScalarTower R S M] →
                                      [inst_13 : Coalgebra S M] →
                                        [inst_14 : Module S N] →
                                          [inst_15 : IsScalarTower R S N] →
                                            [inst_16 : Coalgebra S N] →
                                              [inst_17 : Coalgebra R P] →
                                                [inst_18 : Coalgebra R Q] →
                                                  (M →ₗc[S] N) →
                                                    (P →ₗc[R] Q) → TensorProduct R M P →ₗc[S] TensorProduct R N Q
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant : {n : ℕ} →
  (original_assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
    original_assignments.size = n →
      Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
        (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) → assignments.size = n → Prop
-- Mathlib.Order.SymmDiff
Disjoint.le_symmDiff_sup_symmDiff_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, Disjoint a b → c ≤ symmDiff a c ⊔ symmDiff b c
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The Relation on `Prequotient` saying when two expressions are equal
because of the commutative ring laws, or
because one element is mapped to another by a morphism in the diagram.
 -/
CommRingCat.Colimits.Relation : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F → Prop
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.induction_on : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M),
  (∀ (a : R), P ((algebraMap R (DividedPowerAlgebra R M)) a)) →
    (∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)) →
      (∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * DividedPowerAlgebra.dp R n m)) → P f
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A fully faithful functor reflects limits.  -/
CategoryTheory.Limits.fullyFaithful_reflectsLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The adjunction between the free and forgetful constructions for Eilenberg-Moore algebras for
a monad. cf Lemma 5.2.8 of [Riehl][riehl2017].  -/
CategoryTheory.Monad.adj : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (T : CategoryTheory.Monad C) → T.free ⊣ T.forget
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Mk₁.obj.match_1.eq_1 : ∀ (motive : Fin 2 → Sort u_1) (isLt : 0 < 2) (h_1 : (isLt : 0 < 2) → motive ⟨0, isLt⟩)
  (h_2 : (isLt : 1 < 2) → motive ⟨1, isLt⟩),
  (match ⟨0, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨1, isLt⟩ => h_2 isLt) =
    h_1 isLt
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced)
  (hr : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size),
  Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr =
    match r, hr, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hr, hlr =>
      { k := k, v := v, tree := { impl := l, balanced_impl := hl, size_impl := ⋯ } }
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hr, hlr =>
      match Std.DTreeMap.Internal.Impl.maxView k' v' l' r' ⋯ ⋯ ⋯ with
      | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
        { k := dk, v := dv,
          tree :=
            { impl := Std.DTreeMap.Internal.Impl.balanceLErase k v l dt ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ } }