mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
/-- The stupid truncation of a complex `K : HomologicalComplex C c'` relatively to
an embedding `e : c.Embedding c'` of complex shapes.  -/
HomologicalComplex.stupidTrunc : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [CategoryTheory.Limits.HasZeroObject C] →
                HomologicalComplex C c' → (e : c.Embedding c') → [e.IsRelIff] → HomologicalComplex C c'
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.head_stack_ok : ∀ {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {L₁ L₂ : List ℕ} {L₃ : List Turing.PartrecToTM2.Γ'},
  StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
    { l := some (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack q), var := s,
      stk :=
        Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList L₁) [] []
          (Turing.PartrecToTM2.trList L₂ ++ Turing.PartrecToTM2.Γ'.consₗ :: L₃) }
    { l := some q, var := none,
      stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList (L₂.headI :: L₁)) [] [] L₃ }
-- Mathlib.Topology.EMetricSpace.Defs
EDist.ext : ∀ {α : Type u_2} {x y : EDist α}, edist = edist → x = y
-- Init.WF
PSigma.Lex.right : ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (a : α) {b₁ b₂ : β a},
  s a b₁ b₂ → PSigma.Lex r s ⟨a, b₁⟩ ⟨a, b₂⟩
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyLE_mapHomologicalComplex_obj_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Faithful]
  [inst_5 : F.PreservesZeroMorphisms] (n : ℤ),
  CochainComplex.IsStrictlyLE ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) n ↔ K.IsStrictlyLE n
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
CategoryTheory.monoidalIsoComp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} [inst_1 : CategoryTheory.MonoidalCoherence X Y]
  (f : W ≅ X) (g : Y ≅ Z), CategoryTheory.monoidalIsoComp f g = f ≪≫ CategoryTheory.MonoidalCoherence.iso ≪≫ g
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).f x =
    (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Hom.asOverProp f S)
        (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f x) S)).left
-- Mathlib.Data.Seq.Defs
Stream'.Seq.cons_right_injective : ∀ {α : Type u} (x : α), Function.Injective (Stream'.Seq.cons x)
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanHom_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {B : Set β} {f : α → β} {n : ℕ},
  IsAddFreimanHom n ∅ B f
-- Mathlib.RepresentationTheory.Coinduced
Representation.coind_apply : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {B : Type u_5} [inst_3 : AddCommMonoid B] [inst_4 : Module k B] (ρ : Representation k G B) (h : H),
  (Representation.coind φ ρ) h = (LinearMap.funLeft k B fun x => x * h).restrict ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mkIso_inv_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right)
  (base : ψ.base ≅ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left.hom F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_1)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right.hom G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_3),
  (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).inv.base = base.inv
-- Aesop.Index.Basic
Aesop.IndexingMode.target.inj : ∀ {keys keys_1 : Array Lean.Meta.DiscrTree.Key},
  Aesop.IndexingMode.target keys = Aesop.IndexingMode.target keys_1 → keys = keys_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addU_of_Z_eq_zero_left : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F}, P 2 = 0 → WeierstrassCurve.Projective.addU P Q = 0
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with left composition by continuous linear maps.  -/
ContDiffAt.laplacian_CLM_comp_left : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {x : E} {l : F →L[ℝ] G},
  ContDiffAt ℝ 2 f x → Laplacian.laplacian (⇑l ∘ f) x = (⇑l ∘ Laplacian.laplacian f) x
-- Mathlib.Order.Filter.Map
Filter.push_pull' : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter α) (G : Filter β),
  Filter.map f (Filter.comap f G ⊓ F) = G ⊓ Filter.map f F
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.cons_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a a' : α} {b : δ a}
  {f : (a : α) → a ∈ m → δ a} (h' : a' ∈ a ::ₘ m) (h : a' ≠ a), Multiset.Pi.cons m a b f a' h' = f a' ⋯
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_inf_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G},
  H.relIndex L ≠ 0 → K.relIndex L ≠ 0 → (H ⊓ K).relIndex L ≠ 0
-- Mathlib.Order.OrdContinuous
/-- A left adjoint in a Galois connection is left-continuous in the order-theoretic sense.  -/
GaloisConnection.leftOrdContinuous : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {g : β → α},
  GaloisConnection f g → LeftOrdContinuous f
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.coprodZeroIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Limits.coprodZeroIso X).inv = CategoryTheory.Limits.coprod.inl
-- Init.Tactics
/-- Syntax for adding and removing terms in `solve_by_elim`.  -/
Lean.Parser.Tactic.SolveByElim.args : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} {t : Set 𝕜'} (x : E),
  HasDerivWithinAt h₂ h₂' t y →
    HasFDerivWithinAt f f' s x → Set.MapsTo f s t → y = f x → HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (p : Polynomial R) {ι : Type u_2} [inst_2 : Fintype ι] {f : ι → R},
  Function.Injective f → (∀ (i : ι), Polynomial.eval (f i) p = 0) → p.natDegree < Fintype.card ι → p = 0
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGT.congr_simp : ∀ (s : String.Slice) (offset offset_1 : String.Pos.Raw) (e_offset : offset = offset_1) (h : offset < s.rawEndPos),
  s.posGT offset h = s.posGT offset_1 ⋯
-- Mathlib.RingTheory.Coalgebra.Quotient
Coalgebra.Quotient.counit_comp_mkQ : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] (I : Submodule R C) [inst_4 : I.IsCoideal],
  CoalgebraStruct.counit ∘ₗ I.mkQ = CoalgebraStruct.counit
-- Mathlib.CategoryTheory.Subobject.Comma
/-- Technical lemma for `lift_projectQuotient`.  -/
CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {A : CategoryTheory.CostructuredArrow S T}
  {P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ} (f : P ⟶ Opposite.op A) [inst_2 : CategoryTheory.Mono f.unop.left.op],
  CategoryTheory.CategoryStruct.comp f.unop.left (CategoryTheory.Subobject.underlyingIso f.unop.left.op).hom.unop =
    (CategoryTheory.Subobject.mk f.unop.left.op).arrow.unop
-- Plausible.Testable
Plausible.Testable.runProp : (p : Prop) → [Plausible.Testable p] → Plausible.Configuration → Bool → Plausible.Gen (Plausible.TestResult p)
-- Init.Data.Int.Lemmas
Int.add_def : ∀ {a b : ℤ}, a.add b = a + b
-- Init.Data.UInt.Lemmas
USize.toFin_toBitVec : ∀ (x : USize), x.toBitVec.toFin = x.toFin
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  (forIn m init fun a d => f a.fst d) = forIn m.keys init f
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_eq_restrict : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), M.delete D = M.restrict (M.E \ D)
-- Mathlib.Analysis.Complex.HasPrimitives
Complex.IsConservativeOn.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {U V : Set ℂ},
  U ⊆ V → Complex.IsConservativeOn f V → Complex.IsConservativeOn f U
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(coprod.inr ▷ X) : Z ⊗ X ⟶ (Y ⨿ Z) ⊗ X` and
`(∂R X Y Z).inv :  (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)` is equal to the right coprojection
`coprod.inr : Z ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)`.  -/
CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X) (∂R X Y Z).inv =
    CategoryTheory.Limits.coprod.inr
-- Lean.Elab.Task
/-- Given a monadic value in `MetaM`, creates a task that runs it in the current state,
returning
* a cancellation hook and
* a monadic value with the cached result (and subsequent state as it was after running).
 -/
Lean.Meta.MetaM.asTask : {α : Type} → Lean.MetaM α → Lean.MetaM (BaseIO Unit × Task (Lean.MetaM α))
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.sub_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f g : ZeroAtInftyContinuousMap α β), (f - g) x = f x - g x
-- Lean.Parser.Term
/-- Specify a termination measure for recursive functions.
```
termination_by a - b
```
indicates that termination of the currently defined recursive function follows
because the difference between the arguments `a` and `b` decreases.

If the function takes further argument after the colon, you can name them as follows:
```
def example (a : Nat) : Nat → Nat → Nat :=
termination_by b c => a - b
```

By default, a `termination_by` clause will cause the function to be constructed using well-founded
recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
indicates the function is expected to be structural recursive on the argument. In this case
the body of the `termination_by` clause must be one of the function's parameters.

If omitted, a termination measure will be inferred. If written as `termination_by?`,
the inferred termination measure will be suggested.

 -/
Lean.Parser.Termination.terminationBy : Lean.Parser.Parser
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- The additive subgroup generated by an element of an additive group equals the set
of integer multiples of the element, such that each multiple is a unique element.
This is the stronger version of `AddSubgroup.mem_closure_singleton`.  -/
AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G},
  a ≠ 0 → (b ∈ AddSubgroup.closure {a} ↔ ∃! k, k • a = b)
-- Mathlib.Analysis.Complex.AbelLimit
Complex.nhdsWithin_lt_le_nhdsWithin_stolzSet : ∀ {M : ℝ}, 1 < M → Filter.map Complex.ofReal (nhdsWithin 1 (Set.Iio 1)) ≤ nhdsWithin 1 (Complex.stolzSet M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.flip_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g), t.flip.inr = t.inl
-- Init.Data.SInt.Lemmas
instLawfulCommIdentityInt32HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get_push_ref_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (s : aig.RefVec len)
  (ref : aig.Ref), (s.push ref).get len ⋯ = ref
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId_add'_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] {X : C} (m n p m' n' p' : A) (hm : m' + m = 0) (hn : n' + n = 0)
  (hp : p' + p = 0) (h : m + n = p),
  (CategoryTheory.shiftFunctorCompIsoId C p' p hp).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' C n' m' p' ⋯).hom.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctorAdd' C m n p h).hom.app
          ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C n').obj X)))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C n).map
            ((CategoryTheory.shiftFunctorCompIsoId C m' m hm).hom.app ((CategoryTheory.shiftFunctor C n').obj X)))
          ((CategoryTheory.shiftFunctorCompIsoId C n' n hn).hom.app X)))
-- Mathlib.Algebra.Homology.Linear
HomologicalComplex.instModuleHom : {R : Type u_1} →
  [inst : Semiring R] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] →
            {ι : Type u_4} → {c : ComplexShape ι} → (X Y : HomologicalComplex C c) → Module R (X ⟶ Y)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts**. Special case of
`intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right`
where the functions have a one-sided derivative at the endpoints.  -/
intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  (∀ x ∈ Set.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) →
      IntervalIntegrable u' MeasureTheory.volume a b →
        IntervalIntegrable v' MeasureTheory.volume a b →
          ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.opcycles.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S S_1 : CategoryTheory.ShortComplex C) (e_S : S = S_1) [inst_2 : S.HasRightHomology], S.opcycles = S_1.opcycles
-- Batteries.Data.String.Lemmas
String.Pos.Raw.modify.eq_1 : ∀ (s : String) (i : String.Pos.Raw) (f : Char → Char),
  String.Pos.Raw.modify s i f = String.Pos.Raw.set s i (f (String.Pos.Raw.get s i))
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- Given complementary embeddings of complex shapes
`e₁ : Embedding c₁ c` and `e₂ : Embedding c₂ c`, this is
the obvious bijection `ι₁ ⊕ ι₂ ≃ ι` from the sum of the index
types of `c₁` and `c₂` to the index type of `c`.  -/
ComplexShape.Embedding.AreComplementary.equiv : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} → {e₁ : c₁.Embedding c} → {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → ι₁ ⊕ ι₂ ≃ ι
-- Init.Data.UInt.Basic
/-- Negation of 16-bit unsigned integers, computed modulo `UInt16.size`.

`UInt16.neg a` is equivalent to `65_535 - a + 1`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.neg : UInt16 → UInt16
-- Mathlib.FieldTheory.MvRatFunc.Rank
MvRatFunc.rank_eq_max_lift : ∀ {σ : Type u} {F : Type v} [inst : Field F] [Nonempty σ],
  Module.rank F (FractionRing (MvPolynomial σ F)) =
    max (max (Cardinal.lift.{u, v} (Cardinal.mk F)) (Cardinal.lift.{v, u} (Cardinal.mk σ))) Cardinal.aleph0
-- Init.Data.UInt.Bitwise
UInt16.and_le_left : ∀ {a b : UInt16}, a &&& b ≤ a
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_sUnion_iff_of_countable : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {s : Set (Set α)},
  Order.cof α ≠ Cardinal.aleph0 → s.Countable → (IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x)
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.toAlgHom_convOne : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C], WithConv.toConv ↑(WithConv.ofConv 1) = 1
-- Mathlib.Analysis.RCLike.Basic
/-- The norm squared function.  -/
RCLike.normSq : {K : Type u_1} → [inst : RCLike K] → K →*₀ ℝ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f},
  (m.modify k f)[k'] = if heq : (k == k') = true then f m[k] else m[k']
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.ofNat.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.contract.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) (f : Polynomial R),
  Polynomial.contract p f = ∑ n ∈ Finset.range (f.natDegree + 1), (Polynomial.monomial n) (f.coeff (n * p))
-- Init.Core
Sep.mk : {α : outParam (Type u)} → {γ : Type v} → ((α → Prop) → γ → γ) → Sep α γ
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The monoidal opposite of a morphism `f : X ⟶ Y` is just `f`, thought of as `mop X ⟶ mop Y`.  -/
Quiver.Hom.mop : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → ({ unmop := X } ⟶ { unmop := Y })
-- Lean.Environment
_private.Lean.Environment.0.Lean.saveModuleDataParts.unsafe_impl_2 : Lean.Name → Option Lean.Compactor → System.FilePath → Lean.ModuleData → IO Lean.Compactor
-- Mathlib.Topology.FiberBundle.Trivialization
/-- For fixed `v ∈ F`, `x ↦ e.symm (x,v)` is continuous at any point in the base set.  -/
Bundle.Trivialization.continuousAt_symm_prodMk_left : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} {v : F},
  b ∈ e.baseSet → ContinuousAt (fun x => ↑e.symm (x, v)) b
-- Mathlib.GroupTheory.Subgroup.Simple
/-- An `AddGroup` is simple when it has exactly two normal `AddSubgroup`s.  -/
IsSimpleAddGroup : (A : Type u_2) → [AddGroup A] → Prop
-- Init.Data.Int.DivMod.Lemmas
Int.emod.eq_2 : ∀ (x : ℤ) (m : ℕ), (Int.negSucc m).emod x = Int.subNatNat x.natAbs (m % x.natAbs).succ
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addZeroClass.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M),
  c.addZeroClass = { toZero := c.zero, toAdd := c.hasAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimit : ∀ {C : Type u_1} {D : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} J]
  (K : CategoryTheory.Functor J C) {L L' : CategoryTheory.Functor C D} (α : L ⟶ L')
  [CategoryTheory.IsIso (K.whiskerLeft α)] (c : CategoryTheory.Limits.Cocone K) (hc : CategoryTheory.Limits.IsColimit c)
  [CategoryTheory.Limits.PreservesColimit K L] [CategoryTheory.Limits.PreservesColimit K L'],
  CategoryTheory.IsIso (α.app c.pt)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof : Type
-- Mathlib.Order.WellQuasiOrder
OrderIso.wellQuasiOrderedLE_iff : ∀ {α : Type u_3} {β : Type u_4} [inst : LE α] [inst_1 : LE β] (f : α ≃o β), WellQuasiOrderedLE α ↔ WellQuasiOrderedLE β
-- Lean.Meta.Tactic.Simp.Arith.Nat.Simp
Lean.Meta.Simp.Arith.Nat.simpCnstrPos? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.disjoint_verts_iff_disjoint : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph}, Disjoint H.verts H'.verts ↔ Disjoint H H'
-- Lean.DocString.Types
Lean.Doc.Part.mk : {i : Type u} →
  {b : Type v} →
    {p : Type w} →
      Array (Lean.Doc.Inline i) →
        String → Option p → Array (Lean.Doc.Block i b) → Array (Lean.Doc.Part i b p) → Lean.Doc.Part i b p
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct a morphism `AddGrp.mk G ⟶ AddGrp.mk H` from a  map `f : G ⟶ H` and a `IsAddMonHom f`
instance.  -/
CategoryTheory.AddGrp.ofHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A B : C} →
        [inst_2 : CategoryTheory.AddGrpObj A] →
          [inst_3 : CategoryTheory.AddGrpObj B] →
            (f : A ⟶ B) → [CategoryTheory.IsAddMonHom f] → { X := A, addGrp := inst_2 } ⟶ { X := B, addGrp := inst_3 }
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instPreservesZeroMorphismsEval : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι),
  (HomologicalComplex.eval V c i).PreservesZeroMorphisms