mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
SimpleGraph.IsExtremal.le_iff_eq : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {p : SimpleGraph V → Prop},
  G.IsExtremal p → ∀ {H : SimpleGraph V}, p H → (G ≤ H ↔ G = H)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesLimit.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} →
                [toReflectsLimit : CategoryTheory.Limits.ReflectsLimit K F] →
                  ((c : CategoryTheory.Limits.Cone (K.comp F)) →
                      CategoryTheory.Limits.IsLimit c → CategoryTheory.LiftableCone K F c) →
                    CategoryTheory.CreatesLimit K F
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.zsmul_neg' : ∀ {R : Type u} [self : AddGroupWithOne R] (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_add_right : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] (a b : E), dist b (b + a) = ‖a‖
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → ∀ {g : ↥(alternatingGroup α)}, (↑g).IsThreeCycle → g ∈ commutator ↥(alternatingGroup α)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_injective_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)),
  Function.Injective ⇑(IsLocalization.lift hg) ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ g x = g y
-- Mathlib.Algebra.Ring.Pi
RingHom.pi_apply : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [inst : (i : I) → NonAssocSemiring (f i)] [inst_1 : NonAssocSemiring γ]
  (g : (i : I) → γ →+* f i) (x : γ) (b : I), (RingHom.pi g) x b = (g b) x
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_div : ∀ (a b : BitVec 8), { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj],
  G.LocallyLinear → (G.cliqueFinset 3).card ≤ ruzsaSzemerediNumber α
-- Mathlib.Topology.Category.TopCat.OpenNhds
Topology.IsInducing.functorNhds_obj_coe : ∀ {X Y : TopCat} {f : X ⟶ Y} (h : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X)
  (U : TopologicalSpace.OpenNhds x), ↑((h.functorNhds x).obj U) = h.functor.obj ↑U
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.le_resLE_preimage_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (O : (↑U).Opens) (W : (↑V).Opens),
  W ≤ (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.resLE f U V e).base).obj O ↔
    (AlgebraicGeometry.Scheme.Hom.opensFunctor V.ι).obj W ≤
      (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj O)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instRegularSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [RegularSpace α], RegularSpace (TopologicalSpace.Compacts α)
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that
the product with `c` of (± `y`) (here taking the specified sign) is ± `c * y`.  -/
Mathlib.Tactic.FieldSimp.Sign.mulRight : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (c y : Q(«$M»)) →
        (g : Mathlib.Tactic.FieldSimp.Sign M) →
          Lean.MetaM
            (have a := g.expr y;
            have a_1 := g.expr q(«$c» * «$y»);
            Q(«$a_1» = «$c» * «$a»))
-- Mathlib.Data.Bool.Basic
Bool.and_eq_false_eq_eq_false_or_eq_false : ∀ (a b : Bool), ((a && b) = false) = (a = false ∨ b = false)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.self_le_normalizer_lowerCentralSeries : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) (n : ℕ), S ≤ AddSubgroup.normalizer ↑(S.lowerCentralSeries n)
-- Mathlib.Order.RelIso.Set
Subrel.instIrreflSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Irrefl r] (p : α → Prop), Std.Irrefl (Subrel r p)
-- Mathlib.SetTheory.Ordinal.Arithmetic
_private.Mathlib.SetTheory.Ordinal.Arithmetic.0.Ordinal.mul_eq_zero' : ∀ {a b : Ordinal.{u_4}}, a * b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.Analysis.Quaternion
Quaternion.instNormedDivisionRingReal : NormedDivisionRing (Quaternion ℝ)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_le_mul_iff_right₀`. -/
mul_le_mul_iff_of_pos_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulMono α] [PosMulReflectLE α],
  0 < a → (a * b ≤ a * c ↔ b ≤ c)
-- Mathlib.RingTheory.Smooth.Kaehler
Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Function.Bijective ⇑(Algebra.Extension.CotangentSpace.map P.toInfinitesimal)
-- Init.Prelude
instDecidableEqUSize : DecidableEq USize
-- Mathlib.Algebra.Order.GroupWithZero.Basic
neg_of_div_neg_left : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a b : G₀} [PosMulMono G₀],
  a / b < 0 → 0 ≤ b → a < 0
-- Mathlib.Data.Sym.Sym2
/-- Dependent recursion principle for `Sym2`. See `Quot.rec`.  -/
Sym2.rec : {α : Type u_1} →
  {motive : Sym2 α → Sort u_4} →
    (f : (a b : α) → motive s(a, b)) →
      (∀ (a b c d : α) (h : Sym2.Rel α (a, b) (c, d)), ⋯ ▸ f a b = f c d) → (z : Sym2 α) → motive z
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.mem_of_le : ∀ {α : Type u_1} {s : Set α} {a b : α} {P : α → Prop} [inst : LE α], IsRelLowerSet s P → a ∈ s → b ≤ a → P b → b ∈ s
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instExpr : List Lean.Name → List Lean.Level → Lean.Expr → Lean.Expr
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppLid.eq_1 : ∀ (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : Module R N],
  finsuppTensorFinsuppLid R N ι κ =
    (finsuppTensorFinsupp R R R N ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R N))
-- Mathlib.Logic.Function.Basic
Subtype.mk.hcongr_4 : ∀ (α α' : Sort u),
  α = α' →
    ∀ (p : α → Prop) (p' : α' → Prop),
      p ≍ p' →
        ∀ (val : α) (val' : α'),
          val ≍ val' →
            ∀ (property : p val) (property' : p' val'), property ≍ property' → ⟨val, property⟩ ≍ ⟨val', property'⟩
-- Mathlib.Data.Finset.Option
Finset.image_some_eraseNone : ∀ {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset (Option α)),
  Finset.image some (Finset.eraseNone s) = s.erase none
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmooth.comp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {T : Type u_1} [inst_2 : CommRing T] {g : S →+* T}
  {f : R →+* S}, g.IsStandardSmooth → f.IsStandardSmooth → (g.comp f).IsStandardSmooth
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans'_toPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z)
  (h : e.target = e'.source),
  (e.trans' e' h).toPartialHomeomorph =
    { toPartialEquiv := e.trans' e'.toPartialEquiv h, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0.Cfg.map.match_1.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {Λ : Type u_2} (motive : Turing.TM0.Cfg Γ Λ → Sort u_3) (q : Λ)
  (T : Turing.Tape Γ) (h_1 : (q : Λ) → (T : Turing.Tape Γ) → motive { q := q, Tape := T }),
  (match { q := q, Tape := T } with
    | { q := q, Tape := T } => h_1 q T) =
    h_1 q T
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.comp_sub_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) {Z : C} (h_1 : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g - h) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f h)
      h_1
-- Lean.Meta.LazyDiscrTree
/-- Values for matches ending at this trie.  -/
Lean.Meta.LazyDiscrTree.Trie.values : {α : Type} → Lean.Meta.LazyDiscrTree.Trie α → Array α
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
instDecidableEqOrderedFinpartition.decEq : {n : ℕ} → (x x_1 : OrderedFinpartition n) → Decidable (x = x_1)
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictSupport_nsmul : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] (n : ℕ) (s : Set (σ →₀ ℕ)),
  MvPolynomial.restrictSupport R (n • s) = MvPolynomial.restrictSupport R s ^ n
-- Mathlib.Data.LawfulXor.Basic
xor_right_involutive : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a : α), Function.Involutive fun x => a ^^^ x
-- Lean.Compiler.LCNF.Types
/-- Whether the type is an object which is to say a pointer or a value disguised as a pointer.
 -/
Lean.Compiler.LCNF.ImpureType.Lean.Expr.isObj : Lean.Expr → Bool
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- Given a `Array GoalsLocation` return the array of `SubExpr.Pos` for all locations
in the targets of the relevant goals.  -/
getGoalLocations : Array Lean.SubExpr.GoalsLocation → Array Lean.SubExpr.Pos
-- Aesop.Tree.TreeM
Aesop.Tree.rootMetaState : Aesop.Tree → Lean.Meta.SavedState
-- Lean.Setup
Lean.instInhabitedModuleHeader.default : Lean.ModuleHeader
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β},
  (k, v) ∈ Std.ExtDTreeMap.Const.toList t ↔ t.getKey? k = some k ∧ Std.ExtDTreeMap.Const.get? t k = some v
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.subgraphOfAdj_verts : ∀ {V : Type u} (G : SimpleGraph V) {v w : V} (hvw : G.Adj v w), (G.subgraphOfAdj hvw).verts = {v, w}
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.swap : Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_X₃_carrier : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R), ↑(M.smulShortComplex r).X₃ = (↑M ⧸ r • ⊤)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- When we have six complex shapes `c₁`, `c₂`, `c₃`, `c₁₂`, `c₂₃`, `c`, and total functors
`HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂`,
`HomologicalComplex₂ C c₁₂ c₃ ⥤ HomologicalComplex C c`,
`HomologicalComplex₂ C c₂ c₃ ⥤ HomologicalComplex C c₂₃`,
`HomologicalComplex₂ C c₁ c₂₂₃ ⥤ HomologicalComplex C c`, we get two ways to
compute the total complex of a triple complex in `HomologicalComplex₃ C c₁ c₂ c₃`, then
under this assumption `[Associative c₁ c₂ c₃ c₁₂ c₂₃ c]`, these two complexes
canonically identify (without introducing signs).  -/
ComplexShape.Associative : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {I₁₂ : Type u_4} →
        {I₂₃ : Type u_5} →
          {J : Type u_6} →
            (c₁ : ComplexShape I₁) →
              (c₂ : ComplexShape I₂) →
                (c₃ : ComplexShape I₃) →
                  (c₁₂ : ComplexShape I₁₂) →
                    (c₂₃ : ComplexShape I₂₃) →
                      (c : ComplexShape J) →
                        [TotalComplexShape c₁ c₂ c₁₂] →
                          [TotalComplexShape c₁₂ c₃ c] →
                            [TotalComplexShape c₂ c₃ c₂₃] → [TotalComplexShape c₁ c₂₃ c] → Prop
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- The finset of those partitions in which every part is odd.  -/
Nat.Partition.odds : (n : ℕ) → Finset n.Partition
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {x : R} {s : Set R},
  x ∈ NonUnitalSubsemiring.closure s ↔ ∀ (S : NonUnitalSubsemiring R), s ⊆ ↑S → x ∈ S
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `MeasureTheory.VectorMeasure.of_sdiff`. -/
MeasureTheory.VectorMeasure.of_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [T2Space M] {v : MeasureTheory.VectorMeasure α M} {A B : Set α},
  MeasurableSet A → MeasurableSet B → A ⊆ B → v (B \ A) = v B - v A
-- Mathlib.Algebra.Polynomial.Monomial
Polynomial.ringHom_ext : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : Semiring S] {f g : Polynomial R →+* S},
  (∀ (a : R), f (Polynomial.C a) = g (Polynomial.C a)) → f Polynomial.X = g Polynomial.X → f = g
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.prod_mul_tprod_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  [T2Space α] {s : Finset β}, Multipliable f → (∏ x ∈ s, f x) * ∏' (x : ↑(↑s)ᶜ), f ↑x = ∏' (x : β), f x
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.toLinearEquiv_kroneckerAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m], ↑(Matrix.kroneckerAlgEquiv m n R) = kroneckerLinearEquiv m m n n R
-- Lean.Data.Lsp.InitShutdown
/-- A TraceValue represents the level of verbosity with which the server systematically reports its execution trace using `$/logTrace` notifications.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#traceValue)
 -/
Lean.Lsp.Trace : Type
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioc_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioc a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Ioc a b, f i.castSucc
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_insertUnit_units : ∀ {n : ℕ} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (foundContradiction : Bool)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  have insertUnit_res :=
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l;
  ∀ l' ∈ insertUnit_res.1.toList, l' = l ∨ l' ∈ units.toList
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
IsConjRoot.isIntegral_iff : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y : A},
  IsConjRoot R x y → (IsIntegral R x ↔ IsIntegral R y)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- `FiniteMulArchimedeanClass M` is the quotient of the non-one elements of the group `M` by
multiplicative archimedean equivalence, where two elements `a` and `b` are in the same class iff
`(∃ m : ℕ, |b|ₘ ≤ |a|ₘ ^ m) ∧ (∃ n : ℕ, |a|ₘ ≤ |b|ₘ ^ n)`.

It is defined as the subtype of non-top elements of `MulArchimedeanClass M`
(`⊤ : MulArchimedeanClass M` is the archimedean class of `1`).

This is useful since the family of non-top archimedean classes is linearly independent.  -/
FiniteMulArchimedeanClass : (M : Type u_1) → [inst : CommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedMonoid M] → Type (max 0 u_1)
-- Mathlib.Algebra.Category.Semigrp.Basic
CategoryTheory.Iso.semigrpIsoToMulEquiv.eq_1 : ∀ {X Y : Semigrp} (i : X ≅ Y), i.semigrpIsoToMulEquiv = (Semigrp.Hom.hom i.hom).toMulEquiv (Semigrp.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `LocallyPathConnectedSpace.path_connected_basis`.

---

Each neighborhood filter has a basis of path-connected neighborhoods.  -/
LocPathConnectedSpace.path_connected_basis : ∀ {X : Type u_4} {inst : TopologicalSpace X} [self : LocallyPathConnectedSpace X] (x : X),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPathConnected s) id
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instHasQuotientWeakEquivalencesHomRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C)).HasQuotient
    (HomotopicalAlgebra.FibrantObject.homRel C)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₂Iso.tgtM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Algebra.Order.Ring.Defs
instNoMaxOrderOfNontrivial : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Nontrivial R], NoMaxOrder R
-- Mathlib.GroupTheory.SchurZassenhaus
Subgroup.isComplement'_stabilizer_of_coprime : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : IsMulCommutative ↥H] [inst_2 : H.FiniteIndex]
  [inst_3 : H.Normal] {α : H.QuotientDiff}, (Nat.card ↥H).Coprime H.index → H.IsComplement' (MulAction.stabilizer G α)
-- Mathlib.Topology.SeparatedMap
IsLocallyInjective.comp_left : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] {A : Type u_1} {f : X → Y},
  IsLocallyInjective f → ∀ {g : Y → A}, Function.Injective g → IsLocallyInjective (g ∘ f)
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y} (H : CategoryTheory.SimplicialObject.Homotopy f g) (p q : ℕ),
  CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom H p q =
    if h : p + 1 = q then -∑ k, (-1) ^ ↑k • CategoryTheory.CategoryStruct.comp (H.h k) (CategoryTheory.eqToHom ⋯) else 0
-- Lean.Expr
/-- Same as `getAppArgs` but reverse the output array.  -/
Lean.Expr.getAppRevArgs : Lean.Expr → Array Lean.Expr
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesAt_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  HasFPowerSeriesAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e ↔ ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e
-- Mathlib.Algebra.Group.Action.Defs
IsScalarTower.op_right : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : SMul M α] [inst_1 : SMul M N] [inst_2 : SMul N α]
  [inst_3 : SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [IsScalarTower M N α], IsScalarTower M Nᵐᵒᵖ α
-- Mathlib.Analysis.Analytic.Order
/-- The order of an analytic function `f` at `z₀` equals a natural number `n` iff `f` can locally
be written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic and does not vanish at `z₀`.  -/
AnalyticAt.analyticOrderAt_eq_natCast : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {n : ℕ} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    (analyticOrderAt f z₀ = ↑n ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans_app_uliftYoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] (X : C),
  (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans φ).app
      (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).inv.app X)
      (φ.app X)
-- Mathlib.Data.Num.Bitwise
PosNum.shiftl_succ_eq_bit0_shiftl : ∀ (p : PosNum) (n : ℕ), p <<< n.succ = (p <<< n).bit0
-- Batteries.Control.AlternativeMonad
failure_bind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m]
  (x : α → m β), failure >>= x = failure
-- Init.Data.List.Impl
List.find?_singleton : ∀ {α : Type u_1} {p : α → Bool} {a : α}, List.find? p [a] = if p a = true then some a else none
-- Mathlib.Algebra.Homology.GrothendieckAbelian
HomologicalComplex.ab5OfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C] [CategoryTheory.Limits.HasFiniteLimits C]
  [CategoryTheory.AB5OfSize.{w', w, v, u} C],
  CategoryTheory.AB5OfSize.{w', w, max t v, max (max t u) v} (HomologicalComplex C c)
-- Batteries.Lean.Expr
/-- Like `isAppOf` but ignores metadata.  -/
Lean.Expr.isAppOf' : Lean.Expr → Lean.Name → Bool
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.symmₗ_apply : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : F), (Bundle.Pretrivialization.symmₗ R e b) y = e.symm b y
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.isPatternVar.isAtomicIdent : Lean.Syntax → Bool
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Contravariant.toAddLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddSemigroup α] [inst_1 : PartialOrder α] [inst_2 : AddLeftReflectLE α],
  Contravariant.toAddLeftCancelSemigroup = { toAddSemigroup := inst, toIsLeftCancelAdd := ⋯ }
-- Mathlib.RingTheory.Ideal.Height
Ideal.ne_bot_of_height_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {I : Ideal R}, I.height = 1 → I ≠ ⊥
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isSome_maxKey?_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β}
  {l : List ((_ : α) × β)}, (Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = !l.isEmpty
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_sum_of_subadditive_on_pred : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop),
  f 0 ≤ 0 →
    p 0 →
      (∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) →
        (∀ (a b : α), p a → p b → p (a + b)) → ∀ (s : Multiset α), (∀ a ∈ s, p a) → f s.sum ≤ (Multiset.map f s).sum
-- Mathlib.Tactic.Order.Graph.Basic
/-- DFS algorithm for constructing a proof that `x ≤ y` by finding a path from `x` to `y` in the
`≤`-graph.  -/
Mathlib.Tactic.Order.Graph.buildTransitiveLeProofDFS : Mathlib.Tactic.Order.Graph →
  ℕ → ℕ → Lean.Expr → StateT Mathlib.Tactic.Order.Graph.DFSState Lean.MetaM (Option Lean.Expr)