mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_ofSliceFrom_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  q < String.Slice.Pos.ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h < p
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The homeomorphism between `X ⨯ Y` and the set-theoretic product of `X` and `Y`,
equipped with the product topology.
 -/
TopCat.prodIsoProd : (X Y : TopCat) → X ⨯ Y ≅ TopCat.of (↑X × ↑Y)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_induction : ∀ {M : Type u_3} [inst : CommMonoid M] (p : M → Prop) (s : Multiset M),
  (∀ (a b : M), p a → p b → p (a * b)) → p 1 → (∀ a ∈ s, p a) → p s.prod
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- The essential data of the nerve functor is contained in the 2-truncation, which is
recorded by the composite functor `nerveFunctor₂`.  -/
CategoryTheory.Nerve.nerveFunctor₂ : CategoryTheory.Functor CategoryTheory.Cat (SSet.Truncated 2)
-- Aesop.Tree.Data
Aesop.NodeState.unprovable : Aesop.NodeState
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsPosSemidef.add : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Preorder R] [AddLeftMono R] {B C : LinearMap.BilinForm R M},
  B.IsPosSemidef → C.IsPosSemidef → (B + C).IsPosSemidef
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.coe_of : ∀ (C : CategoryTheory.Cat), CategoryTheory.Cat.of ↑C = C
-- Mathlib.Data.List.Basic
/-- **Alias** of `List.setOfPred_mem_cons`. -/
List.set_of_mem_cons : ∀ {α : Type u} (l : List α) (a : α), {x | x ∈ a :: l} = insert a {x | x ∈ l}
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → List α → Sort u_2) (l₂ acc : List α)
  (h_1 : (l₂ acc : List α) → motive [] l₂ acc) (h_2 : (l₁ acc : List α) → motive l₁ [] acc)
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys acc : List α) → motive (x :: xs) (y :: ys) acc),
  (match [], l₂, acc with
    | [], l₂, acc => h_1 l₂ acc
    | l₁, [], acc => h_2 l₁ acc
    | x :: xs, y :: ys, acc => h_3 x xs y ys acc) =
    h_1 l₂ acc
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- The dilatransvection associated with a linear form `f`
and a vector `v` such that `1 + f v` is a unit.  -/
LinearEquiv.dilatransvection : {R : Type u_1} →
  {V : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → {f : Module.Dual R V} → {v : V} → IsUnit (1 + f v) → V ≃ₗ[R] V
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.Spec.birdDetSpec_zero : ∀ {R : Type u_1} [inst : CommRing R] (A : Matrix (Fin 0) (Fin 0) R), BirdDet.Spec.birdDet A = 1
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.orderIsoMapComap_symm_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M'),
  (RelIso.symm (LieSubmodule.orderIsoMapComap e)) N' = LieSubmodule.comap e.toLieModuleHom N'
-- Mathlib.Topology.Separation.Hausdorff
CompactExhaustion.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] (K : CompactExhaustion X) (n : ℕ), IsClosed (K n)
-- Init.Data.Array.Find
Array.false_of_mem_extract_findIdx : ∀ {α : Type u_1} {x : α} {xs : Array α} {p : α → Bool}, x ∈ xs.extract 0 (Array.findIdx p xs) → p x = false
-- Lean.Elab.InfoTree.Types
/-- Base structure for `TermInfo`, `CommandInfo` and `TacticInfo`.  -/
Lean.Elab.ElabInfo : Type
-- Mathlib.Algebra.Homology.ShortComplex.Linear
/-- Given a homology map data for a morphism `φ`, this is the induced homology
map data for `a • φ`.  -/
CategoryTheory.ShortComplex.HomologyMapData.smul : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            {S₁ S₂ : CategoryTheory.ShortComplex C} →
              {φ : S₁ ⟶ S₂} →
                {h₁ : S₁.HomologyData} →
                  {h₂ : S₂.HomologyData} →
                    CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                      (a : R) → CategoryTheory.ShortComplex.HomologyMapData (a • φ) h₁ h₂
-- Mathlib.Data.PFun
PFun.fixInduction_spec : ∀ {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
  (H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'),
  PFun.fixInduction h H = H a h fun x h' => PFun.fixInduction ⋯ H
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Pair.mk.injEq : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι}
  (toPair : Monoid.CoprodI.Word.Pair G i)
  (normalized : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ toPair.tail.toList → g ∈ d.set i_1)
  (toPair_1 : Monoid.CoprodI.Word.Pair G i)
  (normalized_1 : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ toPair_1.tail.toList → g ∈ d.set i_1),
  ({ toPair := toPair, normalized := normalized } = { toPair := toPair_1, normalized := normalized_1 }) =
    (toPair = toPair_1)
-- Init.Data.Vector.Lemmas
/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices.  -/
Vector.getElem?_reverse' : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ}, i + j + 1 = n → xs.reverse[i]? = xs[j]?
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_π_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_3 : Finite J]
  (F : J → CategoryTheory.Idempotents.Karoubi C) (j : J),
  ((CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).π j).f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map fun j => (F j).p)
      ((CategoryTheory.Limits.biproduct.bicone fun j => (F j).X).π j)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- Copy of a `Subcomplex` with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Topology.RelCWComplex.Subcomplex.copy : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [inst : Topology.RelCWComplex C D] →
        (E : Topology.RelCWComplex.Subcomplex C) →
          (F : Set X) →
            F = ↑E → (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) → J = E.I → Topology.RelCWComplex.Subcomplex C
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyπ_comp_asIsoHomologyπ_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp S.homologyπ (S.asIsoHomologyπ hf).inv = CategoryTheory.CategoryStruct.id S.cycles
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.comp_isClosedEmbedding : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : Zero β] {f : α → β},
  HasCompactSupport f → ∀ {g : α' → α}, Topology.IsClosedEmbedding g → HasCompactSupport (f ∘ g)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldl_eq_foldl_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : δ → α → β → δ}
  {init : δ}, Std.TreeMap.Raw.foldl f init t = Array.foldl (fun a b => f a b.1 b.2) init t.toArray
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `J(a | b)` is `-1`, then `a` is not a square modulo `b`.  -/
ZMod.nonsquare_of_jacobiSym_eq_neg_one : ∀ {a : ℤ} {b : ℕ}, jacobiSym a b = -1 → ¬IsSquare ↑a
-- Init.Data.Int.Linear
Int.Internal.Linear.instInhabitedExpr : Inhabited Int.Internal.Linear.Expr
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hadj : G.Adj v w),
  (G.subgraphOfAdj hadj).spanningCoe = SimpleGraph.fromEdgeSet {s(v, w)}
-- Init.Data.List.Basic
/-- Returns the longest initial segment of `xs` for which `p` returns true.

`O(|xs|)`.

Examples:
* `[7, 6, 4, 8].takeWhile (· > 5) = [7, 6]`
* `[7, 6, 6, 5].takeWhile (· > 5) = [7, 6, 6]`
* `[7, 6, 6, 8].takeWhile (· > 5) = [7, 6, 6, 8]`
 -/
List.takeWhile : {α : Type u} → (α → Bool) → List α → List α
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : NormedAddCommGroup G'] [inst_5 : PartialOrder G'] [inst_6 : NormedSpace ℝ G'] [ClosedIciTopology G'']
  [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ {f g : α → G'},
      MeasureTheory.Integrable f μ →
        MeasureTheory.Integrable g μ → f ≤ᵐ[μ] g → MeasureTheory.setToFun μ T hT f ≤ MeasureTheory.setToFun μ T hT g
-- Mathlib.Data.Int.Init
Int.le_div_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, c < 0 → c ∣ b → (a ≤ b / c ↔ b ≤ c * a)
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzMul.C.eq_1 : ∀ (β : Type u_2) [inst : PseudoMetricSpace β] [inst_1 : Monoid β] [_i : LipschitzMul β],
  LipschitzMul.C β = Classical.choose ⋯
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapEquiv_symm : ∀ {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [inst : CommSemiring S₁] [inst_1 : CommSemiring S₂] (e : S₁ ≃+* S₂),
  (MvPolynomial.mapEquiv σ e).symm = MvPolynomial.mapEquiv σ e.symm
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- Another version of `simply_connected_iff_paths_homotopic`  -/
simply_connected_iff_paths_homotopic' : ∀ {Y : Type u_2} [inst : TopologicalSpace Y],
  SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.δ₀_mk₂_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0))
      (CategoryTheory.ComposableArrows.mk₂ f g) =
    CategoryTheory.ComposableArrows.mk₁ g
-- Mathlib.Data.Real.Basic
Real.instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid ℝ
-- Mathlib.Order.Filter.Pointwise
Filter.bot_add : ∀ {α : Type u_2} [inst : Add α] {g : Filter α}, ⊥ + g = ⊥
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the generation of the given term. Is assumes it has been internalized  -/
Lean.Meta.Grind.getGeneration : Lean.Expr → Lean.Meta.Grind.GoalM ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ1728_j : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (IsUnit 2)], (WeierstrassCurve.ofJ1728 R).j = 1728
-- Mathlib.Order.Hom.Bounded
BotHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] (f : BotHom α β), (BotHom.id β).comp f = f
-- Mathlib.Analysis.InnerProductSpace.Defs
_private.Mathlib.Analysis.InnerProductSpace.Defs.0.InnerProductSpace.Core.«term⟪_,_⟫» : Lean.ParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ ∪ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Topology.Clopen
isClopen_iUnion_of_finite : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Sort u_2} [Finite Y] {s : Y → Set X},
  (∀ (i : Y), IsClopen (s i)) → IsClopen (⋃ i, s i)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.center_eq_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G},
  AddSubgroup.closure s = ⊤ → AddSubgroup.center G = ⨅ g ∈ s, AddSubgroup.centralizer {g}
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given an element `m : M.Elements` of a presheaf of modules `M`, this is the
canonical inclusion `m.freeYoneda ⟶ M.freeYonedaCoproduct`.  -/
PresheafOfModules.ιFreeYonedaCoproduct : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : PresheafOfModules R) → (m : M.Elements) → m.freeYoneda ⟶ M.freeYonedaCoproduct
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.prevn.eq_1 : ∀ (x : Substring.Raw) (x_1 : String.Pos.Raw), x.prevn 0 x_1 = x_1
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_self : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subgroupOf H = ⊤
-- Lean.Meta.Basic
Lean.Meta.MetaM.run : {α : Type} →
  Lean.MetaM α → optParam Lean.Meta.Context { } → optParam Lean.Meta.State { } → Lean.CoreM (α × Lean.Meta.State)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.omap.eq_2 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) (a : α) (b : β), Stream'.Seq.omap f (some (a, b)) = some (a, f b)
-- Mathlib.Algebra.Field.Basic
OrderDual.instDivisionSemiring : {K : Type u_1} → [DivisionSemiring K] → DivisionSemiring Kᵒᵈ
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.entityTooLarge.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.entityTooLarge = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.entryAtIdxD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : (a : α) × β a}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.entryAtIdxD i fallback = t₂.entryAtIdxD i fallback
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M]
  {φ ψ : L.BoundedFormula α n},
  φ.IsQF → ψ.IsPrenex → ∀ {v : α → M} {xs : Fin n → M}, (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs
-- Mathlib.Data.DFinsupp.Module
DFinsupp.equivProdDFinsupp_smul : ∀ {ι : Type u} {γ : Type w} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)]
  [inst_1 : (i : Option ι) → SMulZeroClass γ (α i)] (r : γ) (f : Π₀ (i : Option ι), α i),
  DFinsupp.equivProdDFinsupp (r • f) = r • DFinsupp.equivProdDFinsupp f
-- Init.Data.Array.Lemmas
Array.flatMap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Array γ} {xs : Array α},
  Array.flatMap g (Array.map f xs) = Array.flatMap (fun a => g (f a)) xs
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.snd
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) S.hom) T.hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) h)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.comp_assoc : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] {δ : Type u_2} [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] [inst_4 : Zero δ] (f : ZeroAtInftyContinuousMap γ δ)
  (g : CocompactMap β γ) (h : CocompactMap α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `smul_apply`. -/
SlashInvariantForm.smul_applyℝ : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.FieldTheory.Extension
/-- A chain of lifts has an upper bound.  -/
IntermediateField.Lifts.exists_upper_bound : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (c : Set (IntermediateField.Lifts F E K)),
  IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ ub, ∀ a ∈ c, a ≤ ub
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Submodule.traceDual_le_span_map_traceDual : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [inst_21 : IsScalarTower R₁ B L] [IsScalarTower R₂ B L]
  [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂]
  [Module.IsTorsionFree R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [inst_28 : IsScalarTower A R₂ ↥F₂]
  [inst_29 : IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂]
  [Algebra.IsSeparable (↥F₁) L] [Module.Free A R₂]
  [IsLocalization (Algebra.algebraMapSubmonoid R₂ (nonZeroDivisors A)) ↥F₂],
  F₁.LinearDisjoint ↥F₂ →
    F₁ ⊔ F₂ = ⊤ →
      Submodule.restrictScalars R₁ (Submodule.traceDual R₁ (↥F₁) 1) ≤
        Submodule.span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(Submodule.traceDual A K 1))
-- Mathlib.Order.Atoms
instIsStronglyCoatomicOfPredOrder : ∀ {α : Type u_4} [inst : Preorder α] [PredOrder α], IsStronglyCoatomic α
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The kernel of a reproducing kernel Hilbert space is a matrix of entries given by the
kernel functions.  -/
RKHS.kernel : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            (H : Type u_4) →
              [inst_3 : NormedAddCommGroup H] →
                [inst_4 : InnerProductSpace 𝕜 H] →
                  [RKHS 𝕜 H X V] → [CompleteSpace H] → [CompleteSpace V] → Matrix X X (V →L[𝕜] V)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- A `PComp` stores a linear comparison `Σ cᵢ*xᵢ R 0`,
along with information about how this comparison was derived.
The original expressions fed into `linarith` are each assigned a unique natural number label.
The *historical set* `PComp.history` stores the labels of expressions
that were used in deriving the current `PComp`.
Variables are also indexed by natural numbers. The sets `PComp.effective`, `PComp.implicit`,
and `PComp.vars` contain variable indices.
* `PComp.vars` contains the variables that appear in any inequality in the historical set.
* `PComp.effective` contains the variables that have been effectively eliminated from `PComp`.
  A variable `n` is said to be *effectively eliminated* in `p : PComp` if the elimination of `n`
  produced at least one of the ancestors of `p` (or `p` itself).
* `PComp.implicit` contains the variables that have been implicitly eliminated from `PComp`.
  A variable `n` is said to be *implicitly eliminated* in `p` if it satisfies the following
  properties:
  - `n` appears in some inequality in the historical set (i.e. in `p.vars`).
  - `n` does not appear in `p.c.vars` (i.e. it has been eliminated).
  - `n` was not effectively eliminated.

We track these sets in order to compute whether the history of a `PComp` is *minimal*.
Checking this directly is expensive, but effective approximations can be defined in terms of these
sets. During the variable elimination process, a `PComp` with non-minimal history can be discarded.
 -/
Mathlib.Tactic.Linarith.PComp : Type
-- Std.Internal.Do.WP.Basic
/-- The weakest precondition interpretation of `m` at every result type.  -/
Std.Internal.Do.WPMonad.toWP : {m : Type u → Type v} →
  {Pred : outParam (Type w)} →
    {EPred : outParam (Type w')} →
      {inst : Monad m} →
        {inst_1 : Std.Internal.Do.Assertion Pred} →
          {inst_2 : Std.Internal.Do.Assertion EPred} →
            [self : Std.Internal.Do.WPMonad m Pred EPred] → (α : Type u) → Std.Internal.Do.WP (m α) α Pred EPred
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.DocM.exec.buildContext : Lean.Expr → Lean.Syntax → Lean.Elab.TermElabM (Lean.LocalContext × Lean.LocalInstances)
-- Init.Data.Nat.Lemmas
Nat.add_pos_iff_pos_or_pos : ∀ {m n : ℕ}, 0 < m + n ↔ 0 < m ∨ 0 < n
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_sub : ∀ (a b : UInt32), (a - b).toUInt8 = a.toUInt8 - b.toUInt8
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a b : α}, (a == b) = true → m[a]? = m[b]?
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ElimStatus.failure : List Lean.Expr → Mathlib.Tactic.Choose.ElimStatus
-- Std.Sync.Channel
/-- Send a value through the channel, returning a task that will resolve once the transmission could be
completed.
 -/
Std.Channel.send : {α : Type} → Std.Channel α → α → BaseIO (Task Unit)
-- Mathlib.Algebra.Ring.Parity
Nat.even_sub' : ∀ {m n : ℕ}, n ≤ m → (Even (m - n) ↔ (Odd m ↔ Odd n))
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` as a functor from `R`-Hopf algebras to group schemes over `Spec R`.  -/
AlgebraicGeometry.hopfSpec : (R : CommRingCat) →
  CategoryTheory.Functor (CommHopfAlgCat ↑R)ᵒᵖ (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec R)))
-- Std.Http.Data.Body.Empty
Std.Http.Body.Empty.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.count_support_of_mem : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v},
  c.IsCycle → u ∈ c.support → u ≠ v → List.count u c.support = 1
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instHasTwoOutOfThreePropertyWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopicalAlgebra.weakEquivalences (CochainComplex.Plus C)).HasTwoOutOfThreeProperty
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.add_mem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x y : K), x ∈ A → y ∈ A → x + y ∈ A
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_inf_support_coeff_multisetProd : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T},
  0 ≤ degt 0 →
    (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
      ∀ (m : Multiset (AddMonoidAlgebra R A)),
        (Multiset.map (fun f => f.coeff.support.inf degt) m).sum ≤ m.prod.coeff.support.inf degt
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.assumption.injEq : ∀ (s : Lean.Omega.Constraint) (x : Lean.Omega.Coeffs) (i i_1 : ℕ),
  (Lean.Elab.Tactic.Omega.Justification.assumption s x i = Lean.Elab.Tactic.Omega.Justification.assumption s x i_1) =
    (i = i_1)
-- Mathlib.Topology.Bornology.Absorbs
absorbs_biUnion_finset : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
  {I : Finset ι}, Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)