mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- Composition of `HasForget₂` instances.  -/
CategoryTheory.HasForget₂.trans : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            (D : Type u_3) →
              [inst_3 : CategoryTheory.Category.{v_2, u_3} D] →
                {FD : outParam (D → D → Type u_4)} →
                  {CD : outParam (D → Type w)} →
                    [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] →
                      [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                        (E : Type u_5) →
                          [inst_6 : CategoryTheory.Category.{v_3, u_5} E] →
                            {FE : outParam (E → E → Type u_6)} →
                              {CE : outParam (E → Type w)} →
                                [inst_7 : outParam ((X Y : E) → FunLike (FE X Y) (CE X) (CE Y))] →
                                  [inst_8 : CategoryTheory.ConcreteCategory E FE] →
                                    [CategoryTheory.HasForget₂ C D] →
                                      [CategoryTheory.HasForget₂ D E] → CategoryTheory.HasForget₂ C E
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.mul : ∀ {R : Type u} [inst : CommSemiring R] {𝓟 : Ideal R} {f f' : Polynomial R},
  f.IsWeaklyEisensteinAt 𝓟 → f'.IsWeaklyEisensteinAt 𝓟 → (f * f').IsWeaklyEisensteinAt 𝓟
-- Mathlib.Data.Finset.Image
List.toFinset_filterMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) [inst : DecidableEq α] [inst_1 : DecidableEq β]
  (f_inj : ∀ (a a' : α) (b : β), f a = some b → f a' = some b → a = a') (s : List α),
  (List.filterMap f s).toFinset = Finset.filterMap f s.toFinset f_inj
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The weighted sum is unaffected by removing the base point, if
present, from the set of points.  -/
Finset.weightedVSubOfPoint_erase : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι),
  ((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Map a partial function across a set. The result depends on a proof
that the function is defined on all members of the set.

```
pmap (fin.mk : ∀ n, n < 4 → fin 4) {1, 2} H = {(1 : fin 4), (2 : fin 4)}
```  -/
Ordnode.pmap : {α : Type u_1} → {P : α → Prop} → {β : Type u_2} → ((a : α) → P a → β) → (t : Ordnode α) → Ordnode.All P t → Ordnode β
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- Any continuous ring homomorphism commutes with `NormedSpace.exp`.  -/
NormedSpace.map_exp : ∀ {𝔸 : Type u_1} {𝔹 : Type u_2} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] [inst_3 : NormedRing 𝔹]
  [Algebra ℚ 𝔹] {F : Type u_3} [inst_5 : FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F),
  Continuous ⇑f → ∀ (x : 𝔸), f (NormedSpace.exp x) = NormedSpace.exp (f x)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.isArithmetic_iff_finiteIndex : ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)},
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic ↔ Γ.FiniteIndex
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.exists_lt : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f : CauSeq α abs),
  ∃ a, CauSeq.const abs a < f
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The cocone associated to a colimit presentation.  -/
CategoryTheory.Limits.ColimitPresentation.cocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} → (pres : CategoryTheory.Limits.ColimitPresentation J X) → CategoryTheory.Limits.Cocone pres.diag
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsArtinianRing R],
  PrimeSpectrum.asIdeal ∘ ⇑IsArtinianRing.primeSpectrumEquivMaximalSpectrum.symm = MaximalSpectrum.asIdeal
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.sdiv_eq.match_1.eq_2 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_2 ()
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The `Order.Frame.MinimalAxioms` element corresponding to a frame.  -/
Order.Frame.MinimalAxioms.of : ∀ {α : Type u} [inst : Order.Frame α], Order.Frame.MinimalAxioms α
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X],
  ⊥ ∈ (AlgebraicGeometry.Scheme.grothendieckTopology P) X
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionSemiHomClass.toMulActionHom.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {F : Type u_8} [inst_2 : FunLike F X Y] [inst_3 : MulActionSemiHomClass F φ X Y] (f : F),
  ↑f = { toFun := ⇑f, map_smul' := ⋯ }
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_singleton_right : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G} {g : G}, AddSubgroup.IsComplement S {g} ↔ S = Set.univ
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instPartialOrder : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → PartialOrder (ClopenUpperSet α)
-- Mathlib.RepresentationTheory.Tannaka
/-- For `v : X` and `G` a finite group, the representation morphism from the right
regular representation `rightFDRep` to `X` sending `single 1 1` to `v`.  -/
TannakaDuality.FiniteGroup.ofRightFDRep : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Finite G] → [Fintype G] → (X : FDRep k G) → ↑X.V → (TannakaDuality.FiniteGroup.rightFDRep ⟶ X)
-- Mathlib.Algebra.Group.End
instInhabitedEnd : {α : Type u_4} → Inhabited (Function.End α)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeights.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 →
    ∀ (signs signs_1 : Finset (Fin (n + 1))),
      signs = signs_1 → ∀ (a a_1 : Fin (n + 1)), a = a_1 → s.excenterWeights signs a = s_1.excenterWeights signs_1 a_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_union! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.union! m₂) k =
          Std.DTreeMap.Internal.Impl.Const.getD m₂ k (Std.DTreeMap.Internal.Impl.Const.get! m₁ k)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_disjoint_Ico_consecutive : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Disjoint (Finset.Ico a b) (Finset.Ico b c)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_of_le_of_le_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, b ≤ c → a ≤ 1 → b * a ≤ c
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.mk.injEq : ∀ {α : Type} (state state_1 : Std.Mutex (Std.CloseableChannel.Unbounded.State✝ α)),
  ({ state := state } = { state := state_1 }) = (state = state_1)
-- Mathlib.Data.Seq.Computation
Computation.orElse_think : ∀ {α : Type u} (c₁ c₂ : Computation α), (c₁.think <|> c₂.think) = (c₁ <|> c₂).think
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_zero_succ : ∀ (k : ℕ), Nat.stirlingSecond 0 k.succ = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {k : α},
  t.insertManyIfNewUnit [k] = t.insertIfNew k ()
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.normEq0.eq_def : ∀ (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  p.normEq0 c =
    match p with
    | Lean.Grind.CommRing.Poly.num a =>
      bif a % ↑c == 0 then Lean.Grind.CommRing.Poly.num 0 else Lean.Grind.CommRing.Poly.num a
    | Lean.Grind.CommRing.Poly.add a m p =>
      bif a % ↑c == 0 then p.normEq0 c else Lean.Grind.CommRing.Poly.add a m (p.normEq0 c)
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.prod_flip_apply_eq_integral : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} [CompleteSpace G]
  [MeasureTheory.IsFiniteMeasure μ.variation] {B : F →L[ℝ] E →L[ℝ] G} {s : Set (X × Y)},
  MeasurableSet s → (μ.prod ν B.flip) s = ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' s) ∂[B; μ]
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `LT` instance if available  -/
Lean.Meta.Grind.Arith.Linear.Struct.ltInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Init.Core
imp_not_self : ∀ {a : Prop}, a → ¬a ↔ ¬a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_inverse_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.mapIso i).inverse.map f).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Data.List.DropRight
List.rdropWhile_reverse : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.rdropWhile p l.reverse = (List.dropWhile p l).reverse
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat_inj : ∀ {V : Type u} {G : SimpleGraph V} {u v v' w : V} {p : G.Walk u v} {h : G.Adj v w} {p' : G.Walk u v'} {h' : G.Adj v' w},
  p.concat h = p'.concat h' → ∃ (hv : v = v'), p.copy ⋯ hv = p'
-- Lean.Elab.Match
/-- If `altLHSS + rhss` is encoding `| PUnit.unit => rhs[0]`, return `rhs[0]`
Otherwise, return none.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.isMatchUnit? : List Lean.Meta.Match.AltLHS → Array Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy : Type
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.iInf_rat_gt_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν] (a : α),
      ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q
-- Mathlib.Topology.Closure
Filter.lift'_closure_eq_bot : ∀ {X : Type u} [inst : TopologicalSpace X] {l : Filter X}, l.lift' closure = ⊥ ↔ l = ⊥
-- Mathlib.Order.CompleteLattice.Basic
biSup_ge_eq_sup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : PartialOrder ι] (f : ι → α) (i : ι),
  ⨆ j, ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j
-- Mathlib.Order.Filter.Pointwise
Filter.mem_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β} {s : Set α},
  s ∈ f -ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s
-- Init.Data.List.Sublist
List.subset_cons_of_subset : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, l₁ ⊆ l₂ → l₁ ⊆ a :: l₂
-- Mathlib.Algebra.Polynomial.Div
/-- `modByMonic`, denoted as `p  %ₘ q`, gives the remainder of `p` by a monic polynomial `q`.  -/
Polynomial.modByMonic : {R : Type u} → [inst : Ring R] → Polynomial R → Polynomial R → Polynomial R
-- Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  AlgebraicTopology.DoldKan.N₂.comp (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C ℕ).functor =
    (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).comp
      (AlgebraicTopology.DoldKan.N₁.comp
        ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence (CategoryTheory.Idempotents.Karoubi C)
                ℕ).functor.comp
          ((CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex
            (ComplexShape.down ℕ))))
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The action on morphisms of the obvious functor
`widePushoutShapeOp : WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ`  -/
CategoryTheory.Limits.widePushoutShapeOpMap : (J : Type w) → (X Y : CategoryTheory.Limits.WidePushoutShape J) → (X ⟶ Y) → (Opposite.op X ⟶ Opposite.op Y)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.subLeft.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] [inst_3 : MeasurableNeg G]
  (g : G), MeasurableEquiv.subLeft g = { toEquiv := Equiv.subLeft g, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Init.Data.SInt.Float32
/-- Obtains a `Float32` whose value is near the given `Int64`.

It will be exactly the value of the given `Int64` if such a `Float32` exists. If no such `Float32`
exists, the returned value will either be the smallest `Float32` that is larger than the given
value, or the largest `Float32` that is smaller than the given value.

This function does not reduce in the kernel.
 -/
Int64.toFloat32 : Int64 → Float32
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn_1.go : {α : Type u} →
  {β : Type v} →
    {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1} →
      {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
        {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
          {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1} →
            (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
              ((t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t) →
                ((t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                    Lean.PersistentHashMap.Node.below_1 t → motive_2 t) →
                  ((t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                      Lean.PersistentHashMap.Node.below_2 t → motive_3 t) →
                    ((t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
                        Lean.PersistentHashMap.Node.below_3 t → motive_4 t) →
                      motive_2 t ×' Lean.PersistentHashMap.Node.below_1 t
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.not_anisotropic_iff_exists : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N),
  ¬Q.Anisotropic ↔ ∃ x, x ≠ 0 ∧ Q x = 0
-- Init.Data.List.Lemmas
List.getLast?_cons_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, (a :: b :: l).getLast? = (b :: l).getLast?
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
RingHom.FaithfullyFlat.codescendsAlong_surjective : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f)
  fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` forms an additive
commutative semigroup.  -/
AddSubsemigroup.closureAddCommSemigroupOfComm : (M : Type u_1) →
  [inst : AddSemigroup M] →
    {s : Set M} → (∀ a ∈ s, ∀ b ∈ s, a + b = b + a) → AddCommSemigroup ↥(AddSubsemigroup.closure s)
-- Init.GrindInstances.ToInt
Lean.Grind.instAddInt8SintOfNatNat : Lean.Grind.ToInt.Add Int8 (Lean.Grind.IntInterval.sint 8)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongrAut_apply : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (e : M ≃* M), MonoidAlgebra.domCongrAut e = MonoidAlgebra.domCongr R A e
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabFootnote.name : Lean.Doc.ElabFootnote✝ → Lean.StrLit
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Icc_addNat : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) ⁻¹' Set.Icc (i.addNat m) (j.addNat m) = Set.Icc i j
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b c : CategoryTheory.Bicategory.InducedBicategory C F} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Bicategory.InducedBicategory.forget.mapComp f g).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.hom g.hom)
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_max : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a b : α), (a ⊔ b)⁺ᵐ = a⁺ᵐ ⊔ b⁺ᵐ
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- If a scalar is central, then its right action is measurable when its left action is.  -/
MeasurableSMul₂.op : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace α] [inst_2 : SMul M α]
  [inst_3 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableSMul₂ M α], MeasurableSMul₂ Mᵐᵒᵖ α
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
Antitone.tendsto_setIntegral : ∀ {α : Type u_1} {E : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {s : ℕ → Set α} {f : α → E},
  (∀ (i : ℕ), MeasurableSet (s i)) →
    Antitone s →
      MeasureTheory.IntegrableOn f (s 0) μ →
        Filter.Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) Filter.atTop (nhds (∫ (a : α) in ⋂ n, s n, f a ∂μ))
-- Lean.Data.PersistentHashMap
Lean.PHashMap : (α : Type u) → Type v → [BEq α] → [Hashable α] → Type (max u v)
-- Mathlib.Algebra.Lie.Graded
SetLike.GradedBracket.mk : ∀ {ι : Type u_1} {σ : Type u_2} {L : Type u_4} [inst : SetLike σ L] [inst_1 : Bracket L L] [inst_2 : Add ι] {ℒ : ι → σ},
  (∀ ⦃i j : ι⦄ {gi gj : L}, gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ (i + j)) → SetLike.GradedBracket ℒ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.nnnorm_assoc : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G),
  ‖(TensorProduct.assoc 𝕜 E F G) x‖₊ = ‖x‖₊
-- Mathlib.Analysis.Analytic.Basic
analyticOnNhd_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, AnalyticOnNhd 𝕜 f ∅
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinite_E : ∀ {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E),
  (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).E = E
-- Mathlib.Analysis.BoxIntegral.DivergenceTheorem
/-- Divergence theorem for a Henstock-Kurzweil style integral.

If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is differentiable on a closed rectangular box `I` with derivative `f'`, then
the divergence `∑ i, f' x (Pi.single i 1) i` is Henstock-Kurzweil integrable with integral equal to
the sum of integrals of `f` over the faces of `I` taken with appropriate signs.

More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and
we allow `f` to be non-differentiable (but still continuous) at a countable set of points.  -/
BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [CompleteSpace E]
  (I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E)
  (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E) (s : Set (Fin (n + 1) → ℝ)),
  s.Countable →
    (∀ x ∈ s, ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) →
      (∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) →
        BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => ∑ i, (f' x) (Pi.single i 1) i)
          BoxIntegral.BoxAdditiveMap.volume
          (∑ i,
            (BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i)
                BoxIntegral.BoxAdditiveMap.volume -
              BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP
                (fun x => f (i.insertNth (I.lower i) x) i) BoxIntegral.BoxAdditiveMap.volume))
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.homEquiv_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y), CategoryTheory.InducedCategory.homEquiv f = f.hom
-- Mathlib.Order.Irreducible
supPrime_toDual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, SupPrime (OrderDual.toDual a) ↔ InfPrime a
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d d' : D} (f : d ⟶ d'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d').inv
-- Init.Data.Rat.Lemmas
Rat.intCast_zero : ↑0 = 0
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.instNonemptyFullSubcategoryOfNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty],
  Nonempty P.FullSubcategory
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAt.sub` -/
HasFDerivAt.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → HasFDerivAt g g' x → HasFDerivAt (fun i => f i - g i) (f' - g') x
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
analyticOn_log : AnalyticOn ℝ Real.log (Set.Ioi 0)
-- Mathlib.Data.Set.Function
Function.LeftInverse.rightInvOn_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse f g → Set.RightInvOn f g (Set.range g)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.snd.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousAddMonoidHom.snd A B = { toAddMonoidHom := AddMonoidHom.snd A B, continuous_toFun := ⋯ }