mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_alter_of_not_compare_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {f : Option β → Option β},
  ¬compare k k' = Ordering.eq →
    Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl =
      Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.span_int_root_support : ∀ {ι : 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),
  Submodule.span ℤ (⇑P.root '' ↑b.support) = Submodule.span ℤ (Set.range ⇑P.root)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_mul : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x y : WithVal v), (x * y).ofVal = x.ofVal * y.ofVal
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocRing R] [inst_1 : Fintype n] [inst_2 : Nonempty n]
  [inst_3 : DecidableEq n] (J : TwoSidedIdeal (Matrix n n R)) (x y : R),
  ((RelIso.symm TwoSidedIdeal.orderIsoMatrix) J).ringCon.toSetoid x y =
    ∀ (i j : n), J.ringCon (Matrix.single i j x) (Matrix.single i j y)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.toList_sorted : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t → List.Pairwise (RBTree.RBNode.cmpLT cmp) t.toList
-- Mathlib.Algebra.Group.Action.Defs
vadd_iterate_apply : ∀ {M : Type u_1} {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α] (a : M) (n : ℕ) (x : α),
  (fun x => a +ᵥ x)^[n] x = n • a +ᵥ x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {l : List ((a : α) × β a)}, (↑(t.insertMany! l)).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.tendsto_cofinite : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [self : Filter.TendstoCofinite f],
  Filter.Tendsto f Filter.cofinite Filter.cofinite
-- Mathlib.Data.Set.Monotone
/-- **Alias** of `Monotone.domRestrict`. -/
Monotone.restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ (s : Set α), Monotone (s.domRestrict f)
-- Mathlib.RingTheory.KrullDimension.PID
/-- In a PID that is not a field, every maximal ideal has height one.  -/
IsPrincipalIdealRing.height_eq_one_of_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (m : Ideal R) [m.IsMaximal],
  ¬IsField R → m.height = 1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.right_unitality_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (X : C) {Z : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.ε F))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) h
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.var : ℕ → Mathlib.Tactic.ITauto.IProp
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coprod_toFun : ∀ {A : Type u_2} {B : Type u_3} {E : Type u_6} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [inst_4 : AddCommMonoid E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousAdd E]
  (f : A →ₜ+ E) (g : B →ₜ+ E) (x : A × B), (f.coprod g) x = f x.1 + g x.2
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The extension of scalars by the identity of a ring is isomorphic to the
identity functor.  -/
ModuleCat.extendScalarsId : (R : Type u₁) → [inst : CommRing R] → ModuleCat.extendScalars (RingHom.id R) ≅ CategoryTheory.Functor.id (ModuleCat R)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.addMonoidWithOne : AddMonoidWithOne Ordinal.{u}
-- Mathlib.Order.SuccPred.Basic
Order.succ_eq_succ_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  Order.succ a = Order.succ b ↔ a = b
-- Mathlib.Data.Nat.GCD.Basic
Nat.add_coprime_iff_left : ∀ {a b c : ℕ}, c ∣ b → ((a + b).Coprime c ↔ a.Coprime c)
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.replaceUnsafe : (Lean.Level → Option Lean.Level) → Lean.Expr → Lean.Expr
-- Aesop.Search.Expansion
Aesop.applyPostponedSafeRule : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.PostponedSafeRule → Aesop.GoalRef → Aesop.SearchM Q Aesop.RuleResult
-- Lean.Parser.Command
Lean.Parser.Command.unsafe.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.Measure.mconv_smul_right : ∀ {M : Type u_2} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.SFinite ν] (s : ENNReal), μ.mconv (s • ν) = s • μ.mconv ν
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasProdLocallyUniformlyOn_of_forall_compact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  IsOpen s →
    ∀ [LocallyCompactSpace β], (∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g K) → HasProdLocallyUniformlyOn f g s
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.coneΓ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] (F : CategoryTheory.Sheaf J A),
  F.coneΓ =
    { pt := (CategoryTheory.Sheaf.Γ J A).obj F,
      π := CategoryTheory.Sheaf.ΓHomEquiv.symm (CategoryTheory.CategoryStruct.id ((CategoryTheory.Sheaf.Γ J A).obj F)) }
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.decimalNumberFn.parseOptExp : String.Pos.Raw → Lean.Parser.ParserContext → Lean.Parser.ParserState → Bool → Lean.Parser.ParserState
-- Init.Data.Int.LemmasAux
Int.instAssociativeMin : Std.Associative min
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalCommSemiring` instance along an injective function.  -/
Function.Injective.nonUnitalCommSemiring : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Add S] →
      [inst_1 : Mul S] →
        [inst_2 : Zero S] →
          [inst_3 : SMul ℕ S] →
            [inst_4 : NonUnitalCommSemiring R] →
              (f : S → R) →
                Function.Injective f →
                  f 0 = 0 →
                    (∀ (x y : S), f (x + y) = f x + f y) →
                      (∀ (x y : S), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → NonUnitalCommSemiring S
-- Mathlib.Tactic.NormNum.GCD
/-- Evaluates the `Int.gcd` function.  -/
Mathlib.Meta.NormNum.evalIntGCD : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The second multivariate polynomial used in the proof of Erdős–Ginzburg–Ziv.  -/
_private.Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.0.f₂ : {ι : Type u_1} → {p : ℕ} → [inst : Fact (Nat.Prime p)] → (s : Finset ι) → (ι → ZMod p) → MvPolynomial (↥s) (ZMod p)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.disjointUnion_target : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
  (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x ∈ e.source)]
  [inst_1 : (y : β) → Decidable (y ∈ e.target)], (e.disjointUnion e' hs ht).target = e.target ∪ e'.target
-- Mathlib.Topology.SeparatedMap
isLocallyInjective_iff_isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyInjective f ↔ IsOpenMap (toPullbackDiag f)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.isFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω), MeasureTheory.IsFiniteMeasure ↑μ
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_const_add_iff : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {s : Set E} (c : F), DifferentiableWithinAt 𝕜 (fun y => c + f y) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Init.Data.Vector.Lemmas
Vector.pop_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (Vector.replicate n a).pop = Vector.replicate (n - 1) a
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α), UniformContinuous pkg.coe
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.trans : ∀ {F : Type u → Type v} [q : QPF F] (u v w : (QPF.P F).W), QPF.Wequiv u v → QPF.Wequiv v w → QPF.Wequiv u w
-- Mathlib.CategoryTheory.Presentable.Directed
/-- The diagram containing a single object (and its identity morphism).  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} → [Fact κ.IsRegular] → J → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'.eq_def : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (x : ℕ),
  preNormEDS' b c d x =
    match x with
    | 0 => 0
    | 1 => 1
    | 2 => 1
    | 3 => c
    | 4 => d
    | n.succ.succ.succ.succ.succ =>
      let m := n / 2;
      if hn : Even n then
        (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
          preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b
      else
        have this := ⋯;
        preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
          preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
-- Mathlib.CategoryTheory.Opposites
/-- Taking the opposite of a functor is functorial.
 -/
CategoryTheory.Functor.opHom : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)ᵒᵖ (CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.bounds_nonempty : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂}, ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionUnitIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (Opposite.unop x)).symm.op
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.of.injEq : ∀ (carrier : Type u) [ring : Ring carrier] (carrier_1 : Type u) (ring_1 : Ring carrier_1),
  (RingCat.of carrier = RingCat.of carrier_1) = (carrier = carrier_1 ∧ ring ≍ ring_1)
-- Init.Data.Format.Basic
/-- Renders a `Format` to a string.
* `width`: the total width
* `indent`: the initial indentation to use for wrapped lines
  (subsequent wrapping may increase the indentation)
* `column`: begin the first line wrap `column` characters earlier than usual
  (this is useful when the output String will be printed starting at `column`)
 -/
Std.Format.pretty : Std.Format → optParam ℕ Std.Format.defWidth → optParam ℕ 0 → optParam ℕ 0 → String
-- Mathlib.Util.FormatTable
Alignment.right : Alignment
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toList_filter : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → Bool},
  (Std.Iter.filter f it).toList = List.filter f it.toList
-- Std.Time.Format.Modifier
Std.Time.ExtendedDayPeriod.evening.sizeOf_spec : sizeOf Std.Time.ExtendedDayPeriod.evening = 1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termα_mod_G_3 : Lean.ParserDescr
-- Mathlib.Data.Nat.Init
/-- **Alias** of the forward direction of `Nat.le_succ_iff`. -/
Nat.of_le_succ : ∀ {m n : ℕ}, m ≤ n.succ → m ≤ n ∨ m = n.succ
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D},
  (E.map F).sieve₀ ∈ K (F.obj X) →
    (∀ (i₁ i₂ : E.I₀) ⦃W : D⦄ (p₁ : W ⟶ F.obj (E.X i₁)) (p₂ : W ⟶ F.obj (E.X i₂)),
        CategoryTheory.CategoryStruct.comp p₁ (F.map (E.f i₁)) =
            CategoryTheory.CategoryStruct.comp p₂ (F.map (E.f i₂)) →
          (E.map F).sieve₁ p₁ p₂ ∈ K W) →
      E.IsPreservedBy F K
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.arrayLit : List Lean.Meta.Match.Example → Lean.Meta.Match.Example
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
/-- `TensorProduct.assoc` preserves tensor products of quadratic forms.  -/
QuadraticForm.tensorAssoc : {R : Type uR} →
  {M₁ : Type uM₁} →
    {M₂ : Type uM₂} →
      {M₃ : Type uM₃} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M₁] →
            [inst_2 : AddCommGroup M₂] →
              [inst_3 : AddCommGroup M₃] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R M₃] →
                      [inst_7 : Invertible 2] →
                        (Q₁ : QuadraticForm R M₁) →
                          (Q₂ : QuadraticForm R M₂) →
                            (Q₃ : QuadraticForm R M₃) →
                              QuadraticMap.IsometryEquiv ((Q₁.tmul Q₂).tmul Q₃) (Q₁.tmul (Q₂.tmul Q₃))
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_natCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ), (↑n).imJ = 0
-- Mathlib.Topology.Order.LawsonTopology
Topology.IsLawson.isTopologicalBasis : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLawson α],
  TopologicalSpace.IsTopologicalBasis (Topology.IsLawson.lawsonBasis α)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_add : ∀ (x y : EReal), (x + y).exp = x.exp * y.exp
-- Aesop.Search.SearchM
Aesop.SearchM : (Q : Type) → [Aesop.Queue Q] → Type → Type
-- Mathlib.Logic.Embedding.Basic
/-- Convert a surjective `Embedding` to an `Equiv`  -/
Function.Embedding.equivOfSurjective : {α : Sort u_1} → {β : Sort u_2} → (f : α ↪ β) → Function.Surjective ⇑f → α ≃ β
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).getD k' fallback = k
-- Mathlib.Data.Set.Image
Set.rangeFactorization_eq : ∀ {β : Type u_2} {ι : Sort u_4} {f : ι → β}, Subtype.val ∘ Set.rangeFactorization f = f
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInv_leftInv_eq : ∀ {M : Type u_1} [inst : Monoid M], ∀ S ≤ IsUnit.submonoid M, S.leftInv.leftInv = S
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instBotOfTop : (α : Type u) → [h : Top α] → Bot αᵒᵈ
-- Mathlib.Data.Set.Image
Function.Surjective.image_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Function.Surjective (Set.image f)
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coalgebraToOver_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (A : (CategoryTheory.prodComonad X).Coalgebra),
  (CategoryTheory.coalgebraToOver X).obj A =
    CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)
-- Init.Data.UInt.Lemmas
UInt16.zero_sub : ∀ (a : UInt16), 0 - a = -a
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.of_inner : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {v : β k},
  (Std.DTreeMap.Internal.Cell.of k v).inner = some ⟨k, v⟩
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The naturality condition.  -/
CategoryTheory.Oplax.StrongTrans.Modification.naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Oplax.StrongTrans.Modification η θ)
  {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
      (θ.naturality f).hom =
    CategoryTheory.CategoryStruct.comp (η.naturality f).hom
      (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f))
-- Mathlib.RingTheory.LaurentSeries
Filter.comap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (m : α → β) (f : Filter β),
  Filter.comap m f = { sets := {s | ∃ t ∈ f, m ⁻¹' t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsGeneratedBy.continuous_iff`. -/
DeltaGeneratedSpace.continuous_iff : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] [Topology.IsGeneratedBy X Y] (g : Y → Z),
  Continuous g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑f)
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
le_comap_range_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] (g : N →ₗ[R] P) (q : Q),
  g.range ≤ Submodule.comap ((TensorProduct.mk R P Q).flip q) (LinearMap.rTensor Q g).range
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.full_preadditiveCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.preadditiveCoyoneda.Full
-- Init.Data.Int.DivMod.Basic
Int.ofNat_ediv_negSucc : ∀ {a b : ℕ}, Int.ofNat a / Int.negSucc b = -↑(a / (b + 1))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 0th differential in the complex of inhomogeneous chains of `A : Rep k G`, as a
`k`-linear map `(G →₀ A) → A`. It is defined by `single g a ↦ ρ_A(g⁻¹)(a) - a.`  -/
groupHomology.d₁₀ : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k (G →₀ ↑A) ⟶ ModuleCat.of k ↑A
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_univ : ∀ {α : Type u_2} (M : Matroid α), M.closure Set.univ = M.E
-- Init.Data.Vector.Nat
Vector.sum_reverse_nat : ∀ {n : ℕ} (xs : Vector ℕ n), xs.reverse.sum = xs.sum
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.mk.injEq : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : LinearOrder m] {n : Type u_2} [inst_2 : LinearOrder n] {R : Type u_3}
  [inst_3 : CommRing R] {A : Matrix m n R} (L : Matrix m m R) (σ : Equiv.Perm m) (pivot : m → WithTop n)
  (isPivotedBy : (L * A.submatrix (⇑σ) id).IsPivotedBy pivot) (L_lowerTriangular : L.IsLowerTriangular)
  (L_diag_ne_zero : ∀ (i : m), L.diag i ≠ 0) (L_1 : Matrix m m R) (σ_1 : Equiv.Perm m) (pivot_1 : m → WithTop n)
  (isPivotedBy_1 : (L_1 * A.submatrix (⇑σ_1) id).IsPivotedBy pivot_1) (L_lowerTriangular_1 : L_1.IsLowerTriangular)
  (L_diag_ne_zero_1 : ∀ (i : m), L_1.diag i ≠ 0),
  ({ L := L, σ := σ, pivot := pivot, isPivotedBy := isPivotedBy, L_lowerTriangular := L_lowerTriangular,
        L_diag_ne_zero := L_diag_ne_zero } =
      { L := L_1, σ := σ_1, pivot := pivot_1, isPivotedBy := isPivotedBy_1, L_lowerTriangular := L_lowerTriangular_1,
        L_diag_ne_zero := L_diag_ne_zero_1 }) =
    (L = L_1 ∧ σ = σ_1 ∧ pivot = pivot_1)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_relabel : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {m n : ℕ}
  {φ : L.BoundedFormula α n} {g : α → β ⊕ Fin m} {v : β → M} {xs : Fin (m + n) → M},
  (FirstOrder.Language.BoundedFormula.relabel g φ).Realize v xs ↔
    φ.Realize (Sum.elim v (xs ∘ Fin.castAdd n) ∘ g) (xs ∘ Fin.natAdd m)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_eq_mlieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  UniqueMDiffAt[s] x →
    MDiffAt (T% V) x → MDiffAt (T% W) x → VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracket I V W x
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.instEmptyCollection : EmptyCollection Aesop.RulePatternIndex
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.size.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)),
  (match Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | Ordnode.node sz l x r => h_2 sz l x r) =
    h_1 ()
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Continuity is a "local" predicate on functions to a fixed topological space `T`.
 -/
TopCat.continuousLocal : (X : TopCat) → (T : Type u_3) → [TopologicalSpace T] → TopCat.LocalPredicate fun x => T
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.hasNoErrorMessages : Lean.Elab.Command.CommandElabM Bool
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Algebra F) (r : ℤ)
  (α : A₁ ⟶ A₂), (r • α).f = r • α.f