mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- The value wrapped in `x : Snowflaking X α hα₀ hα₁`.  -/
Metric.Snowflaking.val : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → Metric.Snowflaking X α hα₀ hα₁ → X
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sndPiMap_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (b : J.R),
  CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.Limits.Pi.π I.right b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b)) (I.snd b)
-- Mathlib.Topology.UniformSpace.Completion
/-- The uniform bijection between a complete space and its uniform completion.  -/
UniformSpace.Completion.UniformCompletion.completeEquivSelf : {α : Type u_1} → [inst : UniformSpace α] → [CompleteSpace α] → [T0Space α] → UniformSpace.Completion α ≃ᵤ α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} {M : SheafOfModules R} (f : SheafOfModules.free I ⟶ M)
  (i : I), M.unitHomEquiv.symm (M.freeHomEquiv f i) = CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited β] {a : α}, ∅[a]! = default
-- Mathlib.Geometry.Manifold.ChartedSpace
piChartedSpace_chartAt : ∀ {ι : Type u_5} [inst : Finite ι] (H : ι → Type u_6) [inst_1 : (i : ι) → TopologicalSpace (H i)] (M : ι → Type u_7)
  [inst_2 : (i : ι) → TopologicalSpace (M i)] [inst_3 : (i : ι) → ChartedSpace (H i) (M i)] (f : (i : ι) → M i),
  chartAt (ModelPi H) f = OpenPartialHomeomorph.pi fun i => chartAt (H i) (f i)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_neg_le_tight : ∀ (ctx : Int.Internal.Linear.Context) (d : ℤ) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_neg_le_tight_cert d p₁ p₂ p₃ = true →
    d ∣ Int.Internal.Linear.Poly.denote' ctx p₁ →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_strict_mono : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α}
  [L.NeBot] [L.LeAtTop], Summable f L → Summable g L → f < g → ∑'[L] (n : ι), f n < ∑'[L] (n : ι), g n
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.zero.eq_1 : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M), S.zero = { zero := ⟨0, ⋯⟩ }
-- Init.Data.SInt.Basic
/-- Converts an 8-bit signed integer into the 8-bit unsigned integer that is its two's complement
encoding.
 -/
Int8.toUInt8 : Int8 → UInt8
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.mk.inj : ∀ {R : Type u_2} {inst : NonUnitalNonAssocRing R} {toRingSeminorm : RingSeminorm R}
  {eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0} {toRingSeminorm_1 : RingSeminorm R}
  {eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0},
  { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 } →
    toRingSeminorm = toRingSeminorm_1
-- Mathlib.RingTheory.KrullDimension.Basic
Ideal.IsPrime.isMaximal_of_ne_bot : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] [Ring.KrullDimLE 1 R] {I : Ideal R},
  I.IsPrime → I ≠ ⊥ → I.IsMaximal
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_inj : ∀ {M : Type u_2} [inst : Add M] {S T : AddSubsemigroup Mᵃᵒᵖ}, S.unop = T.unop ↔ S = T
-- Mathlib.RingTheory.Congruence.Basic
RingCon.comap_mono : ∀ {R : Type u_3} {R' : Type u_4} [inst : Add R] [inst_1 : Mul R] [inst_2 : Add R'] [inst_3 : Mul R'] {F : Type u_5}
  [inst_4 : FunLike F R R'] [inst_5 : AddHomClass F R R'] [inst_6 : MulHomClass F R R'] {J J' : RingCon R'} {f : F},
  J ≤ J' → J.comap f ≤ J'.comap f
-- Mathlib.Algebra.BigOperators.Finprod
finprod_false : ∀ {M : Type u_2} [inst : CommMonoid M] (f : False → M), ∏ᶠ (i : False), f i = 1
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- Evaluate a rational function `p` given a ring hom `f` from the scalar field
to the target and a value `x` for the variable in the target.

Fractions are reduced by clearing common denominators before evaluating:
`eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2`, not `0 / 0 = 0`.
 -/
RatFunc.eval : {K : Type u} → [inst : Field K] → {L : Type u} → [inst_1 : Field L] → (K →+* L) → L → RatFunc K → L
-- Mathlib.Order.FixedPoints
OrderHom.nextFixed_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) {y : ↑(Function.fixedPoints ⇑f)},
  x ≤ ↑y → f.nextFixed x hx ≤ y
-- Lean.Data.LBool
Lean.toLBoolM : {m : Type → Type} → [Monad m] → m Bool → m Lean.LBool
-- Mathlib.RingTheory.Flat.Equalizer
/-- The canonical map `T ⊗[R] eq(f, g) →ₐ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g)`.  -/
AlgHom.tensorEqualizer : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [inst_6 : IsScalarTower R S T] →
                    {A : Type u_4} →
                      {B : Type u_5} →
                        [inst_7 : CommRing A] →
                          [inst_8 : CommRing B] →
                            [inst_9 : Algebra R A] →
                              [inst_10 : Algebra R B] →
                                (f g : A →ₐ[R] B) →
                                  TensorProduct R T ↥(f.equalizer g) →ₐ[S]
                                    ↥((Algebra.TensorProduct.map (AlgHom.id S T) f).equalizer
                                        (Algebra.TensorProduct.map (AlgHom.id S T) g))
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.monicDegreeEq.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalFactorizationRing.monicDegreeEq m k hn p =
    ⟨Polynomial.map (algebraMap R (Polynomial.UniversalFactorizationRing m k hn p)) ↑p, ⋯⟩
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_eq_ofReal_iff : ∀ {p q : ℝ}, 0 ≤ p → 0 ≤ q → (ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φQ : ∀ {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] {S : CategoryTheory.ShortComplex C}
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  [inst_6 : F.PreservesRightHomologyOf S] [inst_7 : G.PreservesRightHomologyOf S] (h : S.RightHomologyData) (τ : F ⟶ G),
  (CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φQ = τ.app h.Q
-- Mathlib.NumberTheory.FactorisationProperties
Nat.infinite_even_deficient : {n | Even n ∧ n.Deficient}.Infinite
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.id_fst : ∀ (Δ : SimplexCategoryᵒᵖ), (CategoryTheory.SimplicialObject.Splitting.IndexSet.id Δ).fst = Δ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A finitely strongly measurable function is strongly measurable.  -/
MeasureTheory.FinStronglyMeasurable.stronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
  [inst_1 : TopologicalSpace β], MeasureTheory.FinStronglyMeasurable f μ → MeasureTheory.StronglyMeasurable f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.stepAux_read : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} {enc : Γ → List.Vector Bool n} (dec : List.Vector Bool n → Γ)
  [inst : Inhabited Γ] (enc0 : enc default = List.Vector.replicate n false),
  (∀ (a : Γ), dec (enc a) = a) →
    ∀ (f : Γ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) (v : σ) (L R : Turing.ListBlank Γ),
      Turing.TM1.stepAux (Turing.TM1to1.read dec f) v (Turing.TM1to1.trTape' enc0 L R) =
        Turing.TM1.stepAux (f R.head) v (Turing.TM1to1.trTape' enc0 L R)
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.instMonoidalCategoryHom : {C : Type u} → [inst : CategoryTheory.Bicategory C] → (X : C) → CategoryTheory.MonoidalCategory (X ⟶ X)
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The predicate expressing that, up to equivalence, a functor `L : C ⥤ D`
identifies the category `D` with the localized category of `C` with respect
to `W : MorphismProperty C`.  -/
CategoryTheory.Functor.IsLocalization : {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] →
        CategoryTheory.Functor C D → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.GroupWithZero.Associated
IsPrimal.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α] (a : α),
  IsPrimal a = ∀ ⦃b c : α⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  (∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
      CategoryTheory.IsPullback f' g' g f → P g → P g') →
    P.IsStableUnderBaseChange
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.mkSEvalMethods : Lean.CoreM Lean.Meta.Simp.Methods
-- Mathlib.Analysis.Convex.Combination
/-- A convex combination of two centers of mass is a center of mass as well. This version
works if two centers of mass share the set of original points.  -/
Finset.centerMass_segment : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (s : Finset ι) (w₁ w₂ : ι → R) (z : ι → E),
  ∑ i ∈ s, w₁ i = 1 →
    ∑ i ∈ s, w₂ i = 1 →
      ∀ (a b : R),
        a + b = 1 → a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z
-- Mathlib.Computability.ContextFreeGrammar
/-- A given word `w` belongs to the language generated by a given context-free grammar `g` iff
`g` can derive the word `w` (wrapped as a string) from the initial nonterminal of `g` in some
number of steps.  -/
ContextFreeGrammar.mem_language_iff : ∀ {T : Type u_1} (g : ContextFreeGrammar T) (w : List T),
  w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.liftOn_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S),
  (Localization.mk a b).liftOn f H = f a b
-- Mathlib.LinearAlgebra.Contraction
coe_dualTensorHomEquivOfBasis : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (b : Module.Basis ι R M)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι], ⇑(dualTensorHomEquivOfBasis b) = ⇑(dualTensorHom R M N)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_ne_zero`. -/
Ideal.inertiaDeg_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [p.IsMaximal] [Module.Finite R S] [P.LiesOver p], p.inertiaDeg' P ≠ 0
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_left_le_mk_add_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a ≤ ArchimedeanClass.mk (a + b) ↔ ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b
-- Init.Core
/-- `bind x f` does a monad "bind" operation on the task `x` with function `f`:
that is, it constructs (and immediately launches) a new task which will wait
for the value of `x` to be available and then calls `f` on the result,
resulting in a new task which is then run for a result.

`prio`, if provided, is the priority of the task.
If `sync` is set to true, `f` is executed on the current thread if `x` has already finished and
otherwise on the thread that `x` finished on. `prio` is ignored in this case. This should only be
done when executing `f` is cheap and non-blocking.
 -/
Task.bind : {α : Type u_1} →
  {β : Type u_2} → Task α → (α → Task β) → optParam Task.Priority Task.Priority.default → optParam Bool false → Task β
-- Aesop.Builder.Constructors
Aesop.RuleBuilder.constructors : Aesop.RuleBuilder
-- Mathlib.Algebra.Quaternion
Quaternion.imI_intCast : ∀ {R : Type u_3} [inst : CommRing R] (z : ℤ), (↑z).imI = 0
-- Std.Data.TreeMap.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.TreeMap.Equiv : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Std.TreeMap α β cmp → Prop
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Mathlib.RingTheory.Localization.Basic
/-- Definition of the natural algebra induced by the localization of an algebra.
Given an algebra `R → S`, a submonoid `R` of `M`, and a localization `Rₘ` for `M`,
let `Sₘ` be the localization of `S` to the image of `M` under `algebraMap R S`.
Then this is the natural algebra structure on `Rₘ → Sₘ`, such that the entire square commutes,
where `localization_map.map_comp` gives the commutativity of the underlying maps.

This instance can be helpful if you define `Sₘ := Localization (Algebra.algebraMapSubmonoid S M)`,
however we will instead use the hypotheses `[Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]` in lemmas
since the algebra structure may arise in different ways.
 -/
localizationAlgebra : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            {Rₘ : Type u_4} →
              {Sₘ : Type u_5} →
                [inst_3 : CommSemiring Rₘ] →
                  [inst_4 : CommSemiring Sₘ] →
                    [inst_5 : Algebra R Rₘ] →
                      [IsLocalization M Rₘ] →
                        [inst_7 : Algebra S Sₘ] →
                          [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] → Algebra Rₘ Sₘ
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- `rightSection` splits `π`  -/
CategoryTheory.IsSplitCoequalizer.rightSection_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp self.rightSection (CategoryTheory.CategoryStruct.comp π h) = h
-- Mathlib.Data.List.OfFn
List.ofFn_cons : ∀ {α : Type u} {n : ℕ} (a : α) (f : Fin n → α), List.ofFn (Fin.cons a f) = a :: List.ofFn f
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.map.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_2) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_1 a a_1 f
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A finite-dimensional module has dimension at most 1 iff
there is some `v : V` so every vector is a multiple of `v`.
 -/
finrank_le_one_iff : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] [Module.Finite K V], Module.finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w
-- Mathlib.LinearAlgebra.DFinsupp
iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  (p : ι → Submodule R N),
  iSupIndep p ↔ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.toArray_iterFromIdx : ∀ {β : Type w} {array : Array β} {pos : ℕ}, (array.iterFromIdx pos).toArray = array.extract pos
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_adj : ∀ {V : Type u} {v w : V} (s : Set (Sym2 V)), (SimpleGraph.fromEdgeSet s).Adj v w ↔ s(v, w) ∈ s ∧ v ≠ w
-- Mathlib.Algebra.Category.ModuleCat.Stalk
/-- (Implementation). The scalar multiplication function on `ColimitType`.  -/
CategoryTheory.Limits.colimit.smul : {C : Type u_1} →
  [inst : CategoryTheory.SmallCategory C] →
    [CategoryTheory.IsFiltered C] →
      (R : CategoryTheory.Functor C RingCat) →
        (M : CategoryTheory.Functor C Ab) →
          [inst_2 : (i : C) → Module ↑(R.obj i) ↑(M.obj i)] →
            (∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
                (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
                  (CategoryTheory.ConcreteCategory.hom (R.map f)) r •
                    (CategoryTheory.ConcreteCategory.hom (M.map f)) m) →
              (R.comp (CategoryTheory.forget RingCat)).ColimitType →
                (M.comp (CategoryTheory.forget Ab)).ColimitType → (M.comp (CategoryTheory.forget Ab)).ColimitType
-- Aesop.Stats.Basic
/-- Total elapsed time of successful applications of a rule.
 -/
Aesop.RuleStatsTotals.elapsedSuccessful : Aesop.RuleStatsTotals → Aesop.Nanos
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSigma.match_3.eq_2 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → Fin (Fin.sum f) → Sort u_1) (n : ℕ) (f : Fin (n + 1) → ℕ) (x : ℕ)
  (hx : x < Fin.sum f) (h_1 : (x : Fin 0 → ℕ) → (val : ℕ) → (h : val < Fin.sum x) → motive 0 x ⟨val, h⟩)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : ℕ) → (hx : x < Fin.sum f) → motive n.succ f ⟨x, hx⟩),
  (match n.succ, f, ⟨x, hx⟩ with
    | 0, x, ⟨val, h⟩ => h_1 x val h
    | n.succ, f, ⟨x, hx⟩ => h_2 n f x hx) =
    h_2 n f x hx
-- Mathlib.Data.Finset.Finsupp
Finsupp.mem_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {f : ι →₀ Finset α} {g : ι →₀ α}, g ∈ f.pi ↔ ∀ (i : ι), g i ∈ f i
-- Mathlib.Algebra.Homology.HasNoLoop
/-- The condition that `c.Rel i i` does not hold for any `i`.  -/
ComplexShape.HasNoLoop : {ι : Type u_1} → ComplexShape ι → Prop
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.equal.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (t₁ t₂ : L.Term α),
  t₁.equal t₂ = (FirstOrder.Language.Term.relabel Sum.inl t₁).bdEqual (FirstOrder.Language.Term.relabel Sum.inl t₂)
-- Mathlib.Data.Set.Lattice
Set.iUnion_ofPred : ∀ {α : Type u_1} {ι : Sort u_5} (P : ι → α → Prop), ⋃ i, {x | P i x} = {x | ∃ i, P i x}
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Algebra.IsAlgebraic.isTranscendenceBasis_iff : ∀ {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ι → A} (S : Type u_5) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsAlgebraic R S], IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x
-- Lean.Meta.Tactic.Grind.Injective
_private.Lean.Meta.Tactic.Grind.Injective.0.Lean.Meta.Grind.getSymbols.go : Lean.Expr → StateRefT' IO.RealWorld Lean.NameSet Lean.MetaM Unit
-- Mathlib.Logic.Relation
Relation.ReflTransGen.lift' : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} (f : α → β),
  r ≤ Function.onFun (Relation.ReflTransGen p) f → Relation.ReflTransGen r ≤ Function.onFun (Relation.ReflTransGen p) f
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instInfTopHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β],
  InfTopHomClass (InfTopHom α β) α β
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_fun_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : MeasurableSpace γ}
  {f : α ⊕ β → γ}, Measurable (f ∘ Sum.inl) → Measurable (f ∘ Sum.inr) → Measurable f
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Precoverage C},
  x.coverings = y.coverings → x = y
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zip_cons_cons : ∀ {α : Type u} {s s' : Stream'.Seq α} {x x' : α},
  (Stream'.Seq.cons x s).zip (Stream'.Seq.cons x' s') = Stream'.Seq.cons (x, x') (s.zip s')
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.continuous : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → Continuous f
-- Mathlib.Data.Sym.Sym2.Order
/-- In a linear order, symmetric squares are canonically identified with ordered pairs.  -/
Sym2.sortEquiv : {α : Type u_1} → [inst : LinearOrder α] → Sym2 α ≃ { p // p.1 ≤ p.2 }
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.instEmptyCollection : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Lean.PersistentHashSet α)
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Also see `Module.finrank_top_le_finrank_of_isScalarTower`
for a version with different typeclass constraints.  -/
Module.finrank_top_le_finrank_of_isScalarTower_of_free : ∀ (R : Type u) (S : Type u_1) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [StrongRankCondition R] [inst_4 : Semiring S] [StrongRankCondition S] [inst_6 : Module S M] [inst_7 : Module R S]
  [FaithfulSMul R S] [Module.Finite R S] [IsScalarTower R S S] [IsScalarTower R S M] [Module.Free S M],
  Module.finrank S M ≤ Module.finrank R M
-- Mathlib.Algebra.Order.Module.HahnEmbedding
FiniteArchimedeanClass.closedBall.congr_simp : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M] (c c_1 : FiniteArchimedeanClass M),
  c = c_1 → FiniteArchimedeanClass.closedBall K c = FiniteArchimedeanClass.closedBall K c_1