mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.induct : ∀ (motive : ℤ → Lean.Grind.Linarith.Expr → Prop),
  (∀ (coeff : ℤ), motive coeff Lean.Grind.Linarith.Expr.zero) →
    (∀ (coeff : ℤ) (v : Lean.Grind.Linarith.Var), motive coeff (Lean.Grind.Linarith.Expr.var v)) →
      (∀ (coeff : ℤ) (a b : Lean.Grind.Linarith.Expr), motive coeff a → motive coeff b → motive coeff (a.add b)) →
        (∀ (coeff : ℤ) (a b : Lean.Grind.Linarith.Expr), motive coeff a → motive (-coeff) b → motive coeff (a.sub b)) →
          (∀ (coeff : ℤ) (k : ℕ) (a : Lean.Grind.Linarith.Expr),
              (k == 0) = true → motive coeff (Lean.Grind.Linarith.Expr.natMul k a)) →
            (∀ (coeff : ℤ) (k : ℕ) (a : Lean.Grind.Linarith.Expr),
                (k == 0) = false → motive (coeff.mul ↑k) a → motive coeff (Lean.Grind.Linarith.Expr.natMul k a)) →
              (∀ (coeff k : ℤ) (a : Lean.Grind.Linarith.Expr),
                  (k == 0) = true → motive coeff (Lean.Grind.Linarith.Expr.intMul k a)) →
                (∀ (coeff k : ℤ) (a : Lean.Grind.Linarith.Expr),
                    (k == 0) = false → motive (coeff.mul k) a → motive coeff (Lean.Grind.Linarith.Expr.intMul k a)) →
                  (∀ (coeff : ℤ) (a : Lean.Grind.Linarith.Expr), motive (-coeff) a → motive coeff a.neg) →
                    ∀ (coeff : ℤ) (a : Lean.Grind.Linarith.Expr), motive coeff a
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.pow_carmichael : ∀ {n : ℕ} (a : (ZMod n)ˣ), a ^ ArithmeticFunction.carmichael n = 1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.stack : Turing.PartrecToTM2.K'
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The obvious inclusion
`((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p X₁ X₂ X₃ j` when
`p ⟨i₁, i₂, i₃⟩ = j`.  -/
CategoryTheory.GradedObject.ιMapTrifunctorMapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [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₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) →
                  {I₁ : Type u_7} →
                    {I₂ : Type u_8} →
                      {I₃ : Type u_9} →
                        {J : Type u_10} →
                          (p : I₁ × I₂ × I₃ → J) →
                            (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                              (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                  (i₁ : I₁) →
                                    (i₂ : I₂) →
                                      (i₃ : I₃) →
                                        (j : J) →
                                          p (i₁, i₂, i₃) = j →
                                            [inst_4 :
                                                ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj
                                                          X₂).obj
                                                      X₃).HasMap
                                                  p] →
                                              ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶
                                                CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j
-- Init.Data.Float.Model.Unpacked.Round
/-- The approximation is strictly smaller than the infinitely precise value,
and the given `Ordering` describes the result of comparing the
infinitely precise value and the approximation plus half a ulp.
 -/
Float.Model.UnpackedFloat.Accuracy.inexact : Ordering → Float.Model.UnpackedFloat.Accuracy
-- Mathlib.Logic.Basic
congr_heq : ∀ {α β : Sort u_2} {γ : Sort u_3} {f : α → γ} {g : β → γ} {x : α} {y : β}, f ≍ g → x ≍ y → f x = g y
-- Mathlib.Order.Hom.Bounded
TopHom.instInhabited.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β],
  TopHom.instInhabited = { default := { toFun := fun x => ⊤, map_top' := ⋯ } }
-- Qq.Delab
Qq.Impl.withDelabQuoted : StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM Lean.Term → Lean.PrettyPrinter.Delaborator.Delab
-- Std.Do.WP.Basic
Std.Do.OptionT.instWP : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} → [Std.Do.WP m ps] → Std.Do.WP (OptionT m) (Std.Do.PostShape.except PUnit.{u + 1} ps)
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- A sphere in a product space is a union of spheres on each component restricted to the closed
ball.  -/
sphere_pi : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b)
  {r : ℝ},
  0 < r ∨ Nonempty β → Metric.sphere x r = (⋃ i, Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r
-- Init.Data.Array.Basic
/-- See comment at `forIn'Unsafe`  -/
Array.mapMUnsafe : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → m β) → Array α → m (Array β)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.cons_eval : ∀ (f fs : Turing.ToPartrec.Code),
  (f.cons fs).eval = fun v => do
    let n ← f.eval v
    let ns ← fs.eval v
    pure (n.headI :: ns)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcReleaseParams.fromJson : Lean.Json → Except String Lean.Lsp.RpcReleaseParams
-- Lean.DocString.Parser
Lean.Doc.Parser.BlockCtxt.mk : ℕ → Option ℕ → List Lean.Doc.Parser.InList → Lean.Position → ℕ → Lean.Doc.Parser.BlockCtxt
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.congr_simp : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarRing A]
  [inst_4 : Algebra R A] [inst_5 : StarModule R A], StarSubalgebra R A = StarSubalgebra R A
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_reverse : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β},
  xs.reverse.mapFinIdx f = (xs.mapFinIdx fun i a h => f (n - 1 - i) a ⋯).reverse
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.notMem_span_image : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R],
  LinearIndependent R v → ∀ {s : Set ι} {x : ι}, x ∉ s → v x ∉ Submodule.span R (v '' s)
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.derivePartialCorrectness : Lean.Name → Bool → Lean.MetaM Unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_contains_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  m.WF → (Std.DHashMap.Raw.map f m).contains k = true → m.contains k = true
-- Mathlib.Condensed.Module
/-- The category of condensed abelian groups is defined as condensed `ℤ`-modules.
 -/
CondensedAb : Type (u + 2)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring.injEq : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr)
  (c_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) (lhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring c lhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring c_1 lhs_1) =
    (c = c_1 ∧ lhs = lhs_1)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rcc_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n + 1 - m).toNat → (m...=n).toArray[i]? = some (m + ↑i)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.instCompleteLattice : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → CompleteLattice (IntermediateField F E)
-- Init.System.IO
/-- Converts `s` to a string using its `ToString α` instance, and prints it to the current standard
error (as determined by `IO.getStderr`).
 -/
IO.eprint : {α : Type u_1} → [ToString α] → α → IO Unit
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {f : 𝕜 → F} {R : Type u_3} [inst_3 : DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
        ContDiffWithinAt 𝕜 (↑n) f s x → iteratedDerivWithin n (fun w => c • f w) s x = c • iteratedDerivWithin n f s x
-- Mathlib.Order.SupClosed
/-- **Alias** of the reverse direction of `isSublattice_preimage_ofDual`. -/
IsSublattice.dual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, IsSublattice s → IsSublattice (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.Data.EReal.Operations
EReal.lt_sub_iff_add_lt : ∀ {a b c : EReal}, b ≠ ⊥ ∨ c ≠ ⊤ → b ≠ ⊤ ∨ c ≠ ⊥ → (c < a - b ↔ c + b < a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α) (f : Option (β k) → Option (β k)), (t₁.alter k f).Equiv (t₂.alter k f)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_opcyclesMap_of_isIso_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Epi φ.τ₁]
  [inst_4 : S₁.HasRightHomology] [inst_5 : S₂.HasRightHomology],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)
-- Mathlib.Condensed.Light.Explicit
/-- A `LightCondAb` version of `LightCondensed.ofSheafLightProfinite`.  -/
LightCondAb.ofSheafLightProfinite : (F : CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat ℤ)) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] → CategoryTheory.regularTopology.EqualizerCondition F → LightCondAb
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppRight.eq_1 : ∀ (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] (N : Type u_4)
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (ι : Type u_5) [inst_9 : DecidableEq ι],
  TensorProduct.finsuppRight R S M N ι =
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl S M) (finsuppLEquivDirectSum R N ι) ≪≫ₗ
        TensorProduct.directSumRight R S M fun x => N) ≪≫ₗ
      (finsuppLEquivDirectSum S (TensorProduct R M N) ι).symm
-- Mathlib.Algebra.Group.Finsupp
/-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.

The lemma `induction_on_min` swaps the argument order in the sum.  -/
Finsupp.induction_on_min₂ : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [inst_1 : LinearOrder ι] {motive : (ι →₀ M) → Prop}
  (f : ι →₀ M),
  motive 0 →
    (∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → motive f → motive (f + fun₀ | a => b)) →
      motive f
-- Mathlib.MeasureTheory.Group.Measure
MeasurableSet.mul_closure_one_eq : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : Group G]
  [IsTopologicalGroup G] {s : Set G}, MeasurableSet s → s * closure {1} = s
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isSeparating_iff_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : ∀ (X : C), CategoryTheory.Limits.HasCoproduct (P.coproductFromFamily X)],
  P.IsSeparating ↔ ∀ (X : C), CategoryTheory.Epi (P.coproductFrom X)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_inv : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x y z).inv =
    (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom
-- Lean.Parser.Term.Doc
/-- Recommended spellings for notations, stored in a way so that the recommended spellings for a given
declaration are easily accessible.
 -/
Lean.Parser.Term.Doc.recommendedSpellingByNameExt : Lean.PersistentEnvExtension (Lean.Name × Array Lean.Parser.Term.Doc.RecommendedSpelling)
  (Lean.Parser.Term.Doc.RecommendedSpelling × Array Lean.Name)
  (Lean.NameMap (Array Lean.Parser.Term.Doc.RecommendedSpelling))
-- Mathlib.Tactic.Have
/-- The `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 -/
Mathlib.Tactic.tacticHave_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Action.Basic
AddAction.toPerm_symm_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (a : α) (x : β),
  (Equiv.symm (AddAction.toPerm a)) x = -a +ᵥ x
-- Std.Data.HashMap.Lemmas
Std.HashMap.union_insert_right_equiv_union_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {p : α × β}, (m₁ ∪ m₂.insert p.1 p.2).Equiv ((m₁ ∪ m₂).insert p.1 p.2)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instPreservesMonomorphismsRestrictScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (ModuleCat.restrictScalars f).PreservesMonomorphisms
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The natural map `UniformFun.toFun` from `α →ᵤ β` to `α → β` is uniformly continuous.

In other words, the uniform structure of uniform convergence is finer than that of pointwise
convergence, aka the product uniform structure.  -/
UniformFun.uniformContinuous_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β], UniformContinuous ⇑UniformFun.toFun
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Infix notation for `OrderMonoidHom`.  -/
«term_→*o_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- The postcomposition map `LeftHomotopyClass X Y → (Y ⟶ Z) → LeftHomotopyClass X Z`.  -/
HomotopicalAlgebra.LeftHomotopyClass.postcomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.LeftHomotopyClass X Y → (Y ⟶ Z) → HomotopicalAlgebra.LeftHomotopyClass X Z
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The **valuative criterion** for proper morphisms.  -/
AlgebraicGeometry.IsProper.eq_valuativeCriterion : @AlgebraicGeometry.IsProper =
  AlgebraicGeometry.ValuativeCriterion ⊓ @AlgebraicGeometry.QuasiCompact ⊓ @AlgebraicGeometry.QuasiSeparated ⊓
    @AlgebraicGeometry.LocallyOfFiniteType
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCommSemigroup : {α : Type u_1} → [AddCommSemigroup α] → AddCommSemigroup αᵃᵒᵖ
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension_eq_bot_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.projectiveDimension X = ⊥ ↔ CategoryTheory.Limits.IsZero X
-- Mathlib.CategoryTheory.MorphismProperty.Retract
/-- The class of morphisms that are retracts of morphisms
belonging to `P : MorphismProperty C`.  -/
CategoryTheory.MorphismProperty.retracts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff_splits : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔
    ∃ t₁ t₂, pos₁.Splits t₁ (pat ++ t₂) ∧ pos₂.Splits (t₁ ++ pat) t₂
-- Mathlib.Algebra.Group.Action.TypeTags
Multiplicative.smul : {α : Type u_2} → {β : Type u_3} → [VAdd α β] → SMul (Multiplicative α) β
-- Mathlib.Algebra.Algebra.Defs
/-- Embedding `R →+* A` given by `Algebra` structure.  -/
Algebra.algebraMap : (R : Type u) → (A : Type v) → {inst : CommSemiring R} → {inst_1 : Semiring A} → [self : Algebra R A] → R →+* A
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t₁ \ t₂).getKeyD k fallback = if k ∈ t₂ then fallback else t₁.getKeyD k fallback
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadParentDecl.mk : {m : Type → Type} → m (Option Lean.Name) → Lean.Elab.MonadParentDecl m
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_finSucc' : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  {v : Fin (n + 1) → V},
  LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ Submodule.span K (Set.range (Fin.init v))
-- Init.Data.Nat.Gcd
Nat.div_gcd_pos_of_pos_left : ∀ {a : ℕ} (b : ℕ), 0 < a → 0 < a / a.gcd b
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Multiplicative.ofAdd_le`. -/
Multiplicative.ofAdd_mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Multiplicative.ofAdd a ≤ Multiplicative.ofAdd b
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.of_ne_zero : ∀ {α : Type u_1} (a : α), FreeAddGroup.of a ≠ 0
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The red and the blue arrows in ![this diagram](https://i.imgur.com/q6X1GJ9.png) commute.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))
        U)
      ((D.t k i).c.app
        (Opposite.op
          ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
                (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj
            U))) =
    CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j))
          (Opposite.unop
            (Opposite.op ((TopologicalSpace.Opens.map (D.t' k i j).base).1 (Opposite.unop (Opposite.op U))))))
        ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom ⋯)))
-- Mathlib.Data.Seq.Defs
Stream'.Seq.head_nil : ∀ {α : Type u}, Stream'.Seq.nil.head = none
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of the identity in a topological group is normal.  -/
Subgroup.Normal.pathComponentOne : ∀ (G : Type u_4) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  (Subgroup.pathComponentOne G).Normal
-- Mathlib.Order.CompleteLattice.Basic
sSup_pair : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, sSup {a, b} = a ⊔ b
-- Mathlib.Analysis.Normed.Module.Bases
/-- Projections are uniformly bounded for unconditional bases.  -/
UnconditionalSchauderBasis.exists_norm_proj_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X],
  ∃ C, ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.Hom.h₀`. -/
AlgebraicGeometry.Scheme.Cover.Hom.app : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} → (self : E.Hom F) → (i : E.I₀) → E.X i ⟶ F.X (self.s₀ i)
-- Mathlib.Tactic.SplitIfs
/-- Return the condition and decidable instance of an `if` expression to case split.  -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.findIfToSplit? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.sub : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.ground_sdiff_subset_ground`. -/
Matroid.ground_diff_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.E \ X ⊆ M.E
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordMonoidWithZeroHom.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Nontrivial R], Ring.ordMonoidWithZeroHom R = Ring.ordMonoidWithZeroHom R
-- Mathlib.Algebra.Exact.Basic
/-- Equivalent characterizations of split exact sequences. Also known as the **Splitting lemma**.  -/
Function.Exact.split_tfae : ∀ {R : Type u_8} {M : Type u_9} {N : Type u_10} {P : Type u_11} [inst : Semiring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Injective ⇑f →
      Function.Surjective ⇑g →
        [∃ l, g ∘ₗ l = LinearMap.id, ∃ l, l ∘ₗ f = LinearMap.id,
            ∃ e, f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.mapDomain_add : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} (f : α → β) [inst : AddCommMonoid M] [inst_1 : Filter.TendstoCofinite f]
  (u v : α → M),
  Filter.TendstoCofinite.mapDomain f (u + v) =
    Filter.TendstoCofinite.mapDomain f u + Filter.TendstoCofinite.mapDomain f v
-- Init.Data.Nat.Div.Basic
Nat.div_div_eq_div_mul : ∀ (m n k : ℕ), m / n / k = m / (n * k)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulL : ℕ → Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_eq_map : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), f.range = Submodule.map f ⊤
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.coe_toOrderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : α →Co β), ⇑f.toOrderHom = ⇑f