mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.minKey? = some k ↔
    (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Ideal.ResidueField.liftₐ.congr_simp : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal A) [inst_5 : I.IsPrime] (f f_1 : A →ₐ[R] B) (e_f : f = f_1)
  (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)),
  Ideal.ResidueField.liftₐ I f hf₁ hf₂ = Ideal.ResidueField.liftₐ I f_1 ⋯ ⋯
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (toFun : G → E) (rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom)
  (toFun_1 : G → E) (rightInverse_rightHom_1 : Function.RightInverse toFun_1 ⇑S.rightHom),
  ({ toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } =
      { toFun := toFun_1, rightInverse_rightHom := rightInverse_rightHom_1 }) =
    (toFun = toFun_1)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- An element of the comma category `Comma (Functor.const C) (𝟭 (C ⥤ D))` can be seen as a
functor `WithInitial C ⥤ D`.  -/
CategoryTheory.WithInitial.ofCommaObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) →
          CategoryTheory.Functor (CategoryTheory.WithInitial C) D
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Server.registerStatefulLspRequestHandler : String →
  Lean.Server.RequestHandlerCompleteness →
    (paramType : Type) →
      [Lean.FromJson paramType] →
        [Lean.Lsp.FileSource paramType] →
          (respType : Type) →
            [Lean.ToJson respType] →
              (stateType : Type) →
                [TypeName stateType] →
                  stateType →
                    (paramType → stateType → Lean.Server.RequestM (Lean.Server.LspResponse respType × stateType)) →
                      (Lean.Lsp.DidChangeTextDocumentParams → StateT stateType Lean.Server.RequestM Unit) → IO Unit
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.beq_not_ite' : ∀ {w : ℕ} {a b : BitVec (w + 1)} {c : Bool}, (a == ~~~bif c then b else a) = (c && a == ~~~b)
-- Batteries.Data.DList.Basic
/-- Convert a lazily-evaluated `List` to a `DList`  -/
Batteries.DList.ofThunk : {α : Type u} → Thunk (List α) → Batteries.DList α
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverWs : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Counters.mk.injEq : ∀ (thm : Lean.PHashMap Lean.Meta.Grind.Origin ℕ) (fvarUserNames : Lean.PHashMap Lean.FVarId Lean.Name)
  (case apps : Lean.PHashMap Lean.Name ℕ) (thm_1 : Lean.PHashMap Lean.Meta.Grind.Origin ℕ)
  (fvarUserNames_1 : Lean.PHashMap Lean.FVarId Lean.Name) (case_1 apps_1 : Lean.PHashMap Lean.Name ℕ),
  ({ thm := thm, fvarUserNames := fvarUserNames, case := case, apps := apps } =
      { thm := thm_1, fvarUserNames := fvarUserNames_1, case := case_1, apps := apps_1 }) =
    (thm = thm_1 ∧ fvarUserNames = fvarUserNames_1 ∧ case = case_1 ∧ apps = apps_1)
-- Mathlib.Data.Set.Semiring
SetSemiring.instNonUnitalSemiringOfSemigroup : {α : Type u_1} → [Semigroup α] → NonUnitalSemiring (SetSemiring α)
-- Mathlib.ModelTheory.Algebra.Field.CharP
FirstOrder.Field.charP_of_model_fieldOfChar : ∀ (p : ℕ) (K : Type u_1) [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K]
  [h : K ⊨ FirstOrder.Language.Theory.fieldOfChar p], CharP K p
-- Init.Data.BitVec.Lemmas
BitVec.getElem_eq_iff : ∀ {w : ℕ} {x : Bool} {l : BitVec w} {n : ℕ} {h : n < w}, l[n] = x ↔ l[n]? = some x
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrRight_apply_fst : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : α₁ × β₁),
  ((Equiv.prodCongrRight e) ab).1 = ab.1
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- The inclusion functor from open neighbourhoods of `x`
to open sets in the ambient topological space.  -/
TopologicalSpace.OpenNhds.inclusion : {X : TopCat} → (x : ↑X) → CategoryTheory.Functor (TopologicalSpace.OpenNhds x) (TopologicalSpace.Opens ↑X)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.apply_symm_apply' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {b : B} {x : F}, b ∈ e.baseSet → ↑e (↑e.symm (b, x)) = (b, x)
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabCoeSortNotation : Lean.Elab.Term.TermElab
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance1.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : α) →
        (x_2 : RBTree.RBNode α) →
          ((a : RBTree.RBNode α) →
              (x : α) →
                (b : RBTree.RBNode α) →
                  (y : α) →
                    (c : RBTree.RBNode α) →
                      (z : α) →
                        (d : RBTree.RBNode α) →
                          motive
                            (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z
                            d) →
            ((a : RBTree.RBNode α) →
                (x : α) →
                  (b : RBTree.RBNode α) →
                    (y : α) →
                      (c : RBTree.RBNode α) →
                        (z : α) →
                          (d : RBTree.RBNode α) →
                            (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                                a = RBTree.RBNode.node RBTree.RBColor.red a_1 x b → False) →
                              motive
                                (RBTree.RBNode.node RBTree.RBColor.red a x
                                  (RBTree.RBNode.node RBTree.RBColor.red b y c))
                                z d) →
              ((a : RBTree.RBNode α) →
                  (x : α) →
                    (b : RBTree.RBNode α) →
                      (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
                          a =
                              RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a_1 x b) y
                                c →
                            False) →
                        (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
                            a =
                                RBTree.RBNode.node RBTree.RBColor.red a_1 x
                                  (RBTree.RBNode.node RBTree.RBColor.red b y c) →
                              False) →
                          motive a x b) →
                motive x x_1 x_2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.WorkspaceSymbolParams.query : Lean.Lsp.WorkspaceSymbolParams → String
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.Equiv.age_eq_age : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {N : Type w} [inst_1 : L.Structure N]
  (MN : L.Equiv M N), L.age M = L.age N
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubsemiring.unitization_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : SetLike S R] [hSR : NonUnitalSubsemiringClass S R] (s : S)
  (x : Unitization ℕ ↥s), (NonUnitalSubsemiring.unitization s) x = ↑x.toProd.1 + ↑x.toProd.2
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent_mem : ∀ {A : Type u_1} (M : Type u_2) [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M] [inst_2 : Module A M]
  (x : M), x ∈ Ideal.primaryComponent M I ↔ ∃ n, x ∈ Submodule.torsionBySet A M ↑(I ^ n)
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCurry_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type u_4} {κ : ι → Type u_5} (α : (i : ι) → κ i → Type u_6)
  [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (α i k)] [inst_2 : (i : ι) → (k : κ i) → Module R (α i k)]
  (f : (x : (i : ι) × κ i) → α x.fst x.snd), (LinearEquiv.piCurry R α) f = Sigma.curry f
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- Given the set `i`, `restrictNonposSeq s i` is the sequence of sets defined inductively where
`restrictNonposSeq s i 0 = someExistsOneDivLT s (i \ ∅)` and
`restrictNonposSeq s i (n + 1) = someExistsOneDivLT s (i \ ⋃ k ≤ n, restrictNonposSeq k)`.

For each `n : ℕ`,`s (restrictNonposSeq s i n)` is close to maximal among all subsets of
`i \ ⋃ k ≤ n, restrictNonposSeq s i k`.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → Set α → ℕ → Set α
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.isRef : Lean.IR.CtorInfo → Bool
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.match_1.eq_3 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 :
    ByteArray.utf8DecodeChar?.FirstByte.oneMore = ByteArray.utf8DecodeChar?.FirstByte.invalid →
      motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 :
    ByteArray.utf8DecodeChar?.FirstByte.oneMore = ByteArray.utf8DecodeChar?.FirstByte.done →
      motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 :
    ByteArray.utf8DecodeChar?.FirstByte.oneMore = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 :
    ByteArray.utf8DecodeChar?.FirstByte.oneMore = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 :
    ByteArray.utf8DecodeChar?.FirstByte.oneMore = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match h : ByteArray.utf8DecodeChar?.FirstByte.oneMore with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) =
    h_3 ⋯
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusMap_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (γ : Q ⟶ R) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.plusObj R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.plusMap (CategoryTheory.CategoryStruct.comp η γ)) h =
    CategoryTheory.CategoryStruct.comp (J.plusMap η) (CategoryTheory.CategoryStruct.comp (J.plusMap γ) h)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, Std.DTreeMap.Const.get (t₁ ∪ t₂) k h' = Std.DTreeMap.Const.get t₁ k ⋯
-- Mathlib.Tactic.DuplicateDecls
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.instLEModuleKey : LE Mathlib.Tactic.DuplicateDecls.ModuleKey✝
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.ofAddDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddGroup E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 0 x)
  (h₂ : ∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y),
  NormedAddGroup.ofAddDist' h₁ h₂ =
    { toNorm := (SeminormedAddGroup.ofAddDist' h₁ h₂).toNorm,
      toAddGroup := (SeminormedAddGroup.ofAddDist' h₁ h₂).toAddGroup,
      toPseudoMetricSpace := (SeminormedAddGroup.ofAddDist' h₁ h₂).toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯,
      dist_eq := ⋯ }
-- Mathlib.Computability.EpsilonNFA
εNFA.mem_stepSet_iff : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} {s : σ} {a : α},
  s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_add : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s₁ s₂ : Multiset α), (s₁ + s₂).inf = s₁.inf ⊓ s₂.inf
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_of_last : ∀ {n : ℕ} {i j : Fin n}, i ≤ j → ∀ [NeZero n], (i.cycleIcc j) j = i
-- Mathlib.Combinatorics.Schnirelmann
_private.Mathlib.Combinatorics.Schnirelmann.0.add_eq_univ_of_one_le_schirelmannDensity_add_schnirelmannDensity.match_1_1.eq_2 : ∀ (motive : ℕ ⊕ ℕ → Sort u_1) (y : ℕ) (h_1 : (x : ℕ) → motive (Sum.inl x)) (h_2 : (y : ℕ) → motive (Sum.inr y)),
  (match Sum.inr y with
    | Sum.inl x => h_1 x
    | Sum.inr y => h_2 y) =
    h_2 y
-- Init.Data.SInt.Bitwise
Int8.toInt16_or : ∀ (a b : Int8), (a ||| b).toInt16 = a.toInt16 ||| b.toInt16
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_nsmul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddMonoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G] (f : ContMDiffMap I I' N G n) (n_1 : ℕ), ⇑(n_1 • f) = n_1 • ⇑f
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- The underlying function `ℍ → ℂ`.

Do NOT use directly. Use the coercion instead.  -/
SlashInvariantForm.toFun : {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} → {k : outParam ℤ} → SlashInvariantForm Γ k → UpperHalfPlane → ℂ
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieAlgebra.ext : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : RightPreLieRing L} {x y : RightPreLieAlgebra R L},
  SMul.smul = SMul.smul → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.left =
    CategoryTheory.Iso.refl (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.left)
-- Init.Data.String.Basic
/-- The slice from `p` (inclusive) up to the end of `s`.  -/
String.sliceFrom : (s : String) → s.Pos → String.Slice
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- Recursion principle for `Additive`, supported by `cases` and `induction`.  -/
Additive.rec : {α : Type u} → {motive : Additive α → Sort u_1} → ((a : α) → motive (Additive.ofMul a)) → (a : Additive α) → motive a
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.below.singleton : ∀ {motive : (m : ℕ) → (L : List ℕ) → SimplexCategoryGenRel.IsAdmissible m L → Prop} {m a : ℕ} (ha : a ≤ m),
  SimplexCategoryGenRel.IsAdmissible.below ⋯
-- Mathlib.GroupTheory.Generators
/-- If `G` has a finite generating family, then `G` is finitely generated.  -/
Group.Generators.fg : ∀ {G : Type u_1} {ι : Type u_3} [inst : Group G] [Finite ι] (P : Group.Generators G ι), Group.FG G
-- Mathlib.Data.Prod.Lex
Prod.Lex.covBy_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : Lex (α × β)},
  a ⋖ b ↔
    (ofLex a).1 = (ofLex b).1 ∧ (ofLex a).2 ⋖ (ofLex b).2 ∨
      (ofLex a).1 ⋖ (ofLex b).1 ∧ IsMax (ofLex a).2 ∧ IsMin (ofLex b).2
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Algebra.Ring.Ext
NonUnitalCommSemiring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalCommSemiring R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_eq_one_iff_free : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M], CommRing.Pic.mk R M = 1 ↔ Module.Free R M
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instSMul : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → SMul α (UpperSet α)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A right homology map data for a morphism of short complexes in the opposite category
induces a left homology map data in the original category.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.RightHomologyData} →
            {h₂ : S₂.RightHomologyData} →
              CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.ShortComplex.unopMap φ) h₂.unop h₁.unop
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_smul : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {R : Type u_5}
  [inst_2 : MonoidWithZero R] [inst_3 : DistribMulAction R V₂] [inst_4 : PseudoMetricSpace R]
  [inst_5 : IsBoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂), ⇑(r • f) = r • ⇑f
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.instInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} → {U : I → C} → Inv (CategoryTheory.PresheafOfGroups.OneCochain G U)
-- Init.Data.Nat.MinMax
Nat.max_le_of_le_of_le : ∀ {a b c : ℕ}, a ≤ c → b ≤ c → max a b ≤ c
-- Mathlib.Analysis.Real.Sqrt
Real.strictMonoOn_sqrt : StrictMonoOn Real.sqrt (Set.Ici 0)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates limits, then `F : Cᵒᵖ ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.covariance_fun_eval : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ (s t : NNReal), ProbabilityTheory.covariance (fun ω => B s ω) (fun ω => B t ω) P = ↑(min s t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd W Y) g')
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst W Y) g))
      h =
    CategoryTheory.CategoryStruct.comp (β_ W Y).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g' g) h)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_map : ∀ {α : Type u} {β : Type v} {s : Stream'.Seq α} {f : α → β}, (Stream'.Seq.map f s).length' = s.length'
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.mk.injEq : ∀ (env : Lean.Environment) (options : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl)
  (env_1 : Lean.Environment) (options_1 : Lean.Options) (currNamespace_1 : Lean.Name)
  (openDecls_1 : List Lean.OpenDecl),
  ({ env := env, options := options, currNamespace := currNamespace, openDecls := openDecls } =
      { env := env_1, options := options_1, currNamespace := currNamespace_1, openDecls := openDecls_1 }) =
    (env = env_1 ∧ options = options_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Neg α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s : Finset α) (f : α → β), (-s).inf f = s.inf fun x => f (-x)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero : ∀ (R θ : ℝ), circleMap 0 R θ = ↑R * Complex.exp (↑θ * Complex.I)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Coercion to a function as a `LinearMap`.  -/
ContinuousMap.coeFnLinearMap : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    (R : Type u_3) →
      {M : Type u_5} →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : Semiring R] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : ContinuousAdd M] →
                [inst_5 : Module R M] → [inst_6 : ContinuousConstSMul R M] → C(α, M) →ₗ[R] α → M
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Iterators.Types.FilterMap.instIterator.match_1.splitter : {β γ : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (Option γ)} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property none) → motive ⟨none, h'⟩) →
              ((out' : γ) → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩) → motive __do_lift
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsLe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (t.le n).IsClosedUnderIsomorphisms
-- Aesop.BuiltinRules.Subst
Aesop.BuiltinRules.subst : Aesop.RuleTac
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHomMonomial_add : ∀ {σ : Type u_1} {R : Type u_3} {n : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] {r : R} {t s : Fin n →₀ ℕ},
  MvPolynomial.esymmAlgHomMonomial σ (t + s) r =
    MvPolynomial.esymmAlgHomMonomial σ t r * MvPolynomial.esymmAlgHomMonomial σ s 1
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_row : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α), (Matrix.of f).row = f
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instAdditivePullback : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (AlgebraicGeometry.Scheme.Modules.pullback f).Additive