mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Basic
Nat.add_le_add_right : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), n + k ≤ m + k
-- Std.Time.Zoned.ZoneRules
/-- Universal Time (UT), often referred to as UTC.
 -/
Std.Time.TimeZone.UTLocal.ut : Std.Time.TimeZone.UTLocal
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Construct the adjunction to the comparison functor.
 -/
CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              [∀ (A : adj.toComonad.Coalgebra),
                    CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] →
                CategoryTheory.Functor adj.toComonad.Coalgebra C
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx?.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ),
  x.keyAtIdx? x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, x => none
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n =>
      match compare n l.size with
      | Ordering.lt => l.keyAtIdx? n
      | Ordering.eq => some k
      | Ordering.gt => r.keyAtIdx? (n - l.size - 1)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.superposeAC?.go : Lean.Grind.AC.Seq →
  Lean.Grind.AC.Seq →
    Option Lean.Grind.AC.Seq →
      Option Lean.Grind.AC.Seq →
        Option Lean.Grind.AC.Seq → Option (Lean.Grind.AC.Seq × Lean.Grind.AC.Seq × Lean.Grind.AC.Seq)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.iff_id_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.Limits.IsZero X ↔ CategoryTheory.CategoryStruct.id X = 0
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.LiesOver.embedding_liesOver_of_isReal : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) {v : NumberField.InfinitePlace K} [w.LiesOver v],
  v.IsReal → NumberField.ComplexEmbedding.LiesOver w.embedding v.embedding
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_neg_right`. -/
MonovaryOn.neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g s → AntivaryOn f (-g) s
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_comp : ∀ {o o' : Ordinal.{max u v}} {f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}},
  (∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj) →
    ∀ {g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}} (hg : o'.blsub g = o),
      (o'.blsub fun a ha => f (g a ha) ⋯) = o.blsub f
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAddCommMonoid : {α : Type u} → [AddCommSemigroup α] → AddCommMonoid (WithZero α)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_coe_eq : ∀ {α : Type u_1} {r : NNReal} {f : α → NNReal}, HasSum f r → ∑' (a : α), ↑(f a) = ↑r
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.union_left : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α},
  MeasureTheory.AEDisjoint μ s u → MeasureTheory.AEDisjoint μ t u → MeasureTheory.AEDisjoint μ (s ∪ t) u
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_ofInt : ∀ (i : ℤ) (h : System.Platform.numBits = 32), (ISize.ofInt i).toBitVec32 h = BitVec.ofInt 32 i
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.comap_comp : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (c : AddCon P)
  (g : N → P) (f : M → N) (hg : ∀ (x y : N), g (x + y) = g x + g y) (hf : ∀ (x y : M), f (x + y) = f x + f y),
  AddCon.comap (g ∘ f) ⋯ c = AddCon.comap f hf (AddCon.comap g hg c)
-- Std.Data.Iterators.Producers.Vector
/-- Returns a finite iterator for the given vector starting at the given index.
The iterator yields the elements of the vector in order and then terminates.

The monadic version of this iterator is
`Vector.iterFromIdxM`.

**Termination properties:**

* `Finite` instance: always

* `Productive` instance: always
 -/
Vector.iterFromIdx : {n : ℕ} → {α : Type w} → Vector α n → ℕ → Std.Iter α
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_bijective : ∀ {n : ℕ}, Function.Bijective Composition.reverse
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).get? k = f (m.get? k)
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunctionAux_succ : ∀ {c : ℝ} (f : ℕ → Bool),
  (fun n => Cardinal.cantorFunctionAux c f (n + 1)) = fun n => c * Cardinal.cantorFunctionAux c (fun n => f (n + 1)) n
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.listToPath.eq_1 : ∀ {α : Type u_1}, Quiver.SingleObj.listToPath [] = Quiver.Path.nil
-- Mathlib.CategoryTheory.GradedObject
/-- The equivalence between β-graded objects and γ-graded objects,
given an equivalence between β and γ.
 -/
CategoryTheory.GradedObject.comapEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {β γ : Type w} → β ≃ γ → (CategoryTheory.GradedObject β C ≌ CategoryTheory.GradedObject γ C)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.mem_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α × β} {t : RBTree.RBMap α β cmp}, x ∈ t.toList ↔ x ∈ ↑t
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.find? : Lean.Meta.MVarRenaming → Lean.MVarId → Option Lean.MVarId
-- Mathlib.Topology.Separation.Regular
CompletelyNormalSpace.of_regularSpace_secondCountableTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X], CompletelyNormalSpace X
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g h i j : b ⟶ c} (α : g ≅ h) (η : h ⟶ i)
  {ηs : i ⟶ j} {θ : CategoryTheory.CategoryStruct.comp f i ⟶ CategoryTheory.CategoryStruct.comp f j},
  CategoryTheory.Bicategory.whiskerLeft f ηs = θ →
    CategoryTheory.Bicategory.whiskerLeft f
        (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeftIso f α).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) θ)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s : Finset α} (a : α),
  s / {a} = Finset.image (fun x => x / a) s
-- Mathlib.Topology.UniformSpace.CompareReals
CompareReals.instInhabitedBourbakiℝ : Inhabited CompareReals.Bourbakiℝ
-- Std.Data.ExtHashSet.Basic
/-- Computes the difference of the given hash sets.

This function always iterates through the smaller set.
 -/
Std.ExtHashSet.diff : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → Std.ExtHashSet α → Std.ExtHashSet α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.minKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKey! = t₂.minKey!
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_mul : ∀ {R : Type u} [inst : CommSemiring R] (f g : R),
  PrimeSpectrum.basicOpen (f * g) = PrimeSpectrum.basicOpen f ⊓ PrimeSpectrum.basicOpen g
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGE : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, (compare a k).isGE = true) → (a : α) × β a
-- Mathlib.Tactic.Order.ToInt
/-- Auxiliary definition used by the `order` tactic to transfer facts in a linear order to `ℤ`.  -/
Mathlib.Tactic.Order.ToInt.toInt : {α : Type u_1} → [LinearOrder α] → {n : ℕ} → (Fin n → α) → Fin n → ℤ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_pow_subset : ∀ {α : Type u_2} [inst : Monoid α] {s t : Set α} {n : ℕ}, (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph isomorphism is a bijective map on vertex sets that respects adjacency relations.

The notation `G ≃g G'` represents the type of graph isomorphisms.
 -/
SimpleGraph.«term_≃g_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns a `List` of the key/value pairs in order.  -/
Std.DTreeMap.Internal.Impl.Const.toList : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → List (α × β)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedModifier : Inhabited Std.Time.Modifier
-- Mathlib.Tactic.GCongr.Core
/-- Return the `gcongr` lemmas whose conclusion has the shape `relName (lhs ..) (rhs ..)`,
where `arity` is the number of arguments in `..`. This is used by the `gcongr` tactic.  -/
Mathlib.Tactic.GCongr.findGCongrLemmas? : Lean.Name → Lean.Name → Lean.Name → ℕ → Lean.CoreM (List Mathlib.Tactic.GCongr.GCongrLemma)
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommGroupUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [AddCommGroup β] → AddCommGroup (UniformOnFun α β 𝔖)
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.singleton_inter : ∀ {α : Type u} {a : α} {s : Set α}, ({a} ∩ s).Subsingleton
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoInverseComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E}
  {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D),
  i.isoInverseComp.inv.app X =
    CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Icc : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₂ ≤ a₁ → b₁ ≤ b₂ → Finset.Icc a₁ b₁ ⊆ Finset.Icc a₂ b₂
-- Mathlib.Order.UpperLower.Closure
upperClosure_anti : ∀ {α : Type u_1} [inst : Preorder α], Antitone upperClosure
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.continuous_extension : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β} [CompleteSpace β],
  Continuous (UniformSpace.Completion.extension f)
-- Mathlib.Data.Part
Part.union_def : ∀ {α : Type u_1} [inst : Union α] (a b : Part α),
  a ∪ b = do
    let y ← a
    Part.map (fun x => y ∪ x) b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Topology.UniformSpace.Cauchy
TotallyBounded.eq_1 : ∀ {α : Type u} [uniformSpace : UniformSpace α] (s : Set α),
  TotallyBounded s = ∀ d ∈ uniformity α, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
-- Lean.ExtraModUses
Lean.IndirectModUse.mk.sizeOf_spec : ∀ (kind : String) (declName : Lean.Name),
  sizeOf { kind := kind, declName := declName } = 1 + sizeOf kind + sizeOf declName
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivAt_const_add_iff`. -/
HasDerivAt.const_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasDerivAt f f' x → HasDerivAt (fun x => c + f x) f' x
-- Lean.Meta.Closure
Lean.Meta.Closure.State.mk.injEq : ∀ (visitedLevel : Lean.LevelMap Lean.Level) (visitedExpr : Lean.ExprStructMap Lean.Expr) (levelParams : Array Lean.Name)
  (nextLevelIdx : ℕ) (levelArgs : Array Lean.Level)
  (newLocalDecls newLocalDeclsForMVars newLetDecls : Array Lean.LocalDecl) (nextExprIdx : ℕ)
  (exprMVarArgs exprFVarArgs : Array Lean.Expr) (toProcess : Array Lean.Meta.Closure.ToProcessElement)
  (visitedLevel_1 : Lean.LevelMap Lean.Level) (visitedExpr_1 : Lean.ExprStructMap Lean.Expr)
  (levelParams_1 : Array Lean.Name) (nextLevelIdx_1 : ℕ) (levelArgs_1 : Array Lean.Level)
  (newLocalDecls_1 newLocalDeclsForMVars_1 newLetDecls_1 : Array Lean.LocalDecl) (nextExprIdx_1 : ℕ)
  (exprMVarArgs_1 exprFVarArgs_1 : Array Lean.Expr) (toProcess_1 : Array Lean.Meta.Closure.ToProcessElement),
  ({ visitedLevel := visitedLevel, visitedExpr := visitedExpr, levelParams := levelParams, nextLevelIdx := nextLevelIdx,
        levelArgs := levelArgs, newLocalDecls := newLocalDecls, newLocalDeclsForMVars := newLocalDeclsForMVars,
        newLetDecls := newLetDecls, nextExprIdx := nextExprIdx, exprMVarArgs := exprMVarArgs,
        exprFVarArgs := exprFVarArgs, toProcess := toProcess } =
      { visitedLevel := visitedLevel_1, visitedExpr := visitedExpr_1, levelParams := levelParams_1,
        nextLevelIdx := nextLevelIdx_1, levelArgs := levelArgs_1, newLocalDecls := newLocalDecls_1,
        newLocalDeclsForMVars := newLocalDeclsForMVars_1, newLetDecls := newLetDecls_1, nextExprIdx := nextExprIdx_1,
        exprMVarArgs := exprMVarArgs_1, exprFVarArgs := exprFVarArgs_1, toProcess := toProcess_1 }) =
    (visitedLevel = visitedLevel_1 ∧
      visitedExpr = visitedExpr_1 ∧
        levelParams = levelParams_1 ∧
          nextLevelIdx = nextLevelIdx_1 ∧
            levelArgs = levelArgs_1 ∧
              newLocalDecls = newLocalDecls_1 ∧
                newLocalDeclsForMVars = newLocalDeclsForMVars_1 ∧
                  newLetDecls = newLetDecls_1 ∧
                    nextExprIdx = nextExprIdx_1 ∧
                      exprMVarArgs = exprMVarArgs_1 ∧ exprFVarArgs = exprFVarArgs_1 ∧ toProcess = toProcess_1)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- If `F` is left adjoint to `G`, then the category of algebras over `F` is equivalent to the
category of coalgebras over `G`.  -/
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (F ⊣ G) → (CategoryTheory.Endofunctor.Algebra F ≌ CategoryTheory.Endofunctor.Coalgebra G)
-- Init.Data.Repr
instReprFin : (n : ℕ) → Repr (Fin n)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.subset_closure_withConstants : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A s : Set M},
  A ⊆ ↑((FirstOrder.Language.Substructure.closure (L.withConstants ↑A)).toFun s)
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_empty_left : ∀ {α : Type u_1} (t s : Set α), t.ite ∅ s = s \ t
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.countLeadingSpaces : Lean.FileMap → String.Pos.Raw → ℕ
-- Mathlib.Data.Nat.GCD.Basic
Nat.dvd_lcm_of_dvd_left : ∀ {a b : ℕ}, a ∣ b → ∀ (c : ℕ), a ∣ b.lcm c
-- Mathlib.RingTheory.RingHom.Bijective
RingHom.Bijective.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₂_map_app_f : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : CategoryTheory.Functor C D} (f : X ⟶ Y)
  (P : CategoryTheory.Idempotents.Karoubi C),
  (((CategoryTheory.Idempotents.functorExtension₂ C D).map f).app P).f =
    CategoryTheory.CategoryStruct.comp (f.app P.X) (Y.map P.p)
-- Mathlib.Computability.Primrec.List
Primrec.fin_app : ∀ {σ : Type u_3} [inst : Primcodable σ] {n : ℕ}, Primrec₂ id
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapCongr_inv_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g)
  (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.mapCongr f g h).inv.app X_1).left = CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_μ : ∀ {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 G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ G X Y =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (i.inv.app X) (i.inv.app Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
        (i.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)))
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.hom_ext_iff : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {M : Type u_3} [inst_1 : Monoid M]
  {f g : HNNExtension G A B φ →* M},
  f = g ↔ f.comp HNNExtension.of = g.comp HNNExtension.of ∧ f HNNExtension.t = g HNNExtension.t
-- Init.Data.Format.Syntax
Lean.Syntax.instToFormatTSyntax : {k : Lean.SyntaxNodeKinds} → Std.ToFormat (Lean.TSyntax k)
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) → ((n : ℕ) → motive [] n) → ((a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n) → motive x x_1
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a `LinearIsometryEquiv`.
For an unbundled version see `ContinuousLinearMap.flip`.  -/
ContinuousLinearMap.flipₗᵢ' : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      (E : Type u_4) →
        (F : Type u_6) →
          (G : Type u_8) →
            [inst : SeminormedAddCommGroup E] →
              [inst_1 : SeminormedAddCommGroup F] →
                [inst_2 : SeminormedAddCommGroup G] →
                  [inst_3 : NontriviallyNormedField 𝕜] →
                    [inst_4 : NontriviallyNormedField 𝕜₂] →
                      [inst_5 : NontriviallyNormedField 𝕜₃] →
                        [inst_6 : NormedSpace 𝕜 E] →
                          [inst_7 : NormedSpace 𝕜₂ F] →
                            [inst_8 : NormedSpace 𝕜₃ G] →
                              (σ₂₃ : 𝕜₂ →+* 𝕜₃) →
                                (σ₁₃ : 𝕜 →+* 𝕜₃) →
                                  [inst_9 : RingHomIsometric σ₂₃] →
                                    [inst_10 : RingHomIsometric σ₁₃] →
                                      (E →SL[σ₁₃] F →SL[σ₂₃] G) ≃ₗᵢ[𝕜₃] F →SL[σ₂₃] E →SL[σ₁₃] G
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → C ⊆ M.E
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalGroup.IsSES.mulExact : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C},
  TopologicalGroup.IsSES φ ψ → Function.MulExact ⇑φ ⇑ψ
-- Mathlib.Data.Int.Order.Units
Int.isUnit_sq : ∀ {a : ℤ}, IsUnit a → a ^ 2 = 1
-- Mathlib.Topology.Order.WithTop
WithTop.isOpenEmbedding_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Topology.IsOpenEmbedding WithTop.some
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotal_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂)
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotal c₁₂ i₁ i₂ i₁₂ h)
-- Mathlib.Topology.Sheaves.Flasque
_private.Mathlib.Topology.Sheaves.Flasque.0.TopCat.Sheaf.IsFlasque.epi_of_shortExact.match_1_7.splitter : (motive : Fin 2 → Sort u_1) → (x : Fin 2) → (Unit → motive 0) → (Unit → motive 1) → motive x
-- Batteries.Data.List.Basic
List.zipWithLeft'TR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (as : List α) (bs : List β),
  List.zipWithLeft'TR f as bs = List.zipWithLeft'TR.go f as bs #[]
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α}
  (h₁ : (List.map Prod.fst l).contains k = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) = true},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKey k h' = t.getKey k ⋯
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Constructor for objects in the free category on a reflexive quiver.  -/
CategoryTheory.Cat.FreeRefl.mk : {V : Type u_1} → [inst : CategoryTheory.ReflQuiver V] → V → CategoryTheory.Cat.FreeRefl V
-- Mathlib.CategoryTheory.Subobject.FactorThru
/-- When `f : X ⟶ Y` and `P : MonoOver Y`,
`P.Factors f` expresses that there exists a factorisation of `f` through `P`.
Given `h : P.Factors f`, you can recover the morphism as `P.factorThru f h`.
 -/
CategoryTheory.MonoOver.Factors : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → CategoryTheory.MonoOver Y → (X ⟶ Y) → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
/-- `tan x` takes the junk value `0` when `cos x = 0`  -/
Real.tan_eq_zero_of_cos_eq_zero : ∀ {x : ℝ}, Real.cos x = 0 → Real.tan x = 0
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_toMultiset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), DFinsupp.toMultiset (Multiset.toDFinsupp s) = s