mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastCpopLayer : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len w iterNum : ℕ} {assign : α → Bool} (aig : Std.Sat.AIG α)
  (oldLayer : aig.RefVec (len * w)) (oldLayerBv : BitVec (len * w)) (hold' : 2 * (iterNum - 1) < len),
  (∀ (idx : ℕ) (hidx : idx < len * w),
      ⟦assign, { aig := aig, ref := oldLayer.get idx hidx }⟧ = oldLayerBv.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < (len + 1) / 2 * w),
      ⟦assign,
          {
            aig :=
              (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer aig
                  { w := w, len := len, oldLayer := oldLayer, h := ⋯, hlen := ⋯ }).aig,
            ref :=
              (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer aig
                      { w := w, len := len, oldLayer := oldLayer, h := ⋯, hlen := ⋯ }).vec.get
                idx hidx }⟧ =
        (oldLayerBv.cpopLayer 0#(0 * w) ⋯).getLsbD idx
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.rTensorOne_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submodule R S}
  (y : R) (m : ↥M), M.rTensorOne (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • m
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The subpresheaf of dependent functions on `X` satisfying the "pre-local" predicate `P`.
 -/
TopCat.subpresheafToTypes : {X : TopCat} → {T : ↑X → Type u_1} → TopCat.PrelocalPredicate T → TopCat.Presheaf (Type (max u_1 u_2)) X
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Adding an angle to that with the order of the points reversed results in 0.  -/
EuclideanGeometry.oangle_add_oangle_rev : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), EuclideanGeometry.oangle p₁ p₂ p₃ + EuclideanGeometry.oangle p₃ p₂ p₁ = 0
-- Init.Data.Fin.Lemmas
Fin.eq_zero_or_eq_succ : ∀ {n : ℕ} (i : Fin (n + 1)), i = 0 ∨ ∃ j, i = j.succ
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoToHomologicalComplex_obj_X : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β),
  ((HomologicalComplex.dgoToHomologicalComplex b V).obj X).X i = X.obj i
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_filter_containsKey_of_perm : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ l₃ : List ((a : α) × β a)} [inst : BEq α] [EquivBEq α],
  l₂.Perm l₃ →
    Std.Internal.List.DistinctKeys l₁ →
      (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).Perm
        (List.filter (fun p => Std.Internal.List.containsKey p.fst l₃) l₁)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instPowNat : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module A V] → (ρ : Representation A G V) → Pow (ρ.IntertwiningMap ρ) ℕ
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instCoeAdjoinAuxInsertSet : ∀ {α : Type u_1} (x : α) (s : Set α), Algebra.CoeAdjoinAux x (insert x s)
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccAboveEquiv.eq_1 : ∀ {n : ℕ} (p : Fin (n + 1)), finSuccAboveEquiv p = (Equiv.optionSubtype p) ⟨(finSuccEquiv' p).symm, ⋯⟩
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.mono_null : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {s t : Set Ω} (μ : MeasureTheory.FiniteMeasure Ω), s ⊆ t → μ t = 0 → μ s = 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.disjoint_sum_left : ∀ {α : Type u_6} {a : Multiset α} {i : Multiset (Multiset α)}, Disjoint i.sum a ↔ ∀ b ∈ i, Disjoint b a
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_add : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f g : CentroidHom α), ⇑(f + g) = ⇑f + ⇑g
-- Std.Time.Format.Modifier
Std.Time.Modifier.z.sizeOf_spec : ∀ (presentation : Std.Time.ZoneName), sizeOf (Std.Time.Modifier.z presentation) = 1 + sizeOf presentation
-- Lean.Data.Lsp.Basic
/-- Additional information that describes document changes.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textEdit)  -/
Lean.Lsp.ChangeAnnotation : Type
-- Mathlib.AlgebraicTopology.SingularSet
/-- If `X : TopCat.{u}` and `n : SimplexCategoryᵒᵖ`,
then `(toSSet.obj X).obj n` identifies to the type of continuous
maps from the standard simplex `stdSimplex ℝ (Fin (n.unop.len + 1))` to `X`.  -/
TopCat.toSSetObjEquiv : (X : TopCat) →
  (n : SimplexCategoryᵒᵖ) → (TopCat.toSSet.obj X).obj n ≃ C(↑(stdSimplex ℝ (Fin ((Opposite.unop n).len + 1))), ↑X)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] {d d' : D}
  (f : d ⟶ d') (c : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c)
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d' c) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c))
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_fn_apply : ∀ {R : Type u} [inst : CommSemiring R] {X : Type u_3} (g : Polynomial R) (f : X → R) (x : X),
  (Polynomial.aeval f) g x = (Polynomial.aeval (f x)) g
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- If a morphism of short complexes `φ : S₁ ⟶ S₂` is such that `φ.τ₁` is epi, `φ.τ₂` is an iso,
and `φ.τ₃` is mono, then the induced morphism on right homology is an isomorphism.  -/
CategoryTheory.ShortComplex.instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap φ)
-- Lean.Parser.Types
Lean.Parser.ParserState.mkErrorAt : Lean.Parser.ParserState → String → String.Pos.Raw → optParam (Option ℕ) none → Lean.Parser.ParserState
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- Reinterpret `x : α` as an element of `Multiplicative α`.  -/
Multiplicative.ofAdd : {α : Type u} → α ≃ Multiplicative α
-- Lean.DocString.Types
Lean.Doc.instHashableMathMode : Hashable Lean.Doc.MathMode
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_cancel : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (a : M) (b c : ↥S), f.mk' (a + ↑c) (b + c) = f.mk' a b
-- Init.Try
/-- If `only` is `true`, generates solutions using `grind only` and `simp only`.  -/
Lean.Try.Config.only : Lean.Try.Config → Bool
-- Mathlib.Topology.Baire.BaireMeasurable
MeasurableSet.baireMeasurableSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} [inst_1 : MeasurableSpace α] [BorelSpace α],
  MeasurableSet s → BaireMeasurableSet s
-- Mathlib.Algebra.Lie.TraceForm
/-- Note that this result is slightly stronger than it might look at first glance: we only assume
that `N` is trivial over `I` rather than all of `L`. This means that it applies in the important
case of an Abelian ideal (which has `M = L` and `N = I`).  -/
LieSubmodule.traceForm_eq_zero_of_isTrivial : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M),
  ∀ I ≤ N.idealizer,
    ∀ (x : L) {y : L},
      y ∈ I →
        ∀ [LieModule.IsTrivial ↥I ↥N],
          (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) = 0
-- Mathlib.Order.FixedPoints
OrderHom.gfp_induction : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {p : α → Prop},
  (∀ (a : α), p a → OrderHom.gfp f ≤ a → p (f a)) → (∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) → p (OrderHom.gfp f)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.size.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (sz : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β)
  (h_1 :
    (sz : ℕ) →
      (k : α) →
        (v : β k) → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner sz k v l r))
  (h_2 : Unit → motive Std.DTreeMap.Internal.Impl.leaf),
  (match Std.DTreeMap.Internal.Impl.inner sz k v l r with
    | Std.DTreeMap.Internal.Impl.inner sz k v l r => h_1 sz k v l r
    | Std.DTreeMap.Internal.Impl.leaf => h_2 ()) =
    h_1 sz k v l r
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.posSemidef_tfae : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)},
  [K.PosSemidef,
      K.IsHermitian ∧
        ∀ (f : X × V →₀ 𝕜),
          0 ≤
            RCLike.re
              (f.sum fun xv z => f.sum fun xv' w => (starRingEnd 𝕜) z * w * inner 𝕜 ((K xv'.1 xv.1) xv.2) xv'.2),
      K.IsHermitian ∧
        ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w => vv.sum fun x' w' => inner 𝕜 ((K x' x) w) w')].TFAE
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_top : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (x : M), x ∈ ⊤
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiff.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiff 𝕜 n f → ContDiff 𝕜 n g → (∀ (x : E), g x ≠ 0) → ContDiff 𝕜 n (f / g)
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toList_keysIter : ∀ {α : Type u} {β : α → Type u} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keysIter.toList = m.keys
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.subalgebra.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.EssFiniteType R S],
  Algebra.EssFiniteType.subalgebra R S = Algebra.adjoin R ↑(Algebra.EssFiniteType.finset R S)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.minKey! (Std.Internal.List.insertEntry k v l) =
        (Std.Internal.List.minKey? l).elim k fun k' => if (compare k k').isLE = true then k else k'
-- Mathlib.RingTheory.Congruence.Hom
/-- The uniqueness part of the universal property for quotients of rings.  -/
RingCon.lift_unique : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  (H : c ≤ RingCon.ker f) (g : c.Quotient →+* P), g.comp c.mk' = f → g = c.lift f H
-- Lean.Data.Json.Basic
Lean.Json.str.inj : ∀ {s s_1 : String}, Lean.Json.str s = Lean.Json.str s_1 → s = s_1
-- Mathlib.Order.Defs.LinearOrder
lt_of_not_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬b ≤ a → a < b
-- Init.Internal.Order.Basic
Lean.Order.Example.find_eq : ∀ {P : ℕ → Bool}, Lean.Order.Example.find P = Lean.Order.Example.findF P (Lean.Order.Example.find P)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.notMem_support_iff : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {p : SkewPolynomial R}, n ∉ p.support ↔ p.coeff n = 0
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- A composition induces a partition (just convert the list to a multiset).  -/
Nat.Partition.ofComposition : (n : ℕ) → Composition n → n.Partition
-- Mathlib.RingTheory.Localization.Cardinality
IsLocalization.lift_cardinalMk : ∀ {R : Type u} [inst : CommRing R] (L : Type v) [inst_1 : CommRing L] [inst_2 : Algebra R L] (S : Submonoid R)
  [IsLocalization S L],
  S ≤ nonZeroDivisors R → Cardinal.lift.{u, v} (Cardinal.mk L) = Cardinal.lift.{v, u} (Cardinal.mk R)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.exists_insert_toList_zoom_nil : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {p : RBTree.RBNode.Path α} {v : α}
  {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.zoom (cmp v) t = (RBTree.RBNode.nil, p) →
      ∃ L R, t.toList = L ++ R ∧ (RBTree.RBNode.insert cmp t v).toList = L ++ v :: R
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instInhabitedDecl.default : {α : Type} → Std.Sat.AIG.Decl α
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodE : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          (b₁ : LieAlgebra.Basis ι₁ H₁) →
                            [inst_6 : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} →
                                (b₂ : LieAlgebra.Basis ι₂ H₂) → ι₁ → ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.comp_epiDesc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Epi f] {T : C} (g : X ⟶ T)
  (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0) {Z : C} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.epiDesc f g hg) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ‖(starRingEnd K) z‖ = ‖z‖
-- Mathlib.Tactic.Simps.Basic
/-- syntax that provided `newName`  -/
Simps.ParsedProjectionData.newStx : Simps.ParsedProjectionData → Lean.Syntax
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opHom_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : (CategoryTheory.Functor C D)ᵒᵖ} (α : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.opHom C D).map α).app X_1 = (α.unop.app (Opposite.unop X_1)).op
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousLinearMap.isBoundedLinearMap_comp_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (g : F →L[𝕜] G),
  IsBoundedLinearMap 𝕜 fun f => g ∘SL f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse.map_mul : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a b : CliffordAlgebra Q),
  CliffordAlgebra.reverse (a * b) = CliffordAlgebra.reverse b * CliffordAlgebra.reverse a
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.hashEMatchTheoremPtr : Lean.Meta.Grind.EMatchTheorem → UInt64
-- Batteries.Data.Array.Match
/-- Matcher state.  -/
Array.Matcher.Iterator.state : {σ : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {α : Type u_1} →
      [inst : BEq α] →
        {m : Array.Matcher α} → [inst_1 : Std.Iterator σ n α] → Array.Matcher.Iterator σ n α m → Fin (m.table.size + 1)
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.setTag.sizeOf_spec : ∀ (x : Lean.IR.VarId) (cidx : ℕ) (b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.setTag x cidx b) = 1 + sizeOf x + sizeOf cidx + sizeOf b
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.nontrivial_iff : ∀ {α : Type u_1} {n : ℕ} [Finite α], Nontrivial ↑(Set.powersetCard α n) ↔ 0 < n ∧ n < Nat.card α
-- Lean.LibrarySuggestions.SymbolFrequency
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.instZeroNameMapNat : Zero (Lean.NameMap ℕ)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- A Lie-Rinehart subalgebra forms a Lie ring.  -/
LieRinehartSubalgebra.lieRing : (A : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing A] → [inst_1 : LieRing L] → [inst_2 : Module A L] → (L' : LieRinehartSubalgebra A L) → LieRing ↥L'
-- Mathlib.Topology.Constructions.SumProd
/-- If `f x y` is continuous in `x` for all `y ∈ s`,
then the set of `x` such that `f x` maps `s` to `t` is closed.  -/
IsClosed.setOfPred_mapsTo : ∀ {X : Type u} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {α : Type u_5} {f : X → α → Z}
  {s : Set α} {t : Set Z}, IsClosed t → (∀ a ∈ s, Continuous fun x => f x a) → IsClosed {x | Set.MapsTo (f x) s t}
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.ball_openSubgroup.eq_1 : ∀ (S : Type u_1) [inst : SeminormedGroup S] [inst_1 : IsUltrametricDist S] {r : ℝ} (hr : 0 < r),
  IsUltrametricDist.ball_openSubgroup S hr =
    { carrier := Metric.ball 1 r, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯, isOpen' := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.root_mem_or_neg_mem : ∀ {ι : 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} (self : P.Base)
  (i : ι),
  P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑self.support) ∨
    -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑self.support)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.dvd_modByMonic_sub : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), q ∣ p %ₘ q - p
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_star_eq_natCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α]
  {M : Matrix n n α} {d : ℕ}, M.map star = ↑d ↔ M = ↑d
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C}
  {φ₁ φ₂ : W ⟶ CategoryTheory.ChosenPullbacksAlong.pullbackObj f g},
  CategoryTheory.CategoryStruct.comp φ₁ (CategoryTheory.ChosenPullbacksAlong.fst f g) =
      CategoryTheory.CategoryStruct.comp φ₂ (CategoryTheory.ChosenPullbacksAlong.fst f g) →
    CategoryTheory.CategoryStruct.comp φ₁ (CategoryTheory.ChosenPullbacksAlong.snd f g) =
        CategoryTheory.CategoryStruct.comp φ₂ (CategoryTheory.ChosenPullbacksAlong.snd f g) →
      φ₁ = φ₂
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- The orthogonal complement of a submodule `N` with respect to some bilinear form is the set of
elements `x` which are orthogonal to all elements of `N`; i.e., for all `y` in `N`, `B y x = 0`.

Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
chirality; in addition to this "right" orthogonal complement one could define a "left" orthogonal
complement for which, for all `y` in `N`, `B x y = 0`.  This variant definition is not currently
provided in mathlib.  -/
LinearMap.BilinForm.orthogonal : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → Submodule R M → Submodule R M
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Ioi_castSucc : ∀ {n : ℕ} (i : Fin n), Fin.castSucc ⁻¹' Set.Ioi i.castSucc = Set.Ioi i
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_symm_trans_prod : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (e f : OpenPartialHomeomorph X Y) (e' f' : OpenPartialHomeomorph X' Y'),
  (e.prod e').symm.trans (f.prod f') = (e.symm.trans f).prod (e'.symm.trans f')
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.trans_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasPushout P.i₁ P'.i₀], (P.trans P').π = CategoryTheory.Limits.pushout.desc P.π P'.π ⋯
-- Mathlib.RingTheory.Localization.Algebra
AlgHom.toKerIsLocalization_apply : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] {B : Type u_7} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Rₚ : Type u_8)
  [inst_5 : CommSemiring Rₚ] [inst_6 : Algebra R Rₚ] [inst_7 : IsLocalization M Rₚ] (Aₚ : Type u_9)
  [inst_8 : CommSemiring Aₚ] [inst_9 : Algebra R Aₚ] [inst_10 : Algebra A Aₚ] [inst_11 : IsScalarTower R A Aₚ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type u_10) [inst_13 : CommSemiring Bₚ]
  [inst_14 : Algebra R Bₚ] [inst_15 : Algebra B Bₚ] [inst_16 : IsScalarTower R B Bₚ]
  [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] [inst_18 : Algebra Rₚ Aₚ] [inst_19 : Algebra Rₚ Bₚ]
  [inst_20 : IsScalarTower R Rₚ Aₚ] [inst_21 : IsScalarTower R Rₚ Bₚ] (f : A →ₐ[R] B) (x : ↥(RingHom.ker f)),
  (AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f) x = (RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom ⋯) x
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.Λ.congr_simp : ∀ {Γ Γ_1 : Subgroup (GL (Fin 2) ℝ)} (e_Γ : Γ = Γ_1) [inst : Γ.IsArithmetic] {k k_1 : ℤ} (e_k : k = k_1) (hk : 0 < k)
  {F : Type u_1} [inst_1 : FunLike F UpperHalfPlane ℂ] (f f_1 : F),
  f = f_1 → ∀ [inst_2 : ModularFormClass F Γ k] (a a_1 : ℂ), a = a_1 → ModularForm.Λ hk f a = ModularForm.Λ ⋯ f_1 a_1
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_true : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ∧ ⌜True⌝ ⊣⊢ₛ P
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan_zero : catalan 0 = 1
-- Std.Time.Format.DateFormat
Std.Time.DateFormat.mk : Std.Time.Weekday → Std.Time.Internal.Bounded.LE 0 6 → Std.Time.DateFormatSymbols → Std.Time.DateFormat
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_iff_faithful_coyoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsSeparator G ↔ (CategoryTheory.coyoneda.obj (Opposite.op G)).Faithful
-- Mathlib.Algebra.Group.Hom.Defs
/-- `ZeroHom M N` is the type of functions `M → N` that preserve zero.

When possible, instead of parametrizing results over `(f : ZeroHom M N)`,
you should parametrize over `(F : Type*) [ZeroHomClass F M N] (f : F)`.

When you extend this structure, make sure to also extend `ZeroHomClass`.
 -/
ZeroHom : (M : Type u_10) → (N : Type u_11) → [Zero M] → [Zero N] → Type (max u_10 u_11)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_left_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.left = sq.X₁