mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.instFaithfulSMulCompletionOfUniformContinuousConstSMul : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  {R : Type u_3} [inst_2 : CommSemiring R] [inst_3 : Algebra R K] [UniformContinuousConstSMul R K] [FaithfulSMul R K],
  FaithfulSMul R (UniformSpace.Completion K)
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesLimit_iff : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  (F : CategoryTheory.Functor K J) (G : CategoryTheory.Functor J C),
  CategoryTheory.ObjectProperty.preservesLimit F G ↔ CategoryTheory.Limits.PreservesLimit F G
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If a functor `F` is zero, then any cone for `F` with a zero point is limit.  -/
CategoryTheory.Limits.IsLimit.ofIsZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        [CategoryTheory.Limits.HasZeroMorphisms C] →
          [CategoryTheory.Limits.HasZeroObject C] →
            {F : CategoryTheory.Functor D C} →
              (c : CategoryTheory.Limits.Cone F) →
                CategoryTheory.Limits.IsZero F → CategoryTheory.Limits.IsZero c.pt → CategoryTheory.Limits.IsLimit c
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_int_iff : ∀ (f : CircleDeg1Lift), Continuous ⇑f → ∀ {m : ℤ}, f.translationNumber = ↑m ↔ ∃ x, f x = x + ↑m
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_interSmallerFn : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  (m sofar : Std.DTreeMap.Internal.Impl α β),
  m.WF →
    ∀ (h₂ : sofar.WF) (l : List ((a : α) × β a)) (k : α),
      sofar.toListModel.Perm l →
        (↑(m.interSmallerFn ⟨sofar, ⋯⟩ k)).toListModel.Perm (Std.Internal.List.interSmallerFn m.toListModel l k)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_inter!_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁.inter! m₂).isEmpty = true
-- Mathlib.Data.Setoid.Basic
/-- The equivalence closure of an equivalence relation r is r.  -/
Setoid.eqvGen_of_setoid : ∀ {α : Type u_1} (r : Setoid α), Relation.EqvGen.setoid ⇑r = r
-- Init.Prelude
/-- Resolves the given name to an overload list of global definitions.
The `List String` in each alternative is the deduced list of projections
(which are ambiguous with name components).

Remark: it will not trigger actions associated with reserved names. Recall that Lean
has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
containing stating that `foo` is equal to its definition. The action associated with `foo.def`
automatically proves the theorem. At the macro level, the name is resolved, but the action is not
executed. The actions are executed by the elaborator when converting `Syntax` into `Expr`.
 -/
Lean.Macro.resolveGlobalName : Lean.Name → Lean.MacroM (List (Lean.Name × List String))
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.ofList_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List (α × β)},
  Std.DHashMap.Raw.Const.ofList l =
    ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polar_univ : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E], StrongDual.polar 𝕜 Set.univ = {0}
-- Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
/-- For fans on maps `f₁ : ι₁ → C`, `f₂ : ι₂ → C` and a binary fan on their
cone points, construct one family of morphisms indexed by `ι₁ ⊕ ι₂`  -/
CategoryTheory.Limits.Fan.combPairHoms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {ι₁ : Type u_1} →
      {ι₂ : Type u_2} →
        {f₁ : ι₁ → C} →
          {f₂ : ι₂ → C} →
            (c₁ : CategoryTheory.Limits.Fan f₁) →
              (c₂ : CategoryTheory.Limits.Fan f₂) →
                (bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt) → (i : ι₁ ⊕ ι₂) → bc.pt ⟶ Sum.elim f₁ f₂ i
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.isTopCompl_bot_top : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M], Submodule.IsTopCompl ⊥ ⊤
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instNonAssocSemiring : {𝕜 : Type u_2} →
  {α : Type u_5} →
    [inst : Preorder α] →
      [LocallyFiniteOrder α] → [DecidableEq α] → [inst_3 : NonAssocSemiring 𝕜] → NonAssocSemiring (IncidenceAlgebra 𝕜 α)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_symm_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (f : Matrix m n α) (i : m) (j : n), Matrix.of.symm f i j = f i j
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- **Alias** of the reverse direction of `Finset.prod_ne_zero_iff`. -/
Mathlib.Meta.Positivity.prod_ne_zero : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀]
  [NoZeroDivisors M₀], (∀ a ∈ s, f a ≠ 0) → ∏ x ∈ s, f x ≠ 0
-- Mathlib.Control.Bitraversable.Instances
LawfulBitraversable.const : LawfulBitraversable Functor.Const
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C =
    { obj := fun F => F.mapAddMon.obj (CategoryTheory.AddMon.trivial (CategoryTheory.Discrete PUnit.{w + 1})),
      map := fun {X Y} α =>
        ((CategoryTheory.Functor.mapAddMonFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C).map α).app
          (CategoryTheory.AddMon.trivial (CategoryTheory.Discrete PUnit.{w + 1})),
      map_id := ⋯, map_comp := ⋯ }
-- Aesop.Tree.Data
Aesop.Iteration : Type
-- Mathlib.Computability.NFA
/-- `M.eval x` computes all possible paths though `M` with input `x` starting at an element of
`M.start`.  -/
NFA.eval : {α : Type u} → {σ : Type v} → NFA α σ → List α → Set σ
-- Mathlib.Analysis.Analytic.Constructions
Units.oneSub.eq_1 : ∀ {R : Type u_4} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (t : R) (h : ‖t‖ < 1),
  Units.oneSub t h = { val := 1 - t, inv := ∑' (n : ℕ), t ^ n, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
trdeg_eq_zero_iff : ∀ {R : Type u_3} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
-- Mathlib.Analysis.Real.Pi.Bounds
Real.floor_pi_eq_three : ⌊Real.pi⌋ = 3
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_id : ∀ {α : Type u_2} {x : NonAssocSemiring α}, ⇑(RingHom.id α) = id
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.quotientKerRightHomEquivRight.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G),
  S.quotientKerRightHomEquivRight = QuotientAddGroup.quotientKerEquivOfSurjective S.rightHom ⋯
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepFun_pi_of_prod_bcf : ∀ {Ω : Type u_1} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {F : T → Type u_5} {G : Type u_6}
  [inst : (t : T) → TopologicalSpace (F t)] [inst_1 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)]
  [∀ (t : T), HasOuterApproxClosed (F t)] [inst_4 : TopologicalSpace G] [inst_5 : MeasurableSpace G] [BorelSpace G]
  [HasOuterApproxClosed G] {Y : (t : T) → Ω → F t} {Z : Ω → G} [inst_8 : Fintype T] [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable Z P →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : BoundedContinuousFunction G ℝ) (g : (t : T) → BoundedContinuousFunction (F t) ℝ),
          ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
            (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P) →
        ProbabilityTheory.IndepFun Z (fun ω t => Y t ω) P
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doReassignArrow; doElems`
`doReassignArrow` is of the form
```
(doIdDecl <|> doPatDecl)
```
 -/
Lean.Elab.Term.Do.ToCodeBlock.doReassignArrowToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.mk : {X Y : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        {f g : SSet.RelativeMorphism A B φ} →
          (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 }) ⟶ Y) →
            autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₀ h = f.map)
                SSet.RelativeMorphism.Homotopy.h₀._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₁ h = g.map)
                  SSet.RelativeMorphism.Homotopy.h₁._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 })) h =
                      CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
                        (CategoryTheory.CategoryStruct.comp φ B.ι))
                    SSet.RelativeMorphism.Homotopy.rel._autoParam →
                  f.Homotopy g
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.MutuallySingular.compProd_of_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α},
  μ.MutuallySingular ν → ∀ (κ η : ProbabilityTheory.Kernel α β), (μ.compProd κ).MutuallySingular (ν.compProd η)
-- Mathlib.Topology.PartitionOfUnity
/-- A variation of **Urysohn's lemma**.

In a locally compact T2 space `X`, for a compact set `t` and a finite family of open sets `{s i}_i`
such that `t ⊆ ⋃ i, s i`, there is a family of compactly supported continuous functions `{f i}_i`
supported in `s i`, `∑ i, f i x = 1` on `t` and `0 ≤ f i x ≤ 1`.  -/
exists_continuous_sum_one_of_isOpen_isCompact : ∀ {X : Type v} [inst : TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] {n : ℕ} {t : Set X} {s : Fin n → Set X},
  (∀ (i : Fin n), IsOpen (s i)) →
    IsCompact t →
      t ⊆ ⋃ i, s i →
        ∃ f,
          (∀ (i : Fin n), tsupport ⇑(f i) ⊆ s i) ∧
            Set.EqOn (∑ i, ⇑(f i)) 1 t ∧
              (∀ (i : Fin n) (x : X), (f i) x ∈ Set.Icc 0 1) ∧ ∀ (i : Fin n), HasCompactSupport ⇑(f i)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.mk : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] →
        (toOrderHom : α →o β) →
          (∀ (c : OmegaCompletePartialOrder.Chain α),
              toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom)) →
            α →𝒄 β
-- Mathlib.RingTheory.WittVector.Defs
WittVector.one_coeff_zero : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R], WittVector.coeff 1 0 = 1
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Ico_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Ico c d ↔ b ∈ Set.Ico (c - a) (d - a)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_union_ground : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk (X ∪ M.E) = M.eRank
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.epi_homologyMap_of_epi_cyclesMap' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.Epi (CategoryTheory.ShortComplex.cyclesMap φ) →
    CategoryTheory.Epi (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Dynamics.Minimal
dense_of_nonempty_smul_invariant : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α] {s : Set α}, s.Nonempty → (∀ (c : M), c • s ⊆ s) → Dense s
-- Init.Data.List.Nat.Modify
List.drop_modifyHead_of_pos : ∀ {α : Type u_1} {f : α → α} {l : List α} {i : ℕ}, 0 < i → List.drop i (List.modifyHead f l) = List.drop i l
-- Mathlib.Algebra.Group.Basic
div_eq_inv_self : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a / b = b⁻¹ ↔ a = 1
-- Mathlib.Data.Matrix.Reflection
Matrix.of.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v}, Matrix.of = Equiv.refl (m → n → α)
-- Mathlib.Data.Finset.Max
Finset.min_mem_image_coe : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.Nonempty → s.min ∈ Finset.image WithTop.some s
-- Init.Data.Rat.Lemmas
_private.Init.Data.Rat.Lemmas.0.Rat.divInt.match_3.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (n : ℤ) (d : ℕ) (h_1 : (n : ℤ) → (d : ℕ) → motive n (Int.ofNat d))
  (h_2 : (n : ℤ) → (d : ℕ) → motive n (Int.negSucc d)),
  (match n, Int.ofNat d with
    | n, Int.ofNat d => h_1 n d
    | n, Int.negSucc d => h_2 n d) =
    h_1 n d
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindFunctor_map : ∀ (k : Type u) {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {X Y : Rep.{t, u, v} k G} (f : X ⟶ Y), (Rep.coindFunctor k φ).map f = Rep.coindMap φ f
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
hasProd_one_add_of_hasSum_prod : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommSemiring α] [inst_1 : TopologicalSpace α] {f : ι → α} {a : α},
  HasSum (fun x => ∏ i ∈ x, f i) a → HasProd (fun x => 1 + f x) a
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.mul_mul_mul_inv_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹ ∈ S.inl.range
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If a measure `μ` on a quotient satisfies `QuotientMeasureEqMeasurePreimage` with respect to a
sigma-finite measure, then it is itself `SigmaFinite`.  -/
MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasureTheory.MeasureSpace α]
  [Countable G] [MeasureTheory.SMulInvariantMeasure G α MeasureTheory.volume] [MeasurableConstSMul G α]
  [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasureTheory.HasFundamentalDomain G α MeasureTheory.volume]
  (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α)))
  [MeasureTheory.QuotientMeasureEqMeasurePreimage MeasureTheory.volume μ], MeasureTheory.SigmaFinite μ
-- Lean.Elab.Command
Lean.Elab.Command.instMonadLiftTIOCommandElabM : MonadLiftT IO Lean.Elab.Command.CommandElabM
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- **Conjugation symmetry of the Riemann zeta function**: `ζ (conj s) = conj (ζ s)`.

Since `ζ` has real Dirichlet coefficients, `conj (ζ (conj z)) = ζ z` holds termwise for
`1 < re z`, and the identity principle propagates this to all `s ≠ 1`; the junk value `ζ 1` is
real, so the identity also holds at `s = 1`.  -/
riemannZeta_conj : ∀ (s : ℂ), riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜}, DifferentiableAt 𝕜 (⇑f) x
-- Init.GetElem
/-- The classes `GetElem` and `GetElem?` implement lookup notation,
specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.

Both classes are indexed by types `coll`, `idx`, and `elem` which are
the collection, the index, and the element types.
A single collection may support lookups with multiple index
types. The relation `valid` determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.

For example, an instance for arrays looks like
`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
holds, which is true when `i` is less than the size of the array. `Array`
additionally supports indexing with `USize` instead of `Nat`.
In either case, because the bounds are checked at compile time,
no runtime check is required.

Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
`GetElem coll idx elem valid` and uses this to infer the type of the return
value `elem` and side condition `valid` required to ensure `xs[i]` yields
a valid value of type `elem`. The tactic `get_elem_tactic` is
invoked to prove validity automatically. The `xs[i]'p` notation uses the
proof `p` to satisfy the validity condition.
If the proof `p` is long, it is often easier to place the
proof in the context using `have`, because `get_elem_tactic` tries
`assumption`.


The proof side-condition `valid xs i` is automatically dispatched by the
`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
`get_elem_tactic_extensible` using `macro_rules`.

`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
an `Option elem`, with `none` signalling that the value isn't present, and
the latter returns `elem` but panics if the value isn't there, returning
`default : elem` based on the `Inhabited elem` instance.
These are provided by the `GetElem?` class, for which there is a default instance
generated from a `GetElem` class as long as `valid xs i` is always decidable.

Important instances include:
  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
    side goal `i < l.length`.

 -/
GetElem? : (coll : Type u) → (idx : Type v) → outParam (Type w) → outParam (coll → idx → Prop) → Type (max (max u v) w)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_pow_right₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀]
  [ZeroLEOneClass M₀], 1 < a → m < n → a ^ m < a ^ n
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.coe_comp : ∀ {X Y Z : AddMonCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.RingTheory.Extension.Basic
/-- An extension of an `R`-algebra `S` is an `R` algebra `P` together with a surjection `P →ₐ[R] S`.
Also see `Algebra.Extension.ofSurjective`.
 -/
Algebra.Extension : (R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max (max u v) (w + 1))
-- Mathlib.GroupTheory.OrderOfElement
isOfFinAddOrder_ofMul_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinAddOrder (Additive.ofMul x) ↔ IsOfFinOrder x
-- Mathlib.Topology.Inseparable
SeparationQuotient.preimage_image_mk_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsClosed s → SeparationQuotient.mk ⁻¹' SeparationQuotient.mk '' s = s
-- Mathlib.Topology.Compactness.Compact
IsCompact.compl_mem_coclosedCompact_of_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsClosed s → sᶜ ∈ Filter.coclosedCompact X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} {aig : Std.Sat.AIG α} {w : ℕ}
  (input : aig.RefVec w) (start curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go input start curr hcurr s =
    if h : curr < newWidth then
      have falseRef := aig.mkConstCached false;
      have nextRef := input.getD (start + curr) falseRef;
      have s := s.push nextRef;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go input start (curr + 1) ⋯ s
    else
      have this := ⋯;
      this ▸ s
-- Mathlib.Data.Sigma.Basic
Sigma.curry_update : ∀ {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} [inst : DecidableEq α]
  [inst_1 : (a : α) → DecidableEq (β a)] (i : (a : α) × β a) (f : (i : (a : α) × β a) → γ i.fst i.snd)
  (x : γ i.fst i.snd),
  Sigma.curry (Function.update f i x) =
    Function.update (Sigma.curry f) i.fst (Function.update (Sigma.curry f i.fst) i.snd x)
-- Mathlib.Order.Filter.Extr
sup_eq_of_max : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] [inst_1 : OrderBot β] {D : α → β} {s : Finset α}
  [inst_2 : Nonempty α] {b : β}, b ∈ Set.range D → Function.invFun D b ∈ s → (∀ a ∈ s, D a ≤ b) → s.sup D = b
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_one : ∀ {m : Type um} {R : Type uR} [inst : Semiring R] [Nontrivial R] [inst_2 : DecidableEq m] [StrongRankCondition R],
  Matrix.cRank 1 = Cardinal.lift.{uR, um} (Cardinal.mk m)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.fact_isRegular_aleph0 : Fact Cardinal.aleph0.IsRegular
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.loop.wf.induct_unfolding : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
  (f : (out : α) → LargeEnough out → (c : γ) → n { s // Pl out c s })
  (motive : γ → (next : α) → LargeEnough next → n γ → Prop),
  (∀ (acc : γ) (next : α) (h : LargeEnough next),
      (∀ (acc' : γ),
          Pl next acc (ForInStep.yield acc') →
            ∀ (next' : α) (hs : Std.PRange.succ? next = some next'),
              motive acc' next' ⋯ (Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc' next' ⋯ f)) →
        motive acc next h do
          let __do_lift ← f next h acc
          match __do_lift with
            | ⟨ForInStep.yield acc', property⟩ =>
              match hs : Std.PRange.succ? next with
              | some next' => Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc' next' ⋯ f
              | none => pure acc'
            | ⟨ForInStep.done acc', property⟩ => pure acc') →
    ∀ (acc : γ) (next : α) (h : LargeEnough next),
      motive acc next h (Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc next h f)
-- Mathlib.Algebra.Group.Invertible.Defs
/-- An element in a Dedekind-finite monoid is invertible if it has a left inverse.  -/
invertibleOfLeftInverse : {α : Type u} → [inst : Monoid α] → [IsDedekindFiniteMonoid α] → (a b : α) → b * a = 1 → Invertible a
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.fun_comp_contDiffOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {g : F → G} {f : E → F},
  ContDiff 𝕜 n g → ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (fun x => g (f x)) s
-- Mathlib.Data.Set.Image
Set.preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : Set γ},
  f ⁻¹' g ⁻¹' s = (fun x => g (f x)) ⁻¹' s