mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The tensor of a family of linear maps from `sᵢ` to `tᵢ`, as a multilinear map of
the family.
 -/
PiTensorProduct.mapMultilinear : {ι : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      (s : ι → Type u_7) →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            (t : ι → Type u_11) →
              [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                [inst_4 : (i : ι) → Module R (t i)] →
                  MultilinearMap R (fun i => s i →ₗ[R] t i)
                    ((PiTensorProduct R fun i => s i) →ₗ[R] PiTensorProduct R fun i => t i)
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom_pos : ∀ (n : ℕ), 0 < n.centralBinom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)} {k k' fallback : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).getKeyD k' fallback = k
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.partialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (Additive α)
-- Std.Sync.Broadcast
/-- Try to receive a value from the broadcast receiver, if a message is available right away
return `some value`, otherwise return `none` without blocking.
 -/
Std.Broadcast.Sync.Receiver.tryRecv : {α : Type} → Std.Broadcast.Sync.Receiver α → BaseIO (Option α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step.inj : ∀ {p : Lean.Grind.CommRing.Poly} {k₁ : ℤ} {d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation} {k₂ : ℤ}
  {m₂ : Lean.Grind.CommRing.Mon} {c : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {p_1 : Lean.Grind.CommRing.Poly}
  {k₁_1 : ℤ} {d_1 : Lean.Meta.Grind.Arith.CommRing.PolyDerivation} {k₂_1 : ℤ} {m₂_1 : Lean.Grind.CommRing.Mon}
  {c_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p k₁ d k₂ m₂ c =
      Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p_1 k₁_1 d_1 k₂_1 m₂_1 c_1 →
    p = p_1 ∧ k₁ = k₁_1 ∧ d = d_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1 ∧ c = c_1
-- Lean.Server.Rpc.Basic
/-- Value to use for the next fresh `RpcRef`, monotonically increasing.
 -/
Lean.Server.RpcObjectStore.nextRef : Lean.Server.RpcObjectStore → USize
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.compl_neighborFinset_sdiff_inter_eq : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V] {v w : V},
  (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) =
    ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `M.toQuadraticForm'` is the map `fun x ↦ row x * M * col x` as a quadratic form on `n → R`.  -/
Matrix.toQuadraticForm' : {R : Type u_3} →
  {n : Type w} → [Fintype n] → [DecidableEq n] → [inst : CommRing R] → Matrix n n R → QuadraticForm R (n → R)
-- Lean.Parser.Basic
Lean.Parser.checkColGtFn : String → Lean.Parser.ParserFn
-- Lean.Compiler.IR.CompilerM
Lean.IR.getSorryDep : Lean.Environment → Lean.Name → Option Lean.Name
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instAddGroup : {m : Type u_1} →
  {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → AddGroup (α i j)] → AddGroup (DMatrix m n α)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))
        (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) =
    CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op U))
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_localRingHom : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {f : 𝒜 →+*ᵍ ℬ} {I : Ideal A} [inst_10 : I.IsPrime]
  {J : Ideal B} [inst_11 : J.IsPrime] {hIJ : I = Ideal.comap f J} (x : HomogeneousLocalization.AtPrime 𝒜 I),
  HomogeneousLocalization.val ((HomogeneousLocalization.localRingHom f I J hIJ) x) =
    (Localization.localRingHom I J (↑f) hIJ) (HomogeneousLocalization.val x)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_smul : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (r : α)
  (A : Matrix n n α), (r • A).cramer = r ^ (Fintype.card n - 1) • A.cramer
-- Lean.Parser.Extra
Lean.Parser.withPosition.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.SInt.Bitwise
Int8.toInt64_and : ∀ (a b : Int8), (a &&& b).toInt64 = a.toInt64 &&& b.toInt64
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of limits of shape along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F G : CategoryTheory.Functor C D} (h : F ≅ G)
  [CategoryTheory.Limits.ReflectsLimitsOfShape J F], CategoryTheory.Limits.ReflectsLimitsOfShape J G
-- Mathlib.Order.Cover
CovBy.Iio_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ⋖ b → Set.Iio b = Set.Iic a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_succ_right_eq_push : ∀ {m n : ℤ}, m ≤ n → (m...n + 1).toArray = (m...n).toArray.push n
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
RingOfIntegers.ZModXQuotSpanEquivQuotSpan.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ}
  [inst_2 : Fact (Nat.Prime p)] (hp : ¬p ∣ RingOfIntegers.exponent θ),
  RingOfIntegers.ZModXQuotSpanEquivQuotSpan hp = RingOfIntegers.ZModXQuotSpanEquivQuotSpan hp
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_pt : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D}
  [inst_3 : CategoryTheory.IsConnected J] {B : D} {F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)}
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.CostructuredArrow.proj K B))),
  (CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone c).pt =
    CategoryTheory.CostructuredArrow.mk
      (CategoryTheory.CategoryStruct.comp (K.map (c.π.app (Classical.arbitrary J))) (F.obj (Classical.arbitrary J)).hom)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoMod hp a (b + m • p) = toIcoMod hp a b
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y),
  CategoryTheory.IsPullback (hf.fst g) (F.map (hf.snd g)) f g
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
mulIndicator_iUnion_of_pairwise_disjoint : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β),
  Pairwise (Function.onFun Disjoint s) →
    ∀ (f : β → α), (⋃ d, s d).mulIndicator f = fun i => ∏' (d : γ), (s d).mulIndicator f i
-- Init.Data.Array.Attach
Array.attachWith_append : ∀ {α : Type u_1} {P : α → Prop} {xs ys : Array α} {H : ∀ a ∈ xs ++ ys, P a},
  (xs ++ ys).attachWith P H = xs.attachWith P ⋯ ++ ys.attachWith P ⋯
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.im_inner_self_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (x : E), RCLike.im (inner 𝕜 x (T x)) = 0
-- Init.Data.List.Erase
List.Nodup.erase_eq_filter : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α},
  l.Nodup → ∀ (a : α), l.erase a = List.filter (fun x => x != a) l
-- Mathlib.Data.List.AList
AList.mk_cons_eq_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (c : Sigma β) (l : List (Sigma β)) (h : (c :: l).NodupKeys),
  { entries := c :: l, nodupKeys := h } = AList.insert c.fst c.snd { entries := l, nodupKeys := ⋯ }
-- Mathlib.Algebra.Ring.Prod
RingHom.prod_unique : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (f : R →+* S × T), ((RingHom.fst S T).comp f).prod ((RingHom.snd S T).comp f) = f
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_singleton : ∀ {α : Type u} [inst : CommSemiring α] {x y : α}, x ∈ Ideal.span {y} ↔ y ∣ x
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_X_self : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ}, (MvPowerSeries.pderiv R i) (MvPowerSeries.X i) = 1
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.length_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ShortComplex.mono_of_epi_of_epi_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ShortComplex C} (φ : R₁ ⟶ R₂),
  R₂.Exact → CategoryTheory.Epi R₁.g → CategoryTheory.Epi φ.τ₁ → CategoryTheory.Mono φ.τ₂ → CategoryTheory.Mono φ.τ₃
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isEmbedding_iff : ∀ ⦃A X : TopCat⦄ (f : A ⟶ X), TopCat.isEmbedding f ↔ Topology.IsEmbedding ⇑(TopCat.Hom.hom f)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
/-- Equivalence between `M` and `Mᵈᵐᵃ`.  -/
DomMulAct.mk : {M : Type u_1} → M ≃ Mᵈᵐᵃ
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.Gamma_one : Complex.Gamma 1 = 1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.atIdxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {i : ℕ} {fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.atIdxD i fallback = t₂.atIdxD i fallback
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuousAt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R) {a : R},
  ContinuousAt (fun x => Polynomial.eval x p) a
-- Lean.Meta.Sym.InstantiateS
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRevBetaS'.visit : Array Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Sym.M✝ Lean.Expr
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.hasSum_L : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [inst_2 : ModularFormClass F Γ k],
  ↑k + 1 < s.re →
    HasSum (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑n ^ s)
      (↑Γ.strictWidthInfty ^ (-s) * ModularForm.L hk f s)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
differentiableOn_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedRing R] [HasSummableGeomSeries R]
  [inst_3 : NormedAlgebra 𝕜 R], DifferentiableOn 𝕜 Ring.inverse {x | IsUnit x}
-- Mathlib.Data.Complex.Basic
/-- The natural inclusion of the real numbers into the complex numbers.  -/
Complex.ofReal : ℝ → ℂ
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instOppositeOpOfProjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} [CategoryTheory.Projective P],
  CategoryTheory.Injective (Opposite.op P)
-- Init.Data.UInt.Lemmas
UInt8.eq_iff_toBitVec_eq : ∀ {a b : UInt8}, a = b ↔ a.toBitVec = b.toBitVec
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (input : aig.RefVec w)
  (distance curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s =
    if hidx : curr < w then
      if hdist : distance + curr < w then
        have s := s.push (input.get (distance + curr) hdist);
        Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance (curr + 1) ⋯ s
      else
        have zeroRef := aig.mkConstCached false;
        have s := s.push zeroRef;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance (curr + 1) ⋯ s
    else
      have hcurr := ⋯;
      { aig := aig, vec := hcurr ▸ s }
-- Lean.Meta.Tactic.ExposeNames
/-- Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
If no local declarations require renaming, the original goal is returned unchanged.
 -/
Lean.MVarId.exposeNames : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `L/K` is a Galois extension, then `Gal(L/K)` is a Galois group for `L/K`.  -/
IsGaloisGroup.of_isGalois : ∀ (K : Type u_3) (L : Type u_4) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [IsGalois K L],
  IsGaloisGroup Gal(L/K) K L
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- Eta-expanded form of `fderiv_comp` -/
fderiv_fun_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {g : F → G},
  DifferentiableAt 𝕜 g (f x) →
    DifferentiableAt 𝕜 f x → fderiv 𝕜 (fun x => g (f x)) x = fderiv 𝕜 g (f x) ∘SL fderiv 𝕜 f x
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.support_nonempty : ∀ {ι : 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} (b : P.Base)
  [Nonempty ι] [NeZero 2], b.support.Nonempty
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
      CategoryTheory.ShortComplex.Hom.comm₁₂._autoParam)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃)
      CategoryTheory.ShortComplex.Hom.comm₂₃._autoParam)
  (τ₁_1 : S₁.X₁ ⟶ S₂.X₁) (τ₂_1 : S₁.X₂ ⟶ S₂.X₂) (τ₃_1 : S₁.X₃ ⟶ S₂.X₃)
  (comm₁₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp τ₁_1 S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂_1)
      CategoryTheory.ShortComplex.Hom.comm₁₂._autoParam)
  (comm₂₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp τ₂_1 S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃_1)
      CategoryTheory.ShortComplex.Hom.comm₂₃._autoParam),
  ({ τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ } =
      { τ₁ := τ₁_1, τ₂ := τ₂_1, τ₃ := τ₃_1, comm₁₂ := comm₁₂_1, comm₂₃ := comm₂₃_1 }) =
    (τ₁ = τ₁_1 ∧ τ₂ = τ₂_1 ∧ τ₃ = τ₃_1)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limMap_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap α) (CategoryTheory.Limits.limit.π G j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (α.app j)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_finsetInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  {s : Finset ι} {p : ι → Submodule R M} {x : M}, x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.erase_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α}, ∅.erase k = ∅
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.congr_of_eventuallyEq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → Prod.map f₁ f₁ =ᶠ[L] Prod.map f f → HasDerivAtFilter f₁ f' L
-- Init.Data.List.OfFn
List.ofFn_eq_nil_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α}, List.ofFn f = [] ↔ n = 0
-- Mathlib.Order.Shrink
instPredOrderShrink.eq_1 : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] [inst_2 : PredOrder α],
  instPredOrderShrink = PredOrder.ofOrderIso (orderIsoShrink α)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S : NonUnitalSubalgebra R A},
  S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The first map of a short complex, as a functor.  -/
CategoryTheory.ShortComplex.fFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex C) (CategoryTheory.Arrow C)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two measures which are finite on closed intervals are equal if they agree on all
closed intervals.  -/
MeasureTheory.Measure.ext_of_Icc : ∀ {α : Type u_5} [inst : TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [CompactIccSpace α] [BorelSpace α] (μ ν : MeasureTheory.Measure α)
  [MeasureTheory.IsLocallyFiniteMeasure μ], (∀ ⦃a b : α⦄, a ≤ b → μ (Set.Icc a b) = ν (Set.Icc a b)) → μ = ν
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.homEquiv.eq_1 : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂],
  CategoryTheory.Enriched.FunctorCategory.homEquiv V =
    { toFun := fun τ => CategoryTheory.Limits.end_.lift (fun j => (CategoryTheory.eHomEquiv V) (τ.app j)) ⋯,
      invFun := fun g =>
        {
          app := fun j =>
            (CategoryTheory.eHomEquiv V).symm
              (CategoryTheory.CategoryStruct.comp g
                (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j)),
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.Congruence.Defs
/-- For congruence relations `c, d` on a type `M` with a multiplication, `c ≤ d` iff `∀ x y ∈ M`,
`x` is related to `y` by `d` if `x` is related to `y` by `c`.  -/
Con.instLE : {M : Type u_1} → [inst : Mul M] → LE (Con M)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₄_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.a₄ = 0
-- Qq.AssertInstancesCommute
Qq.Impl.termAssumeInstancesCommuteDummy : Lean.ParserDescr
-- Qq.MetaM
/-- Like `Qq.isLevelDefEqQ`, but throws an error if not defeq.  -/
Qq.assertLevelDefEqQ : (u v : Lean.Level) → Lean.MetaM (PLift (u =QL v))
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.val_step_takeWhile.match_3.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Lean.Meta.Tactic.Grind.Types
/-- Unique index used for pretty printing and debugging purposes.  -/
Lean.Meta.Grind.ENode.idx : Lean.Meta.Grind.ENode → ℕ
-- Init.Util
mkPanicMessageWithDecl : String → String → ℕ → ℕ → String → String
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_mul : ∀ {α : Type u_2} [inst : Group α] {t : Set α}, t.Nonempty → Set.univ * t = Set.univ
-- Mathlib.Topology.Algebra.ProperAction.Basic
ProperVAdd.mk : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup G]
  [inst_3 : AddAction G X], (IsProperMap fun gx => (gx.1 +ᵥ gx.2, gx.2)) → ProperVAdd G X
-- Init.Tactics
/-- A sequence of one or more locations at which a tactic should operate. These can include local
hypotheses and `⊢`, which denotes the goal.
 -/
Lean.Parser.Tactic.locationHyp : Lean.ParserDescr
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] (i : ι) (m : M),
  (fun₀ | i => m).toDFinsupp = fun₀ | i => m
-- Mathlib.RingTheory.Adjoin.Field
IsIntegral.minpoly_splits_tower_top : ∀ {R : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : CommRing M] [inst_4 : Algebra R K] [inst_5 : Algebra R M] [inst_6 : Algebra K M] [IsScalarTower R K M]
  {x : M} [inst_8 : Algebra K L] [inst_9 : Algebra R L] [IsScalarTower R K L],
  IsIntegral R x →
    (Polynomial.map (algebraMap R L) (minpoly R x)).Splits → (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
-- Mathlib.Order.CompleteBooleanAlgebra
/-- A complete Boolean algebra is a Boolean algebra that is also a complete distributive lattice.

It is only completely distributive if it is also atomic.
 -/
CompleteBooleanAlgebra : Type u_1 → Type u_1
-- Lean.Meta.Basic
/-- Return true if the given universe metavariable is "read-only".
That is, its `depth` is different from the current metavariable context depth.
 -/
Lean.LMVarId.isReadOnly : Lean.LMVarId → Lean.MetaM Bool
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_ofReal : Measurable Complex.ofReal
-- Mathlib.Algebra.Central.End
/-- The center of endomorphisms on a free module is trivial,
in other words, it is a central algebra.  -/
Algebra.IsCentral.instEnd : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : CommSemiring S] [inst_5 : Module S M] [inst_6 : SMulCommClass R S M]
  [inst_7 : Algebra S R] [inst_8 : IsScalarTower S R M] [Algebra.IsCentral S R], Algebra.IsCentral S (Module.End R M)