mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_inv_fst_apply : ∀ (X Y : TopCat) (x : ↑X × ↑Y),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst)
      ((CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).inv) x) =
    x.1
-- Init.Data.String.Slice
/-- Checks whether a slice has a match of the pattern `pat` anywhere.

This function is generic over all currently supported patterns.

Examples:

* `"coffee tea water".toSlice.contains Char.isWhitespace = true`

* `"tea".toSlice.contains (fun (c : Char) => c == 'X') = false`

* `"coffee tea water".toSlice.contains "tea" = true`
 -/
String.Slice.contains : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        String.Slice → (pat : ρ) → [String.Slice.Pattern.ToForwardSearcher pat σ] → Bool
-- Init.Data.List.Basic
/-- Checks whether `a` is an element of `as`, using `==` to compare elements.

`O(|as|)`. `List.elem` is a synonym that takes the element before the list.

The preferred simp normal form is `l.contains a`, and when `LawfulBEq α` is available,
`l.contains a = true ↔ a ∈ l` and `l.contains a = false ↔ a ∉ l`.

Examples:
* `[1, 4, 2, 3, 3, 7].contains 3 = true`
* `List.contains [1, 4, 2, 3, 3, 7] 5 = false`
 -/
List.contains : {α : Type u} → [BEq α] → List α → α → Bool
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.mem_codChart_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), f x ∈ h.codChart.source
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If `g : Y ⟶ S` is in the presieve given by the indexed family `fᵢ`, this is a choice
of index such that `g = fᵢ` modulo `eqToHom`.
Note: This should generally not be used! If possible, use the induction principle
for the type `Presieve.ofArrows` instead (using e.g., `rintro / obtain`).  -/
CategoryTheory.Presieve.ofArrows.idx : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ι : Type u_1} →
      {S : C} →
        {X : ι → C} → {f : (i : ι) → X i ⟶ S} → {Y : C} → {g : Y ⟶ S} → CategoryTheory.Presieve.ofArrows X f g → ι
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.List.getElem?_takeWhile : ∀ {α : Type u_1} {l : List α} {P : α → Bool} {k : ℕ},
  (List.takeWhile P l)[k]? = if ∀ k' ≤ k, Option.any P l[k']? = true then l[k]? else none
-- Mathlib.Topology.MetricSpace.Basic
Metric.isClosedEmbedding_of_pairwise_le_dist : ∀ {γ : Type w} [inst : MetricSpace γ] {α : Type u_2} [inst_1 : TopologicalSpace α] [DiscreteTopology α] {ε : ℝ},
  0 < ε → ∀ {f : α → γ}, (Pairwise fun x y => ε ≤ dist (f x) (f y)) → Topology.IsClosedEmbedding f
-- Mathlib.Algebra.Quaternion
Quaternion.instSMulCommClass : ∀ {S : Type u_1} {T : Type u_2} {R : Type u_3} [inst : CommRing R] [inst_1 : SMul S R] [inst_2 : SMul T R]
  [SMulCommClass S T R], SMulCommClass S T (Quaternion R)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
/-- If `HasEnoughRootsOfUnity M n` and `m ∣ n`, then also `HasEnoughRootsOfUnity M m`.  -/
HasEnoughRootsOfUnity.of_dvd : ∀ (M : Type u_1) [inst : CommMonoid M] {m n : ℕ} [NeZero n],
  m ∣ n → ∀ [HasEnoughRootsOfUnity M n], HasEnoughRootsOfUnity M m
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.SeparatingLeft.toBilin' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {M : Matrix ι ι R₂},
  M.SeparatingLeft → LinearMap.SeparatingLeft (Matrix.toBilin' M)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
/-- The frontier of a closed strictly convex set only contains trivial arithmetic progressions.
The idea is that an arithmetic progression is contained on a line and the frontier of a strictly
convex set does not contain lines.  -/
threeAPFree_frontier : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace E] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] {s : Set E},
  IsClosed s → StrictConvex 𝕜 s → ThreeAPFree (frontier s)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M` and a localization map
`g : M →+ P` for the same submonoid, the homomorphism
induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`.  -/
AddSubmonoid.LocalizationMap.lift_localizationMap_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) (x : M) (y : ↥S),
  (f.lift ⋯) (f.mk' x y) = g.mk' x y
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.isFaithful_iff' : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.IsFaithful R L M ↔ ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical `R`-linear inclusion `M → TrivSqZeroExt R M`.  -/
TrivSqZeroExt.inrHom : (R : Type u) →
  (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] TrivSqZeroExt R M
-- Lean.Message
Lean.MessageSeverity.information : Lean.MessageSeverity
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of a `C^n` function at a point and a constant is `C^n` at this
point.  -/
ContDiffAt.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {A : Type u_4} [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsScalarTower 𝕜 A F]
  [IsBoundedSMul A F] {f : E → A} {x : E}, ContDiffAt 𝕜 n f x → ∀ (v : F), ContDiffAt 𝕜 n (fun y => f y • v) x
-- Std.Http.Data.URI.Basic
Std.Http.instInhabitedURI : Inhabited Std.Http.URI
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.sliceFrom_eq_startPos : ∀ {s : String.Slice} {p : s.Pos}, p.sliceFrom p ⋯ = (s.sliceFrom p).startPos
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.hasLeftKanExtension_of_preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [L.HasLeftKanExtension F] [G.PreservesLeftKanExtension F L],
  L.HasLeftKanExtension (F.comp G)
-- Lean.Exception
Lean.instMonadRecDepthMonadCacheTOfMonad : {α : Type} →
  {m : Type → Type} →
    {ω β : Type} →
      [inst : BEq α] →
        [inst_1 : Hashable α] →
          [Monad m] → [inst_3 : STWorld ω m] → [Lean.MonadRecDepth m] → Lean.MonadRecDepth (Lean.MonadCacheT α β m)
-- Lean.Parser.Term
Lean.Parser.Term.structInstDefault.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.RArray
Lean.RArray.leaf.injEq : ∀ {α : Type u} (a a_1 : α), (Lean.RArray.leaf a = Lean.RArray.leaf a_1) = (a = a_1)
-- Mathlib.Topology.Order.LeftRightLim
leftLim_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {a : α},
  Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds (Function.leftLim f a)) →
    Function.leftLim (Function.leftLim f) a = Function.leftLim f a
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Postcomposing of a 1-morphism seen as a strong transformation between pseudofunctors.  -/
CategoryTheory.Bicategory.postcomp₂ : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → (a ⟶ b) → (CategoryTheory.Bicategory.yoneda₀ a ⟶ CategoryTheory.Bicategory.yoneda₀ b)
-- Mathlib.Order.CountableSupClosed
countableSupClosure_empty : ∀ {α : Type u_2} [inst : Preorder α], countableSupClosure ∅ = ∅
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalAlgHom.range.congr_simp : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (φ φ_1 : F), φ = φ_1 → NonUnitalAlgHom.range φ = NonUnitalAlgHom.range φ_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.CategoryTheory.Subobject.Types
/-- The category of `MonoOver α`, for `α : Type u`, is equivalent to the partial order `Set α`.
 -/
Types.monoOverEquivalenceSet : (α : Type u) → CategoryTheory.MonoOver α ≌ Set α
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_not_equiv_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f g : CauSeq β abv}, ¬f ≈ 0 → ¬g ≈ 0 → ¬f * g ≈ 0
-- Lean.MonadEnv
Lean.isEnumType : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Bool
-- Mathlib.SetTheory.Cardinal.Order
/-- Any type can be endowed with a well order, obtained by pulling back the well order over
cardinals by some embedding.  -/
WellOrderingRel : {α : Type u} → α → α → Prop
-- Mathlib.Algebra.Ring.Associator
AddMonoidHom.mulLeft₃_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (x y z : R), ((AddMonoidHom.mulLeft₃ x) y) z = x * y * z
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_const_smul_iff₀ : ∀ {G₀ : Type u_3} {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  [inst_2 : GroupWithZero G₀] [inst_3 : MulAction G₀ β] [MeasurableConstSMul G₀ β] {c : G₀},
  c ≠ 0 → ((Measurable fun x => c • f x) ↔ Measurable f)
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_sup_sup_boundary_inf : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a b : α),
  Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b) = Coheyting.boundary a ⊔ Coheyting.boundary b
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.eq_1 : ∀ {α : Type u_1} (f : α → α) (n : ℕ) (x : α), Function.IsPeriodicPt f n x = Function.IsFixedPt f^[n] x
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.measure_support_lt_top_of_memLp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {p : ENNReal} (f : MeasureTheory.SimpleFunc α E),
  MeasureTheory.MemLp (⇑f) p μ → p ≠ 0 → p ≠ ⊤ → μ (Function.support ⇑f) < ⊤
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.locallySmall_of_univLE : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [UnivLE.{v, w}], CategoryTheory.LocallySmall.{w, v, u} C
-- Init.Data.UInt.Bitwise
UInt16.toUInt64_shiftLeft_of_lt : ∀ (a b : UInt16), b < 16 → (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 65536
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.subcomplex_le_horn_iff : ∀ {n : ℕ} (A : (SSet.stdSimplex.obj { len := n + 1 }).Subcomplex) (i : Fin (n + 2)),
  A ≤ SSet.horn (n + 1) i ↔ ¬SSet.stdSimplex.face {i}ᶜ ≤ A
-- Std.Do.Internal.Ensures.Def
/-- For each `x`, the attached version is bind-faithful with `x`.  -/
Std.Do.Internal.IsAttach.erases : ∀ {m : Type u → Type v} [inst : Bind m] {attach : ⦃α : Type u⦄ → (x : m α) → m { a // Std.Do.Internal.MayReturn x a }},
  Std.Do.Internal.IsAttach attach → ∀ {α : Type u} (x : m α), Std.Do.Internal.ErasesTo (attach x) x
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- `Fintype.linearCombination R v f` is the linear combination of vectors in `v` with weights
in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.

This map is linear in `v` if `R` is commutative, and always linear in `f`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
 -/
Fintype.linearCombination : {α : Type u_1} →
  {M : Type u_2} →
    (R : Type u_3) →
      [Fintype α] → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α → M) → (α → R) →ₗ[R] M
-- Mathlib.Order.Category.LinOrd
LinOrd.coe_id : ∀ {X : LinOrd}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.coordChange_self : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R B F ι) (i : ι),
  ∀ x ∈ self.baseSet i, ∀ (v : F), (self.coordChange i i x) v = v
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDerivWithin' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s t : Set E} {x : E},
  ω₁ =ᶠ[nhdsWithin x s] ω₂ → t ⊆ s → extDerivWithin ω₁ t =ᶠ[nhdsWithin x s] extDerivWithin ω₂ t
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_list_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  {l : List (α × β)},
  (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m₁ l)).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) (↑m₁) l)
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.functorProdToProdFunctorAssociator_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : CategoryTheory.Functor A ((C × D) × E)),
  (CategoryTheory.prod.functorProdToProdFunctorAssociator C D E A).inv.app X =
    CategoryTheory.Prod.mkHom
      (CategoryTheory.CategoryStruct.id
        ((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.fst C (D × E))))
      (CategoryTheory.Prod.mkHom
        (CategoryTheory.CategoryStruct.id
          (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp
            (CategoryTheory.Prod.fst D E)))
        (CategoryTheory.CategoryStruct.id
          (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp
            (CategoryTheory.Prod.snd D E))))
-- Init.Data.Vector.Attach
Vector.pmap_eq_map_attach : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a),
  Vector.pmap f xs H = Vector.map (fun x => f ↑x ⋯) xs.attach
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableSafeRules : Aesop.LocalRuleSet →
  Aesop.ForwardRuleMatches → Lean.MVarId → Aesop.BaseM (Array (Aesop.IndexMatchResult Aesop.SafeRule))
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Module.End.ker_pow_le_ker_pow_finrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (f : Module.End K V) (m : ℕ), LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ Module.finrank K V)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toAddMonoidHom_refl : ∀ {R : Type u_4} [inst : NonAssocSemiring R], (RingEquiv.refl R).toAddMonoidHom = AddMonoidHom.id R
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.mk.sizeOf_spec : ∀ (trueExpr falseExpr natZExpr btrueExpr bfalseExpr ordEqExpr intExpr : Lean.Expr),
  sizeOf
      { trueExpr := trueExpr, falseExpr := falseExpr, natZExpr := natZExpr, btrueExpr := btrueExpr,
        bfalseExpr := bfalseExpr, ordEqExpr := ordEqExpr, intExpr := intExpr } =
    1 + sizeOf trueExpr + sizeOf falseExpr + sizeOf natZExpr + sizeOf btrueExpr + sizeOf bfalseExpr + sizeOf ordEqExpr +
      sizeOf intExpr
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint, then any `F`-linearly independent family on `L` remains
linearly independent over `A`.  -/
IntermediateField.LinearDisjoint.linearIndependent_right' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ {ι : Type u_1} {b : ι → L}, LinearIndependent F b → LinearIndependent (↥A) (⇑(algebraMap L E) ∘ b)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmod_congr_of_sub_mem_span_aux : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) (a b : ℤ),
  x - ↑a ∈ Ideal.span {↑p ^ n} → x - ↑b ∈ Ideal.span {↑p ^ n} → ↑a = ↑b
-- Mathlib.Order.Basic
PartialOrder.toPreorder_injective : ∀ {α : Type u_2}, Function.Injective (@PartialOrder.toPreorder α)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum.eq_1 : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M) (g : α → M → N),
  f.sum g = ∑ a ∈ f.support, g a (f a)
-- Mathlib.Algebra.Group.Basic
sub_eq_of_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = c + b → a - b = c
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommGroupWithZero.toNontrivial : ∀ {α : Type u_3} [self : LinearOrderedCommGroupWithZero α], Nontrivial α
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.BackwardSliceSearcher.endsWith_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → String.Slice.Pattern.BackwardPattern.endsWith pat s = true
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ 0 → ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∃ x ∈ s, p x
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.one_apply : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (m : M), 1 m = m
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instHasLimit : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))], CategoryTheory.Limits.HasLimit F
-- Mathlib.Topology.Algebra.UniformConvergence
instDivUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Div β],
  instDivUniformOnFun = { div := instDivUniformOnFun._aux_1 }
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castLE_uIcc : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.image (Fin.castLE h) (Finset.uIcc a b) = Finset.uIcc (Fin.castLE h a) (Fin.castLE h b)
-- Lean.Compiler.IR.Basic
/-- Extra information associated with a declaration.  -/
Lean.IR.DeclInfo : Type
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
midpoint_le_right : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E}, midpoint k a b ≤ b ↔ a ≤ b
-- Mathlib.Data.List.Infix
List.isPrefix_append_of_length : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.length ≤ l₂.length → (l₁ <+: l₂ ++ l₃ ↔ l₁ <+: l₂)
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- **Alias** of the reverse direction of `Matrix.one_fromRows_isTotallyUnimodular_iff`. -/
Matrix.IsTotallyUnimodular.one_fromRows : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq n] (A : Matrix m n R),
  A.IsTotallyUnimodular → (Matrix.fromRows 1 A).IsTotallyUnimodular
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_apply : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.normSq z = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} (S : C)
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (X_1 : F.DescentData f) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso F S).hom.app X_1).hom i =
    (F.mapId { as := Opposite.op (X i) }).hom.toNatTrans.app (X_1.obj i)
-- Init.Data.Int.Lemmas
_private.Init.Data.Int.Lemmas.0.Int.negSucc_mul_negSucc' : ∀ (m n : ℕ), Int.negSucc m * Int.negSucc n = Int.ofNat (m.succ * n.succ)
-- Mathlib.Data.List.Basic
List.getLastI.eq_1 : ∀ {α : Type u_1} [inst : Inhabited α], [].getLastI = default
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a b : β),
  ⇑e ⁻¹' Set.Ico a b = Set.Ico (e.symm a) (e.symm b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp inr (hP.desc h k w) = k
-- Init.Data.Array.Lemmas
/-- Variant of `foldrM_push` with `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
 -/
Array.foldrM_push' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β} {xs : Array α}
  {a : α} {start : ℕ},
  start = xs.size + 1 →
    Array.foldrM f init (xs.push a) start = do
      let init ← f a init
      Array.foldrM f init xs