mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α}, k ∈ Std.DTreeMap.filter f t → k ∈ t
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.mulOp_symm_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) (a : M),
  (AddMonoidHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
-- Init.Core
PSigma.eta : ∀ {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} (h₁ : a₁ = a₂), h₁ ▸ b₁ = b₂ → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.pointwise_smul_subset_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] {a : α}
  {S T : Subgroup G}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minEntry?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntry? = t₂.minEntry?
-- Init.Control.Do
/-- Exit a loop body via `continue`.  -/
ContinueT.continue : {α : Type w} → {m : Type w → Type x} → [Monad m] → ContinueT m α
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.inclusion_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S), (NonUnitalSubalgebra.inclusion h) ⟨↑x, m⟩ = x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instBot : {α : Type u_1} → [inst : TopologicalSpace α] → Bot (TopologicalSpace.CompactOpens α)
-- Mathlib.Data.Prod.Lex
/-- Variant of `Prod.Lex.toLex_lt_toLex` for partial orders.  -/
Prod.Lex.toLex_lt_toLex' : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {x y : α × β},
  toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
-- Mathlib.Order.Partition.Basic
Partition.rel_iff_partOf_eq_partOf_of_mem : ∀ {α : Type u_1} {x y : α} {u : Set α} (P : Partition u), x ∈ u → y ∈ u → (P.Rel x y ↔ P.partOf x = P.partOf y)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.algebraMap_inj : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x y : R),
  (algebraMap R (TensorAlgebra R M)) x = (algebraMap R (TensorAlgebra R M)) y ↔ x = y
-- Aesop.Stats.Basic
Aesop.instToJsonForwardStateStats : Lean.ToJson Aesop.ForwardStateStats
-- Mathlib.Data.Vector3
vectorAll_iff_forall : ∀ {α : Type u_1} {n : ℕ} (f : Vector3 α n → Prop), VectorAll n f ↔ ∀ (v : Vector3 α n), f v
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- Concrete construction of the symmetric algebra of `M` by quotienting out
the tensor algebra by the commutativity relation.  -/
SymmetricAlgebra : (R : Type u_1) →
  (M : Type u_2) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- The morphism in `C` underlying the morphism in `InducedBicategory C F`.  -/
CategoryTheory.Bicategory.InducedBicategory.Hom.hom : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → {X Y : CategoryTheory.Bicategory.InducedBicategory C F} → X.Hom Y → (F X ⟶ F Y)
-- Init.Data.Ord.Basic
List.compareLex.eq_2 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : List α), (x = [] → False) → List.compareLex cmp [] x = Ordering.lt
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- A distinguished Cartan subalgebra of the Geck construction.  -/
RootPairing.GeckConstruction.cartanSubalgebra' : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} →
                    [inst_5 : P.IsCrystallographic] →
                      (b : P.Base) →
                        [inst_6 : Finite ι] →
                          [inst_7 : IsDomain R] →
                            [inst_8 : CharZero R] →
                              [inst_9 : Fintype ι] →
                                [inst_10 : DecidableEq ι] → LieSubalgebra R ↥(RootPairing.GeckConstruction.lieAlgebra b)
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyClass.sound : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {f g : X ⟶ Y},
  HomotopicalAlgebra.LeftHomotopyRel f g →
    HomotopicalAlgebra.LeftHomotopyClass.mk f = HomotopicalAlgebra.LeftHomotopyClass.mk g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.filter_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  Std.ExtDTreeMap.filter f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.ExtDTreeMap.Const.get t k h) = false
-- Init.Data.SInt.Bitwise
ISize.not_inj : ∀ {a b : ISize}, ~~~a = ~~~b ↔ a = b
-- Mathlib.Data.Sigma.Order
Sigma.mk_le_mk_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LE (α i)] {i : ι} {a b : α i}, ⟨i, a⟩ ≤ ⟨i, b⟩ ↔ a ≤ b
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.add_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) {M N : SheafOfModules R} (f g : M ⟶ N), (f + g).val = f.val + g.val
-- Init.Data.BitVec.Lemmas
BitVec.toFin_ofNatLT : ∀ {w n : ℕ} (h : n < 2 ^ w), (n#'h).toFin = ⟨n, h⟩
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.Hom.ext_iff : ∀ {n : ℕ} {a b : SimplexCategory.Truncated n} {f g : a ⟶ b},
  f = g ↔ SimplexCategory.Hom.toOrderHom f.hom = SimplexCategory.Hom.toOrderHom g.hom
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toListRev_eq : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toListRev = it.toList.reverse
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D]
  (E : CategoryTheory.Functor K J) (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasColimit F] [inst_5 : CategoryTheory.Limits.HasColimit (E.comp F)]
  [inst_6 : CategoryTheory.Limits.HasColimit (F.comp G)] [h : CategoryTheory.Limits.HasColimit ((E.comp F).comp G)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post (E.comp F) G)
      (G.map (CategoryTheory.Limits.colimit.pre F E)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre (F.comp G) E)
      (CategoryTheory.Limits.colimit.post F G)
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finprod_mem_mul_distrib` that only requires `s ∩ mulSupport f` and
`s ∩ mulSupport g` rather than `s` to be finite.  -/
finprod_mem_mul_distrib' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M} {s : Set α},
  (s ∩ Function.mulSupport f).Finite →
    (s ∩ Function.mulSupport g).Finite →
      ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
-- Mathlib.Logic.Function.Defs
Function.prod_apply : ∀ {ι : Sort u_3} {α : ι → Type u_1} {β : ι → Type u_2} (f : (i : ι) → α i) (g : (i : ι) → β i) (i : ι),
  Function.prod f g i = (f i, g i)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.stdin : Lean.Lsp.Ipc.IpcM IO.FS.Stream
-- Lean.Util.HasConstCache
_private.Lean.Util.HasConstCache.0.Lean.HasConstCache.containsUnsafe.cache : {declNames : Array Lean.Name} → Lean.Expr → Bool → StateM (Lean.HasConstCache declNames) Bool
-- Std.Data.HashMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.
 -/
Std.HashMap.getThenInsertIfNew? : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Option β × Std.HashMap α β
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_rco : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_rco._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
    List.filter (fun e => decide ((cmp e lowerBound).isGE = true ∧ (cmp e upperBound).isLT = true)) t.toList
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between two vectors does not depend on their order.  -/
InnerProductGeometry.angle_comm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y x
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivWithinAt_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {F' : ι → Type u_7}
  [inst_1 : (i : ι) → NormedAddCommGroup (F' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i)
  (s' : Set ((i : ι) → F' i)), HasFDerivWithinAt (fun f => f i) (ContinuousLinearMap.proj i) s' f
-- Init.Conv
/-- Traverses into the left subterm of a binary operator.

In general, for an `n`-ary operator, it traverses into the second to last argument.
It is a synonym for `arg -2`.
 -/
Lean.Parser.Tactic.Conv.lhs : Lean.ParserDescr
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `module` is the name of the module containing the deprecated declaration.  -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.module : Mathlib.Tactic.DeprecationInfo✝ → Lean.Name
-- Mathlib.Tactic.Ring.Basic
/-- `ExSum BaseType sα e` stores the structure of a normalized polynomial expression `e`, which is
a sum of monomials.  -/
Mathlib.Tactic.Ring.ExSum : {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toFun_eq_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), (↑↑f.toRingHom).toFun = ⇑f
-- Mathlib.Topology.DiscreteSubset
/-- Any set is codiscrete within itself.  -/
Filter.self_mem_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] (U : Set X), U ∈ Filter.codiscreteWithin U
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.ReflectsMonomorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.ReflectsMonomorphisms] (α : F ≅ G), G.ReflectsMonomorphisms
-- Mathlib.GroupTheory.Sylow
/-- If `H` is a subgroup of `G`, then `Finite (Sylow p G)` implies `Finite (Sylow p H)`.  -/
Sylow.instFiniteSubtypeMemSubgroup : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite (Sylow p G)], Finite (Sylow p ↥H)
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso F' a).hom.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp (F'.map ((CategoryTheory.Functor.commShiftIso L a).inv.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
          ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app X))))
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G → M` satisfies the multiplicative 1-cocycle condition if
`f(gh) = g • f(h) * f(g)` for all `g, h : G`.  -/
groupCohomology.IsMulCocycle₁ : {G : Type u_1} → {M : Type u_2} → [Mul G] → [CommGroup M] → [SMul G M] → (G → M) → Prop
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.tensorObj_def : ∀ (R : Type u) [inst : CommRing R] (X Y : BialgCat R),
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = BialgCat.of R (TensorProduct R X.carrier Y.carrier)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_6 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w w_1 n : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w_1)
  (h : w = w_1 * n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_2 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_2) →
        (h : w = w_2 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.replicate n expr h with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_2 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_6 w w_1 n expr h
-- Mathlib.Data.Finsupp.Order
Finsupp.single_eval_le_sum : ∀ {α : Type u_5} {M : Type u_6} {N : Type u_7} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : PartialOrder N]
  [IsOrderedAddMonoid N] (f : α →₀ M) {g : M → N},
  g 0 = 0 → (0 ≤ fun x => g x) → ∀ (a : α), g (f a) ≤ f.sum fun x m => g m
-- Mathlib.CategoryTheory.EpiMono
/-- The map splitting `f`  -/
CategoryTheory.SplitMono.retraction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.SplitMono f → (Y ⟶ X)
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_counitIso_inv_app : ∀ {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K),
  CategoryTheory.Discrete.sumEquiv.counitIso.inv.app X =
    (match X with
      | Sum.inl x => CategoryTheory.Iso.refl (Sum.inl x)
      | Sum.inr x => CategoryTheory.Iso.refl (Sum.inr x)).inv
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftLift.IsKan.fac : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.LeftLift f g),
  CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight (H.desc s) f) = s.unit
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.map_coe_ker : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂) (x : ↥f.ker), f ↑x = 0
-- Mathlib.CategoryTheory.Limits.VanKampen
_private.Mathlib.CategoryTheory.Limits.VanKampen.0.CategoryTheory.Limits.mapPair.match_1.eq_2 : ∀ (motive : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair → Sort u_1)
  (h_1 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.left })
  (h_2 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.right }),
  (match { as := CategoryTheory.Limits.WalkingPair.right } with
    | { as := CategoryTheory.Limits.WalkingPair.left } => h_1 ()
    | { as := CategoryTheory.Limits.WalkingPair.right } => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Ring.Defs
Distrib.leftDistribClass : ∀ (R : Type u_1) [inst : Distrib R], LeftDistribClass R
-- Mathlib.Order.Ideal
Order.Ideal.carrier_eq_coe : ∀ {P : Type u_1} [inst : LE P] (s : Order.Ideal P), s.carrier = ↑s
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.clm_apply : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} {a : E} {f : E → F →L[ℝ] G} {g : E → F},
  ContDiffPointwiseHolderAt k α f a →
    ContDiffPointwiseHolderAt k α g a → ContDiffPointwiseHolderAt k α (fun x => (f x) (g x)) a
-- Init.MetaTypes
Lean.Meta.TransparencyMode.instances.sizeOf_spec : sizeOf Lean.Meta.TransparencyMode.instances = 1
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The *trivial* absolute value takes the value `1` on all nonzero elements.  -/
AbsoluteValue.trivial : {R : Type u_5} →
  [inst : Semiring R] →
    [DecidablePred fun x => x = 0] →
      [NoZeroDivisors R] →
        {S : Type u_6} →
          [inst_3 : Semiring S] → [inst_4 : PartialOrder S] → [IsOrderedRing S] → [Nontrivial S] → AbsoluteValue R S
-- Mathlib.Tactic.Sat.FromLRAT
/-- Negation turns AND into OR, so `¬⟦f₁ ∧ f₂⟧_v ≡ ¬⟦f₁⟧_v ∨ ¬⟦f₂⟧_v`.  -/
Sat.Fmla.reify_or : ∀ {v : Sat.Valuation} {f₁ : Sat.Fmla} {a : Prop} {f₂ : Sat.Fmla} {b : Prop},
  Sat.Fmla.reify v f₁ a → Sat.Fmla.reify v f₂ b → Sat.Fmla.reify v (f₁.and f₂) (a ∨ b)
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResultCore.solved.sizeOf_spec : sizeOf Lean.Meta.InjectionResultCore.solved = 1
-- Lean.Data.Options
Lean.Options : Type
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.isIso_ranAdjunction_unit_app_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (G : CategoryTheory.Functor D H),
  CategoryTheory.IsIso ((L.ranAdjunction H).unit.app G) ↔
    G.IsRightKanExtension (CategoryTheory.CategoryStruct.id (L.comp G))
-- Mathlib.GroupTheory.Nilpotent
/-- Additive groups with nilpotency class at most one are abelian.  -/
addCommGroupOfNilpotencyClass : {G : Type u_1} → [inst : AddGroup G] → [AddGroup.IsNilpotent G] → AddGroup.nilpotencyClass G ≤ 1 → AddCommGroup G
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Construct an augmented simplicial object from an augmented cosimplicial
object in the opposite category.  -/
CategoryTheory.CosimplicialObject.Augmented.leftOp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ → CategoryTheory.SimplicialObject.Augmented C
-- Mathlib.Algebra.CharP.Defs
CharP.ofNat_eq_zero : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] [inst_2 : p.AtLeastTwo], OfNat.ofNat p = 0
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.apply_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (b : B), e (e.symm b) = b
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRicSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRicSlice._auto_1) →
      Std.Ric.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RicSlice α β)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_union_add_inter : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (f : α → M) (s t : Set α),
  (s ∪ t).indicator f + (s ∩ t).indicator f = s.indicator f + t.indicator f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomWhiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : C} [inst_3 : CategoryTheory.MonObj X]
  [inst_4 : CategoryTheory.MonObj Y] [inst_5 : CategoryTheory.MonObj Z] {f : Y ⟶ Z} [CategoryTheory.IsMonHom f],
  CategoryTheory.IsMonHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
-- Mathlib.Data.Rat.Lemmas
/-- A version of `Rat.mul_den` without division.  -/
Rat.den_mul_den_eq_den_mul_gcd : ∀ (q₁ q₂ : ℚ), q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
-- Lean.Meta.Tactic.Grind.Intro
Lean.Meta.Grind.instInhabitedIntroResult.default : Lean.Meta.Grind.IntroResult✝
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `AddMonoidHom.domRestrict_mrange`. -/
AddMonoidHom.restrict_mrange : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N),
  AddMonoidHom.mrange (f.domRestrict S) = AddSubmonoid.map f S
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.ιColimitType_jointly_surjective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) (t : F.ColimitType),
  ∃ j x, F.ιColimitType j x = t
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.radius_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → 0 < p.radius
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F).hom.app X).hom.left =
    CategoryTheory.CategoryStruct.id X.pt.left
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.π_obj : ∀ (M : Type u_1) [inst : Monoid M] (X : Type u) [inst_1 : MulAction M X] (p : CategoryTheory.ActionCategory M X),
  (CategoryTheory.ActionCategory.π M X).obj p = CategoryTheory.SingleObj.star M