mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Extension
/-- A sequence of two Lie algebra homomorphisms is an extension if it is short exact.  -/
LieAlgebra.IsExtension : {R : Type u_1} →
  {N : Type u_2} →
    {L : Type u_3} →
      {M : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : LieRing N] →
                [inst_4 : LieAlgebra R N] →
                  [inst_5 : LieRing M] → [inst_6 : LieAlgebra R M] → (N →ₗ⁅R⁆ L) → (L →ₗ⁅R⁆ M) → Prop
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R) (k : ℕ),
  (Polynomial.monomial n) r * Polynomial.X ^ k = (Polynomial.monomial (n + k)) r
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
ModuleCat.monoidalClosed_curry : ∀ {R : Type u} [inst : CommRing R] {M N P : ModuleCat R} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P)
  (x : ↑M) (y : ↑N),
  (ModuleCat.Hom.hom ((ModuleCat.Hom.hom (CategoryTheory.MonoidalClosed.curry f)) y)) x =
    (CategoryTheory.ConcreteCategory.hom f) (x ⊗ₜ[R] y)
-- Mathlib.Topology.Category.CompHaus.Basic
stoneCechObj_toTop_carrier : ∀ (X : TopCat), ↑(stoneCechObj X).toTop = StoneCech ↑X
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size.eq_def : ∀ {α : Type u_1} (x : Batteries.PairingHeapImp.Heap α),
  x.size =
    match x with
    | Batteries.PairingHeapImp.Heap.nil => 0
    | Batteries.PairingHeapImp.Heap.node a c s => c.size + 1 + s.size
-- Mathlib.Control.Fold
Monoid.foldlM.ofFreeMonoid.eq_1 : ∀ {m : Type u → Type u} [inst : Monad m] {α β : Type u} [inst_1 : LawfulMonad m] (f : β → α → m β),
  Monoid.foldlM.ofFreeMonoid f =
    { toFun := fun xs => MulOpposite.op (flip (List.foldlM f) (FreeMonoid.toList xs)), map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.Vector.Basic
Vector.instForIn'InferInstanceMembershipOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → {n : ℕ} → [Monad m] → ForIn' m (Vector α n) α inferInstance
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.iso_homₚ_inv_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat)
  {Z : C} (h : (HP'.H i).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (TopPair.ofTopCat X))
        (CategoryTheory.CategoryStruct.comp ((HP'.iso i).inv.app X) h)) =
    CategoryTheory.CategoryStruct.comp ((f.hom i).app X) h
-- Mathlib.Topology.Instances.CantorSet
ofDigits_cantorToTernary_sum_le : ∀ {x : ℝ}, x ∈ cantorSet → ∀ {n : ℕ}, ∑ i ∈ Finset.range n, Real.ofDigitsTerm (cantorToTernary x) i ≤ x
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_inverse_obj : ∀ (R : Type u) [inst : CommRing R] (A : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ),
  (commBialgCatEquivComonCommAlgCat R).inverse.obj A = CommBialgCat.of R ↑(Opposite.unop (Opposite.unop A).X)
-- Init.Data.UInt.Basic
UInt64.modn : UInt64 → ℕ → UInt64
-- Init.Data.Array.Lemmas
List.uset_toArray : ∀ {α : Type u_1} {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size},
  l.toArray.uset i a h = (l.set i.toNat a).toArray
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictDerivAt_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜), HasStrictDerivAt 0 0 x
-- Aesop.Tree.Data
/-- Complete matches of forward rules for the current goal (in the same sense
as above).  -/
Aesop.GoalData.forwardRuleMatches : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.ForwardRuleMatches
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.univ_supports : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ), Turing.TM0.Supports M Set.univ
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- Every weight 12 cusp form for `𝒮ℒ` is a scalar multiple of the discriminant.  -/
CuspForm.exists_smul_discriminant_of_weight_eq_twelve : ∀ (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12), ∃ c, c • CuspForm.discriminant = f
-- Init.Data.Int.Order
Int.nonneg_of_neg_nonpos : ∀ {a : ℤ}, -a ≤ 0 → 0 ≤ a
-- Mathlib.Algebra.Colimit.Module
/-- The direct limit constructed as a quotient of the direct sum is isomorphic to
the direct limit constructed as a quotient of the disjoint union.  -/
Module.DirectLimit.linearEquiv : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                [inst_4 : DecidableEq ι] →
                  [inst_5 : Nonempty ι] →
                    [inst_6 : IsDirectedOrder ι] →
                      [inst_7 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                        Module.DirectLimit G f ≃ₗ[R] DirectLimit G f
-- Mathlib.Order.Hom.Basic
/-- `Prod.snd` as an `OrderHom`.  -/
OrderHom.snd : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α × β →o β
-- Mathlib.RingTheory.RootsOfUnity.Basic
MulEquiv.restrictRootsOfUnity_coe_apply : ∀ {R : Type u_4} {S : Type u_5} {k : ℕ} [inst : CommMonoid R] [inst_1 : CommMonoid S] (σ : R ≃* S)
  (ζ : ↥(rootsOfUnity k R)), ↑↑((σ.restrictRootsOfUnity k) ζ) = σ ↑↑ζ
-- Aesop.Tree.Data
Aesop.TreeSpec.Rapp : Aesop.TreeSpec → Type
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_some_get : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} (h' : a ∈ t), t.get? a = some (t.get a h')
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_ball_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 < r → μ (Metric.ball x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 1)
-- Mathlib.Logic.IsEmpty.Defs
/-- `IsEmpty α` expresses that `α` is empty.  -/
IsEmpty : Sort u → Prop
-- Mathlib.Analysis.Meromorphic.Order
meromorphicOrderAt_smul_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x → g x ≠ 0 → meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.equivToOverUnit_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.equivToOverUnit C).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).obj
                X).left)
          ⋯)
      ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.leftKanExtensionIso.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsDense],
  CategoryTheory.Functor.IsDense.leftKanExtensionIso F =
    (F.leftKanExtension F).leftKanExtensionUnique (F.leftKanExtensionUnit F) (CategoryTheory.Functor.id D)
      F.rightUnitor.inv
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_biInter : ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  s.Finite → (Bornology.IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsCobounded (f i))
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (x : CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n),
  R.extEquivCohomologyClass.symm (-x) = -R.extEquivCohomologyClass.symm x
-- Init.Data.SInt.Bitwise
ISize.or_comm : ∀ (a b : ISize), a ||| b = b ||| a
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_empty : ∀ {ι : Type u_1} {π : ι → Sort u_2} (f g : (i : ι) → π i) [inst : (i : ι) → Decidable (i ∈ ∅)], ∅.piecewise f g = g
-- Mathlib.Order.SupIndep
iSupIndep.eq_1 : ∀ {ι : Sort u_5} {α : Type u_6} [inst : CompleteLattice α] (t : ι → α),
  iSupIndep t = ∀ (i : ι), Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
-- Mathlib.Util.Export
Lean.Export.State : Type
-- Std.Sync.Broadcast
/-- Receive a value from the broadcast receiver, returning a task that will resolve with
the next available message. This will block until a message is available.
 -/
Std.Broadcast.Receiver.recv : {α : Type} → [Inhabited α] → Std.Broadcast.Receiver α → BaseIO (Task (Option α))
-- Lean.Declaration
Lean.instBEqAxiomVal.beq : Lean.AxiomVal → Lean.AxiomVal → Bool
-- Lean.Elab.MutualDef
/-- Mapping from FVarId of mutually recursive functions being defined to "closure" expression.  -/
Lean.Elab.Term.MutualClosure.Replacement : Type
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom S.moduleCatLeftHomologyData.i = S.iCycles
-- Std.Http.Protocol.H1.Parser
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.manyItems.go : {α : Type} →
  Std.Internal.Parsec.ByteArray.Parser (Option α) → ℕ → Array α → Std.Internal.Parsec.ByteArray.Parser (Array α)
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.OrderType.noConfusionType : Sort v✝ → Mathlib.Tactic.Order.OrderType → Mathlib.Tactic.Order.OrderType → Sort v✝
-- Mathlib.Data.FunLike.IsApply
IsPowApply.pow_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : Pow β M} {inst_2 : Pow F M} [self : IsPowApply M F α β] (f : F) (n : M) (x : α), (f ^ n) x = f x ^ n
-- Init.Data.Int.Order
Int.natAbs_mul_self' : ∀ (a : ℤ), ↑a.natAbs * ↑a.natAbs = a * a
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfZeroLE_toSignedMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α)
  (hs : MeasureTheory.VectorMeasure.restrict 0 Set.univ ≤ MeasureTheory.VectorMeasure.restrict s Set.univ),
  (s.toMeasureOfZeroLE Set.univ ⋯ hs).toSignedMeasure = s
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The norm of a `NonUnitalNormedRing` as a `RingNorm`.  -/
normRingNorm : (R : Type u_2) → [inst : NonUnitalNormedRing R] → RingNorm R
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The groupoid of `0`-times continuously differentiable maps is just the groupoid of all
open partial homeomorphisms  -/
contDiffGroupoid_zero_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H},
  contDiffGroupoid 0 I = continuousGroupoid H
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Abelian C} {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀} {x y : E.Hom E'},
  x = y ↔
    @CategoryTheory.SpectralSequence.Hom.hom C inst inst_1 κ c r₀ E E' x =
      @CategoryTheory.SpectralSequence.Hom.hom C inst inst_1 κ c r₀ E E' y
-- Lean.Parser.Basic
Lean.Parser.LeadingIdentBehavior.both.sizeOf_spec : sizeOf Lean.Parser.LeadingIdentBehavior.both = 1
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_forall_exists_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso],
  (∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [CategoryTheory.Limits.HasPushout f g],
      P f → ∃ T inl inr, CategoryTheory.IsPushout f g inl inr ∧ P inr) →
    P.IsStableUnderCobaseChange
-- Std.Data.DHashMap.Raw
/-- Inserts multiple keys with the value `()` into the hash map by iterating over the given collection
and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes
precedence.

This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.
 -/
Std.DHashMap.Raw.Const.insertManyIfNewUnit : {α : Type u} →
  [BEq α] →
    [Hashable α] →
      {ρ : Type w} → [ForIn Id ρ α] → (Std.DHashMap.Raw α fun x => Unit) → ρ → Std.DHashMap.Raw α fun x => Unit
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.lt_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupSeminorm E}, p < q ↔ ⇑p < ⇑q
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_eq_arcsin : ∀ {x : ℝ}, 0 ≤ x → Real.arccos x = Real.arcsin √(1 - x ^ 2)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.eq_symm_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {x : A₂} {y : A₁}, y = e.symm x ↔ e y = x
-- Lean.PrettyPrinter.Delaborator.Metavariable
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.describeMVar.namesToString : List Lean.Name → String
-- Std.Time.DateTime.WallTime
_private.Std.Time.DateTime.WallTime.0.Std.Time.WallTime.mk.injEq : ∀ (val val_1 : Std.Time.Duration), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.nextCoeff_map_eq_of_isUnit_leadingCoeff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] [Nontrivial S] (f : R →+* S),
  IsUnit p.leadingCoeff → (Polynomial.map f p).nextCoeff = f p.nextCoeff
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.isSplitEpi_toNondegComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C], CategoryTheory.IsSplitEpi s.toNondegComplex
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ext : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {A B : E →SWOT[σ] F},
  (∀ (x : E), A x = B x) → A = B
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ}
  {k : α} {fallback : γ} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filterMap f m) k fallback =
    ((Std.DHashMap.Internal.Raw₀.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x).getD fallback
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.map_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.Precylinder X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).π = F.map P.π
-- Init.Data.Option.Array
_private.Init.Data.Option.Array.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Init.Data.Nat.Gcd
Nat.gcd_add_mul_right_left : ∀ (m n k : ℕ), (n + k * m).gcd m = n.gcd m
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.move : {Γ : Type u_1} → Turing.Dir → Turing.TM0.Stmt Γ
-- Mathlib.Topology.MetricSpace.Bounded
/-- A version of the **Extreme Value Theorem**: if the set where a continuous function `f`
into a linearly ordered space takes values `≤ f x₀` is bounded for some `x₀`,
then `f` has a global minimum (under suitable topological assumptions).

This is a convenient combination of `Continuous.exists_forall_le'` and
`Metric.isCompact_of_isClosed_isBounded`.  -/
Continuous.exists_forall_le_of_isBounded : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α]
  [inst_3 : PseudoMetricSpace β] [ProperSpace β] {f : β → α},
  Continuous f → ∀ (x₀ : β), Bornology.IsBounded {x | f x ≤ f x₀} → ∃ x, ∀ (y : β), f x ≤ f y
-- Mathlib.LinearAlgebra.Basis.Basic
Module.card_fintype : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] (b : Module.Basis ι R M) [inst : Fintype R] [inst_4 : Fintype M],
  Fintype.card M = Fintype.card R ^ Fintype.card ι
-- Mathlib.GroupTheory.Finiteness
/-- If `f` `g` are homomorphisms from a canonically ordered and well-quasi-ordered
additive monoid `M` to a cancellative additive monoid `N`, the submonoid of `M` on which `f` and `g`
agree is finitely generated. When `M` and `N` are `ℕ ^ k`, this is also known as a version of
**Gordan's lemma**.  -/
AddSubmonoid.fg_eqLocusM : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M]
  [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] [inst_5 : AddMonoid N] [IsCancelAdd N] (f g : M →+ N),
  (f.eqLocusM g).FG
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.reverse.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β),
  x.reverse =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k v l r => Std.DTreeMap.Internal.Impl.inner sz k v r.reverse l.reverse
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.T_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (n : ℕ), 0 < T n
-- Lean.MetavarContext
/-- Create an application `mvar ys` where `ys` are the free variables.
See "Gruesome details" in the beginning of the file for understanding
how let-decl free variables are handled.  -/
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.mkMVarApp : Lean.LocalContext → Lean.Expr → Array Lean.Expr → Lean.MetavarKind → Lean.Expr
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ (α × β)]
  (t : Std.DTreeMap.Internal.Impl α fun x => β) (l : ρ),
  Std.DTreeMap.Internal.Impl.Const.insertMany! t l =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | (a, b) =>
              have r := ⟨Std.DTreeMap.Internal.Impl.insert! a b ↑r, ⋯⟩;
              pure (ForInStep.yield r)
      have r : Std.DTreeMap.Internal.Impl.Const.IteratedSlowInsertionInto t := __s
      pure r).run
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.map_comp_assoc : ∀ {k : Type u} {G H K : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] [inst_8 : Group K] [inst_9 : TopologicalSpace K] [inst_10 : IsTopologicalGroup K]
  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y)
  (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ) {Z_1 : TopModuleCat k} (h : continuousCohomology n Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (ContinuousCohomology.map (φ.comp ψ)
        (CategoryTheory.CategoryStruct.comp (TopRep.ofHom (ContIntertwiningMap.restrict (↑ψ) (TopRep.Hom.hom f))) g) n)
      h =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map φ f n)
      (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map ψ g n) h)
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.comp_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z),
  (f.comp g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_of_charC_cert : ℕ → Lean.Grind.Linarith.Poly → Bool
-- Init.Data.FloatArray.Basic
FloatArray.set : (ds : FloatArray) → (i : ℕ) → Float → autoParam (i < ds.size) FloatArray.set._auto_1 → FloatArray
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.MemLp f p 0
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `Measurable.inv` -/
Measurable.fun_inv : ∀ {G : Type u_2} {α : Type u_3} [inst : Inv G] [inst_1 : MeasurableSpace G] [MeasurableInv G] {m : MeasurableSpace α}
  {f : α → G}, Measurable f → Measurable fun i => (f i)⁻¹
-- Mathlib.Data.List.Destutter
List.destutter'.eq_2 : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (x h : α) (l : List α),
  List.destutter' R x (h :: l) = if R x h then x :: List.destutter' R h l else List.destutter' R x l
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An additive `n`-Freiman homomorphism preserves sums of `n` elements.  -/
IsAddFreimanHom.map_sum_eq_map_sum : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  IsAddFreimanHom n A B f →
    ∀ ⦃s t : Multiset α⦄,
      (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
        (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
          s.card = n → t.card = n → s.sum = t.sum → (Multiset.map f s).sum = (Multiset.map f t).sum
-- Mathlib.Topology.Algebra.Monoid
/-- If `R` acts on `A` via `A`, then continuous addition implies
continuous affine addition by constants.  -/
VAddAssocClass.continuousConstVAdd : ∀ {R : Type u_6} {A : Type u_7} [inst : AddMonoid A] [inst_1 : VAdd R A] [VAddAssocClass R A A]
  [inst_3 : TopologicalSpace A] [SeparatelyContinuousAdd A], ContinuousConstVAdd R A
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.snd_comp_inl : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0], (MonoidWithZeroHom.snd G₀ H₀).comp (MonoidWithZeroHom.inl G₀ H₀) = 1
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_div_left_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableInv G] [MeasurableMul G]
  (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] [μ.IsInvInvariant] (x : G),
  Filter.map (fun t => x / t) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent.eq_1 : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R]
  (M : Matrix n n R), M.permanent = ∑ σ, ∏ i, M (σ i) i
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapRingHom_id_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : CommRing.Pic R}, (CommRing.Pic.mapRingHom (RingHom.id R)) M = M
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∉ t₁ → k ∉ t₁ \ t₂
-- Mathlib.Algebra.Category.FGModuleCat.Basic
ModuleCat.isFG_iff : ∀ {R : Type u} [inst : Ring R] (V : ModuleCat R), ModuleCat.isFG R V ↔ Module.Finite R ↑V