mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_interior_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} {s : Affine.Simplex k P n} {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ s.interior ↔ ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1)
-- Mathlib.Data.Tree.Basic
instDecidableEqBinaryTree.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : BinaryTree α) → Decidable (x = x_1)
-- Lean.Meta.Tactic.Simp.Main
/-- For `rfl` theorems and simprocs, there might not be an explicit reference in the proof term, so
we record (all non-builtin) usages explicitly.
 -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.recordSimpUses : Lean.Meta.Simp.State → Lean.MetaM Unit
-- Mathlib.Algebra.Free
FreeAddMagma.length.eq_2 : ∀ {α : Type u} (x_1 y : FreeAddMagma α), (x_1.add y).length = x_1.length + y.length
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.eapprox_lt_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal) (n : ℕ) (a : α),
  (MeasureTheory.SimpleFunc.eapprox f n) a < ⊤
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balanceL_eq_balance' : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Balanced →
    r.Balanced →
      l.Sized →
        r.Sized →
          ((∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨
              ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r') →
            l.balanceL x r = l.balance' x r
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_eq_sum_sq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] [inst_2 : Fintype α] (s t : Finset α),
  s.mulEnergy t = ∑ a, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrResult.mk.inj : ∀ {lhs rhs : Lean.Expr} {pf? : Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr)}
  {lhs_1 rhs_1 : Lean.Expr} {pf?_1 : Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr)},
  { lhs := lhs, rhs := rhs, pf? := pf? } = { lhs := lhs_1, rhs := rhs_1, pf? := pf?_1 } →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ pf? = pf?_1
-- Mathlib.Topology.Order
nhds_nhdsAdjoint_same : ∀ {α : Type u} (a : α) (f : Filter α), nhds a = pure a ⊔ f
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Even.not_odd : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NeZero 2], ψ.Even → ¬ψ.Odd
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.map_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F]
  [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F],
  CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i →
    (CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i) ↔ CategoryTheory.IsPullback f g h i)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkWrap : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM Lean.Expr
-- Lean.Util.PtrSet
/-- Map of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
 -/
Lean.PtrMap : Type → Type → Type
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- **Cauchy–Schwarz inequality**.
We need this for the `PreInnerProductSpace.Core` structure to prove the triangle inequality below
when showing the core is a normed group and to take the quotient.

(This is not intended for general use; see `Analysis.InnerProductSpace.Basic` for a variety of
versions of Cauchy-Schwarz for an inner product space, rather than a `PreInnerProductSpace.Core`).
 -/
InnerProductSpace.Core.inner_mul_inner_self_le : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F),
  ‖inner 𝕜 x y‖ * ‖inner 𝕜 y x‖ ≤ RCLike.re (inner 𝕜 x x) * RCLike.re (inner 𝕜 y y)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t.contains a = false → t[a]! = default
-- Std.Http.Data.Body.Basic
Std.Http.Body.instFromByteArrayByteArray : Std.Http.Body.FromByteArray ByteArray
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instPartialOrderOpenSubgroup : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenSubgroup G)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- When its possible to compare the two, the composition of two `IsStronglyCartesian.map` will also
be given by a `IsStronglyCartesian.map`. In other words, given diagrams
```
a''         a'        a --φ--> b
|           |         |        |
v           v         v        v
R'' --g'--> R' --g--> R --f--> S
```
and
```
a' --φ'--> b
|          |
v          v
R' --f'--> S
```
and
```
a'' --φ''--> b
|            |
v            v
R'' --f''--> S
```
such that `φ` and `φ'` are strongly Cartesian morphisms, and such that `f' = g ≫ f` and
`f'' = g' ≫ f'`. Then composing the induced map from `a'' ⟶ a'` with the induced map from
`a' ⟶ a` gives the induced map from `a'' ⟶ a`.  -/
CategoryTheory.Functor.IsStronglyCartesian.map_comp_map_assoc : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  {R' R'' : 𝒮} {a' a'' : 𝒳} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'}
  (H : f' = CategoryTheory.CategoryStruct.comp g f) (H' : f'' = CategoryTheory.CategoryStruct.comp g' f') (φ' : a' ⟶ b)
  (φ'' : a'' ⟶ b) [inst_3 : p.IsStronglyCartesian f' φ'] [inst_4 : p.IsHomLift f'' φ''] {Z : 𝒳} (h : a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f' φ' H' φ'')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ H φ') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ'') h
-- Mathlib.Algebra.Ring.Ext
CommRing.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : CommRing R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_zero_map_μ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m : M}
  {X Y : C} (f : X ⟶ (F.obj m).obj Y) [inst_3 : F.Monoidal],
  CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).map f)
      ((CategoryTheory.Functor.LaxMonoidal.μ F m (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)
      (CategoryTheory.CategoryStruct.comp f ((F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).inv).app Y))
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mk.inj : ∀ {ι : Type u_5} {B : Type u_6} {inst : TopologicalSpace B} {F : Type u_7} {inst_1 : TopologicalSpace F}
  {baseSet : ι → Set B} {isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)} {indexAt : B → ι}
  {mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)} {coordChange : ι → ι → B → F → F}
  {coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), coordChange i i x v = v}
  {continuousOn_coordChange :
    ∀ (i j : ι), ContinuousOn (fun p => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ Set.univ)}
  {coordChange_comp :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ (v : F), coordChange j k x (coordChange i j x v) = coordChange i k x v}
  {baseSet_1 : ι → Set B} {isOpen_baseSet_1 : ∀ (i : ι), IsOpen (baseSet_1 i)} {indexAt_1 : B → ι}
  {mem_baseSet_at_1 : ∀ (x : B), x ∈ baseSet_1 (indexAt_1 x)} {coordChange_1 : ι → ι → B → F → F}
  {coordChange_self_1 : ∀ (i : ι), ∀ x ∈ baseSet_1 i, ∀ (v : F), coordChange_1 i i x v = v}
  {continuousOn_coordChange_1 :
    ∀ (i j : ι), ContinuousOn (fun p => coordChange_1 i j p.1 p.2) ((baseSet_1 i ∩ baseSet_1 j) ×ˢ Set.univ)}
  {coordChange_comp_1 :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet_1 i ∩ baseSet_1 j ∩ baseSet_1 k,
        ∀ (v : F), coordChange_1 j k x (coordChange_1 i j x v) = coordChange_1 i k x v},
  { baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at,
        coordChange := coordChange, coordChange_self := coordChange_self,
        continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } =
      { baseSet := baseSet_1, isOpen_baseSet := isOpen_baseSet_1, indexAt := indexAt_1,
        mem_baseSet_at := mem_baseSet_at_1, coordChange := coordChange_1, coordChange_self := coordChange_self_1,
        continuousOn_coordChange := continuousOn_coordChange_1, coordChange_comp := coordChange_comp_1 } →
    baseSet = baseSet_1 ∧ indexAt = indexAt_1 ∧ coordChange = coordChange_1
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_I : (-Complex.I).arg = -(Real.pi / 2)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- To construct a morphism of structured arrows,
we need a morphism of the objects underlying the target,
and to check that the triangle commutes.
 -/
CategoryTheory.StructuredArrow.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            {f f' : CategoryTheory.StructuredArrow S T} →
              (g : f.right ⟶ f'.right) →
                autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom)
                    CategoryTheory.StructuredArrow.homMk._auto_1 →
                  (f ⟶ f')
-- Mathlib.Algebra.Star.StarAlgHom
Pi.evalNonUnitalStarAlgHom_apply : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) (j : ι) [inst : Monoid R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → DistribMulAction R (A i)]
  [inst_3 : (i : ι) → Star (A i)] (a : (i : ι) → A i),
  (Pi.evalNonUnitalStarAlgHom R A j) a = (Pi.evalMulHom A j).toFun a
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.treesOfNumNodesEq_zero : BinaryTree.treesOfNumNodesEq 0 = {BinaryTree.nil}
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_neighborSet : ∀ {n : ℕ} {v : Fin (n + 2)}, (SimpleGraph.cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_erase_eq_of_not_compare_minD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).isEmpty = false → ¬cmp k (t.minD fallback) = Ordering.eq → (t.erase k).minD fallback = t.minD fallback
-- Mathlib.Order.Hom.BoundedLattice
/-- Composition of `SupBotHom`s as a `SupBotHom`.  -/
SupBotHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Max α] →
        [inst_1 : Bot α] →
          [inst_2 : Max β] →
            [inst_3 : Bot β] → [inst_4 : Max γ] → [inst_5 : Bot γ] → SupBotHom β γ → SupBotHom α β → SupBotHom α γ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.exactlyChars.go.eq_def : ∀ (parse : Std.Internal.Parsec.String.Parser Char) (size : ℕ) (acc : String) (count : ℕ),
  Std.Time.exactlyChars.go✝ parse size acc count =
    if count ≥ size then pure acc
    else do
      let res ← parse
      Std.Time.exactlyChars.go✝ parse size (acc.push res) count.succ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.isIso_map : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ),
  CategoryTheory.IsIso
      ((X.H n₀).map
        ((CategoryTheory.ComposableArrows.functorArrows ι 2 3 3 CategoryTheory.Abelian.SpectralObject.isIso_map._proof_6
              CategoryTheory.Abelian.SpectralObject.shortComplexMap._proof_3).map
          α)) →
    CategoryTheory.IsIso
        ((X.H n₁).map
          ((CategoryTheory.ComposableArrows.functorArrows ι 1 2 3
                CategoryTheory.Abelian.SpectralObject.isIso_map._proof_8
                CategoryTheory.Abelian.SpectralObject.isIso_map._proof_6).map
            α)) →
      CategoryTheory.IsIso
          ((X.H n₂).map
            ((CategoryTheory.ComposableArrows.functorArrows ι 0 1 3
                  CategoryTheory.Abelian.SpectralObject.isIso_map._proof_10
                  CategoryTheory.Abelian.SpectralObject.isIso_map._proof_12).map
              α)) →
        ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isIso_map._auto_1)
          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_map._auto_3),
          CategoryTheory.IsIso (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
-- Std.Http.Data.URI.Config
/-- Maximum number of path segments.
Prevents excessive segment counts that could arise from paths like `/a/b/c/…` repeated many times.
 -/
Std.Http.URI.Config.maxPathSegments : Std.Http.URI.Config → ℕ
-- Init.Data.Option.Lemmas
Option.all_eq_false : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.all p x = false ↔ ∃ y, x = some y ∧ p y = false
-- Mathlib.MeasureTheory.Measure.Restrict
Subtype.instMeasurableSpace.eq_1 : ∀ {α : Type u_6} {p : α → Prop} [m : MeasurableSpace α],
  Subtype.instMeasurableSpace = MeasurableSpace.comap Subtype.val m
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.self_le_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {kmi : α}, (t.insert k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_3.eq_1 : ∀ {α₂ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₂ m β] (it₂ : Std.IterM m β)
  (motive : it₂.Step → Sort u_3) (it₂' : Std.IterM m β) (out : β)
  (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out))
  (h_1 :
    (it₂' : Std.IterM m β) →
      (out : β) → (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩)
  (h_2 :
    (it₂' : Std.IterM m β) → (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩)
  (h_3 : (h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₂' out, h⟩ with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => h_1 it₂' out h
    | ⟨Std.IterStep.skip it₂', h⟩ => h_2 it₂' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₂' out h
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α) [inst_2 : Fintype ↑(Set.Ico a b)],
  Fintype.card ↑(Set.Ico a b) = (Finset.Ico a b).card
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_rcc : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) (Std.Slice.toList xs))
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
For any subset `S ⊆ B`, the centralizer of `1 ⊗ S ⊆ A ⊗ B` is `A ⊗ C_B(S)` where `C_B(S)` is the
centralizer of `S` in `B`.
 -/
Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Set B) [Module.Free R A],
  Subalgebra.centralizer R (⇑Algebra.TensorProduct.includeRight '' S) =
    (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.centralizer R S).val).range
-- Mathlib.Analysis.RCLike.Basic
RCLike.sub_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), z - (starRingEnd K) z = 2 * ↑(RCLike.im z) * RCLike.I
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_below_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T], q.ramificationIdx R ≤ r.ramificationIdx R
-- Lean.Elab.Tactic.Omega.Core
/-- Decides which variable to run Fourier-Motzkin elimination on, and returns the associated data.

We prefer eliminations which introduce no new inequalities, or otherwise exact eliminations,
and break ties by the number of new inequalities introduced.
 -/
Lean.Elab.Tactic.Omega.Problem.fourierMotzkinSelect : Array Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → Lean.MetaM Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData
-- Mathlib.AlgebraicGeometry.Spec
/-- The spectrum, as a contravariant functor from commutative rings to topological spaces.
 -/
AlgebraicGeometry.Spec.toTop : CategoryTheory.Functor CommRingCatᵒᵖ TopCat
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo.mk.injEq : ∀ (lctx : Lean.LocalContext) (stx output : Lean.Syntax) (lctx_1 : Lean.LocalContext) (stx_1 output_1 : Lean.Syntax),
  ({ lctx := lctx, stx := stx, output := output } = { lctx := lctx_1, stx := stx_1, output := output_1 }) =
    (lctx = lctx_1 ∧ stx = stx_1 ∧ output = output_1)
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.flatMap.congr_simp : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (l l_1 : Turing.ListBlank Γ),
  l = l_1 →
    ∀ (f f_1 : Γ → List Γ') (e_f : f = f_1) (hf : ∃ n, f default = List.replicate n default),
      l.flatMap f hf = l_1.flatMap f_1 ⋯
-- Init.Data.Fin.Fold
/-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))`   -/
Fin.foldr.loop : {α : Sort u_1} → (n : ℕ) → (Fin n → α → α) → (i : ℕ) → i ≤ n → α → α
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.idealFactorsFunOfQuotHom_id`. -/
idealFactorsFunOfQuotHom_id : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDedekindDomain A] {J : Ideal A},
  IsDedekindDomain.idealFactorsFunOfQuotHom ⋯ = OrderHom.id
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- The image of a reverse is the reverse of the image.  -/
Prefunctor.MapReverse.map_reverse' : ∀ {U : Type u_1} {V : Type u_2} {inst : Quiver U} {inst_1 : Quiver V} {inst_2 : Quiver.HasReverse U}
  {inst_3 : Quiver.HasReverse V} {φ : U ⥤q V} [self : φ.MapReverse] {u v : U} (e : u ⟶ v),
  φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
-- Init.Control.Lawful.Instances
instLawfulApplicativeExcept : ∀ {ε : Type u_1}, LawfulApplicative (Except ε)
-- Mathlib.Data.Set.NAry
Set.image_subset_image2_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α},
  a ∈ s → f a '' t ⊆ Set.image2 f s t
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instIsScalarTower : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [IsScalarTower M N α], IsScalarTower Mᵒᵈ N α
-- Mathlib.RingTheory.Spectrum.Prime.Topology
Ideal.prod.eq_1 : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal R) (J : Ideal S),
  I.prod J = Ideal.comap (RingHom.fst R S) I ⊓ Ideal.comap (RingHom.snd R S) J
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_precompR_apply : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup E'']
  [inst_3 : NormedAddCommGroup F] {f : G → E} [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 E']
  [inst_7 : NormedSpace 𝕜 E''] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [inst_11 : NormedAddCommGroup G] [BorelSpace G]
  {g : G → E'' →L[𝕜] E'},
  MeasureTheory.LocallyIntegrable f μ →
    HasCompactSupport g →
      Continuous g →
        ∀ (x₀ : G) (x : E''),
          (MeasureTheory.convolution f g (ContinuousLinearMap.precompR E'' L) μ x₀) x =
            MeasureTheory.convolution f (fun a => (g a) x) L μ x₀
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits.eq_3 : ∀ (b : ℕ), b.succ.succ.digits = (b + 2).digitsAux ⋯
-- Mathlib.Algebra.GroupWithZero.Basic
/-- Multiplying `a` by itself and then dividing by itself results in `a`, whether or not `a` is
zero.  -/
mul_self_div_self : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a * a / a = a
-- Mathlib.Control.ULiftable
/-- map function that moves down universes  -/
ULiftable.downMap : {F : Type (max u₀ v₀) → Type u₁} →
  {G : Type u₀ → Type v₁} → [ULiftable G F] → [Functor F] → {α : Type (max u₀ v₀)} → {β : Type u₀} → (α → β) → F α → G β
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest replacing a sequence of tactics with `grind` if that also solves the goal.  -/
Mathlib.TacticAnalysis.terminalToGrind : Mathlib.TacticAnalysis.Config
-- Aesop.Forward.State
/-- The source of a pattern substitution. The same substitution can have
multiple sources.  -/
Aesop.PatSubstSource : Type
-- Mathlib.Data.Finset.Sum
Finset.map_inr_subset_iff_subset_toRight : ∀ {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (α ⊕ β)},
  Finset.map Function.Embedding.inr t ⊆ u ↔ t ⊆ u.toRight
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.descShortComplex_triangleOfSESδ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact)
  {Z : DerivedCategory C}
  (h : (CategoryTheory.shiftFunctor (DerivedCategory C) 1).obj (DerivedCategory.Q.obj S.X₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map (CochainComplex.mappingCone.descShortComplex S))
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.triangleOfSESδ hS) h) =
    CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map (CochainComplex.mappingCone.triangle S.f).mor₃)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso DerivedCategory.Q 1).hom.app S.X₁) h)
-- Mathlib.Control.EquivFunctor
/-- The composition of `mapEquiv`s is carried over the `EquivFunctor`.
For plain `Functor`s, this lemma is named `map_map` when applied
or `map_comp_map` when not applied.
 -/
EquivFunctor.mapEquiv_trans : ∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] {α β γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ),
  (EquivFunctor.mapEquiv f ab).trans (EquivFunctor.mapEquiv f bc) = EquivFunctor.mapEquiv f (ab.trans bc)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries.map`. -/
upperCentralSeries.map : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] {f : G →* H},
  Function.Surjective ⇑f → ∀ (n : ℕ), Subgroup.map f (Subgroup.upperCentralSeries G n) ≤ Subgroup.upperCentralSeries H n
-- Mathlib.Order.Extension.Well
IsWellFounded.wellOrderExtension.isWellFounded_lt : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r], IsWellFounded α LT.lt
-- Mathlib.AlgebraicGeometry.Scheme
/-- The empty scheme.  -/
AlgebraicGeometry.Scheme.empty : AlgebraicGeometry.Scheme