mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is conjugate linear in the first coordinate.  -/
PreInnerProductSpace.Core.smul_left : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (self : PreInnerProductSpace.Core 𝕜 F) (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_map_comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  (K : Ideal S) [inst_3 : RingHomClass F R S], Ideal.comap f (Ideal.map f (Ideal.comap f K)) = Ideal.comap f K
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum_indep_iff : ∀ {α : Type u} {β : Type v} (M : Matroid α) (N : Matroid β) {I : Set (α ⊕ β)},
  (M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
RCLike.borelSpace : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], BorelSpace 𝕜
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbit.eq_1 : ∀ (γ : Type u_2) {α : Type u_3} [inst : SMul γ α] (a : α), MulAction.orbit γ a = Set.range fun m => m • a
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ico_succ_right_eq_Icc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Finset.Ico a (Order.succ b) = Finset.Icc a b
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ici_succ_eq_Ioi_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : SuccOrder α] {a : α},
  ¬IsMax a → Finset.Ici (Order.succ a) = Finset.Ioi a
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `p` is prime, `J(a | p) = -1` and `p` divides `x^2 - a*y^2`, then `p` must divide
`x` and `y`.  -/
jacobiSym.prime_dvd_of_eq_neg_one : ∀ {p : ℕ} [Fact (Nat.Prime p)] {a : ℤ}, jacobiSym a p = -1 → ∀ {x y : ℤ}, ↑p ∣ x ^ 2 - a * y ^ 2 → ↑p ∣ x ∧ ↑p ∣ y
-- Lean.Meta.CollectFVars
_private.Lean.Meta.CollectFVars.0.Lean.CollectFVars.State.addDependencies.go : StateRefT' IO.RealWorld ℕ (StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM) Unit
-- Init.Data.String.Lemmas.Search
_private.Init.Data.String.Lemmas.Search.0.String.Pos.find.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {s : String} (pos : s.Pos) (pattern : ρ)
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pattern σ],
  pos.find pattern = String.Pos.ofToSlice (pos.toSlice.find pattern)
-- Mathlib.NumberTheory.FermatPsp
_private.Mathlib.NumberTheory.FermatPsp.0.Nat.b_id_helper : ∀ {a b : ℕ}, 2 ≤ a → 2 < b → 2 ≤ (a ^ b + 1) / (a + 1)
-- Mathlib.Topology.Algebra.MulAction
ContinuousOn.fun_vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {s : Set Y},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun i => f i +ᵥ g i) s
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.StronglyMeasurable.integral_condExpKernel' : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
-- Mathlib.RingTheory.Binomial
/-- The Chu-Vandermonde identity for binomial rings  -/
Ring.add_choose_eq : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : BinomialRing R] {r s : R} (k : ℕ),
  Commute r s →
    Ring.choose (r + s) k = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal k, Ring.choose r ij.1 * Ring.choose s ij.2
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_succ_X_mul : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ : PowerSeries R),
  (PowerSeries.coeff (n + 1)) (PowerSeries.X * φ) = (PowerSeries.coeff n) φ
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
FreeNonUnitalNonAssocAlgebra.hom_ext_iff : ∀ {R : Type u_1} {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A},
  F₁ = F₂ ↔ ∀ (x : X), F₁ (FreeNonUnitalNonAssocAlgebra.of R x) = F₂ (FreeNonUnitalNonAssocAlgebra.of R x)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.isLink_congr : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  x ∈ H.vertexSet → H.IsClosedSubgraph G → (H.IsLink e x y ↔ G.IsLink e x y)
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.mono' : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : One β] [inst_2 : One γ] {f : α → β}
  {f' : α → γ}, HasCompactMulSupport f → Function.mulSupport f' ⊆ mulTSupport f → HasCompactMulSupport f'
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.injective : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], M ≤ nonZeroDivisors R → Function.Injective ⇑(algebraMap R S)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.compUliftCoyonedaIso_hom_app_app_hom_apply_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X_1 : D)
  (x : ULift.{max v₁ w, v₂} (F.obj (Opposite.unop X) ⟶ X_1)),
  ((CategoryTheory.ConcreteCategory.hom ((adj.compUliftCoyonedaIso.hom.app X).app X_1)) x).down =
    CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X)) (G.map x.down)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instSingleton : Singleton ZFSet.{u_1} ZFSet.{u_1}
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold.denote_go_and : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {aig : Std.Sat.AIG α}
  (acc : aig.Ref),
  ∀ curr ≤ len,
    ∀ (input : aig.RefVec len),
      (⟦assign,
            { aig := (Std.Sat.AIG.RefVec.fold.go aig acc curr len input Std.Sat.AIG.mkAndCached).aig,
              ref := (Std.Sat.AIG.RefVec.fold.go aig acc curr len input Std.Sat.AIG.mkAndCached).ref }⟧ =
          true) =
        (⟦assign, { aig := aig, ref := acc }⟧ = true ∧
          ∀ (idx : ℕ) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.closure_zero_prod : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (t : Set N),
  AddSubmonoid.closure ({0} ×ˢ t) = ⊥.prod (AddSubmonoid.closure t)
-- Init.Data.Array.Lemmas
Array.flatMap_id' : ∀ {α : Type u_1} {xss : Array (Array α)}, Array.flatMap (fun xs => xs) xss = xss.flatten
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.flatten_equiv : ∀ {α : Type u} {c : Computation (Stream'.WSeq α)} {s : Stream'.WSeq α}, s ∈ c → Stream'.WSeq.flatten c ~ʷ s
-- Lean.Meta.Tactic.Generalize
Lean.Meta.GeneralizeArg.xName? : Lean.Meta.GeneralizeArg → Option Lean.Name
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- If `X ⟶ S`, `Y ⟶ S` are open embeddings, then so is `X ×ₛ Y ⟶ S`.  -/
TopCat.isOpenEmbedding_of_pullback : ∀ {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S},
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g) →
      Topology.IsOpenEmbedding
        ⇑(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one))
-- Mathlib.Data.Real.Embedding
/-- Set of rational numbers that are less than the "number" `x / 1`.
Formally, these are numbers `p / q` such that `p • 1 < q • x`.  -/
Archimedean.ratLt : {M : Type u_1} → [AddCommGroup M] → [LinearOrder M] → [One M] → M → Set ℚ
-- Init.Data.Vector.Lemmas
Vector.getElem?_setIfInBounds : ∀ {α : Type u_1} {n i j : ℕ} {xs : Vector α n} {x : α},
  (xs.setIfInBounds i x)[j]? = if i = j then if i < n then some x else none else xs[j]?
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_strictMono : StrictMono Cardinal.ofENat
-- Mathlib.Algebra.Group.Basic
mul_left_iterate_apply_one : ∀ {M : Type u_4} [inst : Monoid M] {n : ℕ} (a : M), (fun x => a * x)^[n] 1 = a ^ n
-- Mathlib.Order.Atoms
IsSimpleOrder.toNontrivial : ∀ {α : Type u_4} {inst : LE α} {inst_1 : BoundedOrder α} [self : IsSimpleOrder α], Nontrivial α
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.emptyOn_isBase_iff : ∀ {α : Type u_1} {B : Set α}, (Matroid.emptyOn α).IsBase B ↔ B = ∅
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Multiset «$α»)} {a : Q(«$α»)} {s' : Q(Multiset «$α»)}
  {pf : Q(«$s» = «$a» ::ₘ «$s'»)} {a_1 : Q(«$α»)} {s'_1 : Q(Multiset «$α»)} {pf_1 : Q(«$s» = «$a_1» ::ₘ «$s'_1»)},
  Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons a s' pf =
      Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons a_1 s'_1 pf_1 →
    a = a_1 ∧ s' = s'_1 ∧ pf = pf_1
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is differentiable.

We give here a version of this statement within a set at a point.  -/
MDifferentiableWithinAt.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {M : Type u_6}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8}
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : VectorBundle 𝕜 F₃ E₃] {b : M → B}, ⋯
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_ofList_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashSet.Raw.ofList l).size ≤ l.length
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Result.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {E : Q(«$α») → Type u_1} {e : Q(«$α»)} (expr : Q(«$α»)) (val : E expr)
  (proof : Q(«$e» = «$expr»)) (expr_1 : Q(«$α»)) (val_1 : E expr_1) (proof_1 : Q(«$e» = «$expr_1»)),
  ({ expr := expr, val := val, proof := proof } = { expr := expr_1, val := val_1, proof := proof_1 }) =
    (expr = expr_1 ∧ val ≍ val_1 ∧ proof = proof_1)
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_smul_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] {𝕝 : Type u_5}
  [inst_4 : CommSemiring 𝕝] [inst_5 : StarRing 𝕝] [inst_6 : Algebra 𝕝 𝕜] [StarModule 𝕝 𝕜] [SMulCommClass ℝ 𝕝 𝕜]
  [inst_9 : (i : ι) → Module 𝕝 (E i)] [∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝) (w : ι → ℝ) (f g : (i : ι) → E i),
  ⟪c • f, g⟫_[𝕜, w] = star c • ⟪f, g⟫_[𝕜, w]
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs is said to contain identities if `P` holds
for the identity homomorphism of every ring.  -/
RingHom.ContainsIdentities : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A trident on `f` is just a `Cone (parallelFamily f)`.  -/
CategoryTheory.Limits.Trident : {J : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (J → (X ⟶ Y)) → Type (max (max w u) v)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
fderivWithin_continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {g : (i : ι) → E → F i →L[𝕜] G i} {s : Set E}
  {x : E} [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  DifferentiableWithinAt 𝕜 f s x →
    (∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x) →
      UniqueDiffWithinAt 𝕜 s x →
        fderivWithin 𝕜 (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x) s x =
          (ContinuousMultilinearMap.compContinuousLinearMapL fun x_1 => g x_1 x) ∘SL fderivWithin 𝕜 f s x +
            ((f x).fderivCompContinuousLinearMap fun x_1 => g x_1 x) ∘SL
              ContinuousLinearMap.pi fun i => fderivWithin 𝕜 (g i) s x
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : true = true → motive true) (h_2 : true = false → motive false),
  (match hP : true with
    | true => h_1 hP
    | false => h_2 hP) =
    h_1 ⋯
-- Std.Time.Zoned
/-- Converts a `PlainDateTime` to a `Timestamp` using the `TimeZone`.
 -/
Std.Time.PlainDateTime.toTimestampWithZone : Std.Time.PlainDateTime → Std.Time.TimeZone → Std.Time.Timestamp
-- Mathlib.Data.Nat.Choose.Basic
/-- `choose n r` is maximised when `r` is `n/2`.  -/
Nat.choose_le_middle : ∀ (r n : ℕ), n.choose r ≤ n.choose (n / 2)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.op_zsmul : ∀ {α : Type u_1} [inst : SubNegMonoid α] (x : α) (z : ℤ), AddOpposite.op (z • x) = z • AddOpposite.op x
-- Mathlib.Data.TypeVec
TypeVec.fst_diag : ∀ {n : ℕ} {α : TypeVec.{u_1} n}, TypeVec.comp TypeVec.prod.fst TypeVec.prod.diag = TypeVec.id
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.add_add : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} {g₁ g₂ : α → ℝ},
  f₁ =O[l] g₁ → f₂ =O[l] g₂ → (fun x => f₁ x + f₂ x) =O[l] fun x => ‖g₁ x‖ + ‖g₂ x‖
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.instIsUltrametricDist : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], IsUltrametricDist ℚ_[p]
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
CategoryTheory.Functor.instPreservesLimitOfIsCoreflexivePairDiscreteObjWhiskeringLeftIncl : ∀ (I : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C],
  CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair
    ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete I) I C).obj (CategoryTheory.Functor.incl✝ I))
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.δ.injEq : ∀ {n : ℕ} (i i_1 : Fin (n + 2)), (FreeSimplexQuiver.Hom.δ i = FreeSimplexQuiver.Hom.δ i_1) = (i = i_1)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_linearEquivTuple : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R],
  ⇑(QuaternionAlgebra.linearEquivTuple c₁ c₂ c₃) = ⇑(QuaternionAlgebra.equivTuple c₁ c₂ c₃)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeEquivalence_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  (CategoryTheory.Limits.Cone.postcomposeEquivalence α).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun s =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯)
      ⋯
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelMonoid α],
  Lex.instLeftCancelMonoid = { toMonoid := Lex.instMonoid, toIsLeftCancelMul := ⋯ }
-- Mathlib.Topology.Defs.Basic
/-- The closure of `s` is the smallest closed set containing `s`.  -/
closure : {X : Type u} → [TopologicalSpace X] → Set X → Set X
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.add_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (v : NumberField.FinitePlace K) (x y : K),
  v (x + y) ≤ max (v x) (v y)
-- Mathlib.Topology.Algebra.UniformField
UniformSpace.Completion.mul_hatInv_cancel : ∀ {K : Type u_1} [inst : Field K] [inst_1 : UniformSpace K] [IsTopologicalDivisionRing K] [CompletableTopField K]
  [IsUniformAddGroup K] {x : UniformSpace.Completion K}, x ≠ 0 → x * x.hatInv = 1
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_eq_top_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (f : β → α) (S : Finset β),
  S.inf f = ⊤ ↔ ∀ s ∈ S, f s = ⊤
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.ext : ∀ {X : Type u_1} {Y : Type u_2} {x y : TypeCat.Fun X Y}, x.toFun = y.toFun → x = y
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- If `s : Set R` is absorbing under multiplication, then its `TwoSidedIdeal.span` coincides with
its `AddSubgroup.closure`, as sets.  -/
TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing : ∀ {R : Type u_1} [inst : NonUnitalRing R] {s : Set R},
  (∀ (x y : R), y ∈ s → x * y ∈ s) →
    (∀ (y x : R), y ∈ s → y * x ∈ s) → ∀ {z : R}, z ∈ TwoSidedIdeal.span s ↔ z ∈ AddSubgroup.closure s
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProduct_bot_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.extensionProduct ⊥ = ⊥
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) (h : HomotopicalAlgebra.FibrantBrownFactorization f) [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence h.p
-- Mathlib.Logic.Relation
Relation.ReflGen.instIsPreorderOfIsTrans : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r], IsPreorder α (Relation.ReflGen r)
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_submodule_iff_right_eq_zero_of_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  (r : R), IsSMulRegular (↥N) r ↔ ∀ x ∈ N, r • x = 0 → x = 0
-- Mathlib.Algebra.GradedMulAction
SetLike.toGSMul : {ιA : Type u_1} →
  {ιB : Type u_2} →
    {S : Type u_5} →
      {R : Type u_6} →
        {N : Type u_7} →
          {M : Type u_8} →
            [inst : SetLike S R] →
              [inst_1 : SetLike N M] →
                [inst_2 : SMul R M] →
                  [inst_3 : VAdd ιA ιB] →
                    (A : ιA → S) →
                      (B : ιB → N) → [SetLike.GradedSMul A B] → GradedMonoid.GSMul (fun i => ↥(A i)) fun i => ↥(B i)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An injective presentation of an object `X` consists of a monomorphism `f : X ⟶ J`
to some injective object `J`.
 -/
CategoryTheory.InjectivePresentation.J : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.InjectivePresentation X → C
-- Mathlib.Data.List.Induction
List.reverseRec.eq_def : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) (x : List α),
  List.reverseRec nil append_singleton x =
    match x with
    | [] => nil
    | a :: l =>
      ⋯ ▸
        append_singleton (a :: l).dropLast ((a :: l).getLast ⋯) (List.reverseRec nil append_singleton (a :: l).dropLast)
-- Lean.Parser.Syntax
Lean.Parser.Command.infixl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.eq_1 : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (s N : Set X),
  Metric.IsCover ε s N = SetRel.IsCover {(x, y) | edist x y ≤ ↑ε} s N
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.le_of_intCast_le_intCast : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a b : ℤ), ↑a ≤ ↑b → a ≤ b
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The first hexagon identity.  -/
CategoryTheory.BraidedCategory.hexagon_forward_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z X) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom) h))
-- Lean.Meta.DecLevel
Lean.Meta.DecLevelContext.mk.sizeOf_spec : ∀ (canAssignMVars : Bool), sizeOf { canAssignMVars := canAssignMVars } = 1 + sizeOf canAssignMVars
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n] (v : n → α)
  (A : Matrix m n α), A.mulVec (-v) = -A.mulVec v
-- Mathlib.Analysis.Complex.Basic
RCLike.complexLinearIsometryEquiv_apply : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (h : RCLike.im RCLike.I = 1) (a : 𝕜),
  (RCLike.complexLinearIsometryEquiv h) a = (RCLike.complexRingEquiv h).toFun a
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.tendsto_atTop : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α} {a : α},
  Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε