mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasFDerivAt_multiset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] [inst_3 : DecidableEq ι] [Finite ι] {u : Multiset ι} {x : ι → 𝔸'},
  HasFDerivAt (fun x => (Multiset.map x u).prod)
    (Multiset.map (fun i => (Multiset.map x (u.erase i)).prod • ContinuousLinearMap.proj i) u).sum x
-- Mathlib.Topology.Constructions
Filter.Eventually.prod_nhdsSet : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y}
  {p : X × Y → Prop} {px : X → Prop} {py : Y → Prop},
  (∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)) →
    (∀ᶠ (x : X) in nhdsSet s, px x) → (∀ᶠ (y : Y) in nhdsSet t, py y) → ∀ᶠ (q : X × Y) in nhdsSet (s ×ˢ t), p q
-- Init.Data.Vector.Algebra
/-- Componentwise subtraction of vectors.  -/
Vector.sub : {α : Type u_1} → {n : ℕ} → [Sub α] → Vector α n → Vector α n → Vector α n
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommMonoidOfAddMonoidHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddCommMonoid (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] → AddCommMonoid (DirectLimit G f)
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Reflexive (crude) monadicity theorem. If `G` has a right adjoint, `D` has and `G` preserves
reflexive coequalizers and `G` reflects isomorphisms, then `G` is monadic.
 -/
CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (F ⊣ G) →
              [CategoryTheory.Limits.HasReflexiveCoequalizers D] →
                [G.ReflectsIsomorphisms] →
                  [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] → CategoryTheory.MonadicRightAdjoint G
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.prodMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {F' : Type u_5} {H : Type u_6} {H' : Type u_7}
  {G : Type u_8} {G' : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : NormedAddCommGroup F']
  [inst_8 : NormedSpace 𝕜 F'] [inst_9 : TopologicalSpace H] [inst_10 : TopologicalSpace H']
  [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F' G'} {M : Type u_10}
  {M' : Type u_11} {N : Type u_12} {N' : Type u_13} [inst_13 : TopologicalSpace M] [inst_14 : ChartedSpace H M]
  [inst_15 : TopologicalSpace M'] [inst_16 : ChartedSpace H' M'] [inst_17 : TopologicalSpace N]
  [inst_18 : ChartedSpace G N] [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞}
  {f : M → N} {x : M} {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} [IsManifold I n M]
  [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N']
  {Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop}
  {R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop},
  Manifold.LiftSourceTargetPropertyAt I J n f x P → ∀ {g : M' → N'} {x' : M'}, ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.mk.inj : ∀ {thm : Lean.Meta.Grind.EMatchTheorem} {proof prop : Lean.Expr} {generation : ℕ}
  {guards : List Lean.Meta.Grind.TheoremGuard} {sources : List Lean.Meta.Grind.EMatchDiagNode}
  {thm_1 : Lean.Meta.Grind.EMatchTheorem} {proof_1 prop_1 : Lean.Expr} {generation_1 : ℕ}
  {guards_1 : List Lean.Meta.Grind.TheoremGuard} {sources_1 : List Lean.Meta.Grind.EMatchDiagNode},
  { thm := thm, proof := proof, prop := prop, generation := generation, guards := guards, sources := sources } =
      { thm := thm_1, proof := proof_1, prop := prop_1, generation := generation_1, guards := guards_1,
        sources := sources_1 } →
    thm = thm_1 ∧ proof = proof_1 ∧ prop = prop_1 ∧ generation = generation_1 ∧ guards = guards_1 ∧ sources = sources_1
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_neg : ∀ (x : ENNReal) (m : ℤ), x ^ (-m) = (x ^ m)⁻¹
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.FastIsEmpty.mk : ∀ {α : Sort u} [inst : IsEmpty α], Lean.Meta.FastIsEmpty α
-- Mathlib.NumberTheory.LucasLehmer
/-- Calculate `LucasLehmer.LucasLehmerTest p` for `2 ≤ p` by using kernel reduction for the
`sMod'` function.  -/
LucasLehmer.norm_num_ext.evalLucasLehmerTest : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.le_codRestrict : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f g : L.PartialEquiv M N) {A : L.Substructure N}, f.cod ≤ A → ∀ (hg : A ≤ g.cod), f ≤ g → f ≤ g.codRestrict hg
-- Mathlib.Topology.DiscreteSubset
discreteTopology_subtype_iff' : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {S : Set Y}, DiscreteTopology ↑S ↔ ∀ y ∈ S, ∃ U, IsOpen U ∧ U ∩ S = {y}
-- Mathlib.Combinatorics.Matroid.Basic
/-- Typeclass for a matroid having nonempty ground set. Just a wrapper for `M.E.Nonempty`.  -/
Matroid.Nonempty : {α : Type u_1} → Matroid α → Prop
-- Batteries.Data.AssocList
/-- Boolean equality for `AssocList`.
(This relation cares about the ordering of the key-value pairs.)
 -/
Batteries.AssocList.instBEq : {α : Type u_1} → {β : Type u_2} → [BEq α] → [BEq β] → BEq (Batteries.AssocList α β)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g)
  {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelIsoOfEq h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h_1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_6 : ∀ (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr q.succ =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main
      (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.bit1))
        (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit0)
          (Turing.TM2.Stmt.goto fun x => q.succ))
        (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.cons))
          (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.cons)
            (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.bit1)
              (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q)))
          (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.bit1)
            (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q))))
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.LocalizerMorphism.smallShiftedHomMap_comp : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type w'}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {X₁ Y₁ Z₁ : C₁} {X₂ Y₂ Z₂ : C₂}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂)
  (eY : Φ.functor.obj Y₁ ≅ Y₂) (eZ : Φ.functor.obj Z₁ ≅ Z₂) [inst_10 : W₁.IsCompatibleWithShift M]
  [inst_11 : W₂.IsCompatibleWithShift M] [inst_12 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁]
  [inst_13 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂]
  [inst_14 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂]
  [inst_15 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Z₁]
  [inst_16 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁]
  [inst_17 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Z₂] {a b c : M}
  (f : CategoryTheory.Localization.SmallShiftedHom W₁ X₁ Y₁ a)
  (g : CategoryTheory.Localization.SmallShiftedHom W₁ Y₁ Z₁ b) (h : b + a = c),
  Φ.smallShiftedHomMap eX eZ (f.comp g h) = (Φ.smallShiftedHomMap eX eY f).comp (Φ.smallShiftedHomMap eY eZ g) h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_eq_get!_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α}, Std.DTreeMap.Const.get! t a = (Std.DTreeMap.Const.get? t a).get!
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] {V : TopologicalSpace.Opens ↑↑Y}
  (U : TopologicalSpace.Opens ↑↑X),
  V = (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U →
    CategoryTheory.IsIso (f.c.app (Opposite.op V))
-- Mathlib.Order.Hom.WithTopBot
InfHom.withBot_id : ∀ {α : Type u_1} [inst : SemilatticeInf α], (InfHom.id α).withBot = InfHom.id (WithBot α)
-- Mathlib.Combinatorics.Quiver.Basic
/-- Notation for the type of edges/arrows/morphisms between a given source and target
in a quiver or category.
 -/
«term_⟶_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.toMon_mon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C), M.toMon.mon = M.instMonObjFunctor
-- Mathlib.Util.Export
Lean.ExportM : Type → Type
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.mk.injEq : ∀ (stxTrav : Lean.Syntax.Traverser) (contPrec : Option ℕ) (contCat : Lean.Name) (minPrec trailPrec : Option ℕ)
  (trailCat : Lean.Name) (visitedToken : Bool) (stxTrav_1 : Lean.Syntax.Traverser) (contPrec_1 : Option ℕ)
  (contCat_1 : Lean.Name) (minPrec_1 trailPrec_1 : Option ℕ) (trailCat_1 : Lean.Name) (visitedToken_1 : Bool),
  ({ stxTrav := stxTrav, contPrec := contPrec, contCat := contCat, minPrec := minPrec, trailPrec := trailPrec,
        trailCat := trailCat, visitedToken := visitedToken } =
      { stxTrav := stxTrav_1, contPrec := contPrec_1, contCat := contCat_1, minPrec := minPrec_1,
        trailPrec := trailPrec_1, trailCat := trailCat_1, visitedToken := visitedToken_1 }) =
    (stxTrav = stxTrav_1 ∧
      contPrec = contPrec_1 ∧
        contCat = contCat_1 ∧
          minPrec = minPrec_1 ∧ trailPrec = trailPrec_1 ∧ trailCat = trailCat_1 ∧ visitedToken = visitedToken_1)
-- Init.Data.List.Sort.Impl
/-- `O(|l₁| + |l₂|)`. Merge two lists using `le` as a switch.
 -/
List.MergeSort.Internal.mergeTR : {α : Type u_1} → List α → List α → (α → α → Bool) → List α
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_add_measure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  {ν : MeasureTheory.Measure Ω},
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) ν →
      ProbabilityTheory.mgf X (μ + ν) t = ProbabilityTheory.mgf X μ t + ProbabilityTheory.mgf X ν t
-- Mathlib.Order.SuccPred.Relation
/-- For `n ≤ m`, `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ succ i`
for all `i` between `n` and `m`.  -/
reflTransGen_of_succ_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → n ≤ m → Relation.ReflTransGen r n m
-- Mathlib.Tactic.Algebraize
/-- Function elaborating `Algebraize.Config`.  -/
Mathlib.Tactic.Algebraize.elabAlgebraizeConfig : Lean.Syntax →
  optParam Mathlib.Tactic.Algebraize.Config { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.Algebraize.Config
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- If `x` is not congruent to `a` modulo `p`, then `toIocDiv` is locally constant near `x`.  -/
eventuallyEq_toIocDiv_nhds : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜},
  ¬x ≡ a [PMOD p] → toIocDiv hp a =ᶠ[nhds x] fun x_1 => toIocDiv hp a x
-- Mathlib.Topology.Separation.Regular
IsCompact.lift'_closure_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {K : Set X},
  IsCompact K → (nhdsSet K).lift' closure = nhdsSet K
-- Mathlib.Tactic.FunProp.Core
/-- Try to prove `e` using the *constant lambda theorem*.

For example, `e = q(Continuous fun x ↦ y)` and `funPropDecl` is `FunPropDecl` for `Continuous`.
 -/
Mathlib.Meta.FunProp.applyConstRule : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
      Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.pos_mono : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {s t : Set Ω} (μ : MeasureTheory.FiniteMeasure Ω), s ⊆ t → 0 < μ s → 0 < μ t
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- If `f` is a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, then for every
`n : ℕ` and `a : α`, we have `f (n * a) ≤ (f a)`.  -/
IsNonarchimedean.nmul_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3}
  [inst_2 : NonAssocSemiring α] [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {n : ℕ} {a : α}, f (↑n * a) ≤ f a
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_neg_one_diagonal : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (d : n → R),
  Matrix.detp (-1) (Matrix.diagonal d) = 0
-- Mathlib.Order.Category.FinPartOrd
/-- Construct a bundled `FinPartOrd` from `PartialOrder` + `Fintype`.  -/
FinPartOrd.of : (α : Type u_1) → [PartialOrder α] → [Fintype α] → FinPartOrd
-- Mathlib.Order.Booleanisation
Booleanisation.comp_sdiff_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.comp a \ Booleanisation.comp b = Booleanisation.lift (b \ a)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.smul_apply : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] {S : Type u_10} [inst_7 : TopologicalSpace W] [inst_8 : Monoid S]
  [inst_9 : DistribMulAction S W] [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] (t : S)
  (f : P →ᴬ[R] W) (x : P), (t • f) x = t • f x
-- Mathlib.Analysis.BoundedVariation
BoundedVariationOn.mul : ∀ {α : Type u_2} [inst : LinearOrder α] {f g : α → ℝ} {s : Set α},
  BoundedVariationOn f s → BoundedVariationOn g s → BoundedVariationOn (f * g) s
-- Mathlib.Algebra.Torsor.Basic
/-- Dividing two points by the same point produces equal results
if and only if those points are equal.  -/
sdiv_left_cancel_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {p₁ p₂ p : P}, p₁ /ₛ p = p₂ /ₛ p ↔ p₁ = p₂
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mk.sizeOf_spec : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : SizeOf ι]
  [inst_2 : (a : ι) → SizeOf (M a)] (toList : List ((i : ι) × M i)) (ne_one : ∀ l ∈ toList, l.snd ≠ 1)
  (chain_ne : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList),
  sizeOf { toList := toList, ne_one := ne_one, chain_ne := chain_ne } = 1 + sizeOf toList + sizeOf chain_ne
-- Mathlib.Combinatorics.Matroid.Basic
/-- A `Matroid α` is a ground set `E` of type `Set α`, and a nonempty collection of its subsets
satisfying the exchange property and the maximal subset property. Each such set is called a
`Base` of `M`. An `Indep`endent set is just a set contained in a base, but we include this
predicate as a structure field for better definitional properties.

In most cases, using this definition directly is not the best way to construct a matroid,
since it requires specifying both the bases and independent sets. If the bases are known,
use `Matroid.ofBase` or a variant. If just the independent sets are known,
define an `IndepMatroid`, and then use `IndepMatroid.matroid`.
 -/
Matroid : Type u_1 → Type u_1
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_inv : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α),
  MulAction.period g⁻¹ a = MulAction.period g a
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_apply_apply : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] (e' : Bundle.Trivialization F Bundle.TotalSpace.proj)
  {x : Bundle.TotalSpace F E}, x ∈ e'.source → ↑e'.symm (↑e' x) = x
-- Mathlib.Order.CompleteLattice.Basic
eq_singleton_top_of_sInf_eq_top_of_nonempty : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sInf s = ⊤ → s.Nonempty → s = {⊤}
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.HasAffineProperty.SpecMap_iff_of_affineAnd : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ {R S : CommRingCat} (f : R ⟶ S), P (AlgebraicGeometry.Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.mk.sizeOf_spec : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  [inst_2 : SizeOf α] (max : ℕ) (map : Std.HashMap α ℕ) (inv1 : Std.Sat.AIG.RelabelNat.State.Inv1 max map)
  (inv2 : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map),
  sizeOf { max := max, map := map, inv1 := inv1, inv2 := inv2 } =
    1 + sizeOf max + sizeOf map + sizeOf inv1 + sizeOf inv2
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_zero_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), ↑0 n = 0
-- Init.Internal.Order.Basic
Lean.Order.CCPO.toPartialOrder : {α : Sort u} → [self : Lean.Order.CCPO α] → Lean.Order.PartialOrder α
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_exponent_top_eq_essSup : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {f : α → E}, MeasureTheory.MemLp f ⊤ μ → MeasureTheory.lpNorm f ⊤ μ = essSup (fun x => ‖f x‖) μ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE._auto_3),
  CategoryTheory.CategoryStruct.comp
      (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁)
      (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) =
    0
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabAtomicDiscr : Lean.Syntax → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Tactic.Attr.Register
/-- `coassoc_simps` is a simp set useful to prove tautologies on coalgebras.

The general algorithm it follows is to push the associators `TensorProduct.assoc` and
commutators `TensorProduct.comm` inwards (to the right) until they cancel against
co-multiplications.

The simp set makes the following choice of normal form
* It regards `TensorProduct.map`, `TensorProduct.assoc`, `TensorProduct.comm` as the primitive
  constructions and rewrites everything else such as `lTensor`, `leftComm` using them.
* It rewrites both sides into a right associated composition of linear maps.
  In particular `LinearMap.comp_assoc` and `LinearEquiv.coe_trans` are tagged.
* It rewrites `(f₂ ⊗ g₂) ∘ (f₁ ⊗ g₁)` into `(f₂ ∘ f₁) ⊗ (g₂ ∘ g₁)`.

## Notes

- It is not confluent with `(ε ⊗ₘ id) ∘ₗ δ = λ⁻¹`.
  It is often useful to `trans` (or `calc`) with a term containing
  `(ε ⊗ₘ _) ∘ₗ δ` or `(_ ⊗ₘ ε) ∘ₗ δ`,
  and use one of `map_counit_comp_comul_left` `map_counit_comp_comul_right`
  `map_counit_comp_comul_left_assoc` `map_counit_comp_comul_right_assoc` to continue.

- Some lemmas (e.g. `lid_comp_map : λ ∘ₗ (f ⊗ₘ g) = g ∘ₗ λ ∘ₗ (f ⊗ₘ id)`) loops when tagged as simp,
  so we wrap it inside a rudimentary simproc that only fires when `g ≠ id`.
 -/
Parser.Attr.coassoc_simps : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.piLinearEquiv_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : Semiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : Module A M] {ι' : Type u_6} {M' : ι' → Type u_7}
  [inst_5 : (i : ι') → AddCommMonoid (M' i)] [inst_6 : (i : ι') → TopologicalSpace (M' i)]
  [inst_7 : ∀ (i : ι'), ContinuousAdd (M' i)] [inst_8 : (i : ι') → Module R (M' i)]
  [inst_9 : (i : ι') → Module A (M' i)] [inst_10 : ∀ (i : ι'), SMulCommClass A R (M' i)]
  [inst_11 : ∀ (i : ι'), ContinuousConstSMul R (M' i)] (a : M [⋀^ι]→L[A] ((i : ι') → M' i)) (i : ι'),
  ContinuousAlternatingMap.piLinearEquiv.symm a i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap a
-- Aesop.Frontend.Saturate
Aesop.Frontend.mkHypForwardRule : Lean.FVarId → Aesop.ElabM Aesop.LocalRuleSetMember
-- Mathlib.Control.Functor.Multivariate
/-- adapt `MvFunctor.LiftP` to accept predicates as arrows  -/
MvFunctor.LiftP' : {n : ℕ} →
  {α : TypeVec.{u} n} → {F : TypeVec.{u} n → Type v} → [MvFunctor F] → α.Arrow (TypeVec.repeat n Prop) → F α → Prop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] (m m_1 : Std.ExtDHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.getKey! a = m_1.getKey! a_1