mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.ExprLens
/-- `foldAncestors k init p e` folds over the strict ancestor subexpressions of the given expression `e` above position `p`, starting at the root expression and working down.
The fold function `k` is given the newly instantiated free variables, the ancestor subexpression, and the coordinate
that will be explored next. -/
Lean.Meta.foldAncestors : {M : Type → Type} →
  [Monad M] →
    [MonadLiftT Lean.MetaM M] →
      [MonadControlT Lean.MetaM M] →
        [Lean.MonadError M] →
          {α : Type} → (Array Lean.Expr → Lean.Expr → ℕ → α → M α) → α → Lean.SubExpr.Pos → Lean.Expr → M α
-- Mathlib.Algebra.Group.Defs
nsmulRec_eq : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : Zero M] (k : ℕ) (m : M), nsmulRec (k + 1) m = 0 + nsmulRec' (k + 1) m
-- Mathlib.Algebra.Group.End
Equiv.Perm.symm_mul : ∀ {α : Type u_4} (e : Equiv.Perm α), Equiv.symm e * e = 1
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.pointed_toConvexCone : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (C : PointedCone R E), (↑C).Pointed
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.finrank_lattice : ∀ (L : PeriodPair), Module.finrank ℤ ↥L.lattice = 2
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.instRespectsLeftInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  (Q : CategoryTheory.MorphismProperty C) [P.RespectsLeft Q], P.ind.RespectsLeft Q
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.foldlM_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- **Alias** of `TensorProduct.finsuppScalarRight`.

---

The tensor product of `M` and `ι →₀ R` is linearly equivalent to `ι →₀ M`  -/
TensorProduct.finsuppScalarRight' : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    (ι : Type u_5) → [DecidableEq ι] → TensorProduct R M (ι →₀ R) ≃ₗ[S] ι →₀ M
-- Mathlib.Data.Nat.Cast.Defs
/-- An `AddMonoidWithOne` is an `AddMonoid` with a `1`.
It also contains data for the unique homomorphism `ℕ → R`.  -/
AddMonoidWithOne : Type u_2 → Type u_2
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddGroup : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [AddGroup A] → AddGroup (CStarMatrix m n A)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α] [t : TopologicalSpace α]
  [Topology.IsScottHausdorff α D], IsOpen s → DirSupInaccOn D s
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.symm : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ s₂ : Set (Set Ω)},
  ProbabilityTheory.IndepSets s₁ s₂ μ → ProbabilityTheory.IndepSets s₂ s₁ μ
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheoremsArray.isErased : Lean.Meta.SimpTheoremsArray → Lean.Meta.Origin → Bool
-- Mathlib.Topology.Continuous
continuous_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {y : Y}, Continuous fun x => y
-- Lean.Util.LeanOptions
Lean.instReprLeanOptionValue.repr : Lean.LeanOptionValue → ℕ → Std.Format
-- Mathlib.Order.Heyting.Basic
bot_himp : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), ⊥ ⇨ a = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The left unitor isomorphism for binary products with the terminal object.  -/
CategoryTheory.Limits.prod.leftUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] →
      (P : C) → [inst_2 : CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P] → (⊤_ C) ⨯ P ≅ P
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The kind of rewrite  -/
Mathlib.Tactic.LibraryRewrite.Kind : Type
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The sum of a function `g` defined only on a set `s` is equal to
the sum of a function `f` defined everywhere,
as long as `f` and `g` agree on `s`, and `f = 0` off `s`.  -/
Finset.sum_congr_set : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Fintype ι] (s : Set ι)
  [inst_2 : DecidablePred fun x => x ∈ s] (f : ι → M) (g : ↑s → M),
  (∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩) → (∀ x ∉ s, f x = 0) → ∑ i, f i = ∑ i, g i
-- Mathlib.Data.Nat.PrimeFin
/-- The prime factors of a natural number as a finset.  -/
Nat.primeFactors : ℕ → Finset ℕ
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nndist_snd_le : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoMetricSpace α]
  [inst_1 : PseudoMetricSpace β] (x y : WithLp p (α × β)), nndist x.snd y.snd ≤ nndist x y
-- Mathlib.Topology.EMetricSpace.Pi
/-- The product of a finite number of pseudoemetric spaces, with the max distance, is still
a pseudoemetric space.
This construction would also work for infinite products, but it would not give rise
to the product topology. Hence, we only formalize it in the good situation of finitely many
spaces.  -/
pseudoEMetricSpacePi : {β : Type v} →
  {X : β → Type u_2} → [Fintype β] → [(b : β) → PseudoEMetricSpace (X b)] → PseudoEMetricSpace ((b : β) → X b)
-- Mathlib.GroupTheory.NoncommPiCoprod
Subgroup.noncommPiCoprod.eq_1 : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} [inst_1 : Fintype ι]
  (hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y),
  Subgroup.noncommPiCoprod hcomm = MonoidHom.noncommPiCoprod (fun i => (H i).subtype) ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastAdd : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (assign : α → Bool) (input : aig.BinaryRefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd aig input).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd aig input).vec.get idx hidx }⟧ =
          (lhs + rhs).getLsbD idx
-- Lean.Parser.Command
Lean.Parser.Command.structure : Lean.Parser.Parser
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk_re : ∀ (z : ℂ) (h : 0 < z.im), { coe := z, coe_im_pos := h }.re = z.re
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAddCommMonoid.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddCommMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R],
  BoundedContinuousFunction.instAddCommMonoid =
    { toAddMonoid := BoundedContinuousFunction.instAddMonoid, add_comm := ⋯ }
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg.eq_1 : ∀ (i : Int8), i.toNatClampNeg = i.toInt.toNat
-- Mathlib.Data.Quot
Quotient.map_mk : ∀ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : α → β) (h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b)
  (x : α), Quotient.map f h ⟦x⟧ = ⟦f x⟧
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `sinh` is surjective, `∀ b, ∃ a, sinh a = b`. In this case, we use `a = arsinh b`.  -/
Real.sinh_surjective : Function.Surjective Real.sinh
-- Mathlib.Order.WellFoundedSet
Set.isWF_univ_iff : ∀ {α : Type u_2} [inst : LT α], Set.univ.IsWF ↔ WellFoundedLT α
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instLinearCoind₁Functor : ∀ {G : Type v} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] {k : Type u}
  [inst_3 : CommRing k] [inst_4 : TopologicalSpace k], CategoryTheory.Functor.Linear k (TopRep.coind₁Functor k G)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The compatibility isomorphism of the monoidal functor `toMonoidalCategory L W ε`
with respect to the tensor product.  -/
CategoryTheory.Localization.Monoidal.μ : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      (X Y : C) →
                        CategoryTheory.MonoidalCategoryStruct.tensorObj
                            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
                            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ≅
                          (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Order.Hom.Lattice
instCoeTCLatticeHomOfLatticeHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Lattice α] → [inst_2 : Lattice β] → [LatticeHomClass F α β] → CoeTC F (LatticeHom α β)
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseScheme : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI.Scheme
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- A family of additive subgroups on a ring `A` is a subgroups basis if it satisfies some
axioms ensuring there is a topology on `A` which is compatible with the ring structure and
admits this family as a basis of neighborhoods of zero.  -/
RingSubgroupsBasis : {A : Type u_1} → {ι : Type u_2} → [inst : Ring A] → (ι → AddSubgroup A) → Prop
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_add_one : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {n : ℕ} {a : α},
  Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?
-- Std.Data.ExtDHashMap.Lemmas
_private.Std.Data.ExtDHashMap.Lemmas.0.Std.ExtDHashMap.Const.insertMany_list_mk : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m : Std.DHashMap α fun x => β} {l : List (α × β)},
  Std.ExtDHashMap.Const.insertMany (Std.ExtDHashMap.mk m) l = Std.ExtDHashMap.mk (Std.DHashMap.Const.insertMany m l)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
Submonoid.mem_closure_iff_exists_finset_subset : ∀ {M : Type u_1} [inst : CommMonoid M] {x : M} {s : Set M},
  x ∈ Submonoid.closure s ↔ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x
-- Init.Data.List.Lex
List.append_left_le : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {l₁ l₂ l₃ : List α}, l₂ ≤ l₃ → l₁ ++ l₂ ≤ l₁ ++ l₃
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : β → β}, k' ∈ m.modify k f ↔ k' ∈ m
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trPosNum.match_1.eq_3 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match n.bit1 with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_3 n
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Q.IsLocalization (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
-- Mathlib.Analysis.Convex.Cone.Basic
ConvexCone.Pointed.of_nonempty_of_isClosed : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : AddCommMonoid E] [inst_1 : TopologicalSpace E] [inst_2 : Semifield 𝕜]
  [inst_3 : LinearOrder 𝕜] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace 𝕜] [OrderTopology 𝕜] [DenselyOrdered 𝕜]
  [NoMaxOrder 𝕜] [ContinuousSMul 𝕜 E] {C : ConvexCone 𝕜 E}, (↑C).Nonempty → IsClosed ↑C → C.Pointed
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} [IsDomain S]
  {y : S}, y ≠ x → (Polynomial.aeval y) (minpoly R x) = 0 → Polynomial.eval y (minpolyDiv R x) = 0
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates equalizers and products, it creates limits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating limits" in the literature, and whether or not the condition can be dropped seems to depend
on the specific definition that is used.  -/
CategoryTheory.Limits.createsLimitsOfSizeOfCreatesEqualizersAndProducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Limits.HasEqualizers D] →
          [CategoryTheory.Limits.HasProducts D] →
            (G : CategoryTheory.Functor C D) →
              [G.ReflectsIsomorphisms] →
                [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] →
                  [(J : Type w) → CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) G] →
                    CategoryTheory.CreatesLimitsOfSize.{w, w, v, v₂, u, u₂} G
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A]
  (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) (X : CategoryTheory.Functor Cᵒᵖ A)
  {X_1 Y : SimplexCategory} (f : X_1 ⟶ Y),
  ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X).map f =
    CategoryTheory.Limits.Pi.lift fun i =>
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun i => X.obj (Opposite.op ((E.obj (Opposite.op X_1)).obj i))) ((E.map f.op).f i))
        (X.map ((E.map f.op).φ i).op)
-- Mathlib.Topology.Path
Path.symm_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), Set.range ⇑γ.symm = Set.range ⇑γ
-- Std.Internal.Parsec.Basic
/-- Parses zero or more chars with `p`, accumulates into a string.
 -/
Std.Internal.Parsec.manyCharsCore : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι Char → String → Std.Internal.Parsec ι String
-- Lean.Meta.Tactic.Grind.Split
/-- Given `[t₁, ..., tₙ]`, returns `t₁ <;> ... <;> tₙ`
 -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.Action.mkAndThenSeq : List (Lean.TSyntax `grind) → Lean.CoreM (Lean.TSyntax `grind)
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Eventually.ratCast_atBot : ∀ {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop},
  (∀ᶠ (x : R) in Filter.atBot, p x) → ∀ᶠ (n : ℚ) in Filter.atBot, p ↑n
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBotWithTop'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder β] (f : LatticeHom α β),
  f.withBotWithTop' = { toLatticeHom := f.withTop'.withBot', map_top' := ⋯, map_bot' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt64.sub_left_inj : ∀ {a b : UInt64} (c : UInt64), a - c = b - c ↔ a = b
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.PreservesLeftHomologyOf.mk : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D}
  [inst_4 : F.PreservesZeroMorphisms] {S : CategoryTheory.ShortComplex C},
  (∀ (h : S.LeftHomologyData), h.IsPreservedBy F) → F.PreservesLeftHomologyOf S
-- Mathlib.CategoryTheory.Galois.Basic
/-- In a `GaloisCategory` the set of automorphism of a connected object is finite.  -/
CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (A : C)
  [CategoryTheory.PreGaloisCategory.IsConnected A], Finite (CategoryTheory.Aut A)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.surjective_comp_left_of_exists_rightInverse : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃}
  {σ₃₂ : R₃ →+* R₂} [inst_7 : RingHomInvPair σ₂₃ σ₃₂] [RingHomCompTriple σ₁₃ σ₃₂ σ₁₂],
  (∃ f', f ∘ₛₗ f' = LinearMap.id) → Function.Surjective fun g => f ∘ₛₗ g
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_union_Ico_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  a ≤ b → b ≤ c → Finset.Ico a b ∪ Finset.Ico b c = Finset.Ico a c
-- Mathlib.Data.Semiquot
Semiquot.mem_pure' : ∀ {α : Type u_1} {a b : α}, a ∈ Semiquot.pure b ↔ a = b
-- Mathlib.Order.SuccPred.Limit
/-- The lemma formerly named `not_isPredPrelimit_iff` is now
`not_isPredPrelimit_iff_pred_eq`  -/
Order.not_isPredPrelimit_iff_exists_covBy : ∀ {α : Type u_1} [inst : LT α] {a : α}, ¬Order.IsPredPrelimit a ↔ ∃ b, a ⋖ b
-- Lean.Elab.DocString
/-- Environment extension for docstring commands  -/
Lean.Doc.docCommandExt : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap (Array Lean.Name))
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleAddGroup.instIsSimpleOrderAddSubgroup : ∀ {C : Type u_3} [inst : AddCommGroup C] [IsSimpleAddGroup C], IsSimpleOrder (AddSubgroup C)
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- pullback commutes with composition (up to a natural isomorphism)  -/
CategoryTheory.MonoOver.pullbackComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            CategoryTheory.MonoOver.pullback (CategoryTheory.CategoryStruct.comp f g) ≅
              (CategoryTheory.MonoOver.pullback g).comp (CategoryTheory.MonoOver.pullback f)
-- Mathlib.Order.UpperLower.Basic
isUpperSet_sInter : ∀ {α : Type u_1} [inst : LE α] {S : Set (Set α)}, (∀ s ∈ S, IsUpperSet s) → IsUpperSet (⋂₀ S)
-- Mathlib.Order.CompleteLattice.Basic
le_biSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} {s : Set ι} (f : ι → α) {i : ι}, i ∈ s → f i ≤ ⨆ i ∈ s, f i
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measureUnivNNReal_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α}, MeasureTheory.measureUnivNNReal 0 = 0
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.isIntegral : ∀ (R : Type u_1) {A : Type u_2} (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [IsIntegralClosure A R B] [inst_6 : Algebra R A] [IsScalarTower R A B]
  (x : A), IsIntegral R x
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural isomorphism arising from `mapComp_eq`.  -/
CategoryTheory.Over.mapComp : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y Z : T} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g) ≅
            (CategoryTheory.Over.map f).comp (CategoryTheory.Over.map g)
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- See `zero_lt_three` for a version with the type implicit.  -/
zero_lt_three' : ∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 3
-- Mathlib.Data.List.Destutter
List.isChain_cons_destutter'_of_rel : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α) {a b : α},
  R a b → List.IsChain R (a :: List.destutter' R b l)
-- Mathlib.Order.Cover
CovBy.wcovBy : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b → a ⩿ b
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- This function produces a subword of a word `L` by cancelling the first and last
letters of `L` as long as possible. If `L` is reduced, the resulting word will be cyclically
reduced.  -/
FreeAddGroup.reduceCyclically : {α : Type u} → [DecidableEq α] → List (α × Bool) → List (α × Bool)
-- Mathlib.Data.Set.NAry
Set.image2_curry : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α × β → γ) (s : Set α) (t : Set β),
  Set.image2 (fun a b => f (a, b)) s t = f '' s ×ˢ t
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso_hom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.LeftExtension f g} (P : s.IsKan) (Q : t.IsKan),
  CategoryTheory.StructuredArrow.Hom.right (P.uniqueUpToIso Q).hom = P.desc t
-- Mathlib.Util.Notation3
/-- The dynamic state of a `Matcher`.  -/
Mathlib.Notation3.MatchState : Type
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion : ∀ {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  (⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x)).PairwiseDisjoint id
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.map_g : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (P : StandardEtalePair R) (f : R →+* S),
  (P.map f).g = Polynomial.map f P.g
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_lt_top : ∀ {x : ENNReal}, x⁻¹ < ⊤ ↔ 0 < x
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.le_ord_iff_card_le_of_lt_aleph0 : ∀ (o : Ordinal.{u_1}) {c : Cardinal.{u_1}}, c < Cardinal.aleph0 → (o ≤ c.ord ↔ o.card ≤ c)
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.Subobject Y) (f f_1 : X ⟶ Y)
  (e_f : f = f_1) (h : P.Factors f), P.factorThru f h = P.factorThru f_1 ⋯
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.instInhabited : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → Inhabited (C ≌ C)
-- Mathlib.Topology.DiscreteSubset
tendsto_cofinite_cocompact_of_discrete : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  [DiscreteTopology X],
  Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y) → Filter.Tendsto f Filter.cofinite (Filter.cocompact Y)