mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.restrictFreeVar.match_1.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : ℕ) → (x_1 : L.BoundedFormula α x) → (↥x_1.freeVarFinset → β) → Sort u_4) (_n : ℕ)
  (φ₁ φ₂ : L.BoundedFormula α _n) (f : ↥(φ₁.imp φ₂).freeVarFinset → β)
  (h_1 :
    (_n : ℕ) →
      (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β) →
        motive _n FirstOrder.Language.BoundedFormula.falsum _f)
  (h_2 :
    (_n : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin _n)) →
        (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β) →
          motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂) f)
  (h_3 :
    (_n l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) →
          (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β) →
            motive _n (FirstOrder.Language.BoundedFormula.rel R ts) f)
  (h_4 : (_n : ℕ) → (φ₁ φ₂ : L.BoundedFormula α _n) → (f : ↥(φ₁.imp φ₂).freeVarFinset → β) → motive _n (φ₁.imp φ₂) f)
  (h_5 : (_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → (f : ↥φ.all.freeVarFinset → β) → motive _n φ.all f),
  (match _n, φ₁.imp φ₂, f with
    | _n, FirstOrder.Language.BoundedFormula.falsum, _f => h_1 _n _f
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f => h_2 _n t₁ t₂ f
    | _n, FirstOrder.Language.BoundedFormula.rel R ts, f => h_3 _n l R ts f
    | _n, φ₁.imp φ₂, f => h_4 _n φ₁ φ₂ f
    | _n, φ.all, f => h_5 _n φ f) =
    h_4 _n φ₁ φ₂ f
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.beq_self_eq_true : ∀ (a : Bool), (a == a) = true
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasStrictFDerivAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {f' : E →L[𝕜] ℂ} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) • f') x
-- Aesop.Util.UnionFind
Aesop.UnionFind.size : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Aesop.UnionFind α → ℕ
-- Mathlib.Analysis.Normed.Group.Defs
NNNorm.toENorm : {E : Type u_8} → [NNNorm E] → ENorm E
-- Init.Core
Std.LawfulIdentity.mk : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [toIdentity : Std.Identity op o]
  [toLawfulLeftIdentity : Std.LawfulLeftIdentity op o] [toLawfulRightIdentity : Std.LawfulRightIdentity op o],
  Std.LawfulIdentity op o
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.snd_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) (a : J.L),
  K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (J.snd a))
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.mk_eq_top_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M} (hp : p ∈ f.invtSubmodule), ⟨p, hp⟩ = ⊤ ↔ p = ⊤
-- Mathlib.Data.Fin.SuccPred
/-- Embedding `Fin n` into `Fin (n + 1)` with a hole around zero embeds by `succ`.  -/
Fin.succAbove_zero : ∀ {n : ℕ}, Fin.succAbove 0 = Fin.succ
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.zero_contLinear : ∀ {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] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P], ContinuousAffineMap.contLinear 0 = 0
-- Init.Data.Nat.Bitwise.Lemmas
Nat.mod_two_pos_mod_two_eq_one : ∀ {x j : ℕ}, x % 2 ^ j % 2 = 1 ↔ 0 < j ∧ x % 2 = 1
-- Mathlib.Algebra.Lie.Subalgebra
/-- A Lie subalgebra is closed under Lie bracket.  -/
LieSubalgebra.lie_mem' : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (self : LieSubalgebra R L) {x y : L}, x ∈ self.carrier → y ∈ self.carrier → ⁅x, y⁆ ∈ self.carrier
-- Init.Data.List.Lemmas
List.getLast?_eq_none_iff : ∀ {α : Type u_1} {xs : List α}, xs.getLast? = none ↔ xs = []
-- Mathlib.Combinatorics.Schnirelmann
/-- **Alias** of `schnirelmannDensity_setOfPred_Odd`. -/
schnirelmannDensity_setOf_Odd : schnirelmannDensity (Set.ofPred Odd) = 2⁻¹
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_map_of_surjective' : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F),
  Function.Surjective ⇑f → ∀ (I : Ideal R), Ideal.comap f (Ideal.map f I) = I ⊔ RingHom.ker f
-- Mathlib.Geometry.Convex.Cone.Dual
/-- The dual cone of a set `s` with respect to a bilinear pairing `p` is the cone consisting of all
points `y` such that for all points `x ∈ s` we have `0 ≤ p x y`.  -/
PointedCone.dual : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommMonoid M] →
            [inst_4 : Module R M] →
              {N : Type u_3} →
                [inst_5 : AddCommMonoid N] → [inst_6 : Module R N] → (M →ₗ[R] N →ₗ[R] R) → Set M → PointedCone R N
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
Finset.sum_sq_le_sum_mul_sum_of_sq_eq_mul : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [ExistsAddOfLE R] (s : Finset ι) {r f g : ι → R},
  (∀ i ∈ s, 0 ≤ f i) →
    (∀ i ∈ s, 0 ≤ g i) → (∀ i ∈ s, r i ^ 2 = f i * g i) → (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.Model.BackwardStringSearcher.instLawfulBackwardPatternModel : ∀ {pat : String}, String.Slice.Pattern.Model.LawfulBackwardPatternModel pat
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M)
  {c : FiniteArchimedeanClass M} {a : M}, a ∈ u.stratum c → a ≠ 0 → ArchimedeanClass.mk a = ↑c
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} {p : P},
  s.IsTangentAt p as → s.radius ≠ 0 → Module.finrank ℝ ↥as.direction + 1 = Module.finrank ℝ V → as = s.orthRadius p
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.mk.injEq : ∀ {R : Type u_1} [inst : CommRing R] (toSubring : Subring R) [isLocalRing : IsLocalRing ↥toSubring]
  (toSubring_1 : Subring R) (isLocalRing_1 : IsLocalRing ↥toSubring_1),
  ({ toSubring := toSubring, isLocalRing := isLocalRing } =
      { toSubring := toSubring_1, isLocalRing := isLocalRing_1 }) =
    (toSubring = toSubring_1)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.reduceBin : Lean.Name → ℕ → (ℕ → ℕ → ℕ) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The free-forgetful adjoint for `TopModuleCat R`.  -/
TopModuleCat.freeAdj : (R : Type u) →
  [inst : Ring R] → [inst_1 : TopologicalSpace R] → TopModuleCat.free R ⊣ CategoryTheory.forget₂ (TopModuleCat R) TopCat
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.kerLift.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P),
  AddCon.kerLift f = (AddCon.ker f).lift f ⋯
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.piecewise_add : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] (s : Set I) [inst_1 : (i : I) → Decidable (i ∈ s)]
  (f₁ f₂ g₁ g₂ : (i : I) → f i), s.piecewise (f₁ + f₂) (g₁ + g₂) = s.piecewise f₁ g₁ + s.piecewise f₂ g₂
-- Lean.Language.Basic
/-- Do not mark as being processed. Child nodes are still visited.  -/
Lean.Language.SnapshotTask.ReportingRange.skip : Lean.Language.SnapshotTask.ReportingRange
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.simpMatchCore : Lean.Name → Lean.Name → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.triangleOpEquivalence_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ],
  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor =
    CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C
-- Mathlib.Data.Num.Lemmas
Num.cast_lt : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {m n : Num}, ↑m < ↑n ↔ m < n
-- Lean.Meta.Eqns
/-- Returns an "unfold" theorem (`f.eq_def`) for the given declaration.
By default, we do not create unfold theorems for nonrecursive definitions.
You can use `nonRec := true` to override this behavior.
 -/
Lean.Meta.getUnfoldEqnFor? : Lean.Name → optParam Bool false → Lean.MetaM (Option Lean.Name)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.powers_eq_zpowers : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x → ↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_hom_app : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF).hom.app X =
    CategoryTheory.CategoryStruct.comp
      (eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X)))))
      (CategoryTheory.CategoryStruct.comp
        (eB.inverse.map (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj X)))))
        (CategoryTheory.CategoryStruct.comp (eB.inverse.map (e'.counitIso.hom.app (eB.functor.obj X)))
          (eB.unitIso.inv.app X)))
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Incompatible.symm : ∀ {α : Type u} {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f1 f2 ↔ Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f2 f1
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- **Alias** of the forward direction of `sub_eq_zero`. -/
Mathlib.Tactic.LinearCombination.eq_rearrange : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b = 0 → a = b
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive], CategoryTheory.Limits.PreservesFiniteBiproducts F
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.findSomeM?.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.IteratorLoop α m m] (it : Std.IterM m β) (f : β → m (Option γ)),
  it.findSomeM? f =
    forIn it none fun x x_1 => do
      let __do_lift ← f x
      match __do_lift with
        | none => pure (ForInStep.yield none)
        | some fx => pure (ForInStep.done (some fx))
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has limits of shape `J` then any reflective subcategory has limits of shape `J`.  -/
CategoryTheory.hasLimitsOfShape_of_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasLimitsOfShape J C]
  (R : CategoryTheory.Functor D C) [CategoryTheory.Reflective R], CategoryTheory.Limits.HasLimitsOfShape J D
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a `CommGroup` by a congruence relation is a `CommGroup`.  -/
Con.commGroup : {M : Type u_4} → [inst : CommGroup M] → (c : Con M) → CommGroup c.Quotient
-- Mathlib.Order.Completion
/-- Variant of `DedekindCut.lt_iff_exists` with `<` and `≤` swapped  -/
DedekindCut.lt_iff_exists' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : DedekindCut α},
  a < b ↔ ∃ c, a ≤ DedekindCut.principal c ∧ DedekindCut.principal c < b
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Reinterpret a `AffineIsometryEquiv` as a `ContinuousAffineEquiv`.  -/
AffineIsometryEquiv.instCoeContinuousAffineEquiv : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] → Coe (P ≃ᵃⁱ[𝕜] P₂) (P ≃ᴬ[𝕜] P₂)
-- Mathlib.Data.List.Forall2
List.Forall₂.get : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {x : List α} {y : List β},
  List.Forall₂ R x y → ∀ ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length), R (x.get ⟨i, hx⟩) (y.get ⟨i, hy⟩)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.decidableMemZMultiples : {G : Type u_1} → [inst : AddGroup G] → {a : G} → DecidablePred fun x => x ∈ AddSubgroup.zmultiples a
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.msymm_one : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ],
  MvPolynomial.msymm σ R (Nat.Partition.indiscrete 1) = ∑ i, MvPolynomial.X i
-- Mathlib.Tactic.Core
/-- Simulates the `<;>` tactic combinator.
First runs `tac1` and then runs `tac2` on all newly-generated subgoals.
 -/
Lean.Elab.Tactic.andThenOnSubgoals : Lean.Elab.Tactic.TacticM Unit → Lean.Elab.Tactic.TacticM Unit → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Order.Minimal
Maximal.le : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : LinearOrder α], Maximal P x → P y → y ≤ x
-- Init.GrindInstances.ToInt
Int16.size.eq_1 : Int16.size = 65536
-- Mathlib.GroupTheory.Congruence.Defs
Con.induction_on_units : ∀ {M : Type u_1} [inst : Monoid M] {c : Con M} {p : c.Quotientˣ → Prop} (u : c.Quotientˣ),
  (∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }) → p u
-- Mathlib.Algebra.Order.ToIntervalMod
/-- `toIcoMod` as an equiv from the quotient.  -/
QuotientAddGroup.equivIcoMod : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] →
      [IsOrderedAddMonoid α] →
        [hα : Archimedean α] → {p : α} → 0 < p → (a : α) → α ⧸ AddSubgroup.zmultiples p ≃ ↑(Set.Ico a (a + p))
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_top : ∀ {M : Type u_2} [inst : Mul M], ⊤.op = ⊤
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.continuous_transReflReparamAux : Continuous Path.Homotopy.transReflReparamAux
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_to_countable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Countable α] [inst_2 : MeasurableSpace β] {f : β → α},
  (∀ (y : β), MeasurableSet (f ⁻¹' {f y})) → Measurable f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.anchor_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : LieRing L₁]
  [inst_3 : Module A₁ L₁] [inst_4 : LieRingModule L₁ A₁] [inst_5 : Algebra R A₁] [inst_6 : LieAlgebra R L₁]
  [inst_7 : LieRinehartRing A₁ L₁] [inst_8 : LieRinehartAlgebra R A₁ L₁] (l : L₁) (a : A₁),
  ((LieRinehartAlgebra.anchor R A₁ L₁).toLieHom l) a = ⁅l, a⁆
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of `C^n` functions, with summable uniform bounds on the successive
derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative.  -/
iteratedFDeriv_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞},
  (∀ (i : α), ContDiff 𝕜 (↑N) (f i)) →
    (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) →
      (∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) →
        ∀ {k : ℕ},
          ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
-- Mathlib.RingTheory.TensorProduct.Basic
Submodule.map_range_rTensor_subtype_lid : ∀ {R : Type u_1} {Q : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid Q] [inst_2 : Module R Q]
  {I : Submodule R R}, Submodule.map (↑(TensorProduct.lid R Q)) (LinearMap.rTensor Q I.subtype).range = I • ⊤
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instSemiring : {R : Type u_1} → [Semiring R] → Semiring Rᵐᵒᵖ
-- Aesop.RuleSet
/-- The simprocs stored in this rule set.
 -/
Aesop.GlobalRuleSet.simprocs : Aesop.GlobalRuleSet → Lean.Meta.Simprocs
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If the image of a family of points in affine space under an affine transformation is affine-
independent, then the original family of points is also affine-independent.  -/
AffineIndependent.of_comp : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂),
  AffineIndependent k (⇑f ∘ p) → AffineIndependent k p
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The unique two-coloring of a tree that colors the given vertex with zero  -/
SimpleGraph.IsTree.coloringTwoOfVert : {V : Type u_1} → {G : SimpleGraph V} → G.IsTree → V → G.Coloring (Fin 2)
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_of_group_fg : ∀ {G : Type u_3} [inst : Group G] [Group.FG G], Monoid.FG G
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulOneClass.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : MulOneClass M],
  Filter.Germ.instMulOneClass =
    { toOne := Filter.Germ.instOne, toMul := Filter.Germ.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_lt : PrimrecRel fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.one_compl : ∀ {R : Type u_1} [inst : NonAssocRing R], 1ᶜ = 0
-- Mathlib.Order.RelIso.Basic
RelEmbedding.swap_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (a : α), f.swap a = f a
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X X_1 : C),
  X = X_1 →
    ∀ (Y Y_1 : C),
      Y = Y_1 → ∀ (n n_1 : ℕ), n = n_1 → CategoryTheory.Abelian.Ext X Y n = CategoryTheory.Abelian.Ext X_1 Y_1 n_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.instHasLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasLimits (CategoryTheory.CosimplicialObject.Truncated C n)
-- Lean.Parser.Basic
Lean.Parser.categoryParserFn : Lean.Name → Lean.Parser.ParserFn
-- Batteries.Data.List.Basic
/-- An auxiliary function for `List.mapWithPrefixSuffix`.  -/
List.mapWithPrefixSuffixAux : {α : Type u_1} → {β : Type u_2} → (List α → α → List α → β) → List α → List α → List β
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  ⦃f g : α →ₙ+* β⦄, (∀ (x : α), f x = g x) → f = g
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.mk.sizeOf_spec : ∀ (text : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (sections : Array (ℕ × Lean.DeclarationRange × Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
  (declarationRange : Lean.DeclarationRange),
  sizeOf { text := text, sections := sections, declarationRange := declarationRange } =
    1 + sizeOf text + sizeOf sections + sizeOf declarationRange
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_comm : ∀ {γ : Type w} {ι₁ : Type u_3} {ι₂ : Type u_4} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} [inst : DecidableEq ι₁]
  [inst_1 : DecidableEq ι₂] [inst_2 : (i : ι₁) → Zero (β₁ i)] [inst_3 : (i : ι₂) → Zero (β₂ i)]
  [inst_4 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [inst_5 : (i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)]
  [inst_6 : AddCommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i)
  (h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ),
  (f₁.sum fun i₁ x₁ => f₂.sum fun i₂ x₂ => h i₁ x₁ i₂ x₂) = f₂.sum fun i₂ x₂ => f₁.sum fun i₁ x₁ => h i₁ x₁ i₂ x₂
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.comp_eq_comp : ∀ {X Y Z : CategoryTheory.ReflQuiv} (F : X ⟶ Y) (G : Y ⟶ Z), CategoryTheory.CategoryStruct.comp F G = F ⋙rq G
-- Mathlib.GroupTheory.GroupAction.Hom
SMulCommClass.toMulActionHom.eq_1 : ∀ {M : Type u_11} (N : Type u_9) (α : Type u_10) [inst : SMul M α] [inst_1 : SMul N α] [inst_2 : SMulCommClass M N α]
  (c : M), SMulCommClass.toMulActionHom N α c = { toFun := fun x => c • x, map_smul' := ⋯ }
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.State.mk.injEq : ∀ (equalMVarIds : Std.HashMap Lean.MVarId Lean.MVarId) (equalLMVarIds : Std.HashMap Lean.LMVarId Lean.LMVarId)
  (leftUnassignedMVarValues rightUnassignedMVarValues : Std.HashMap Lean.MVarId Lean.Expr)
  (equalMVarIds_1 : Std.HashMap Lean.MVarId Lean.MVarId) (equalLMVarIds_1 : Std.HashMap Lean.LMVarId Lean.LMVarId)
  (leftUnassignedMVarValues_1 rightUnassignedMVarValues_1 : Std.HashMap Lean.MVarId Lean.Expr),
  ({ equalMVarIds := equalMVarIds, equalLMVarIds := equalLMVarIds, leftUnassignedMVarValues := leftUnassignedMVarValues,
        rightUnassignedMVarValues := rightUnassignedMVarValues } =
      { equalMVarIds := equalMVarIds_1, equalLMVarIds := equalLMVarIds_1,
        leftUnassignedMVarValues := leftUnassignedMVarValues_1,
        rightUnassignedMVarValues := rightUnassignedMVarValues_1 }) =
    (equalMVarIds = equalMVarIds_1 ∧
      equalLMVarIds = equalLMVarIds_1 ∧
        leftUnassignedMVarValues = leftUnassignedMVarValues_1 ∧ rightUnassignedMVarValues = rightUnassignedMVarValues_1)
-- Init.Prelude
HOrElse.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → (Unit → β) → γ) → HOrElse α β γ
-- Std.Time.DateTime.WallTime
Std.Time.instLTWallTime : LT Std.Time.WallTime