mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.obj.Δ_def_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.OplaxMonoidal] (X : C) [inst_5 : CategoryTheory.ComonObj X] {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) h)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_copy : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (s : Set L) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_sup : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
  {v : α → M} {xs : Fin l → M}, (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.numSteps : Lean.Meta.Simp.State → ℕ
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The functor `EInt ⥤ C ⥤ C` which sends `⊥` to the zero functor,
`n : ℤ` to `t.truncLT n` and `⊤` to `𝟭 C`.  -/
CategoryTheory.Triangulated.TStructure.eTruncLT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 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] →
              CategoryTheory.Triangulated.TStructure C → CategoryTheory.Functor EInt (CategoryTheory.Functor C C)
-- Init.Data.Range.Polymorphic.Iterators
Std.Rco.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (r : Std.Rco α),
  Std.Rco.Internal.iter r = { internalState := { next := some r.lower, upperBound := r.upper } }
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.ext.sizeOf_spec : ∀ (ext₁? : Option Lean.Meta.SimpExtension) (ext₂? : Option Lean.Meta.Simp.SimprocExtension)
  (h : (ext₁?.isSome || ext₂?.isSome) = true),
  sizeOf (Lean.Elab.Tactic.ResolveSimpIdResult.ext ext₁? ext₂? h) = 1 + sizeOf ext₁? + sizeOf ext₂? + sizeOf h
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.mk : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (Ring : Type w) →
            [commRing : CommRing Ring] →
              [algebra₁ : Algebra R Ring] →
                [algebra₂ : Algebra Ring S] →
                  [isScalarTower : IsScalarTower R Ring S] →
                    (σ : S → Ring) → (∀ (x : S), (algebraMap Ring S) (σ x) = x) → Algebra.Extension R S
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.card_support_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.card = 0 ↔ p = 0
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.lt : Bool → Mathlib.Ineq.WithStrictness
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_smul_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Gal(K/k)}
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsUnramified k (σ • w) ↔ NumberField.InfinitePlace.IsUnramified k w
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.of_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {x y z : C} (f : x ⟶ y)
  (g : y ⟶ z), W f → W.multiplicativeClosure' g → W.multiplicativeClosure' (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Order.WithBot
WithBot.none_eq_bot : ∀ {α : Type u_1}, none = ⊥
-- Lean.Data.Json.Basic
Lean.Json.brecOn_4.eq : ∀ {motive_1 : Lean.Json → Sort u} {motive_2 : Array Lean.Json → Sort u}
  {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} {motive_4 : List Lean.Json → Sort u}
  {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u}
  {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u}
  (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) (F_1 : (t : Lean.Json) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t)
  (F_3 : (t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t)
  (F_4 : (t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t)
  (F_5 : (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t)
  (F_6 : (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Lean.Json.below_5 t → motive_6 t),
  Lean.Json.brecOn_4 t F_1 F_2 F_3 F_4 F_5 F_6 = F_5 t (Lean.Json.brecOn_4.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.coe_toDiffeomorph_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (e : E ≃L[𝕜] E'), ⇑e.toDiffeomorph.symm = ⇑e.symm
-- Mathlib.Order.Category.BddLat
BddLat.instCoeSortType : CoeSort BddLat (Type u_1)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Dir.ofNat : ℕ → Turing.Dir
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_factorial_le : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), padicValNat p n.factorial ≤ n
-- Init.Prelude
/-- The number of bytes used by the string's UTF-8 encoding.

At runtime, this function takes constant time because the byte length of strings is cached.
 -/
String.utf8ByteSize : String → ℕ
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The (exact) short complex `K.homology n ⟶ L.homology n ⟶ (S f n).homology n`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} → (K ⟶ L) → [CategoryTheory.EnoughInjectives C] → ℤ → CategoryTheory.ShortComplex C
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- If `0 : ℕ` is not in the support of `f : ℕ →₀ ℕ` then `0 < ∏ x ∈ f.support, x ^ (f x)`.  -/
Nat.prod_pow_pos_of_zero_notMem_support : ∀ {f : ℕ →₀ ℕ}, 0 ∉ f.support → 0 < f.prod fun x1 x2 => x1 ^ x2
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Given an affinely independent family of points, two affine combinations (with sum of weights 1)
are equal if and only if their weights are pointwise equal.  -/
AffineIndependent.affineCombination_eq_iff_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w₁ w₂ : ι → k} {s : Finset ι},
      ∑ i ∈ s, w₁ i = 1 →
        ∑ i ∈ s, w₂ i = 1 →
          ((Finset.affineCombination k s p) w₁ = (Finset.affineCombination k s p) w₂ ↔ ∀ i ∈ s, w₁ i = w₂ i)
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.ordConnected : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → s.OrdConnected
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableSet.exists_measurable_proj : ∀ {α : Type u_1} {s : Set α} {x : MeasurableSpace α},
  MeasurableSet s → s.Nonempty → ∃ f, Measurable f ∧ ∀ (x : ↑s), f ↑x = x
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coeMonoidWithZeroHom_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  (self : { x // x ∈ Set.Icc 0 1 }), Set.Icc.coeMonoidWithZeroHom self = ↑self
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_comm_of_u_comm : ∀ {X : Type u_2} [inst : Preorder X] {Y : Type u_3} [inst_1 : Preorder Y] {Z : Type u_4} [inst_2 : Preorder Z]
  {W : Type u_5} [inst_3 : PartialOrder W] {lYX : X → Y} {uXY : Y → X},
  GaloisConnection lYX uXY →
    ∀ {lWZ : Z → W} {uZW : W → Z},
      GaloisConnection lWZ uZW →
        ∀ {lWY : Y → W} {uYW : W → Y},
          GaloisConnection lWY uYW →
            ∀ {lZX : X → Z} {uXZ : Z → X},
              GaloisConnection lZX uXZ → (∀ (w : W), uXZ (uZW w) = uXY (uYW w)) → ∀ {x : X}, lWZ (lZX x) = lWY (lYX x)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₁ = 0 ↔ CategoryTheory.Mono T.mor₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertManyIfNewUnit_empty_list : ∀ {α : Type u} {instOrd : Ord α} {l : List α} {k : α} {fallback : Unit},
  Std.DTreeMap.Internal.Impl.Const.getD
      (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)) k fallback =
    ()
-- Mathlib.Combinatorics.Colex
Finset.Colex.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (Colex (Finset α))
-- Init.Data.BitVec.Lemmas
BitVec.allOnes_or : ∀ {w : ℕ} {x : BitVec w}, BitVec.allOnes w ||| x = BitVec.allOnes w
-- Mathlib.Analysis.Analytic.IsolatedZeros
AnalyticOnNhd.eqOn_of_preconnected_of_mem_closure : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜},
  AnalyticOnNhd 𝕜 f U →
    AnalyticOnNhd 𝕜 g U → IsPreconnected U → z₀ ∈ U → z₀ ∈ closure ({z | f z = g z} \ {z₀}) → Set.EqOn f g U
-- Mathlib.Order.Filter.Map
Filter.comap_surjective_eq_bot : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, Function.Surjective m → (Filter.comap m f = ⊥ ↔ f = ⊥)
-- Mathlib.Algebra.CharP.Lemmas
multiset_sum_pow_char : ∀ {R : Type u_3} [inst : CommSemiring R] (p : ℕ) [ExpChar R p] (s : Multiset R),
  s.sum ^ p = (Multiset.map (fun x => x ^ p) s).sum
-- Mathlib.Algebra.Group.Defs
DivInvOneMonoid.toDivInvMonoid : {G : Type u_2} → [self : DivInvOneMonoid G] → DivInvMonoid G
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Auxiliary lemma, used in proving the more general result `isBigO_cocompact_rpow`.  -/
SchwartzMap.isBigO_cocompact_zpow_neg_nat : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (k : ℕ), ⇑f =O[Filter.cocompact E] fun x => ‖x‖ ^ (-↑k)
-- Mathlib.Data.Sym.Sym2
Sym2.exact : ∀ {α : Type u_1} {a b c d : α}, s(a, b) = s(c, d) → Sym2.Rel α (a, b) (c, d)
-- Init.Prelude
/-- Failure handling that does not depend on specific exception values.

The `Backtrackable δ σ` instance is used to save a snapshot of part of the state prior to running
`x₁`. If an exception is caught, the state is updated with the saved snapshot, rolling back part of
the state. If no instance of `Backtrackable` is provided, a fallback instance in which `δ` is `Unit`
is used, and no information is rolled back.
 -/
EStateM.orElse : {ε σ α δ : Type u} → [EStateM.Backtrackable δ σ] → EStateM ε σ α → (Unit → EStateM ε σ α) → EStateM ε σ α
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instPartialOrder.eq_1 : ∀ {α : Type u} [inst : Group α], GroupTopology.instPartialOrder = PartialOrder.lift GroupTopology.toTopologicalSpace ⋯
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.cacheSize : USize
-- Mathlib.Topology.Constructions
continuousAt_pi' : ∀ {X : Type u} {ι : Type u_5} {A : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (A i)]
  {f : X → (i : ι) → A i} {x : X}, (∀ (i : ι), ContinuousAt (fun y => f y i) x) → ContinuousAt f x
-- Init.Data.UInt.Lemmas
UInt16.not_lt : ∀ {a b : UInt16}, ¬a < b ↔ b ≤ a
-- Mathlib.Order.Defs.Unbundled
empty_relation_apply : ∀ {α : Sort u_1} (a b : α), emptyRelation a b ↔ False
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.trivial.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Grp.trivial C = { X := (CategoryTheory.Mon.trivial C).X, grp := CategoryTheory.GrpObj.instTensorUnit }
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Submodule.IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [Module.FaithfullyFlat R A] [inst_4 : AddCommGroup M] [inst_5 : Module R M],
  IsArtinian A (TensorProduct R A M) → IsArtinian R M
-- Lean.Parser.Level
Lean.Parser.Level.max.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Logic.Equiv.Prod
Equiv.boolArrowEquivProd_apply : ∀ (α : Type u_9) (f : Bool → α), (Equiv.boolArrowEquivProd α) f = (f false, f true)
-- Mathlib.Order.Hom.Lattice
InfHom.subtypeVal_apply : ∀ {β : Type u_3} [inst : SemilatticeInf β] {P : β → Prop} (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y))
  (x : { x // P x }), (InfHom.subtypeVal Pinf) x = ↑x
-- Aesop.RuleTac.Basic
Aesop.RuleTacInput.mk.inj : ∀ {goal : Lean.MVarId} {mvars : Aesop.UnorderedArraySet Lean.MVarId}
  {indexMatchLocations : Array Aesop.IndexMatchLocation} {patternSubsts? : Option (Array Aesop.Substitution)}
  {options : Aesop.Options'} {goal_1 : Lean.MVarId} {mvars_1 : Aesop.UnorderedArraySet Lean.MVarId}
  {indexMatchLocations_1 : Array Aesop.IndexMatchLocation} {patternSubsts?_1 : Option (Array Aesop.Substitution)}
  {options_1 : Aesop.Options'},
  { goal := goal, mvars := mvars, indexMatchLocations := indexMatchLocations, patternSubsts? := patternSubsts?,
        options := options } =
      { goal := goal_1, mvars := mvars_1, indexMatchLocations := indexMatchLocations_1,
        patternSubsts? := patternSubsts?_1, options := options_1 } →
    goal = goal_1 ∧
      mvars = mvars_1 ∧
        indexMatchLocations = indexMatchLocations_1 ∧ patternSubsts? = patternSubsts?_1 ∧ options = options_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.toAdd_eq_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α] {a : Multiplicative α}, Multiplicative.toAdd a = ⊤ ↔ a = ⊤
-- Batteries.Data.AssocList
/-- `O(n)`. Fold a monadic function over the list, from head to tail.  -/
Batteries.AssocList.foldlM : {m : Type u_1 → Type u_2} →
  {δ : Type u_1} → {α : Type u_3} → {β : Type u_4} → [Monad m] → (δ → α → β → m δ) → δ → Batteries.AssocList α β → m δ
-- Lean.Data.Lsp.Ipc
/-- Reads response, discarding notifications and server-to-client requests in between.
This function is meant purely for testing where we use `collectDiagnostics` explicitly
if we do care about such notifications.
 -/
Lean.Lsp.Ipc.readResponseAs : Lean.JsonRpc.RequestID → (α : Type) → [Lean.FromJson α] → Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Response α)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.coconeOfHasColimitEval_pt_X : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))] (n : ι),
  (HomologicalComplex.coconeOfHasColimitEval F).pt.X n =
    CategoryTheory.Limits.colimit (F.comp (HomologicalComplex.eval C c n))
-- Mathlib.Algebra.GCDMonoid.Basic
Prime.dvd_lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b p : α},
  Prime p → (p ∣ lcm a b ↔ p ∣ a ∨ p ∣ b)
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsPreFibered.pullbackMap.IsCartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : p.IsPreFibered] {R S : 𝒮} {a : 𝒳} (ha : p.obj a = S) (f : R ⟶ S),
  p.IsCartesian f (CategoryTheory.Functor.IsPreFibered.pullbackMap ha f)
-- Init.Data.Bool
Bool.not'_eq_not : ∀ (a : Bool), a.not' = !a
-- Aesop.Tree.Data
Aesop.Goal.postNormGoalAndMetaState? : Aesop.Goal → Option (Lean.MVarId × Lean.Meta.SavedState)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
divp_mk0 : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {b : G₀} (a : G₀) (hb : b ≠ 0), a /ₚ Units.mk0 b hb = a / b
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_intCast_mul : ∀ {x : ℝ}, 0 ≤ x → ∀ (n : ℤ) (z : ℝ), x ^ (↑n * z) = (x ^ n) ^ z
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  {Y Z : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)} (f : Y ⟶ Z),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).map f).right =
    CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right f).right ⋯
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Ring.HasFiniteQuotients.instNorthcottHeightOneSpectrumNatCoeMonoidWithZeroHomIdealAbsNormAsIdeal : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] [inst_2 : IsDedekindDomain R]
  [inst_3 : Module.Free ℤ R], Northcott fun p => Ideal.absNorm p.asIdeal
-- Mathlib.Data.Finset.Prod
Finset.product_eq_biUnion_right : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq (α × β)] (s : Finset α) (t : Finset β),
  s ×ˢ t = t.biUnion fun b => Finset.image (fun a => (a, b)) s
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.locallyLipschitzOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], IsOpen C → ConvexOn ℝ C f → LocallyLipschitzOn C f
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_comp_self : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e.symm ∘ ⇑e = id
-- Batteries.Data.PairingHeap
/-- A `Heap` is the nodes of the pairing heap.
Each node have two pointers: `child` going to the first child of this node,
and `sibling` goes to the next sibling of this tree.
So it actually encodes a forest where each node has children
`node.child`, `node.child.sibling`, `node.child.sibling.sibling`, etc.

Each edge in this forest denotes a `le a b` relation that has been checked, so
the root is smaller than everything else under it.
 -/
Batteries.PairingHeapImp.Heap : Type u → Type u
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfc_real_eq_complex : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal] [T2Space A] {a : A} (f : ℝ → ℝ),
  autoParam (IsSelfAdjoint a) cfc_real_eq_complex._auto_1 → cfc f a = cfc (fun x => ↑(f x.re)) a
-- Std.Data.ExtHashSet.Basic
/-- Checks whether an element is present in a set and inserts the element if it was not found.
If the hash set already contains an element that is equal (with regard to `==`) to the given
element, then the hash set is returned unchanged.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.ExtHashSet.containsThenInsert : {α : Type u} →
  {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → α → Bool × Std.ExtHashSet α
-- Mathlib.Tactic.Abel
/-- The monad for `Abel` contains, in addition to the `AtomM` state,
some information about the current type we are working over, so that we can consistently
use group lemmas or monoid lemmas as appropriate.  -/
Mathlib.Tactic.Abel.M : Type → Type
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_eq_false : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ) (e : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Poly.isUnsatDvd k e.norm = true → (k ∣ Int.Internal.Linear.Expr.denote ctx e) = False
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.closedComplemented_ker_of_rightInverse : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} {N : Type u_3} [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace N] [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M]
  [inst_6 : Module R N] [ContinuousSub M] (f₁ : M →L[R] N) (f₂ : N →L[R] M),
  Function.RightInverse ⇑f₂ ⇑f₁ → (↑f₁).ker.ClosedComplemented
-- Init.Data.List.Count
List.countP_singleton : ∀ {α : Type u_1} {p : α → Bool} {a : α}, List.countP p [a] = if p a = true then 1 else 0
-- Mathlib.Topology.Compactness.Compact
exists_clusterPt_of_compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] (f : Filter X) [f.NeBot], ∃ x, ClusterPt x f
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprBlockCtxt.repr : Lean.Doc.Parser.BlockCtxt → ℕ → Std.Format
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instBEqPosition : BEq Lean.Lsp.Position
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.condition_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] (j₁ j₂ : J) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f)
      (CategoryTheory.CategoryStruct.comp (f j₁) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f)
      (CategoryTheory.CategoryStruct.comp (f j₂) h)
-- Mathlib.Analysis.Convex.Deriv
StrictConvexOn.slope_lt_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S y → slope f x y < derivWithin f S y
-- Mathlib.Tactic.Convert
Convert.CheapConfig.mk.injEq : ∀ (toConfig toConfig_1 : Congr!.Config),
  ({ toConfig := toConfig } = { toConfig := toConfig_1 }) = (toConfig = toConfig_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- A `WeierstrassCurve` is in normal form of characteristic = 2, if it is
`Y² + XY = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharTwoJNeZeroNF`) or
`Y² + a₃Y = X³ + a₄X + a₆` (`WeierstrassCurve.IsCharTwoJEqZeroNF`).  -/
WeierstrassCurve.IsCharTwoNF : {R : Type u_1} → [CommRing R] → WeierstrassCurve R → Prop
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.chainBotCoeff_add_chainTopCoeff_le_two : ∀ {ι : 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 : Finite ι]
  [inst_6 : CharZero R] [inst_7 : IsDomain R] (i j : ι) [inst_8 : P.IsNotG2],
  RootPairing.chainBotCoeff i j + RootPairing.chainTopCoeff i j ≤ 2
-- Mathlib.Algebra.Ring.Defs
Ring.sub_eq_add_neg : ∀ {R : Type u} [self : Ring R] (a b : R), a - b = a + -b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_of_contains_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool} {k : α}, (Std.ExtHashSet.filter f m).contains k = true → m.contains k = true