mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivCLM_eq_of_scalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  (𝕜' : Type u_6) [inst_8 : NontriviallyNormedField 𝕜'] [inst_9 : NormedSpace 𝕜' F] [inst_10 : Algebra ℝ 𝕜']
  [inst_11 : IsScalarTower ℝ 𝕜' F] {v : E}, ⇑(TestFunction.lineDerivCLM 𝕜 v) = ⇑(TestFunction.lineDerivCLM 𝕜' v)
-- Mathlib.NumberTheory.Padics.RingHoms
/-- Given a family of ring homs `f : Π n : ℕ, R →+* ZMod (p ^ n)`,
`nthHom f r` is an integer-valued sequence
whose `n`th value is the unique integer `k` such that `0 ≤ k < p ^ n`
and `f n r = (k : ZMod (p ^ n))`.
 -/
PadicInt.nthHom : {R : Type u_1} → [inst : NonAssocSemiring R] → {p : ℕ} → ((k : ℕ) → R →+* ZMod (p ^ k)) → R → ℕ → ℤ
-- Mathlib.Order.BoundedOrder.Basic
subsingleton_iff_bot_eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊥ = ⊤ ↔ Subsingleton α
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
FiberBundle.mdifferentiableAt_extend : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (F : Type u_5) [inst_6 : NormedAddCommGroup F]
  {V : M → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → AddCommGroup (V x)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : NormedSpace 𝕜 F] {x : M}
  (σ₀ : V x), (MDiffAt fun x' => ⟨x', FiberBundle.extend F σ₀ x'⟩) x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.getKey a ⋯
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_plift : ∀ (α : Type u_3), Nat.card (PLift α) = Nat.card α
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_3 : ∀ (motive : Lean.Expr → Sort u_1) (deBruijnIndex : ℕ) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.bvar deBruijnIndex with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_3 deBruijnIndex
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.computeKind : Lean.Elab.Modifiers → Lean.Elab.ComputeKind
-- Mathlib.Data.Nat.Prime.Nth
Nat.nth_prime_zero_eq_two : Nat.nth Nat.Prime 0 = 2
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.self_le_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k kmi : α},
  (t.insert k).max?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.isPropFormerType.go : Lean.Expr → Array Lean.Expr → Lean.MetaM Bool
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.quotDepth : Lean.Parser.CacheableParserContext → ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.homotopyEquivNormalizedChainComplex_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  (X.homotopyEquivNormalizedChainComplex R).inv = X.fromNormalizedChainComplex R
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The natural monoid hom from a submonoid of monoid `M` to `M`.  -/
Submonoid.subtype : {M : Type u_4} → [inst : MulOneClass M] → (S : Submonoid M) → ↥S →* M
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
map_normEDS : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {F : Type u_3} [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) (b c d : R) (n : ℤ), f (normEDS b c d n) = normEDS (f b) (f c) (f d) n
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerLeft.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C) {Y₁ Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂),
  X.whiskerLeft f = { f := CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.fst f.f, comm := ⋯ }
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrRight_refl : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : Semiring 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] [inst_3 : (i : ι) → Module 𝕜 (α i)],
  (LinearIsometryEquiv.piLpCongrRight p fun i => LinearIsometryEquiv.refl 𝕜 (α i)) =
    LinearIsometryEquiv.refl 𝕜 (PiLp p α)
-- Init.Prelude
Char.ext : ∀ {c d : Char}, c.val = d.val → c = d
-- Mathlib.MeasureTheory.Measure.Lebesgue.Integral
integral_comp_neg_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (c : ℝ) (f : ℝ → E),
  ∫ (x : ℝ) in Set.Ioi c, f (-x) = ∫ (x : ℝ) in Set.Iic (-c), f x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_zero : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Zero Y], ⇑0 = 0
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurryMid_curryMid : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (i : Fin (n + 1)) (f : MultilinearMap R M M₂),
  LinearMap.uncurryMid i (MultilinearMap.curryMid i f) = f
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- Two real Gaussian distributions are equal iff they have the same mean and variance.  -/
ProbabilityTheory.gaussianReal_ext_iff : ∀ {μ₁ μ₂ : ℝ} {v₁ v₂ : NNReal},
  ProbabilityTheory.gaussianReal μ₁ v₁ = ProbabilityTheory.gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeUnop_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.unop),
  (CategoryTheory.Limits.coneOfCoconeUnop c).pt = Opposite.op c.pt
-- Mathlib.Analysis.SpecificLimits.Normed
hasSum_choose_mul_geometric_of_norm_lt_one : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜},
  ‖r‖ < 1 → HasSum (fun n => ↑((n + k).choose k) * r ^ n) (1 / (1 - r) ^ (k + 1))
-- Mathlib.CategoryTheory.Monoidal.Closed.Types
CategoryTheory.instIsLeftAdjointTensorLeft : ∀ (X : Type v₁), (CategoryTheory.MonoidalCategory.tensorLeft X).IsLeftAdjoint
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_unique : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (φ : MvPolynomial σ R →ₐ[R] S₁), φ = MvPolynomial.aeval (⇑φ ∘ MvPolynomial.X)
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.additive_of_preservesBinaryBiproducts : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasBinaryBiproducts C] [inst_5 : F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesBinaryBiproducts F], F.Additive
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.σ_ε₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) {c₂ : ComplexShape I₂}
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₂ c₁ c₁₂]
  [inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' → c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂'
-- Mathlib.Order.Basic
eq_or_lt_of_le : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → a = b ∨ a < b
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- A practical constructor for cochains.  -/
CochainComplex.HomComplex.Cochain.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        {n : ℤ} → ((p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)) → CochainComplex.HomComplex.Cochain F G n
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.injective_ringHomComp : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  {f : R' →+* R''}, Function.Injective ⇑f → Function.Injective fun x => x.ringHomComp f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- If a linear map preserves the quadratic forms and is surjective, then the algebra
maps it induces between Clifford algebras is also surjective.  -/
CliffordAlgebra.map_surjective : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
  {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂), Function.Surjective ⇑f → Function.Surjective ⇑(CliffordAlgebra.map f)
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.listSum_map_zero : ∀ {α : Type u_1} {n : ℕ} {l : List α} {f : α → ℕ}, (∀ x ∈ l, f x ≡ 0 [MOD n]) → (List.map f l).sum ≡ 0 [MOD n]
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.cancel_right_of_respectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [hP : P.RespectsIso]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g], P (CategoryTheory.CategoryStruct.comp f g) ↔ P f
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.reflects_cocone_isomorphism`.

---

If `F` reflects isomorphisms, then `Cocones.functoriality F` reflects isomorphisms
as well.
 -/
CategoryTheory.Limits.Cocones.reflects_cone_isomorphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms]
  (K : CategoryTheory.Functor J C), (CategoryTheory.Limits.Cocone.functoriality K F).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.snd_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ F₂ : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.SemiCartesianMonoidalCategory.snd F₁ F₂).app j =
    CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)
-- Aesop.Forward.State
/-- Extract stats from an `InstMap`.  -/
Aesop.InstMap.stats : Aesop.InstMap → Array Aesop.ForwardInstantiationStats
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_functor_obj_left_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (X : C),
  (CategoryTheory.WithTerminal.equivComma.functor.obj F).left.obj X = F.obj (CategoryTheory.WithTerminal.incl.obj X)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃Obj_obj : ∀ {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6)
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂),
  (CategoryTheory.Functor.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).obj F₂ =
    CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent_const : ∀ {f : ℝ → ℝ} {c : ℝ}, (Asymptotics.IsEquivalent Filter.atTop f fun x => c) → AkraBazziRecurrence.GrowsPolynomially f
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.isClassQuick? : Lean.Expr → Lean.MetaM (Lean.LOption Lean.Name)
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.mk.injEq : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (c : Fin N.succ → α) (r : Fin N.succ → ℝ)
  (rpos : ∀ (i : Fin N.succ), 0 < r i)
  (h : Pairwise fun i j => r i ≤ dist (c i) (c j) ∧ r j ≤ τ * r i ∨ r j ≤ dist (c j) (c i) ∧ r i ≤ τ * r j)
  (hlast : ∀ i < Fin.last N, r i ≤ dist (c i) (c (Fin.last N)) ∧ r (Fin.last N) ≤ τ * r i)
  (inter : ∀ i < Fin.last N, dist (c i) (c (Fin.last N)) ≤ r i + r (Fin.last N)) (c_1 : Fin N.succ → α)
  (r_1 : Fin N.succ → ℝ) (rpos_1 : ∀ (i : Fin N.succ), 0 < r_1 i)
  (h_1 :
    Pairwise fun i j =>
      r_1 i ≤ dist (c_1 i) (c_1 j) ∧ r_1 j ≤ τ * r_1 i ∨ r_1 j ≤ dist (c_1 j) (c_1 i) ∧ r_1 i ≤ τ * r_1 j)
  (hlast_1 : ∀ i < Fin.last N, r_1 i ≤ dist (c_1 i) (c_1 (Fin.last N)) ∧ r_1 (Fin.last N) ≤ τ * r_1 i)
  (inter_1 : ∀ i < Fin.last N, dist (c_1 i) (c_1 (Fin.last N)) ≤ r_1 i + r_1 (Fin.last N)),
  ({ c := c, r := r, rpos := rpos, h := h, hlast := hlast, inter := inter } =
      { c := c_1, r := r_1, rpos := rpos_1, h := h_1, hlast := hlast_1, inter := inter_1 }) =
    (c = c_1 ∧ r = r_1)
-- Lean.Elab.App
/-- Auxiliary function for computing the resulting type of a function application.
Simulates `ElabAppArgs.main` without elaborating anything.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getResultingTypeCore? : Bool → Bool → ℕ → ℕ → ℕ → List Lean.Elab.Term.NamedArg → Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_add_right_eq_map : ∀ {m n : ℕ}, (m...m + n).toArray = Array.map (fun x => x + m) (0...n).toArray
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.mk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (app app_1 : (a : B) → η.app a ⟶ θ.app a) (e_app : app = app_1)
  (naturality :
    ∀ {a b : B} (f : a ⟶ b),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
          (θ.naturality f).hom =
        CategoryTheory.CategoryStruct.comp (η.naturality f).hom
          (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f))),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.symm_p_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] {Z : C} (h : A ⨯ A ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.symm.p h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom) h
-- Mathlib.Order.Lattice
Monotone.map_inf_le : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β},
  Monotone f → ∀ (x y : α), f (x ⊓ y) ≤ f x ⊓ f y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyGE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGE! k = t₂.getKeyGE! k
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instAddSemigroup : {m : Type u_1} →
  {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → AddSemigroup (α i j)] → AddSemigroup (DMatrix m n α)
-- Init.Data.Array.Lemmas
Array.ne_empty_of_size_eq_add_one : ∀ {n : ℕ} {α : Type u_1} {xs : Array α}, xs.size = n + 1 → xs ≠ #[]
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_nsmul : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (n : ℕ) (ψ : AddChar A M),
  ⇑(n • ψ) = ⇑ψ ^ n
-- Mathlib.Algebra.Ring.NegOnePow
Int.coe_negOnePow_natCast : ∀ (n : ℕ), ↑(↑n).negOnePow = (-1) ^ n
-- Mathlib.Data.List.Nodup
List.inj_on_of_nodup_map : ∀ {α : Type u} {β : Type v} {f : α → β} {l : List α},
  (List.map f l).Nodup → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y
-- Mathlib.Data.List.MinMax
List.minimum_concat : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α) (l : List α), (l ++ [a]).minimum = min l.minimum ↑a
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a diagram `D` of colimit cocones over the `F.obj j`, and a cocone over `uncurry.obj F`,
we can construct a cocone over the diagram consisting of the cocone points from `D`.
 -/
CategoryTheory.Limits.coconeOfCoconeUncurry : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              {D : CategoryTheory.Limits.DiagramOfCocones F} →
                ((j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) →
                  CategoryTheory.Limits.Cocone (CategoryTheory.Functor.uncurry.obj F) →
                    CategoryTheory.Limits.Cocone D.coconePoints
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry'_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  [inst_2 : CategoryTheory.Closed X],
  CategoryTheory.MonoidalClosed.curry' (CategoryTheory.CategoryStruct.id X) = CategoryTheory.MonoidalClosed.id X
-- Init.Data.Int.Order
Int.lt_of_sub_lt_sub_left : ∀ {a b c : ℤ}, c - a < c - b → b < a
-- Mathlib.Data.Fintype.Basic
Finset.univ_fin2 : Finset.univ = {0, 1}
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ico_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ico a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Ico a b, f i.castSucc
-- Mathlib.Algebra.Ring.Nat
Nat.instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring ℕ
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `isClosed_setOfPred_map_one`. -/
isClosed_setOf_map_one : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : One M₁] [inst_3 : One M₂],
  IsClosed {f | f 1 = 1}
-- Mathlib.RepresentationTheory.Action
/-- The unit of the linearize functor.  -/
Representation.LinearizeMonoidal.η : (k : Type u) →
  (G : Type v) →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        (Representation.linearize k G
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G))).IntertwiningMap
          (Representation.trivial k G k)
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- The property of scheme morphisms `Etale` is associated with the ring
homomorphism property `Etale`.  -/
AlgebraicGeometry.Etale.instHasRingHomPropertyEtale : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.Etale fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fstHom_comp_map : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N),
  (TrivSqZeroExt.fstHom R' R' N).comp (TrivSqZeroExt.map f) = TrivSqZeroExt.fstHom R' R' M
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_eq_elem_of_subsingleton : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] [Subsingleton n]
  (A : Matrix n n R) (k : n), A.permanent = A k k
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : SizeOf G] (toSubmonoid : Submonoid G)
  (eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1),
  sizeOf { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem' } = 1 + sizeOf toSubmonoid
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_unop : ∀ {G : Type u_2} [inst : AddGroup G] (S : AddSubgroup Gᵃᵒᵖ), S.unop.op = S
-- Mathlib.Algebra.Lie.Weights.Basic
/-- The proposition that a weight of a Lie module is non-zero.  -/
LieModule.Weight.IsNonZero : {R : Type u_2} →
  {L : Type u_3} →
    {M : Type u_4} →
      [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] → [inst_7 : LieRing.IsNilpotent L] → LieModule.Weight R L M → Prop
-- Mathlib.Topology.Sheaves.Limits
TopCat.limit_isSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{v_1, w} J]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] {X : TopCat}
  (F : CategoryTheory.Functor J (TopCat.Presheaf C X)),
  (∀ (j : J), (F.obj j).IsSheaf) → (CategoryTheory.Limits.limit F).IsSheaf
-- Mathlib.Data.W.Basic
instInhabitedWTypeUnitEmpty : Inhabited (WType fun x => Empty)
-- Mathlib.NumberTheory.LSeries.Basic
/-- The indicator function of `{1} ⊆ ℕ` with values in `ℂ`.  -/
LSeries.notation.termδ : Lean.ParserDescr
-- Mathlib.Logic.Basic
congr_arg_refl : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : α), ⋯ = ⋯
-- Lean.Server.Requests
Lean.Server.chainStatefulLspRequestHandler : String →
  (paramType : Type) →
    [Lean.FromJson paramType] →
      [Lean.ToJson paramType] →
        [Lean.Lsp.FileSource paramType] →
          (respType : Type) →
            [Lean.FromJson respType] →
              [Lean.ToJson respType] →
                (stateType : Type) →
                  [TypeName stateType] →
                    (paramType →
                        Lean.Server.LspResponse respType →
                          stateType → Lean.Server.RequestM (Lean.Server.LspResponse respType × stateType)) →
                      (Lean.Lsp.DidChangeTextDocumentParams → StateT stateType Lean.Server.RequestM Unit) → IO Unit