mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.insertMany t l) k fallback =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if cmp a k = Ordering.eq then some b else none)
              l).getD
          (Std.DTreeMap.Raw.Const.getD t k fallback)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence f ↔ HomotopicalAlgebra.WeakEquivalence f.hom
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.algebraMap_mem_iff : ∀ (S : Type u_3) {R : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [inst_7 : Module R A]
  [IsScalarTower R S A] {a : A} {r : R}, (algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a
-- Std.Do.WP.Monad
Std.Do.WPMonad.mk : {m : Type u → Type v} →
  {ps : outParam Std.Do.PostShape} →
    [inst : Monad m] →
      [toLawfulMonad : LawfulMonad m] →
        [toWP : Std.Do.WP m ps] →
          (∀ {α : Type u} (a : α), Std.Do.wp (pure a) = pure a) →
            (∀ {α β : Type u} (x : m α) (f : α → m β),
                (Std.Do.wp do
                    let a ← x
                    f a) =
                  do
                  let a ← Std.Do.wp x
                  Std.Do.wp (f a)) →
              Std.Do.WPMonad m ps
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.cons_zero_zero : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α], Matrix.vecCons 0 0 = 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → Inhabited (CategoryTheory.AddMon C)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.toFunctor_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (F : CategoryTheory.StrictPseudofunctor B C) {X Y : B} (a : X ⟶ Y), F.toFunctor.map a = F.map a
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
/-- `BoxIntegral.Box.splitCenterBox` bundled as a `Function.Embedding`.  -/
BoxIntegral.Box.splitCenterBoxEmb : {ι : Type u_1} → BoxIntegral.Box ι → Set ι ↪ BoxIntegral.Box ι
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Option.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match none, none with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_1 ()
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.Equiv.rfl : ∀ {self : Batteries.UnionFind} {a : ℕ}, self.Equiv a a
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.setIntegral_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} {μ : MeasureTheory.Measure β}
  {s : Set β}, ∫ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β) in s, f x ∂μ
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_iSup_comap_of_surjective : ∀ {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)
  [inst_3 : RingHomClass F R S] {ι : Sort u_3},
  Function.Surjective ⇑f → ∀ (K : ι → Ideal S), Ideal.map f (⨆ i, Ideal.comap f (K i)) = iSup K
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑Y.toTopCat),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) =
    Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.comap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsAddMonHom f],
  CategoryTheory.AddMod.comap f =
    { obj := fun M => { X := M.X, addMod := CategoryTheory.AddMod.scalarRestriction f M.X },
      map := fun {M N} g => { hom := g.hom, isAddModHom := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Right.pos_add_of_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [IsBotZeroClass α] [AddRightStrictMono α] {a : α},
  0 < a → ∀ (b : α), 0 < a + b
-- Std.Do.Triple.SpecLemmas
List.Cursor.mk : {α : Type u} → {l : List α} → («prefix» suffix : List α) → «prefix» ++ suffix = l → l.Cursor
-- Mathlib.Data.Nat.Bits
Nat.bit_add : ∀ (b : Bool) (n m : ℕ), Nat.bit b (n + m) = Nat.bit false n + Nat.bit b m
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_bijective : Function.Bijective ENNReal.log
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNat_ratCast : ∀ {R : Type u_1} [inst : DivisionRing R] {q : ℚ} {n : ℕ},
  Mathlib.Meta.NormNum.IsNat q n → Mathlib.Meta.NormNum.IsNat (↑q) n
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.mem_subsetSum_iff : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M} {a : M},
  a ∈ A.subsetSum ↔ ∃ B ⊆ A, ∑ b ∈ B, b = a
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology : ∀ {X : LightProfinite}, TotallyDisconnectedSpace ↑X.toTop
-- Mathlib.Data.Ordmap.Ordset
/-- O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, the set is returned as is.  -/
Ordset.insert' : {α : Type u_1} → [inst : Preorder α] → [Std.Total fun x1 x2 => x1 ≤ x2] → [DecidableLE α] → α → Ordset α → Ordset α
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.ι_mapBifunctorMapMap_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : CategoryTheory.GradedObject J C₂}
  (g : Y₁ ⟶ Y₂) [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
  [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (i : I) (j : J) (k : K)
  (h : p (i, j) = k) {Z : C₃} (h_1 : CategoryTheory.GradedObject.mapBifunctorMapObj F p X₂ Y₂ k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j))
      (CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h) h_1))
-- Mathlib.Order.Hom.Basic
OrderIso.symm_refl : ∀ (α : Type u_6) [inst : LE α], (OrderIso.refl α).symm = OrderIso.refl α
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.locallyCoverDense_of_isCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.IsLocallyFull K] [G.IsCoverDense K], G.LocallyCoverDense K
-- Mathlib.SetTheory.Cardinal.NatCard
/-- If `f` is surjective, then `Nat.card β ≤ Nat.card α`. We must also assume
`Nat.card α = 0 → Nat.card β = 0` since `Nat.card` is defined to be `0` for infinite types.  -/
Finite.card_le_of_surjective' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Surjective f → (Nat.card α = 0 → Nat.card β = 0) → Nat.card β ≤ Nat.card α
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_product_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : One β], 1 ×ˢ 1 = 1
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_map : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₂ X₂' : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) (g' : R.obj X₂' ⟶ B.obj X₃) (γ : X₂' ⟶ X₂)
  (hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g') {A A' : w.CostructuredArrowDownwards g} (φ : A ⟶ A'),
  (w.costructuredArrowDownwardsPrecomp g g' γ hγ).map φ =
    CategoryTheory.CostructuredArrow.homMk
      (CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right φ.left) ⋯) ⋯
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.mapCoeffs.congr_simp : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b b_1 : Module.Basis ι R M),
  b = b_1 →
    ∀ {R' : Type u_13} [inst_3 : Semiring R'] [inst_4 : Module R' M] (f f_1 : R ≃+* R') (e_f : f = f_1)
      (h : ∀ (c : R) (x : M), f c • x = c • x), b.mapCoeffs f h = b_1.mapCoeffs f_1 ⋯
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.comp_id : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : U ⥤q V), F ⋙q 𝟭q V = F
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Specialization of `Finset.sum_nbij'` that automatically fills in most arguments.

See `Fintype.sum_equiv` for the version where `s` and `t` are `univ`.  -/
Finset.sum_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (e : ι ≃ κ), (∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → ∑ i ∈ s, f i = ∑ i ∈ t, g i
-- Mathlib.RingTheory.Noetherian.Basic
/-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules.  -/
IsNoetherian.induction : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  {P : Submodule R M → Prop}, (∀ (I : Submodule R M), (∀ J > I, P J) → P I) → ∀ (I : Submodule R M), P I
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.minKey?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMultispan.functorExt.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MultispanShape} (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) (i : J.R)
  (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right i)),
  (match CategoryTheory.Limits.WalkingMultispan.right i with
    | CategoryTheory.Limits.WalkingMultispan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMultispan.right i => h_2 i) =
    h_2 i
-- Init.Data.Iterators.Consumers.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.Iter.length : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → ℕ
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.graphRel.adj : FirstOrder.Language.graphRel 2
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {Q : Type u_4} [inst_3 : CommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T),
  (f.mulEquivOfMulEquiv k H).toMonoidHom = f.map ⋯ k
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ GrpCat MonCat)
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.quotNilradicalPowEquivPi_symm_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsArtinianRing R] (n : ℕ)
  (a : (I : MaximalSpectrum R) → R ⧸ I.asIdeal ^ n),
  (IsArtinianRing.quotNilradicalPowEquivPi R n).symm a =
    (Ideal.quotientEquivAlgOfEq R ⋯) ((Ideal.quotientInfRingEquivPiQuotient (fun I => I.asIdeal ^ n) ⋯).symm a)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.equivQuotientZSMulOfEquiv_symm : ∀ {A B : Type u} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] (e : A ≃+ B) (n : ℤ),
  (QuotientAddGroup.equivQuotientZSMulOfEquiv e n).symm = QuotientAddGroup.equivQuotientZSMulOfEquiv e.symm n
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.finite_co_support_prod_smul : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  [inst_5 : VAdd Γ Γ'] [inst_6 : IsOrderedCancelVAdd Γ Γ'] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ' V β) (g : Γ'),
  Finite ↑{ab | ((fun ab => (HahnModule.of R).symm (s ab.1 • (HahnModule.of R) (t ab.2))) ab).coeff g ≠ 0}
-- Mathlib.Algebra.Order.SuccPred.PartialSups
/-- See `partialSups_succ` for another decomposition of `(partialSups f) (Order.succ i)`.  -/
partialSups_succ' : ∀ {ι : Type u_2} [inst : LinearOrder ι] {α : Type u_3} [inst_1 : SemilatticeSup α] [inst_2 : LocallyFiniteOrder ι]
  [inst_3 : SuccOrder ι] [inst_4 : OrderBot ι] (f : ι → α) (i : ι),
  (partialSups f) (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) i
-- Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
/-- Schur's Lemma: If `V` is a representation of an algebra `A` over an algebraically closed field
`k`, then any endomorphism of `V` is scalar.  -/
IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed : ∀ {A : Type u_1} {V : Type u_2} (k : Type u_3) [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : Module A V] [inst_6 : IsScalarTower k A V]
  [IsSimpleModule A V] [FiniteDimensional k V] [IsAlgClosed k], Function.Bijective ⇑(algebraMap k (Module.End A V))
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.epi_πQ : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
      {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
      CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        ∀ {K Q : A} {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q}
          {γ : ι.obj Q ⟶ (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))},
          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
            ∀ [inst_7 : ι.Full] [CategoryTheory.Preadditive A] [ι.Faithful],
              CategoryTheory.Epi (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (f : X ⟶ Y), HomotopicalAlgebra.RightHomotopyRel f f
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The equivalence relation on left fractions for a morphism property `W`.  -/
CategoryTheory.MorphismProperty.LeftFractionRel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction X Y → W.LeftFraction X Y → Prop
-- Mathlib.LinearAlgebra.AffineSpace.MidpointZero
pi_midpoint_apply : ∀ {k : Type u_1} {ι : Type u_2} {V : ι → Type u_3} {P : ι → Type u_4} [inst : Ring k] [inst_1 : Invertible 2]
  [inst_2 : (i : ι) → AddCommGroup (V i)] [inst_3 : (i : ι) → Module k (V i)] [inst_4 : (i : ι) → AddTorsor (V i) (P i)]
  (f g : (i : ι) → P i) (i : ι), midpoint k f g i = midpoint k (f i) (g i)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The underlying morphism  -/
CategoryTheory.Mon.Hom.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {M N : CategoryTheory.Mon C} → M.Hom N → (M.X ⟶ N.X)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.coe_toLocallyBoundedMap : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β}
  (hf : LipschitzWith K f), ⇑(LipschitzWith.toLocallyBoundedMap f hf) = f
-- Init.Data.BitVec.Basic
/-- Negation of bitvectors. This can be interpreted as either signed or unsigned negation modulo `2^n`.
Usually accessed via the `-` prefix operator.

SMT-LIB name: `bvneg`.
 -/
BitVec.neg : {n : ℕ} → BitVec n → BitVec n
-- Init.Data.Int.Order
Int.toNat.eq_1 : ∀ (n : ℕ), (Int.ofNat n).toNat = n
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_withDensity : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) (f : α → ENNReal),
  (ν.withDensity f).singularPart ν = 0
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- the apex of the span  -/
CategoryTheory.Span.apex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} → {c c' : C} → CategoryTheory.Span Wₗ Wᵣ c c' → C
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.toContDiffBump : {E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type uM} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] → {c : M} → SmoothBumpFunction I c → ContDiffBump (↑(extChartAt I c) c)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_restrict' : ∀ {α : Type u_1} (I E R : Set α), (Matroid.uniqueBaseOn I E).restrict R = Matroid.uniqueBaseOn (I ∩ R ∩ E) R
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.mem_corootSpace : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] [inst_4 : H.IsCartanSubalgebra] [inst_5 : IsNoetherian R L]
  (α : ↥H → R) {x : ↥H},
  x ∈ LieAlgebra.corootSpace α ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ LieAlgebra.rootSpace H α, ∃ z ∈ LieAlgebra.rootSpace H (-α), ⁅y, z⁆ = x}
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.one.injEq : ∀ (name name_1 : Lean.TSyntax `Lean.binderIdent),
  (Lean.Parser.Tactic.MCasesPat.one name = Lean.Parser.Tactic.MCasesPat.one name_1) = (name = name_1)
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.HoldsForLocalization.mk : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (∀ {R : Type u} [inst : CommRing R] (M : Submonoid R), P (algebraMap R (Localization M))) →
      RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => P
-- Lean.Expr
/-- The unique free variable identifier. It is just a hierarchical name,
but we wrap it in `FVarId` to make sure they don't get mixed up with `MVarId`.

This is not the user-facing name for a free variable. This information is stored
in the local context (`LocalContext`). The unique identifiers are generated using
a `NameGenerator`.
 -/
Lean.FVarId : Type
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- The space of coordinates for affine combinations indexed by a `Fintype`.  -/
fintypeAffineCoords : (ι : Type u_1) → (k : Type u_2) → [inst : Ring k] → [Fintype ι] → AffineSubspace k (ι → k)
-- Mathlib.Data.List.Cycle
Cycle.decidableNontrivialCoe.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x : List α),
  Cycle.decidableNontrivialCoe x =
    match x with
    | [] => isFalse ⋯
    | [x] => isFalse ⋯
    | x :: y :: l => if h : x = y then decidable_of_iff' (↑(x :: l)).Nontrivial ⋯ else isTrue ⋯
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.add : ∀ {X : Type u_1} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε''] [inst_3 : ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} [ContinuousAdd ε'']
  {f g : X → ε''},
  MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable g μ → MeasureTheory.LocallyIntegrable (f + g) μ
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_add : ∀ (m n : ℕ∞), ↑(m + n) = ↑m + ↑n
-- Mathlib.Algebra.Category.CoalgCat.Basic
CategoryTheory.Iso.toCoalgEquiv_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : CoalgCat R} (e : X ≅ Y), e.symm.toCoalgEquiv = e.toCoalgEquiv.symm
-- Mathlib.Geometry.Euclidean.Congruence
/-- **Side–Side–Side (SSS) congruence**
If all three corresponding sides of two triangles are equal, then the triangles are congruent.
This holds even if the triangles are degenerate.  -/
EuclideanGeometry.side_side_side : ∀ {P₁ : Type u_4} {P₂ : Type u_5} [inst : MetricSpace P₁] [inst_1 : MetricSpace P₂] {a b c : P₁} {a' b' c' : P₂},
  dist a b = dist a' b' → dist b c = dist b' c' → dist c a = dist c' a' → Congruent ![a, b, c] ![a', b', c']
-- Init.Data.Rat.Lemmas
Rat.maybeNormalize_eq : ∀ {num : ℤ} {den g : ℕ} (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0)
  (reduced : (num / ↑g).natAbs.Coprime (den / g)),
  Rat.maybeNormalize num den g dvd_num dvd_den den_nz reduced =
    { num := num.divExact (↑g) dvd_num, den := den / g, den_nz := den_nz, reduced := reduced }