mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.internalizeFn : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toPermFiber_injective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X),
  Function.Injective ⇑(hf.toPermFiber x)
-- Mathlib.Logic.Equiv.Defs
Equiv.mk.inj : ∀ {α : Sort u_1} {β : Sort u_2} {toFun : α → β} {invFun : β → α}
  {left_inv : autoParam (Function.LeftInverse invFun toFun) Equiv.left_inv._autoParam}
  {right_inv : autoParam (Function.RightInverse invFun toFun) Equiv.right_inv._autoParam} {toFun_1 : α → β}
  {invFun_1 : β → α} {left_inv_1 : autoParam (Function.LeftInverse invFun_1 toFun_1) Equiv.left_inv._autoParam}
  {right_inv_1 : autoParam (Function.RightInverse invFun_1 toFun_1) Equiv.right_inv._autoParam},
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toFun = toFun_1 ∧ invFun = invFun_1
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_eq_lieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableAt 𝕜 V x →
      DifferentiableAt 𝕜 W x → VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracket 𝕜 V W x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `sub_apply`. -/
ContinuousLinearMap.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_denom_add : ∀ {K : Type u} [inst : Field K] (x y : RatFunc K),
  (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkDoSeq : Array Lean.Syntax → Lean.Syntax
-- Mathlib.Data.List.Intervals
List.Ico.succ_singleton : ∀ {n : ℕ}, List.Ico n (n + 1) = [n]
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : EInt) (X : C),
  (t.eTruncLTGELTSelfToLTGE a b).app X = (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X))
-- Mathlib.Data.Sum.Order
_private.Mathlib.Data.Sum.Order.0.Option.elim.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : Option α → β → (α → β) → Sort u_2) →
      (x : Option α) →
        (x_1 : β) →
          (x_2 : α → β) →
            ((x : α) → (x_3 : β) → (f : α → β) → motive (some x) x_3 f) →
              ((y : β) → (x : α → β) → motive none y x) → motive x x_1 x_2
-- Mathlib.Topology.CompactOpen
/-- **Alias** of `ContinuousMap.isOpen_setOfPred_mapsTo`. -/
ContinuousMap.isOpen_setOf_mapsTo : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {K : Set X} {U : Set Y},
  IsCompact K → IsOpen U → IsOpen {f | Set.MapsTo (⇑f) K U}
-- Mathlib.Analysis.Subadditive
/-- A real-valued sequence is subadditive if it satisfies the inequality `u (m + n) ≤ u m + u n`
for all `m, n`.  -/
Subadditive : (ℕ → ℝ) → Prop
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `AddAction` across an `Equiv`  -/
Equiv.addAction : (M : Type u_1) → {α : Type u_4} → {β : Type u_5} → [inst : AddMonoid M] → α ≃ β → [AddAction M β] → AddAction M α
-- Init.Tactics
/-- `clear x...` removes the given hypotheses, or fails if there are remaining
references to a hypothesis.
 -/
Lean.Parser.Tactic.clear : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.isPlausibleStep_iff_step_eq : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.LawfulDeterministicIterator α Id]
  {it : Std.Iter β} {step : Std.IterStep (Std.Iter β) β}, it.IsPlausibleStep step ↔ ↑it.step = step
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.fromCompletion_unique : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  [inst_12 : T0Space β] [inst_13 : CompleteSpace β] (f : α →SL[σ] β) (g : UniformSpace.Completion α →SL[σ] β),
  (∀ (e : α), f e = g ↑e) → f.fromCompletion = g
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {fallback : β k'} {f : Option (β k) → Option (β k)},
  (m.alter k f).getD k' fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback
-- Lean.Parser.Attr
Lean.Parser.Attr.macro : Lean.Parser.Parser
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.card_triangles : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [inst_3 : Fintype α] [inst_4 : Fintype β] [inst_5 : Fintype γ]
  [SimpleGraph.TripartiteFromTriangles.NoAccidental t],
  ((SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3).card = t.card
-- Mathlib.Data.Multiset.Fintype
Multiset.consEquiv.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {v : α},
  Multiset.consEquiv =
    { toFun := fun x => if h : x.fst = v ∧ ↑x.snd = Multiset.count v m then none else some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩,
      invFun := fun x => x.elim ⟨v, ⟨Multiset.count v m, ⋯⟩⟩ fun x => ⟨x.fst, Fin.castLE ⋯ x.snd⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Std.Data.HashMap.Iterator
/-- Returns a finite iterator over the entries of a hash map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashMap.keysIter : {α β : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Std.Iter α
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Frame.MinimalAxioms.inf_sSup_eq : ∀ {α : Type u} (s : Set α) (a : α) [inst : CompleteLattice α], Order.Frame.MinimalAxioms α → a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
-- Mathlib.Topology.MetricSpace.Basic
Metric.isClosed_of_pairwise_le_dist : ∀ {γ : Type w} [inst : MetricSpace γ] {s : Set γ} {ε : ℝ}, 0 < ε → (s.Pairwise fun x y => ε ≤ dist x y) → IsClosed s
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- Group topologies on `γ` form a complete lattice, with `⊥` the discrete topology and
`⊤` the indiscrete topology.

The infimum of a collection of group topologies is the topology generated by all their open sets
(which is a group topology).

The supremum of two group topologies `s` and `t` is the infimum of the family of all group
topologies contained in the intersection of `s` and `t`.  -/
AddGroupTopology.instCompleteSemilatticeInf : {α : Type u} → [inst : AddGroup α] → CompleteSemilatticeInf (AddGroupTopology α)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameTactic : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.eq_of_degree_le_of_eval_index_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι),
  Set.InjOn v ↑s →
    f.degree ≤ ↑s.card →
      f.degree = g.degree →
        f.leadingCoeff = g.leadingCoeff → (∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) → f = g
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instTop.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M], SubAddAction.instTop = { top := { carrier := Set.univ, vadd_mem' := ⋯ } }
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_nat : ∀ (x : ℕ), ↑x = ↑x
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_filterMap' : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {l : List ((a : α) × β a)} {f : (a : α) → β a → Option (γ a)},
  Std.Internal.List.keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
    Std.Internal.List.keys (List.filter (fun p => (f p.fst p.snd).isSome) l)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful] (X : C),
  CategoryTheory.IsIso (h.unit.app X)
-- Lean.Expr
/-- The `fvar` constructor represents free variables. Such a *free* variable
occurrence is not bound by an earlier `lam`, `forallE`, or `letE`
constructor and its binder exists in a local context only.

Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://doi.org/10.1145/1017472.1017477)
for additional details.

When "visiting" the body of a binding expression (i.e. `lam`, `forallE`, or `letE`),
bound variables are converted into free variables using a unique identifier,
and their user-facing name, type, value (for `letE`), and binder annotation
are stored in the `LocalContext`.
 -/
Lean.Expr.fvar : Lean.FVarId → Lean.Expr
-- Init.Data.String.Basic
String.Pos.Raw.isValid_iff_exists_take_toList : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p ↔ ∃ i, p.byteIdx = (String.ofList (List.take i s.toList)).utf8ByteSize
-- Mathlib.Order.Concept
/-- The concept generated from the upper polar of a set, i.e. the smallest concept containing the
set of objects `s`.  -/
Concept.ofObjects : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → Set α → Concept α β r
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.setIntegral_tilted_mul_eq_cgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (g : Ω → E) (s : Set Ω),
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    (∫ (x : Ω) in s, g x ∂μ.tilted fun x => t * X x) =
      ∫ (x : Ω) in s, Real.exp (t * X x - ProbabilityTheory.cgf X μ t) • g x ∂μ
-- Lean.Parser.Types
Lean.Parser.InputContext.endPos_valid : ∀ (self : Lean.Parser.InputContext), self.endPos ≤ self.inputString.rawEndPos
-- Lean.Elab.InfoTree.Types
Lean.Elab.ErrorNameInfo.mk : Lean.Syntax → Lean.Name → Lean.Elab.ErrorNameInfo
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.le_def : ∀ {M : Type u_1} [inst : AddGroup M] [inst_1 : Lattice M] {a b : ArchimedeanOrder M},
  a ≤ b ↔ ∃ n, |ArchimedeanOrder.val b| ≤ n • |ArchimedeanOrder.val a|
-- Mathlib.Order.Lattice
/-- Pointwise minimum of two monotone functions is a monotone function.  -/
Monotone.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β},
  Monotone f → Monotone g → Monotone fun x => min (f x) (g x)
-- Init.SizeOf
ByteArray.mk.sizeOf_spec : ∀ (data : Array UInt8), sizeOf { data := data } = 1 + sizeOf data
-- Mathlib.Order.WellFoundedSet
Finset.isWF : ∀ {α : Type u_2} [inst : Preorder α] (s : Finset α), (↑s).IsWF
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_eq_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), gcd a b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_inv_app_right : ∀ {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 Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.right =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.right)
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.centralizer_le : ∀ {M : Type u_1} {S T : Set M} [inst : Monoid M], S ⊆ T → Submonoid.centralizer T ≤ Submonoid.centralizer S
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
/-- For a global integral curve `γ`, if it crosses itself at `a b : ℝ`, then it is periodic with
period `a - b`.  -/
IsMIntegralCurve.periodic_of_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} [T2Space M] {a b : ℝ}
  [BoundarylessManifold I M],
  IsMIntegralCurve γ v → (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) → γ a = γ b → Function.Periodic γ (a - b)
-- Mathlib.Lean.ContextInfo
/-- Run a tactic computation in the context of an infotree node, capturing InfoTrees produced.  -/
Lean.Elab.ContextInfo.runTacticCapturingInfoTree : {α : Type} →
  Lean.Elab.ContextInfo →
    Lean.Elab.TacticInfo →
      Lean.MVarId →
        (Lean.MVarId → Lean.MetaM α) → Lean.Elab.Command.CommandElabM (α × Lean.PersistentArray Lean.Elab.InfoTree)
-- Mathlib.Data.Fintype.Inv
Function.Embedding.invFun_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β) [inst_2 : Nonempty α],
  (Set.range ⇑f).domRestrict (Function.invFun ⇑f) = f.invOfMemRange
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.toList.eq_def : ∀ {V : Type u} [inst : Quiver V] {a : V} (x : V) (x_1 : Quiver.Path a x),
  x_1.toList =
    match x, x_1 with
    | .(a), Quiver.Path.nil => []
    | x, p.cons a_1 => c :: p.toList
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.Set.functor_map_hom_apply_coe : ∀ (X : Type u) (κ : Cardinal.{u}) {X_1 Y : HasCardinalLT.Set X κ} (f : X_1 ⟶ Y) (x : ↑(⋯.functor.obj X_1)),
  ↑((CategoryTheory.ConcreteCategory.hom ((HasCardinalLT.Set.functor X κ).map f)) x) = ↑x
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.corootSpace.congr_simp : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] [inst_4 : H.IsCartanSubalgebra] [inst_5 : IsNoetherian R L]
  (α α_1 : ↥H → R), α = α_1 → LieAlgebra.corootSpace α = LieAlgebra.corootSpace α_1
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.allM_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Std.Iter β} {f : β → m (Option β')}
  {p : β' → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.Iter.filterMapM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => p fx
          | none => pure { down := true })
      (Std.Iter.mapM pure it)
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.QuotStep.transportAlongEquiv.congr_simp : ∀ {α₁ : Type u_1} {m : Type u_1 → Type u_2} {β α₂ : Type u_1} [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [inst_2 : Monad m] [inst_3 : LawfulMonad m] {ita : Std.IterM m β} {itb : Std.IterM m β}
  (h : ita.Equiv itb) (a a_1 : ita.QuotStep),
  a = a_1 → Std.IterM.QuotStep.transportAlongEquiv h a = Std.IterM.QuotStep.transportAlongEquiv h a_1
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousLinearEquiv.compContinuousAlternatingMap_coe : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] [inst_6 : TopologicalSpace N] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N']
  [inst_9 : TopologicalSpace N'] (e : N ≃L[R] N') (f : M [⋀^ι]→L[R] N),
  ⇑(e.continuousAlternatingMapCongrRightEquiv f) = ⇑e ∘ ⇑f
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for isomorphisms in `ComposableArrows C 2`.  -/
CategoryTheory.ComposableArrows.isoMk₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 2} →
      (app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝) →
        (app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝) →
          (app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝) →
            autoParam
                (CategoryTheory.CategoryStruct.comp
                    (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝) app₁.hom =
                  CategoryTheory.CategoryStruct.comp app₀.hom
                    (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
                CategoryTheory.ComposableArrows.isoMk₂._auto_1 →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂.hom =
                    CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_247✝))
                  CategoryTheory.ComposableArrows.isoMk₂._auto_3 →
                (f ≅ g)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.mk : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [inst : ENorm 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : TopologicalSpace F] [inst_3 : Zero E] [inst_4 : Zero F] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 F]
  {l : Filter α} {f : α → E} {g : α → F},
  (∀ U ∈ nhds 0, ∃ V ∈ nhds 0, (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => egauge 𝕜 V (g x)) → f =O[𝕜; l] g
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsClosedEmbedding.uliftMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → Topology.IsClosedEmbedding (ULift.map f)
-- Mathlib.Data.List.MinMax
List.le_maximum_of_length_pos_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {b : α} (h : 0 < l.length),
  b ≤ List.maximum_of_length_pos h ↔ ↑b ≤ l.maximum
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Hom.of.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {as as_1 : CategoryTheory.Oplax.LaxTrans.Modification η θ},
  { as := as } = { as := as_1 } → as = as_1
-- Init.Data.String.Lemmas.Basic
String.sliceTo_endPos : ∀ {s : String}, s.sliceTo s.endPos = s.toSlice
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `MDifferentiableWithinAt` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabMDifferentiableWithinAt : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.wn : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp S.opcyclesOpIso.hom S.toCycles.op = S.op.fromOpcycles
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The parts in a complete equipartite subgraph are pairwise disjoint.  -/
SimpleGraph.CompleteEquipartiteSubgraph.disjoint : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t), (↑K.parts).Pairwise Disjoint
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_triangle_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q r : P), ((signedDist v) p) r - ((signedDist v) q) r = ((signedDist v) p) q
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalDataValueExprCore : Lean.Expr → Lean.MetaM Lean.DataValue
-- Mathlib.Order.UpperLower.Closure
UpperSet.lt_erase : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {a : α}, s < s.erase a ↔ a ∈ s
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The canonical map from a component to the direct limit.  -/
DirectLimit.NonUnitalRing.of : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                    [inst_6 : Nonempty ι] → (i : ι) → G i →ₙ+* DirectLimit G f
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_finitary : ∀ {α : Type u_1} {E : Set α}, (Matroid.freeOn E).Finitary
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.le_sup_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeSup β] [inst_3 : ContinuousSup β] (f g : α →ₘ[μ] β), g ≤ f ⊔ g
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformContinuous_restrict : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (S : Set ι), UniformContinuous S.domRestrict
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.union_eq_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulUpwardEnumerableLeast?OfNatNat : Std.PRange.LawfulUpwardEnumerableLeast? (Fin 0)
-- Init.Data.List.MinMax
List.max?_eq_max?_attach : ∀ {α : Type u_1} [inst : Max α] [inst_1 : Std.MaxEqOr α] {xs : List α}, xs.max? = Option.map Subtype.val xs.attach.max?
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The proposition that two submodules are orthogonal, denoted as `U ⟂ V`.  -/
Submodule.«term_⟂_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_eq_of_two_nsmul_eq : ∀ {θ ψ : Real.Angle}, 2 • θ = 2 • ψ → θ.tan = ψ.tan
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_mgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ]
  (s : Set Ω),
  (μ.tilted fun x => t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a) / ProbabilityTheory.mgf X μ t) ∂μ
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- The Roth number is a subadditive function. Note that by Fekete's lemma this shows that
the limit `rothNumberNat N / N` exists, but Roth's theorem gives the stronger result that this
limit is actually `0`.  -/
rothNumberNat_add_le : ∀ (M N : ℕ), rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mul_left : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (a b : N ⋊[φ] G),
  (a * b).left = a.left * (φ a.right) b.left
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
AffineBasis.toMatrix_apply : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} (q : ι' → P) (i : ι') (j : ι),
  b.toMatrix q i j = (b.coord j) (q i)