mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SuccPred.Tree
/-- The coercion from a `SubRootedTree` to a `RootedTree`.
 -/
SubRootedTree.coeTree : {t : RootedTree} → SubRootedTree t → RootedTree
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.weakEqualizer.lift_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakEqualizer.lift k h)
      (CategoryTheory.Limits.weakEqualizer.ι f g) =
    k
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.precoverage.eq_1 : ∀ (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.ProEt.precoverage S =
    CategoryTheory.Precoverage.comap ((AlgebraicGeometry.Scheme.ProEt.forget S).comp (CategoryTheory.Over.forget S))
      AlgebraicGeometry.Scheme.proetalePrecoverage
-- Init.Data.List.Lemmas
List.mem_insert_of_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {l : List α}, a ∈ l → a ∈ List.insert b l
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right]
  (X :
    CategoryTheory.Limits.Cofork
      (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))
      (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))),
  (I.multicoforkEquivSigmaCofork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `α` is a preorder with bot, then `⊥` is an initial object.  -/
CategoryTheory.Limits.isInitialBot : {α : Type u_1} → [inst : Preorder α] → [inst_1 : OrderBot α] → CategoryTheory.Limits.IsInitial ⊥
-- Mathlib.Order.RelClasses
/-- **Alias** of `isTrans_ge`. -/
transitive_ge : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun a a_1 => a_1 ≤ a
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_symm_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_3} [inst_1 : Monoid N]
  (f : Monoid.CoprodI M →* N) (x : ι), Monoid.CoprodI.lift.symm f x = f.comp Monoid.CoprodI.of
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.hasLeftResolutions : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  [self : Φ.IsLeftDerivabilityStructure], Φ.HasLeftResolutions
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiable_smul_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜}
  {s : (x : B) → E x}, MDiff f → MDiff (T% s) → MDiff fun x => ⟨x, (f • s) x⟩
-- Mathlib.Tactic.NormNum.Ineq
/-- Helper function to synthesize typed `Semiring α` `PartialOrder α` `IsOrderedRing α`
expressions.  -/
Mathlib.Meta.NormNum.inferOrderedSemiring : {u : Lean.Level} →
  (α : Q(Type u)) → Lean.MetaM ((x : Q(Semiring «$α»)) × (x_1 : Q(PartialOrder «$α»)) × Q(IsOrderedRing «$α»))
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabWaitIfContainsMVar : Lean.Elab.Term.TermElab
-- Mathlib.NumberTheory.ModularForms.LFunction
/-- A `WeakFEPair` structure associated to a modular form.  -/
ModularForm.weakFEPair : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  [Γ.IsArithmetic] →
    {k : ℤ} → 0 < k → {F : Type u_1} → [inst : FunLike F UpperHalfPlane ℂ] → F → [ModularFormClass F Γ k] → WeakFEPair ℂ
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instMul : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} → [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → Mul (A →A[R] A)
-- Init.Data.Option.Lemmas
Option.isNone_pfilter_iff : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  (o.pfilter p).isNone = true ↔ ∀ (a : α) (ha : o = some a), p a ha = false
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- The reflection in `(𝕜 ∙ v)ᗮ` of `v` is `-v`.  -/
Submodule.reflection_orthogonalComplement_singleton_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v : E), (𝕜 ∙ v)ᗮ.reflection v = -v
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.instSubHomComma : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    [inst_1 : CategoryTheory.Preadditive A] →
      {B : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_3 : CategoryTheory.Preadditive B] →
            {T : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} T] →
                [inst_5 : CategoryTheory.Preadditive T] →
                  (L : CategoryTheory.Functor A T) →
                    [L.Additive] →
                      (R : CategoryTheory.Functor B T) → [R.Additive] → {u v : CategoryTheory.Comma L R} → Sub (u ⟶ v)
-- Init.Data.List.Attach
/-- Implementation of `pmap` using the zero-copy version of `attach`.  -/
List.pmapImpl : {α : Type u_1} → {β : Type u_2} → {P : α → Prop} → ((a : α) → P a → β) → (l : List α) → (∀ a ∈ l, P a) → List β
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.mk.inj : ∀ {oldInlayHints : Array Lean.Elab.InlayHintInfo} {oldFinishedSnaps : ℕ} {lastEditTimestamp? : Option ℕ}
  {isFirstRequestAfterEdit : Bool} {oldInlayHints_1 : Array Lean.Elab.InlayHintInfo} {oldFinishedSnaps_1 : ℕ}
  {lastEditTimestamp?_1 : Option ℕ} {isFirstRequestAfterEdit_1 : Bool},
  { oldInlayHints := oldInlayHints, oldFinishedSnaps := oldFinishedSnaps, lastEditTimestamp? := lastEditTimestamp?,
        isFirstRequestAfterEdit := isFirstRequestAfterEdit } =
      { oldInlayHints := oldInlayHints_1, oldFinishedSnaps := oldFinishedSnaps_1,
        lastEditTimestamp? := lastEditTimestamp?_1, isFirstRequestAfterEdit := isFirstRequestAfterEdit_1 } →
    oldInlayHints = oldInlayHints_1 ∧
      oldFinishedSnaps = oldFinishedSnaps_1 ∧
        lastEditTimestamp? = lastEditTimestamp?_1 ∧ isFirstRequestAfterEdit = isFirstRequestAfterEdit_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α}, (Std.TreeMap.unitOfList l cmp)[k]! = ()
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_one_fst_of_isMulCocycle₂ : ∀ {G : Type u_1} {M : Type u_2} [inst : Monoid G] [inst_1 : CommGroup M] [inst_2 : MulAction G M] {f : G × G → M},
  groupCohomology.IsMulCocycle₂ f → ∀ (g : G), f (1, g) = f (1, 1)
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_neg : ∀ {α : Type u_1} [inst : Neg α] (a : αˢʸᵐ), SymAlg.unsym (-a) = -SymAlg.unsym a
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.EvalTacticFailure.mk.inj : ∀ {exception : Lean.Exception} {state : Lean.Elab.Tactic.Grind.SavedState} {exception_1 : Lean.Exception}
  {state_1 : Lean.Elab.Tactic.Grind.SavedState},
  { exception := exception, state := state } = { exception := exception_1, state := state_1 } →
    exception = exception_1 ∧ state = state_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMinEntry_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {he : t₁.isEmpty = false} (h : t₁.Equiv t₂), Std.DTreeMap.Const.minEntry t₁ he = Std.DTreeMap.Const.minEntry t₂ ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.kind? : Lean.Lsp.ResolvableCompletionItem → Option Lean.Lsp.CompletionItemKind
-- Mathlib.Data.Set.Lattice
exists_sUnion : ∀ {α : Type u_1} {S : Set (Set α)} {p : α → Prop}, (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible derivative
at `a`, returns a function that is locally inverse to `f`.  -/
ContDiffAt.localInverse : {𝕂 : Type u_1} →
  [inst : RCLike 𝕂] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕂 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕂 F] →
                [CompleteSpace E] →
                  {f : E → F} →
                    {f' : E ≃L[𝕂] F} →
                      {a : E} → {n : WithTop ℕ∞} → ContDiffAt 𝕂 n f a → HasFDerivAt f (↑f') a → n ≠ 0 → F → E
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_comp_i_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k}
  (h : (groupHomology.shortComplexH2 B).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 B).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap₂ f φ) h)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {V W : QuadraticModuleCat R} → (V.form →qᵢ W.form) → V.Hom W
-- Mathlib.Data.Finset.Image
Function.Semiconj.finset_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β} {ga : α → α} {gb : β → β},
  Function.Semiconj f ga gb → Function.Semiconj (Finset.image f) (Finset.image ga) (Finset.image gb)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coneOfPreserves_pt_left : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R]
  (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R)))
  {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂),
  (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.left = c₁.pt
-- Mathlib.Data.Set.Prod
Set.univ_pi_eq_empty_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)}, Set.univ.pi t = ∅ ↔ ∃ i, t i = ∅
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_of_nonneg : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.abs_of_nonneg._auto_1 → CFC.abs a = a
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- The absolute value satisfies the triangle inequality.  -/
mabs_mul_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), |a * b|ₘ ≤ |a|ₘ * |b|ₘ
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_cons_of_le : ∀ {w n acc : ℕ} {x : BitVec w} {b : Bool}, n ≤ w → (BitVec.cons b x).cpopNatRec n acc = x.cpopNatRec n acc
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasUnifEigenvalue.pow : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.HasUnifEigenvalue μ 1 → ∀ (n : ℕ), (f ^ n).HasUnifEigenvalue (μ ^ n) 1
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {Fₗ Gₗ : CategoryTheory.Functor C E} (α : Fₗ ≅ Gₗ)
  (H : CategoryTheory.Functor D E'),
  (CategoryTheory.Join.mapIsoWhiskerRight α H).hom = CategoryTheory.Join.mapWhiskerRight α.hom H
-- Mathlib.Analysis.Normed.Group.Pointwise
infEDist_neg_neg : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (x : E) (s : Set E), Metric.infEDist (-x) (-s) = Metric.infEDist x s
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.preservesColimitsOfShape_rightFunc : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  [CategoryTheory.Limits.HasColimitsOfShape J T],
  CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Arrow.rightFunc
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_add : ∀ {a b : UInt16}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Init.Data.Vector.Lemmas
Vector.getElem?_reverse : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, i < n → xs.reverse[i]? = xs[n - 1 - i]?
-- Batteries.Data.Fin.Basic
/-- Inner loop for `Fin.dfoldrM`.
```
Fin.dfoldrM.loop n f i h xᵢ = do
  let xᵢ₋₁ ← f (i-1) xᵢ
  ...
  let x₁ ← f 1 x₂
  let x₀ ← f 0 x₁
  pure x₀
```
 -/
Fin.dfoldrM.loop : {m : Type u_1 → Type u_2} →
  [Monad m] →
    (n : ℕ) →
      (α : Fin (n + 1) → Type u_1) →
        ((i : Fin n) → α i.succ → m (α i.castSucc)) → (i : ℕ) → (h : i < n + 1) → α ⟨i, h⟩ → m (α 0)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.isClass : Lean.Elab.Command.InductiveView → Bool
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_univ₂_eventually₁ : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] [PreconnectedSpace X] {a : X} {l : Filter X} [l.NeBot] {f g : X → α},
  Continuous f → Continuous g → f a ≤ g a → g ≤ᶠ[l] f → ∃ x, f x = g x
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.uniformContinuous_sup : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous fun x => x.1 ⊔ x.2
-- Mathlib.CategoryTheory.Monoidal.Center
/-- A morphism in the Drinfeld center of `C`.  -/
CategoryTheory.Center.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Center C → CategoryTheory.Center C → Type v₁
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
Lean.Meta.RefinedDiscrTree.MatchResult.mk : {α : Type} → Std.TreeMap ℕ (Array (Array α)) compare → Lean.Meta.RefinedDiscrTree.MatchResult α
-- Mathlib.Probability.Distributions.Fernique
/-- A sequence of real thresholds that will be used to cut the space into annuli.
Chosen such that for a rotation invariant measure, an application of lemma
`measure_le_mul_measure_gt_le_of_map_rotation_eq_self` gives
`μ {x | ‖x‖ ≤ a} * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2`.  -/
ProbabilityTheory.Fernique.normThreshold : ℝ → ℕ → ℝ
-- Mathlib.Topology.Path
Path.continuousMapClass : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, ContinuousMapClass (Path x y) (↑unitInterval) X
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
CuspForm.discriminantEquiv_apply : ∀ {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (z : UpperHalfPlane),
  (CuspForm.discriminantEquiv f) z = f z / ModularForm.discriminant z
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangleMap_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂),
  (CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₂ = b
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_linearIsometryEquiv_conj_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ[𝕜] E}
  (f : E ≃ₗᵢ[𝕜] F), (↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv).IsPositive ↔ T.IsPositive
-- Mathlib.Data.Finset.Card
Finset.strongDownwardInduction_eq : ∀ {α : Type u_1} {n : ℕ} {p : Finset α → Sort u_4}
  (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Finset α),
  Finset.strongDownwardInduction H s = H s fun {t} ht x => Finset.strongDownwardInduction H t ht
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.domExtend_baseSet : ∀ {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] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Bundle.Trivialization F fun z => proj ↑z)
  [inst_3 : Nonempty (Z → F)], (Bundle.Trivialization.domExtend hps e).baseSet = e.toPretrivialization.baseSet
-- Mathlib.Data.W.Constructions
/-- The isomorphism from the naturals to its corresponding `WType`  -/
WType.ofNat : ℕ → WType WType.Natβ
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.indexEquivAllRoots_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [inst_6 : Finite ι] [inst_7 : CharZero R] [inst_8 : IsDomain R] [inst_9 : P.IsIrreducible]
  (x : ↥(RootPairing.EmbeddedG2.allRoots P).toFinset),
  (RootPairing.EmbeddedG2.indexEquivAllRoots P).symm x = Exists.choose ⋯
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.kerLiftAlg_mk : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (f : A →ₐ[R₁] B) (a : A),
  (Ideal.kerLiftAlg f) ((Ideal.Quotient.mk (RingHom.ker f)) a) = f a
-- Mathlib.Order.Category.DistLat
DistLat.hasForgetToLat : CategoryTheory.HasForget₂ DistLat Lat
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- If two affine maps agree on a set, their linear parts agree on the vector span of that set.  -/
AffineMap.linear_eqOn_vectorSpan : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] {V₂ : Type u_8} {P₂ : Type u_9} [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] {s : Set P₁} {f g : P₁ →ᵃ[k] P₂},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f.linear ⇑g.linear ↑(vectorSpan k s)
-- Mathlib.Data.Fin.Basic
Fin.exists_eq_add_of_lt : ∀ {n : ℕ} {a b : Fin (n + 1)}, a < b → ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ArbitraryShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.GroupTheory.Index
/-- Typeclass for a subgroup `H` to have finite index in a subgroup `K`.  -/
Subgroup.IsFiniteRelIndex : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G → Prop
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁.union s == s₂`  -/
Lean.Grind.AC.SubsetResult.strict : Lean.Grind.AC.Seq → Lean.Grind.AC.SubsetResult
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.toCommGroup.eq_1 : ∀ {G : Type u_3} [inst : CommGroup G] (H : Subgroup G), H.toCommGroup = SubgroupClass.toCommGroup H
-- Mathlib.Data.List.SplitBy
List.splitBy.loop.eq_def : ∀ {α : Type u} (R : α → α → Bool) (a : List α) (a_1 : α) (a_2 : List α) (a_3 : List (List α)),
  List.splitBy.loop R a a_1 a_2 a_3 =
    match a, a_1, a_2, a_3 with
    | a :: as, b, r, acc =>
      match R b a with
      | true => List.splitBy.loop R as a (b :: r) acc
      | false => List.splitBy.loop R as a [] ((b :: r).reverse :: acc)
    | [], ag, r, acc => ((ag :: r).reverse :: acc).reverse
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.associativity_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  (m₁ m₂ m₃ : M) (X : C) [inst_3 : F.LaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ m₂).app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
        ((F.map (CategoryTheory.MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
      ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
-- Mathlib.Logic.IsEmpty.Basic
not_isEmpty_of_nonempty : ∀ (α : Sort u_1) [h : Nonempty α], ¬IsEmpty α
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesColimit.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D},
  (∀ {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c),
      Nonempty (CategoryTheory.Limits.IsColimit (F.mapCocone c))) →
    CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.swap_compProd_posterior : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω],
  ((μ.bind ⇑κ).compProd (ProbabilityTheory.posterior κ μ)).bind ⇑(ProbabilityTheory.Kernel.swap 𝓧 Ω) = μ.compProd κ
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The functor taking a functor `Discrete α ⥤ C` to a functor `Finset (Discrete α) ⥤ C` by taking
coproducts.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (α : Type w) →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Discrete α) C)
          (CategoryTheory.Functor (Finset (CategoryTheory.Discrete α)) C)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constAddHom_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : Add β] (a : β) (a_1 : α), (Pi.constAddHom α β) a a_1 = Function.const α a a_1
-- Batteries.Data.MLList.Basic
/-- Lift the monad of a lazy list.  -/
MLList.liftM : {m n : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → [Monad n] → [MonadLiftT m n] → MLList m α → MLList n α