mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ : C)
  {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ C).obj X₁).map φ).app X₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₃))
        (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₂ X₃).inv)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂` via a two-by-two matrix whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct an isomorphism `X₂ ≅ Y₂`, via Gaussian elimination.
 -/
CategoryTheory.Biprod.isoElim' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ Y₁ Y₂ : C} →
          (f₁₁ : X₁ ⟶ Y₁) →
            (f₁₂ : X₁ ⟶ Y₂) →
              (f₂₁ : X₂ ⟶ Y₁) →
                (f₂₂ : X₂ ⟶ Y₂) →
                  [CategoryTheory.IsIso f₁₁] →
                    [CategoryTheory.IsIso (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)] → X₂ ≅ Y₂
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.integerComplement_eq : Complex.integerComplement = {z | ¬∃ n, ↑n = z}
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_ac.sizeOf_spec : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.simp_ac lhs s c₁ c₂) = 1 + sizeOf lhs + sizeOf s + sizeOf c₁ + sizeOf c₂
-- Lean.Elab.Term.TermElabM
/-- Return the name of the declaration being elaborated if available.  -/
Lean.Elab.Term.getDeclName? : Lean.Elab.TermElabM (Option Lean.Name)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : α} {fallback : β},
  ∅.getD a fallback = fallback
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.ediam_Ico : ∀ (a b : ℝ), Metric.ediam (Set.Ico a b) = ENNReal.ofReal (b - a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_toArray_rco : ∀ {n : ℕ}, (*...n).toArray = (0...n).toArray
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.locallyConnectedSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  LocallyConnectedSpace (TopologicalSpace.Compacts α) ↔ LocallyConnectedSpace α
-- Init.Data.Array.Bootstrap
Array.foldl_toList : ∀ {β : Type u_1} {α : Type u_2} (f : β → α → β) {init : β} {xs : Array α},
  List.foldl f init xs.toList = Array.foldl f init xs
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsVarsEquiv_symm_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (a : L.Term (γ ⊕ α)),
  FirstOrder.Language.Term.constantsVarsEquiv.symm a = a.varsToConstants
-- Lean.Meta.Match.MatcherApp.Transform
/-- Given
- matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and
- expression `e : B[discrs]`,
Construct the term
`match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`.

We only abstract discriminants that are fvars.  We used to use `kabstract` to abstract all
discriminants from `B[discrs]`, but that changes the type of the arg in ways that make it no
longer compatible with the original recursive function (issue #7322).

If this is still not great, then we could try to use `kabstract`, but only on the last parameter
of the `arg` (the termination proof obligation).

This method assumes
- the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
- each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`

This is used in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
the argument provided by `fix` to refine type of the local variable used for recursive calls,
which may mention `major`. See there for how to use this function.
 -/
Lean.Meta.MatcherApp.addArg : Lean.Meta.MatcherApp → Lean.Expr → Lean.MetaM Lean.Meta.MatcherApp
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.differentiable_iteratedDeriv_sinh : ∀ (n : ℕ), Differentiable ℂ (iteratedDeriv n Complex.sinh)
-- Mathlib.GroupTheory.GroupAction.Pointwise
/-- `preimage_smul_setₛₗ` when `c` is a unit and `σ` is a monoid homomorphism.  -/
MonoidHom.preimage_smul_setₛₗ : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Monoid M] [inst_1 : Monoid N]
  [inst_2 : MulAction M α] [inst_3 : MulAction N β] {c : M} {F : Type u_6} (σ : M →* N) [inst_4 : FunLike F α β]
  [MulActionSemiHomClass F (⇑σ) α β] (f : F), IsUnit c → ∀ (t : Set β), ⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_le : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : TopologicalSpace.Opens G)
  (K : TopologicalSpace.Compacts G), ↑U ⊆ ↑K → μ.outerMeasure ↑U ≤ μ K
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G} [inst_1 : DecidableEq G],
  IsOfFinAddOrder x →
    (y ∈ AddSubgroup.zmultiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x)))
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedState.mk.sizeOf_spec : ∀ (parserState : Lean.Parser.ModuleParserState)
  (processedSnap : Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot),
  sizeOf { parserState := parserState, processedSnap := processedSnap } = 1 + sizeOf parserState + sizeOf processedSnap
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillZero : {α : Type} → Std.Internal.Parsec.ByteArray.Parser α → Std.Internal.Parsec.ByteArray.Parser (Array α)
-- Lean.Elab.MutualInductive
/-- Step to do final term elaboration error reporting, done immediately after universe levels are fully elaborated, but before the final level checks.  -/
Lean.Elab.Command.InductiveElabStep2.finalizeTermElab : Lean.Elab.Command.InductiveElabStep2 → Lean.Elab.TermElabM Unit
-- Mathlib.Data.EReal.Operations
EReal.toReal_mul : ∀ {x y : EReal}, (x * y).toReal = x.toReal * y.toReal
-- Mathlib.MeasureTheory.Category.MeasCat
/-- `Measure X` is the measurable space of measures over the measurable space `X`. It is the
weakest measurable space, s.t. `fun μ ↦ μ s` is measurable for all measurable sets `s` in `X`. An
important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad,
the pure values are the Dirac measure, and the bind operation maps to the integral:
`(μ >>= ν) s = ∫ x. (ν x) s dμ`.

In probability theory, the `MeasCat`-morphisms `X → Prob X` are (sub-)Markov kernels (here `Prob` is
the restriction of `Measure` to (sub-)probability spaces.)
 -/
MeasCat.Measure : CategoryTheory.Functor MeasCat MeasCat
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_add_succ_right_eq_append : ∀ {m n : ℕ}, (m<...=m + n + 1).toList = (m<...=m + n).toList ++ [m + n + 1]
-- Lean.Declaration
Lean.mkAxiomValEx : Lean.Name → List Lean.Name → Lean.Expr → Bool → Lean.AxiomVal
-- Mathlib.Analysis.Distribution.TestFunction
/-- Note: we cannot express the full generality of `lineDerivCLM` purely in terms of this typeclass,
because (by design) the target type `𝓓^{k}_{K}(E, F)` is not determined by the input type
`𝓓^{n}_{K}(E, F)`.  -/
TestFunction.instLineDerivTopENat : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] → LineDeriv E (TestFunction Ω F ⊤) (TestFunction Ω F ⊤)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_inf : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : Lattice β]
  [inst_3 : HasSolidNorm β] [inst_4 : IsOrderedAddMonoid β] (f g : BoundedContinuousFunction α β), ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.Data.FunLike.Group
FunLike.semigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Semigroup β]
  [inst_3 : IsMulApply F α β], FunLike.semigroup = Function.Injective.semigroup (fun f => ⇑f) ⋯ ⋯
-- Mathlib.Data.Fintype.EquivFin
Finite.of_surjective : ∀ {α : Sort u_4} {β : Sort u_5} [Finite α] (f : α → β), Function.Surjective f → Finite β
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.tensoringLeft_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C),
  ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X).Additive
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.comp_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B C_1 : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  (f : A ⟶ B) (g : B ⟶ C_1),
  (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplit.h : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof
-- Lean.Meta.Tactic.Grind.Arith.Simproc
/-- Applies `a^0 = 1`, `a^1 = a`.

We do normalize `a^0` and `a^1` when converting expressions into polynomials,
but we need to normalize them here when for other preprocessing steps such as
`a / b = a*b⁻¹`. If `b` is of the form `c^1`, it will be treated as an
atom in the ring module.

**Note**: We used to expand `a^(n+m)` here, but it prevented `grind` from solving
simple problems such as
```
example {k : Nat} (h : k - 1 + 1 = k) :
    2 ^ (k - 1 + 1) = 2 ^ k := by
  grind
```
We now use a propagator for `a^(n+m)` which adds the `a^n*a^m` to the equivalence class.
 -/
Lean.Meta.Grind.Arith.expandPow01 : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Spectral.ConstructibleTopology
/-- The subbasis of the constructible topology on a topological space `X`: It consists
of the open and compact sets of `X` and their complements.  -/
constructibleTopologySubbasis : (X : Type u_2) → [TopologicalSpace X] → Set (Set X)
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `atBot` and `g` tends to `C` then `f * g` tends to `atBot`.  -/
Filter.Tendsto.atBot_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Lean.Data.Json.Basic
Lean.JsonNumber.mantissa : Lean.JsonNumber → ℤ
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
minpolyDiv_spec : ∀ (R : Type u_2) {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
  minpolyDiv R x * (Polynomial.X - Polynomial.C x) = Polynomial.map (algebraMap R S) (minpoly R x)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newDepHyp : Lean.Meta.Grind.Goal → Lean.Meta.Grind.IntroResult✝
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_a_eq_zero' : ∀ {R : Type u_1} {b c d : R} [inst : Semiring R], { a := 0, b := b, c := c, d := d }.toPoly.degree ≤ 2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair.eq_1 : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : M),
  Convexity.convexCombPair s t hs ht hst x y = Convexity.sConvexComb (Convexity.StdSimplex.duple x y hs ht hst)
-- Mathlib.GroupTheory.GroupAction.Transitive
AddAction.isPretransitive_congr : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N]
  [inst_2 : AddAction M α] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective φ → Function.Bijective ⇑f → (AddAction.IsPretransitive M α ↔ AddAction.IsPretransitive N β)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.add : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → Add ↥p
-- Std.Do.SPred.Laws
Std.Do.SPred.entails.trans : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ Q) → (Q ⊢ₛ R) → P ⊢ₛ R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.eq_3 : ∀ {α : Type u_1} (sep x_1 : List α) (xs : List (List α)),
  (xs = [] → False) → sep.intercalateTR (x_1 :: xs) = List.intercalateTR.go✝ sep.toArray x_1 xs #[]
-- Mathlib.FieldTheory.Perfect
powMulEquiv_eq_toMulEquiv_frobeniusEquiv : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  powMulEquiv R p = (frobeniusEquiv R p).toMulEquiv
-- Mathlib.Data.Int.Cast.Field
Int.cast_div : ∀ {α : Type u_1} [inst : DivisionRing α] {m n : ℤ}, n ∣ m → ↑n ≠ 0 → ↑(m / n) = ↑m / ↑n
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.incl_map_f : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  (x : { I := PUnit.{w + 1}, obj := fun x => X }.I),
  ((CategoryTheory.Limits.FormalCoproduct.incl C).map f).f x = PUnit.unit
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.subtype_toEquiv : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {q : Y → Prop}
  (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x ↔ q (h x)), (h.subtype h_iff).toEquiv = h.subtypeEquiv h_iff
-- Mathlib.Order.RelIso.Basic
RelIso.eq_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : β} {y : α},
  y = e.symm x ↔ e y = x
-- Mathlib.Order.KrullDimension
/-- There exists a series ending in an element for any length up to the element’s height.  -/
Order.exists_series_of_le_height : ∀ {α : Type u_1} [inst : Preorder α] (a : α) {n : ℕ}, ↑n ≤ Order.height a → ∃ p, RelSeries.last p = a ∧ p.length = n
-- Init.Data.Array.Count
Array.count_eq_size : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, Array.count a xs = xs.size ↔ ∀ b ∈ xs, a = b
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_disjUnion : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} (H : Disjoint π₁.iUnion π₂.iUnion),
  J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.Slice.Pattern.Model.split_eq_split_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} (f curr : s.Pos) (hle : f ≤ curr),
  String.Slice.Pattern.Model.split p f curr hle = String.Slice.Pattern.Model.split (fun x => decide (p x)) f curr hle
-- Mathlib.GroupTheory.Commutator.Basic
/-- The commutator subgroup of a group G is the normal subgroup
generated by the commutators `[p,q] = p * q * p⁻¹ * q⁻¹`.  -/
commutator : (G : Type u_1) → [inst : Group G] → Subgroup G
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.isSeparated_zero : ∀ {X : Type u_3} [inst : EMetricSpace X] (s : Set X), Metric.IsSeparated 0 s
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.interior_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α}, TopologicalSpace.Opens.interior (↑U)ᶜ = Uᶜ
-- Mathlib.CategoryTheory.Abelian.Exact
/-- A functor which preserves exactness preserves monomorphisms.  -/
CategoryTheory.Functor.preservesMonomorphisms_of_map_exact : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Abelian A] [inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B)
  [inst_4 : L.PreservesZeroMorphisms],
  (∀ (S : CategoryTheory.ShortComplex A), S.Exact → (S.map L).Exact) → L.PreservesMonomorphisms
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β], MeasureTheory.Measure.fst 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_zero_comp_δ_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (self.h 0) (Y.δ 0) = g.app (Opposite.op { len := n })
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isFilteredOrEmpty_of_semilatticeSup : ∀ (α : Type u) [inst : SemilatticeSup α], CategoryTheory.IsFilteredOrEmpty α
-- Mathlib.Combinatorics.Nullstellensatz
/-- The leading coefficient of `Alon.P S i` is `1`.  -/
_private.Mathlib.Combinatorics.Nullstellensatz.0.MvPolynomial.Alon.monic_P : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} (m : MonomialOrder σ) (S : Finset R) (i : σ),
  m.Monic (MvPolynomial.Alon.P✝ S i)
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_div_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] {p q : ℚ}, ↑p.den ≠ 0 → ↑q.num ≠ 0 → ↑(p / q) = ↑p / ↑q
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.lift_cardinalMk_le_trdeg : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R],
  AlgebraicIndependent R x → Cardinal.lift.{v, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, v} (Algebra.trdeg R A)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.sheafify_isSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F),
  CategoryTheory.Presieve.IsSheaf J F →
    CategoryTheory.Presieve.IsSheaf J (CategoryTheory.Subfunctor.sheafify J G).toFunctor
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.mk.injEq : ∀ {ρ : Type} {pat : ρ} {s : String.Slice} (currPos currPos_1 : s.Pos),
  ({ currPos := currPos } = { currPos := currPos_1 }) = (currPos = currPos_1)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.imp.sizeOf_spec : ∀ (a a_1 : Mathlib.Tactic.ITauto.IProp), sizeOf (a.imp a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.Array.Perm
/-- `Perm as bs` asserts that `as` and `bs` are permutations of each other.

This is a wrapper around `List.Perm`, and for now has much less API.
For more complicated verification, use `perm_iff_toList_perm` and the `List` API.
 -/
Array.Perm : {α : Type u_1} → Array α → Array α → Prop
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct an isomorphism between whiskered extensions.  -/
CategoryTheory.Bicategory.LeftExtension.whiskerIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {s t : CategoryTheory.Bicategory.LeftExtension f g} →
            (s ≅ t) → {x : B} → (h : c ⟶ x) → s.whisker h ≅ t.whisker h
-- Mathlib.Topology.Continuous
continuous_congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : X → Y},
  (∀ (x : X), f x = g x) → (Continuous f ↔ Continuous g)
-- Mathlib.Analysis.Calculus.Deriv.Abs
ContDiff.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ},
  ContDiff ℝ (↑n) f → (∀ (x : E), f x ≠ 0) → ContDiff ℝ ↑n fun y => |f y|
-- Mathlib.Data.Countable.Basic
instCountablePProd : ∀ {α : Sort u} {β : Sort v} [Countable α] [Countable β], Countable (α ×' β)
-- Init.Data.Array.Basic
/-- Applies a monadic function to the corresponding elements of two arrays, left-to-right, stopping at
the end of the shorter array. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)`.
 -/
Array.zipWithM : {α : Type u} →
  {β : Type u_1} → {γ : Type v} → {m : Type v → Type w} → [Monad m] → (α → β → m γ) → Array α → Array β → m (Array γ)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.Normal.of_isPullback_η : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] {φ : H ⟶ G}
  [CategoryTheory.IsAddMonHom φ] {P : C} (p : G ⟶ P) [inst_5 : CategoryTheory.AddGrpObj P]
  [CategoryTheory.IsAddMonHom p],
  CategoryTheory.IsPullback φ (CategoryTheory.SemiCartesianMonoidalCategory.toUnit H) p CategoryTheory.AddMonObj.zero →
    CategoryTheory.IsAddMonHom.Normal φ
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoal.mk.inj : ∀ {toInteractiveGoalCore : Lean.Widget.InteractiveGoalCore} {userName? : Option String} {goalPrefix : String}
  {mvarId : Lean.MVarId} {isInserted? isRemoved? : Option Bool}
  {toInteractiveGoalCore_1 : Lean.Widget.InteractiveGoalCore} {userName?_1 : Option String} {goalPrefix_1 : String}
  {mvarId_1 : Lean.MVarId} {isInserted?_1 isRemoved?_1 : Option Bool},
  { toInteractiveGoalCore := toInteractiveGoalCore, userName? := userName?, goalPrefix := goalPrefix, mvarId := mvarId,
        isInserted? := isInserted?, isRemoved? := isRemoved? } =
      { toInteractiveGoalCore := toInteractiveGoalCore_1, userName? := userName?_1, goalPrefix := goalPrefix_1,
        mvarId := mvarId_1, isInserted? := isInserted?_1, isRemoved? := isRemoved?_1 } →
    toInteractiveGoalCore = toInteractiveGoalCore_1 ∧
      userName? = userName?_1 ∧
        goalPrefix = goalPrefix_1 ∧ mvarId = mvarId_1 ∧ isInserted? = isInserted?_1 ∧ isRemoved? = isRemoved?_1
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_sub_le_of_le : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} {a b : WithBot ℕ},
  p.degree ≤ a → q.degree ≤ b → (p - q).degree ≤ max a b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).getKey? k = (t₂.getKey? k).or (t₁.getKey? k)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_zero_of_eventually_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} (c : F), (f =ᶠ[nhds x] fun x => c) → HasFDerivAt f 0 x
-- Mathlib.Analysis.RCLike.Basic
RCLike.instNormSMulClassInt : ∀ {K : Type u_1} [inst : RCLike K], NormSMulClass ℤ K
-- Mathlib.RingTheory.Binomial
Ring.multichoose_zero_right : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [inst_3 : MulOneClass R]
  [NatPowAssoc R] (r : R), Ring.multichoose r 0 = 1
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isOrtho_def : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] [inst_4 : CommSemiring R₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₂ M₂] [inst_7 : AddCommMonoid M] [inst_8 : Module R M] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} {x : M₁} {y : M₂}, B.IsOrtho x y ↔ (B x) y = 0