mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.lctx : Lean.Elab.Term.LevelMVarErrorInfo → Lean.LocalContext
-- Lean.Elab.PreDefinition.Main
/-- Checks consistency of a clique of TerminationHints:

* If not all have a hint, the hints are ignored (log error)
* None have both `termination_by` and `partial_fixpoint` (throw error)
* If one has `structural` or `partial_fixpoint`, check that all have it (else throw error)
* A `structural` should not have a `decreasing_by` (else log error)

 -/
Lean.Elab.checkTerminationByHints : Array Lean.Elab.PreDefinition → Lean.CoreM Unit
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.normed_le_div_measure_closedBall_rOut : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsAddHaarMeasure] (K : ℝ),
  f.rOut ≤ K * f.rIn → ∀ (x : E), f.normed μ x ≤ K ^ Module.finrank ℝ E / μ.real (Metric.closedBall c f.rOut)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.instDecidableEqHom_1 : {ι : Type v} → {i j : CategoryTheory.Pairwise ι} → [DecidableEq ι] → DecidableEq (i ⟶ j)
-- Mathlib.Data.Finset.Sups
Finset.infs_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s : Finset α}, s ⊼ ∅ = ∅
-- Mathlib.Tactic.Simps.Basic
/-- Checks if there are declarations in the current file in the namespace `{str}.Simps` that are
not used.  -/
Simps.checkForUnusedCustomProjs : Lean.Syntax → Lean.Name → Array Simps.ParsedProjectionData → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesMonomorphisms.iso_iff`. -/
CategoryTheory.Functor.preservesMonomorphisms.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), F.PreservesMonomorphisms ↔ G.PreservesMonomorphisms
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_iff_eq_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α} [inst_2 : OrderTop α], Order.succ a ≤ a ↔ a = ⊤
-- Lean.Data.Lsp.Utf16
Lean.DeclarationRange.ofStringPositions : Lean.FileMap → String.Pos.Raw → String.Pos.Raw → Lean.DeclarationRange
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.X : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : TopologicalSpace R],
  MvPowerSeries.HasEval fun s => MvPowerSeries.X s
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.injective : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x → ∀ [Nontrivial R], Function.Injective x
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_ofReal_mul : ∀ {r : ℝ}, 0 < r → ∀ {x : ℂ}, x ≠ 0 → Complex.log (↑r * x) = ↑(Real.log r) + Complex.log x
-- Init.Data.Nat.Lemmas
Nat.mul_self_sub_mul_self_eq : ∀ (a b : ℕ), a * a - b * b = (a + b) * (a - b)
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.  -/
Pi.sum_norm_apply_le_norm' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i),
  ∑ i, ‖f i‖ ≤ Fintype.card ι • ‖f‖
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.congr_fun : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {D1 D2 : LieDerivation R L M}, D1 = D2 → ∀ (a : L), D1 a = D2 a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- This instance is needed to create an instance for `AddCommMonoid (MultiseriesExpansion basis)`,
which is necessary for using the `abel` tactic in our proofs.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.instZeroMultiseries : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Zero (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.notNilRec_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1}
  (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯) (h' : G.Adj u v)
  (q' : G.Walk v w), SimpleGraph.Walk.notNilRec (fun {u v w} => cons) (SimpleGraph.Walk.cons h' q') ⋯ = cons h' q'
-- Mathlib.NumberTheory.SmoothNumbers
/-- The `n`-smooth numbers agree with the `primesBelow n`-factored numbers.  -/
Nat.smoothNumbers_eq_factoredNumbers_primesBelow : ∀ (n : ℕ), n.smoothNumbers = Nat.factoredNumbers n.primesBelow
-- Mathlib.Algebra.Homology.Homotopy
/-- If `f` if a homotopy equivalence and `h` is a homotopy from `f.hom` to
a morphism `g`, then this is a homotopy equivalence whose `hom` field is `g`.  -/
HomotopyEquiv.copy : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} → (f : HomotopyEquiv C D) → {g : C ⟶ D} → Homotopy f.hom g → HomotopyEquiv C D
-- Lean.Server.CodeActions.Provider
/-- Merges the results of two `FindTacticResult`s. This just prefers the second (inner) one,
unless the inner tactic is a dispreferred tactic sequence and the outer one is preferred.
This is used to implement whitespace-sensitive selection of tactic sequences.  -/
_private.Lean.Server.CodeActions.Provider.0.Lean.CodeAction.findTactic?.merge : Option Lean.CodeAction.FindTacticResult → Lean.CodeAction.FindTacticResult → Lean.CodeAction.FindTacticResult
-- Mathlib.Control.Bifunctor
LawfulBifunctor.mk : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F],
  (∀ {α : Type u₀} {β : Type u₁} (x : F α β), bimap id id x = x) →
    (∀ {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
        (x : F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x) →
      LawfulBifunctor F
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.get_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {a : α} {h : a ∈ m}, m.get a h = Std.DHashMap.Internal.Raw₀.get ⟨m, ⋯⟩ a ⋯
-- Mathlib.Topology.MetricSpace.Gluing
Metric.toInductiveLimit.eq_1 : ∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)} (I : ∀ (n : ℕ), Isometry (f n))
  (n : ℕ) (x : X n), Metric.toInductiveLimit I n x = Quotient.mk'' ⟨n, x⟩
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats : Type
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection.congr_simp : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i i_1 : ι}
  (e_i : i = i_1) {j j_1 : ι} (e_j : j = j_1) (hij : i ≠ j) (b b_1 : F),
  b = b_1 → Matrix.SpecialLinearGroup.transvection hij b = Matrix.SpecialLinearGroup.transvection ⋯ b_1
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `s` is a limit kernel fork and `k : W ⟶ X` satisfies `k ≫ f = 0`, then there is some
`l : W ⟶ s.X` such that `l ≫ fork.ι s = k`.  -/
CategoryTheory.Limits.KernelFork.IsLimit.lift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {s : CategoryTheory.Limits.KernelFork f} →
            CategoryTheory.Limits.IsLimit s →
              {W : C} →
                (k : W ⟶ X) →
                  CategoryTheory.CategoryStruct.comp k f = 0 →
                    { l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.Fork.ι s) = k }
-- Mathlib.Logic.Small.Defs
small_type : Small.{max (u + 1) v, u + 1} (Type u)
-- Init.Data.UInt.Lemmas
USize.toUInt32_mul : ∀ (a b : USize), (a * b).toUInt32 = a.toUInt32 * b.toUInt32
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.exists_null_frontier_thickening : ∀ {Ω : Type u_1} [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (s : Set Ω) {a b : ℝ},
  a < b → ∃ r ∈ Set.Ioo a b, μ (frontier (Metric.thickening r s)) = 0
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.encodeSigma.match_1.eq_1 : ∀ {α : Type u_1} {γ : α → Type u_2} (motive : Sigma γ → Sort u_3) (a : α) (b : γ a)
  (h_1 : (a : α) → (b : γ a) → motive ⟨a, b⟩),
  (match ⟨a, b⟩ with
    | ⟨a, b⟩ => h_1 a b) =
    h_1 a b
-- Mathlib.Topology.NhdsSet
Filter.Eventually.union_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X} {p : X → Prop},
  (∀ᶠ (x : X) in nhdsSet (s ∪ t), p x) ↔ (∀ᶠ (x : X) in nhdsSet s, p x) ∧ ∀ᶠ (x : X) in nhdsSet t, p x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.isUpperSet_orderDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α], Topology.IsUpperSet αᵒᵈ ↔ Topology.IsLowerSet α
-- Mathlib.Algebra.Group.Finsupp
/-- A finitely supported function can be built by adding up `single a b` for increasing `a`.

The lemma `induction_on_max₂` swaps the argument order in the sum.  -/
Finsupp.induction_on_max : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [inst_1 : LinearOrder ι] {motive : (ι →₀ M) → Prop}
  (f : ι →₀ M),
  motive 0 →
    (∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive ((fun₀ | a => b) + f)) →
      motive f
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.center.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M], Submonoid.center M = { carrier := Set.center M, mul_mem' := ⋯, one_mem' := ⋯ }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, k ∈ t → (f (t.get? k)).isSome = true → (t.alter k f).size = t.size
-- Mathlib.Data.Prod.Basic
/-- Delaborator for `Prod.snd x` as `x.2`.  -/
Prod.PrettyPrinting.delabProdSnd : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.zero_le_restrict_not_measurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  ¬MeasurableSet i → MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i
-- Mathlib.RingTheory.Ideal.Over
Ideal.LiesOver.smul : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] {P : Ideal B}
  {p : Ideal A} {G : Type u_5} [inst_3 : Group G] [inst_4 : MulSemiringAction G B] (g : G) [SMulCommClass G A B]
  [h : P.LiesOver p], (g • P).LiesOver p
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMulDistribMulActionOfMulActionHomClass : {R : Type u_1} →
  {ι : 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 : Nonempty ι] →
                    [inst_5 : Monoid R] →
                      [inst_6 : (i : ι) → Monoid (G i)] →
                        [inst_7 : (i : ι) → MulDistribMulAction R (G i)] →
                          [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] →
                            [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] →
                              MulDistribMulAction R (DirectLimit G f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α},
      Std.DHashMap.Internal.Raw₀.Const.get? (m.erase k) a =
        if (k == a) = true then none else Std.DHashMap.Internal.Raw₀.Const.get? m a
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
IntermediateField.transcendental_adjoin_iff : ∀ {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Ring S] [inst_4 : Algebra E S] {x : S},
  Transcendental (↥(IntermediateField.adjoin F s)) x ↔ Transcendental (↥(Algebra.adjoin F s)) x
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.upperBound : {α : Type u} → Std.Rxo.Iterator α → α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp}, t₁.Equiv t₂ ↔ t₁.keys.Perm t₂.keys
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.opensCone_π_app : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (i : I) (U : (D.obj i).Opens) (j : CategoryTheory.Over i),
  (AlgebraicGeometry.opensCone D c i U).π.app j =
    AlgebraicGeometry.Scheme.Hom.resLE (c.π.app j.left) ((TopologicalSpace.Opens.map (D.map j.hom).base).obj U)
      ((TopologicalSpace.Opens.map (c.π.app i).base).obj U) ⋯
-- Mathlib.FieldTheory.Separable
IsSeparable.of_algHom : ∀ {F : Type u_1} [inst : Field F] {E : Type u_3} {E' : Type u_4} [inst_1 : Field E] [inst_2 : Field E']
  [inst_3 : Algebra F E] [inst_4 : Algebra F E'] (f : E →ₐ[F] E') {x : E}, IsSeparable F (f x) → IsSeparable F x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.splitter : {n : ℕ} →
  (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) →
    (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
      (Unit → motive none) → ((c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)) → motive cOpt
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_vadd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : VAdd M X] [inst_2 : ContinuousConstVAdd M X]
  (c : M) (x : X), SeparationQuotient.mk (c +ᵥ x) = c +ᵥ SeparationQuotient.mk x
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.leftFun_eq_iff_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (x : E) in nhds φ.pt, φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 →
    ∀ (x x_1 : α),
      x = x_1 →
        ∀ (i i_1 : ℕ),
          i = i_1 →
            ∀ (j j_1 : ℕ),
              j = j_1 →
                ∀ (xs xs_1 : List α), xs = xs_1 → List.minIdxOn.go✝ f x i j xs = List.minIdxOn.go✝ f_1 x_1 i_1 j_1 xs_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toSSetFunctor_obj : ∀ {X : SSet} (A : X.Subcomplex), SSet.Subcomplex.toSSetFunctor.obj A = A.toSSet
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNNReal_le_natCast : ∀ {r : NNReal} {n : ℕ}, ↑r ≤ ↑n ↔ r ≤ ↑n
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting'_eq_zero_iff : ∀ {n : ℕ}, n.primeCounting' = 0 ↔ n ≤ 2
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerRight_whiskerRight_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} (D : Type u_4) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {F G : CategoryTheory.Functor A B} (η : F ⟶ G)
  (H : CategoryTheory.Functor B C) {Z : CategoryTheory.Functor (CategoryTheory.Join A D) (CategoryTheory.Join C D)}
  (h : CategoryTheory.Join.mapPair (G.comp H) (CategoryTheory.Functor.id D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Join.mapWhiskerRight (CategoryTheory.Functor.whiskerRight η H) (CategoryTheory.Functor.id D)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft D F H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.mapWhiskerRight η (CategoryTheory.Functor.id D))
          (CategoryTheory.Join.mapPair H (CategoryTheory.Functor.id D)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft D G H).inv h))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.instInhabitedState : Inhabited Lean.Meta.Grind.Injective.State
-- Lean.Environment
/-- Constant info and environment extension states eventually resulting from async elaboration.
 -/
_private.Lean.Environment.0.Lean.AsyncConst : Type
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ici_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iic b ∪ Set.Ici a = Set.univ
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
/-- `A.HasOrthogonalRows` means matrix `A` has orthogonal rows (with respect to
`dotProduct`).  -/
Matrix.HasOrthogonalRows : {α : Type u_1} → {n : Type u_2} → {m : Type u_3} → [Mul α] → [AddCommMonoid α] → Matrix m n α → [Fintype n] → Prop
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.match_3.splitter : (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) →
  (rhsTerms lhsTerms : Lean.Meta.Grind.SolverTerms) →
    (Unit → motive Lean.Meta.Grind.SolverTerms.nil Lean.Meta.Grind.SolverTerms.nil) →
      ((solverId : ℕ) →
          (e : Lean.Expr) →
            (rest : Lean.Meta.Grind.SolverTerms) →
              motive Lean.Meta.Grind.SolverTerms.nil (Lean.Meta.Grind.SolverTerms.next solverId e rest)) →
        ((solverId : ℕ) →
            (e : Lean.Expr) →
              (rest : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next solverId e rest) Lean.Meta.Grind.SolverTerms.nil) →
          ((id₁ : ℕ) →
              (rhs : Lean.Expr) →
                (rhsTerms : Lean.Meta.Grind.SolverTerms) →
                  (id₂ : ℕ) →
                    (lhs : Lean.Expr) →
                      (lhsTerms : Lean.Meta.Grind.SolverTerms) →
                        motive (Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms)
                          (Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms)) →
            motive rhsTerms lhsTerms
-- Mathlib.Analysis.ODE.DiscreteGronwall
/-- Discrete Grönwall inequality, exponential form: if `u (n+1) ≤ (1 + c n) * u n + b n` with
`b`, `c`, and `u n₀` non-negative, then `u n ≤ (u n₀ + ∑ b k) * exp (∑ c i)`.  -/
discrete_gronwall : ∀ {u b c : ℕ → ℝ} {n₀ : ℕ},
  0 ≤ u n₀ →
    (∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) →
      (∀ n ≥ n₀, 0 ≤ c n) →
        (∀ n ≥ n₀, 0 ≤ b n) →
          ∀ ⦃n : ℕ⦄, n₀ ≤ n → u n ≤ (u n₀ + ∑ k ∈ Finset.Ico n₀ n, b k) * Real.exp (∑ i ∈ Finset.Ico n₀ n, c i)
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.cons_map : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α} (b : δ a)
  (f : (a' : α) → a' ∈ m → δ a') {δ' : α → Sort u_3} (φ : ⦃a' : α⦄ → δ a' → δ' a'),
  (Multiset.Pi.cons m a (φ b) fun a' ha' => φ (f a' ha')) = fun a' ha' => φ (Multiset.Pi.cons m a b f a' ha')
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Lift a ring homomorphism `R →+* T` to `S →+* T` by specifying a root `x` of `f` in `T`,
where `S` is given by adjoining a root of `f` to `R`.  -/
IsAdjoinRoot.lift : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        {f : Polynomial R} →
          [inst_2 : Algebra R S] →
            IsAdjoinRoot S f →
              {T : Type u_1} → [inst_3 : CommRing T] → (i : R →+* T) → (x : T) → Polynomial.eval₂ i x f = 0 → S →+* T
-- Lean.Elab.Quotation
/-- All necessary information on a pattern head.  -/
Lean.Elab.Term.Quotation.HeadInfo : Type
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_le_val_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) {x : K}, x ≠ 0 → (1 ≤ v x ↔ v x⁻¹ ≤ 1)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Each fiber of a trivialization is homeomorphic to the specified fiber.  -/
Bundle.Trivialization.preimageSingletonHomeomorph : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              (e : Bundle.Trivialization F proj) → {b : B} → b ∈ e.baseSet → ↑(proj ⁻¹' {b}) ≃ₜ F
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R), (TwoSidedIdeal.asIdeal I).IsTwoSided
-- Mathlib.Algebra.Ring.Action.Rat
Rat.instDistribSMul : {R : Type u_1} → [inst : DivisionRing R] → DistribSMul ℚ R
-- Mathlib.Order.UpperLower.Prod
LowerSet.disjoint_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β},
  Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.binder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.add : ∀ {α : Type u} {β : Type v} [inst : Add β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → f + f' =ᶠ[l] g + g'
-- Init.Data.Int.Order
Int.natAbs.eq_1 : ∀ (n_1 : ℕ), (Int.ofNat n_1).natAbs = n_1
-- Mathlib.RingTheory.PowerBasis
/-- `pb.liftEquiv'` states that elements of the root set of the minimal
polynomial of `pb.gen` correspond to maps sending `pb.gen` to that root.  -/
PowerBasis.liftEquiv' : {S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      {B : Type u_5} →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra A S] →
                [inst_5 : IsDomain B] → (pb : PowerBasis A S) → (S →ₐ[A] B) ≃ { y // y ∈ (minpoly A pb.gen).aroots B }
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_singleton_right_iff : ∀ {s : String.Slice} {p : s.Pos} {c : Char} {t : String},
  p.Splits t (String.singleton c) ↔
    ∃ (h : s.endPos ≠ s.startPos), p = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c ∧ s.copy = t ++ String.singleton c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forM_eq_forM_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → m PUnit.{w + 1}},
  Std.DTreeMap.Internal.Impl.forM (fun a x => f a) t = Array.forM f t.keysArray
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.toAttrString : Lean.ReducibilityStatus → String
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_min_of_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a : R} [PosMulMono R] (b c : R),
  0 ≤ a → a * min b c = min (a * b) (a * c)
-- Mathlib.RingTheory.Jacobson.Ring
instIsJacobsonRingOfIsArtinianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R], IsJacobsonRing R