mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDeriv_zero : ∀ {𝕜 : 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] {n : ℕ},
  iteratedFDeriv 𝕜 n 0 = 0
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- `cramer A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,
and thus `cramer A b` is the vector output by Cramer's rule on `A` and `b`.

If `A * x = b` has a unique solution in `x`, `cramer A` sends the vector `b` to `A.det • x`.
Otherwise, the outcome of `cramer` is well-defined but not necessarily useful.
 -/
Matrix.cramer : {n : Type v} → {α : Type w} → [DecidableEq n] → [Fintype n] → [inst : CommRing α] → Matrix n n α → (n → α) →ₗ[α] n → α
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- If `S : Subalgebra 𝕜 A` is a closed subalgebra of a Banach algebra `A`, then for any
`x : S`, the boundary of the spectrum of `x` relative to `S` is a subset of the spectrum of
`↑x : A` relative to `A`.  -/
Subalgebra.frontier_spectrum : ∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A]
  (S : SA) [hS : IsClosed ↑S] (x : ↥S), frontier (spectrum 𝕜 x) ⊆ spectrum 𝕜 ↑x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular Q → P 2 = 0 → Q 2 = 0 → W.add P Q = P 0 ^ 2 • ![1, 1, 0]
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hasFiniteSupport_smul : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  (s : HahnSeries.SummableFamily Γ R α) (t : HahnSeries.SummableFamily Γ' V β) (gh : Γ × Γ'),
  Function.HasFiniteSupport fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char.0.Char.reduceBoolPred : Lean.Name → ℕ → (Char → Char → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsFiniteKernel.exists_univ_le : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [self : ProbabilityTheory.IsFiniteKernel κ], ∃ C < ⊤, ∀ (a : α), (κ a) Set.univ ≤ C
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.eq_add_neg_iff_add_eq : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit c → (a = b + -c ↔ a + c = b)
-- Mathlib.Order.CompleteLattice.Defs
CompleteSemilatticeSup.toPartialOrder : {α : Type u_8} → [self : CompleteSemilatticeSup α] → PartialOrder α
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.congr_fun : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α} {a : α}
  {L : SummationFilter β}, HasSum f a L → (∀ (x : β), g x = f x) → HasSum g a L
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_diagonal : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Zero R] [inst_3 : DecidableEq n] {A : X → n → R}, Continuous A → Continuous fun x => Matrix.diagonal (A x)
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.map_cstarMatrix_nonneg' : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  (self : CompletelyPositiveMap A₁ A₂) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑self.toLinearMap
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_trans_symm : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e e' : Bundle.Pretrivialization F proj), (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv
-- Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
/-- A family of continuous linear maps is `C^n` on `s` if all its applications are.  -/
contDiffOn_clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {F : Type uF}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f : D → E →L[𝕜] F}
  {s : Set D} [FiniteDimensional 𝕜 E], ContDiffOn 𝕜 n f s ↔ ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.ζ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.AddMonObj X],
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.AddMonObj.zero)
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.IsPullback.hasLiftingProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z W : C} {f : X ⟶ Y} {s : X ⟶ Z} {g : Z ⟶ W}
  {t : Y ⟶ W},
  CategoryTheory.IsPullback s f g t →
    ∀ {X' Y' : C} (f' : X' ⟶ Y') [CategoryTheory.HasLiftingProperty f' g], CategoryTheory.HasLiftingProperty f' f
-- Lean.Meta.HasAssignableMVar
/-- Return `true` iff expression contains a metavariable that can be assigned.  -/
Lean.Meta.hasAssignableMVar : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) '' Set.Ioc i j = Set.Ioc (i.addNat m) (j.addNat m)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.isAddCommutative_iSup : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} [Nonempty ι] {S : ι → AddSubgroup G}
  [hS : ∀ (i : ι), IsAddCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsAddCommutative ↥(⨆ i, S i)
-- Init.Data.List.Control
List.findM?_pure : ∀ {α : Type} {m : Type → Type u_1} [inst : Monad m] [LawfulMonad m] (p : α → Bool) (as : List α),
  List.findM? (fun x => pure (p x)) as = pure (List.find? p as)
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_eq_zero_iff_even : ∀ {n : ℤ}, ↑n = 0 ↔ Even n
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hom_inv_apply : ∀ {R S : CommRingCat} (e : R ≅ S) (s : ↑S),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun'.eq_def : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (b x : α),
  IncidenceAlgebra.muFun'✝ 𝕜 b x =
    let a := x;
    if a = b then 1
    else
      -∑ x_1 ∈ (Finset.Ioc a b).attach,
          have h := ⋯;
          have this := ⋯;
          IncidenceAlgebra.muFun'✝ 𝕜 b ↑x_1
-- Batteries.Data.Vector.Lemmas
Vector.scanrM.loop.congr_simp : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f f_1 : α → β → m β),
  f = f_1 →
    ∀ (as as_1 : Vector α n),
      as = as_1 →
        ∀ (cur cur_1 : β),
          cur = cur_1 →
            ∀ (i : ℕ) (hi : i ≤ n) (acc acc_1 : Vector β (n - i)),
              acc = acc_1 → Vector.scanrM.loop f as cur i hi acc = Vector.scanrM.loop f_1 as_1 cur_1 i hi acc_1
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Left unitor as a natural isomorphism.  -/
CategoryTheory.Bicategory.leftUnitorNatIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b : B) →
      (CategoryTheory.Bicategory.precomposing a a b).obj (CategoryTheory.CategoryStruct.id a) ≅
        CategoryTheory.Functor.id (a ⟶ b)
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem.inter : ∀ {α : Type u_1} {S : Set (Set α)} {s t : Set α},
  generatePiSystem S s → generatePiSystem S t → (s ∩ t).Nonempty → generatePiSystem S (s ∩ t)
-- Mathlib.Topology.UniformSpace.Defs
/-- The triangle inequality for `UniformSpace.ball`  -/
UniformSpace.mem_ball_comp : ∀ {β : Type ub} {V W : Set (β × β)} {x y z : β},
  y ∈ UniformSpace.ball x V → z ∈ UniformSpace.ball y W → z ∈ UniformSpace.ball x (SetRel.comp V W)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_eq_setOfPred_isBasis_insert : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I → M.closure I = {x | M.IsBasis I (insert x I)}
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {f : α → β → γ} {k : α} {fallback : γ},
  (Std.ExtHashMap.map f m).getD k fallback = (Option.map (f k) m[k]?).getD fallback
-- Mathlib.Data.EReal.Basic
/-- The map from extended reals to reals sending infinities to zero.  -/
EReal.toReal : EReal → ℝ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.HashMap.filterMap f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => (f x_2 m[x_2]).isSome).get!
-- Mathlib.Logic.Equiv.Functor
Bifunctor.mapEquiv_refl_refl : ∀ {α : Type u} {α' : Type v} (F : Type u → Type v → Type w) [inst : Bifunctor F] [inst_1 : LawfulBifunctor F],
  Bifunctor.mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')
-- Init.Sym.Lemmas
Lean.Sym.Char.eq_eq_false : ∀ (a b : Char), decide (a = b) = false → (a = b) = False
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.instHasInitialElementsOfIsCorepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type u_1)}
  [F.IsCorepresentable], CategoryTheory.Limits.HasInitial F.Elements
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).getKey? k = some k
-- Mathlib.Order.Category.DistLat
DistLat.mk.injEq : ∀ (carrier : Type u_1) [str : DistribLattice carrier] (carrier_1 : Type u_1) (str_1 : DistribLattice carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Analysis.Complex.OpenMapping
/-- If the modulus of a holomorphic function `f` is bounded below by `ε` on a circle, then its range
contains a disk of radius `ε / 2`.  -/
DiffContOnCl.ball_subset_image_closedBall : ∀ {f : ℂ → ℂ} {z₀ : ℂ} {ε r : ℝ},
  DiffContOnCl ℂ f (Metric.ball z₀ r) →
    0 < r →
      (∀ z ∈ Metric.sphere z₀ r, ε ≤ ‖f z - f z₀‖) →
        (∃ᶠ (z : ℂ) in nhds z₀, f z ≠ f z₀) → Metric.ball (f z₀) (ε / 2) ⊆ f '' Metric.closedBall z₀ r
-- Init.Data.BitVec.Lemmas
/-- The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
 -/
BitVec.toNat_intMin : ∀ {w : ℕ}, (BitVec.intMin w).toNat = 2 ^ (w - 1) % 2 ^ w
-- Mathlib.Data.Num.ZNum
ZNum.mod_to_int : ∀ (n d : ZNum), ↑(n % d) = ↑n % ↑d
-- Init.Prelude
/-- `a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. -/
HMul.hMul : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HMul α β γ] → α → β → γ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smulRight.congr_simp : ∀ {M₁ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁] {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {R : Type u_9} {S : Type u_10} [inst_4 : Semiring R]
  [inst_5 : Semiring S] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R S] [inst_9 : Module S M₂]
  [inst_10 : IsScalarTower R S M₂] [inst_11 : TopologicalSpace S] [inst_12 : ContinuousSMul S M₂] (c c_1 : M₁ →L[R] S),
  c = c_1 → ∀ (f f_1 : M₂), f = f_1 → c.smulRight f = c_1.smulRight f_1
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.finsetProd_mem_finsetProd`.

---

An n-ary version of `Set.mul_mem_mul`.  -/
Set.finset_prod_mem_finset_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → ∏ i ∈ t, g i ∈ ∏ i ∈ t, f i
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} [inst_1 : Fintype α],
  p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.length = Fintype.card α
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.vecMulLinear_transpose : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n] (M : Matrix m n R),
  M.transpose.vecMulLinear = M.mulVecLin
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.add_congr : ∀ (w : ℕ) (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs' + rhs' = lhs + rhs
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pushforwardSections_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {M : SheafOfModules R}
  (s : M.sections) (x : Cᵒᵖ), ↑(SheafOfModules.pushforwardSections φ s) x = ↑s (F.op.obj x)
-- Init.Meta.Defs
Lean.Meta.ApplyConfig.mk.sizeOf_spec : ∀ (newGoals : Lean.Meta.ApplyNewGoals) (synthAssignedInstances allowSynthFailures approx : Bool),
  sizeOf
      { newGoals := newGoals, synthAssignedInstances := synthAssignedInstances,
        allowSynthFailures := allowSynthFailures, approx := approx } =
    1 + sizeOf newGoals + sizeOf synthAssignedInstances + sizeOf allowSynthFailures + sizeOf approx
-- Mathlib.RingTheory.HahnSeries.Lex
FiniteArchimedeanClass.mk.congr_simp : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a a_1 : M)
  (e_a : a = a_1) (h : a ≠ 0), FiniteArchimedeanClass.mk a h = FiniteArchimedeanClass.mk a_1 ⋯
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.isArithTerm : Lean.Expr → Bool
-- Mathlib.Data.Sign.Defs
SignType.instBoundedOrder : BoundedOrder SignType
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueAdd` is preserved by inverse images under injective, additive maps.  -/
UniqueAdd.addHom_preimage : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] (f : G →ₙ+ H) (hf : Function.Injective ⇑f) (a0 b0 : G)
  {A B : Finset H}, UniqueAdd A B (f a0) (f b0) → UniqueAdd (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_vadd_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, (s +ᵥ t).Nonempty → t.Nonempty
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.mem_range_of_degree_eq_one : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
  (minpoly A x).degree = 1 → x ∈ (algebraMap A B).range
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) (F.map h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) h_1) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv
            h_1)))
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.coeff_eq_zero_of_lt_trailingDegree : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, ↑n < p.trailingDegree → p.coeff n = 0
-- ProofWidgets.Component.PenroseDiagram
/-- Maximum number of optimization steps to take before showing the diagram.
Optimization may converge earlier, before taking this many steps.  -/
ProofWidgets.Penrose.DiagramProps.maxOptSteps : ProofWidgets.Penrose.DiagramProps → ℕ
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.ncard_eq_ncard_of_isBase : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → B₁.ncard = B₂.ncard
-- Mathlib.Order.Atoms.Finite
IsSimpleOrder.instFinite : ∀ {α : Type u_1} [inst : LE α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], Finite α
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.mk.sizeOf_spec : ∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  [inst_3 : SizeOf α] [inst_4 : SizeOf β] (toContinuousMap : C(α, β))
  (hasCompactSupport' : HasCompactSupport toContinuousMap.toFun),
  sizeOf { toContinuousMap := toContinuousMap, hasCompactSupport' := hasCompactSupport' } = 1 + sizeOf toContinuousMap
-- Std.Http.Internal.Char
/-- vchar = %x21-7E
; Visible (printing) ASCII characters.
 -/
Std.Http.Internal.Char.vchar : Char → Bool
-- Mathlib.Data.Sym.Sym2
/-- Get the other element of the unordered pair using the decidable equality.
This is the computable version of `Mem.other`.  -/
Sym2.Mem.other' : {α : Type u_1} → [DecidableEq α] → {a : α} → {z : Sym2 α} → a ∈ z → α
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAt_comp_add_right : ∀ {𝕜 : 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 : E → F}
  {f' : E →L[𝕜] F} {x : E} (a : E), HasFDerivAt (fun x => f (x + a)) f' x ↔ HasFDerivAt f f' (x + a)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.mk.injEq : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier : Set α) (isClopen' : IsClopen carrier) (carrier_1 : Set α)
  (isClopen'_1 : IsClopen carrier_1),
  ({ carrier := carrier, isClopen' := isClopen' } = { carrier := carrier_1, isClopen' := isClopen'_1 }) =
    (carrier = carrier_1)
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
/-- The equivalence of categories between monoids internal to `C`
and monoids internal to the monoidal opposite of `C`.  -/
MonObj.mopEquiv : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Mon C ≌ CategoryTheory.Mon Cᴹᵒᵖ
-- Mathlib.Data.Nat.Log
Nat.clog_zero_right : ∀ (b : ℕ), Nat.clog b 0 = 0
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_sdiff_singleton : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' (s \ {x}) x ↔ HasDerivWithinAt f f' s x
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.σ₀_mk₀_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : C),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (CategoryTheory.nerve C) 0))
      (CategoryTheory.ComposableArrows.mk₀ x) =
    CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.id x)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_χ₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C)
  (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω)
  (isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth)
  (uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
      CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m)
  (Y : C), (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ₀ Y = t.from Y
-- Init.Data.Array.Lemmas
Array.replicate_append_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {m : ℕ}, Array.replicate n a ++ Array.replicate m a = Array.replicate (n + m) a
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R) (p q : Polynomial R),
  (Polynomial.taylor r) (p * q) = (Polynomial.taylor r) p * (Polynomial.taylor r) q
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixing subgroup of union is intersection  -/
fixingSubgroup_union : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {s t : Set α},
  fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.erased.sizeOf_spec : sizeOf Lean.IR.IRType.erased = 1
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- **Alias** of `MeasureTheory.hausdorffMeasure_orthogonalProjectionOnto_le`.

---

Let `s` be a subset of `𝕜`-inner product space, and `K` a subspace. Then the `d`-dimensional
Hausdorff measure of the orthogonal projection of `s` onto `K` is less than or equal to the
`d`-dimensional Hausdorff measure of `s`.
 -/
MeasureTheory.hausdorffMeasure_orthogonalProjection_le : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (K : Submodule 𝕜 E) [inst_5 : K.HasOrthogonalProjection] (d : ℝ)
  (s : Set E),
  0 ≤ d →
    (MeasureTheory.Measure.hausdorffMeasure d) (⇑K.orthogonalProjectionOnto '' s) ≤
      (MeasureTheory.Measure.hausdorffMeasure d) s
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.exists_find?_insert_self : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {c : RBTree.RBColor} {n : ℕ} {v : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut] {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.Ordered cmp t →
      cut v = Ordering.eq → ∃ x, RBTree.RBNode.find? cut (RBTree.RBNode.insert cmp t v) = some x
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.finrank_maxGenEigenspace_eq : ∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M) (μ : K),
  Module.finrank K ↥(φ.maxGenEigenspace μ) = Polynomial.rootMultiplicity μ (LinearMap.charpoly φ)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_val : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k) (a : Fin m ⊕ Fin k),
  (MvPolynomial.universalFactorizationMapPresentation R n m k hn).val a =
    Sum.elim (fun x => MvPolynomial.X x ⊗ₜ[R] 1) (fun x => 1 ⊗ₜ[R] MvPolynomial.X x) a
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A version of `isLocallyNoetherian_iff_of_iSup_eq_top` using `Scheme.OpenCover`.  -/
AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)],
  AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑((𝒰.X i).presheaf.obj (Opposite.op ⊤))