mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.range_structureMap : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι},
  Set.range (RestrictedProduct.structureMap R A 𝓕) = {f | ∀ (i : ι), ↑f i ∈ A i}
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_set : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α},
  a ∈ MulAction.stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hasForgetToGroup : CategoryTheory.HasForget₂ CommGrpCat GrpCat
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.instDecidableEqPoint.decEq : {R : Type u_1} →
  {inst : CommRing R} → {W' : WeierstrassCurve.Affine R} → [DecidableEq R] → (x x_1 : W'.Point) → Decidable (x = x_1)
-- Mathlib.Data.Set.Function
/-- **Alias** of the forward direction of `Equiv.bijOn_symm`. -/
Set.BijOn.of_equiv_symm : ∀ {α : Type u_1} {β : Type u_2} {e : α ≃ β} {s : Set α} {t : Set β}, Set.BijOn (⇑e.symm) t s → Set.BijOn (⇑e) s t
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- If the support of each element in a generating set of a permutation group is finite,
then the support of every element in the group is finite.  -/
finite_compl_fixedBy_closure_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {S : Set G},
  (∀ g ∈ Subgroup.closure S, (MulAction.fixedBy α g)ᶜ.Finite) ↔ ∀ g ∈ S, (MulAction.fixedBy α g)ᶜ.Finite
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_union_distrib_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE_apply_mk : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (g : ↥s),
  (AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE H h) ↑g = ↑((AddSubgroup.inclusion h) g)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instAdd : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → Add (CentroidHom α)
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Filter.Tendsto.compMeasurePreservingLp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [R1Space X]
  [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3}
  [inst_10 : NormedAddCommGroup E] {p : ENNReal} [inst_11 : Fact (1 ≤ p)] {α : Type u_4} {l : Filter α}
  {f : α → ↥(MeasureTheory.Lp E p ν)} {f₀ : ↥(MeasureTheory.Lp E p ν)} {g : α → C(X, Y)} {g₀ : C(X, Y)},
  Filter.Tendsto f l (nhds f₀) →
    Filter.Tendsto g l (nhds g₀) →
      ∀ (hgm : ∀ (a : α), MeasureTheory.MeasurePreserving (⇑(g a)) μ ν)
        (hgm₀ : MeasureTheory.MeasurePreserving (⇑g₀) μ ν),
        p ≠ ⊤ →
          Filter.Tendsto (fun a => (MeasureTheory.Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l
            (nhds ((MeasureTheory.Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
-- Mathlib.Tactic.ContinuousFunctionalCalculus
/-- A tactic used to automatically discharge goals relating to the non-unital continuous functional
calculus, specifically concerning whether `f 0 = 0`.  -/
cfcZeroTac : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Invertible
eq_of_invOf_add_eq_invOf_add_invOf : ∀ {R : Type u_1} [inst : Ring R] {a b : R} [inst_1 : Invertible a] [inst_2 : Invertible b]
  [inst_3 : Invertible (a + b)], ⅟(a + b) = ⅟a + ⅟b → a * ⅟b * a = b * ⅟a * b
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.map_closure_eq : ∀ {α : Type u_2} {β : Type u_3} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) (X : Set β),
  (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
-- Init.MetaTypes
Lean.Meta.TransparencyMode.implicit.sizeOf_spec : sizeOf Lean.Meta.TransparencyMode.implicit = 1
-- Init.Data.List.MinMaxOn
List.apply_minOn_append_le_right : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (h : ys ≠ []), f (List.minOn f (xs ++ ys) ⋯) ≤ f (List.minOn f ys h)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.inv_mul_integral_comp_div : ∀ {a b : ℝ} {f : ℝ → ℝ} (c : ℝ), c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe : ∀ {V : Type u} (G : SimpleGraph V) (u v : V) (w : ↑(G.commonNeighbors u v)),
  ↑((G.walkLengthTwoEquivCommonNeighbors u v).symm w) = (SimpleGraph.Adj.toWalk ⋯).concat ⋯
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_const_le : ∀ {α : Type u_1} {b c : α} {K : Type u_2} [inst : Semiring K] [inst_1 : PartialOrder K] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : Module K α] [PosSMulMono K α], b ≤ c → ∀ {s : K}, 0 ≤ s → s • b ≤ s • c
-- Mathlib.Analysis.Real.Hyperreal
/-- Standard part predicate.
**Do not use.** This is equivalent to the conjunction of `0 ≤ ArchimedeanClass.mk x` and
`ArchimedeanClass.stdPart x = r`.  -/
Hyperreal.IsSt : ℝ* → ℝ → Prop
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_roi : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, (Std.Roi.Sliceable.mkSlice xs lo<...*).start = min (lo + 1) xs.size
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₁ = false) {h' : k ∈ m₁.union m₂ ⋯ ⋯},
  (m₁.union m₂ ⋯ ⋯).get k h' = m₂.get k ⋯
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryGE.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, (compare a k).isGE = true) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.replaceEntry.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (x : List ((a : α) × β a)),
  Std.Internal.List.replaceEntry k v x =
    match x with
    | [] => []
    | ⟨k', v'⟩ :: l => bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: Std.Internal.List.replaceEntry k v l
-- Init.Data.Vector.Monadic
Vector.forIn'_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m]
  [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : (b : β) → b ∈ Vector.map g xs → γ → m (ForInStep γ)),
  forIn' (Vector.map g xs) init f = forIn' xs init fun a h y => f (g a) ⋯ y
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.image_eq_preimage_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E), ⇑e '' s = ⇑e.symm ⁻¹' s
-- Mathlib.CategoryTheory.Shift.CommShift
/-- **Alias** of `CategoryTheory.Functor.CommShift.comp_commShiftIso_inv_app`. -/
CategoryTheory.Functor.commShiftIso_comp_inv_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [inst_3 : AddMonoid A]
  [inst_4 : CategoryTheory.HasShift C A] [inst_5 : CategoryTheory.HasShift D A] [inst_6 : CategoryTheory.HasShift E A]
  [inst_7 : F.CommShift A] [inst_8 : G.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (F.comp G) a).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G a).inv.app (F.obj X))
      (G.map ((CategoryTheory.Functor.commShiftIso F a).inv.app X))
-- Init.Control.Lawful.Instances
OptionT.seqLeft_eq : ∀ {α β : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β),
  x <* y = Function.const β <$> x <*> y
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eraseKey_eq_of_beq_maxKey?_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (∀ {km : α}, Std.Internal.List.maxKey? l = some km → (k == km) = false) →
      Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey? l
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.nsmul_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (n : ℕ) (f : BoundedContinuousFunction α R) (x : α),
  (n • f) x = n • f x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSliceData.treeMap : {α : Type u} → {β : Type v} → Std.DTreeMap.Internal.Const.RiiSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Std.Do.WP.SimpLemmas
Std.Do.WP.lift_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Std.Do.WP m ps] [inst_1 : Monad m]
  (x : m α), (Std.Do.wp (OptionT.lift x)).apply Q = (Std.Do.wp (MonadLift.monadLift x)).apply Q
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comp_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' L'' : Φ.LeftResolution X₂} (φ : L.Hom L') (ψ : L'.Hom L''),
  (φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
-- Mathlib.Topology.Order.ScottTopology
Topology.upperSet_le_scott : ∀ {α : Type u_1} [inst : Preorder α], Topology.upperSet α ≤ Topology.scott α Set.univ
-- Mathlib.Topology.ContinuousMap.Units
/-- Equivalence between continuous maps into the units of a monoid with continuous multiplication
and the units of the monoid of continuous maps.  -/
ContinuousMap.unitsLift : {X : Type u_1} →
  {M : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : Monoid M] → [inst_2 : TopologicalSpace M] → [inst_3 : ContinuousMul M] → C(X, Mˣ) ≃ C(X, M)ˣ
-- Mathlib.Tactic.Sat.FromLRAT
/-- The list of literals as read from the input file  -/
Mathlib.Tactic.Sat.Clause.lits : Mathlib.Tactic.Sat.Clause → Array ℤ
-- Mathlib.Analysis.Convex.Basic
/-- Alternative definition of set convexity, using division.  -/
convex_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E},
  Convex 𝕜 s ↔
    ∀ ⦃x : E⦄,
      x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.mono : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l₁ l₂ : Filter α} {f : α → E} {g : α → F},
  f =O[𝕜; l₁] g → l₂ ≤ l₁ → f =O[𝕜; l₂] g
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.hInv_iso_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : C₁ ≌ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : C₃ ≌ C₄) (x : CategoryTheory.CatCommSq T.functor L R B.functor) (X : C₂),
  (CategoryTheory.CatCommSq.iso T.inverse R L B.inverse).inv.app X =
    CategoryTheory.CategoryStruct.comp (B.inverse.map (R.map (T.counitIso.inv.app X)))
      (CategoryTheory.CategoryStruct.comp
        (B.inverse.map ((CategoryTheory.CatCommSq.iso T.functor L R B.functor).hom.app (T.inverse.obj X)))
        (B.unitIso.inv.app (L.obj (T.inverse.obj X))))
-- Aesop.BuiltinRules.Split
Aesop.BuiltinRules.splitHypothesesCore : Lean.MVarId → Aesop.ScriptM (Option (Array Lean.MVarId))
-- Std.Sat.AIG.Basic
/-- An `Array Decl` is a Direct Acyclic Graph (DAG) if a gate at index `i` only points to nodes with index lower than `i`.
 -/
Std.Sat.AIG.IsDAG : (α : Type) → Array (Std.Sat.AIG.Decl α) → Prop
-- Mathlib.Topology.MetricSpace.Polish
PolishSpace.mk : ∀ {α : Type u_3} [h : TopologicalSpace α] [toSecondCountableTopology : SecondCountableTopology α]
  [toIsCompletelyMetrizableSpace : TopologicalSpace.IsCompletelyMetrizableSpace α], PolishSpace α
-- Mathlib.Order.Atoms
Set.isCoatom_singleton_compl : ∀ {α : Type u_2} (x : α), IsCoatom {x}ᶜ
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndependent_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, ¬LinearIndependent R v ↔ ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0
-- Mathlib.Order.RelClasses
/-- **Alias** of `ssubset_iff_subset_and_ne`.

---

Set notation form of `lt_iff_le_and_ne` -/
ssubset_iff_subset_ne : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊂ b ↔ a ⊆ b ∧ a ≠ b
-- Mathlib.Tactic.Simps.NotationClass
Simps.AutomaticProjectionData.mk.inj : ∀ {className : Lean.Name} {isNotation : Bool} {findArgs className_1 : Lean.Name} {isNotation_1 : Bool}
  {findArgs_1 : Lean.Name},
  { className := className, isNotation := isNotation, findArgs := findArgs } =
      { className := className_1, isNotation := isNotation_1, findArgs := findArgs_1 } →
    className = className_1 ∧ isNotation = isNotation_1 ∧ findArgs = findArgs_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_insertManyIfNewUnit_list : ∀ {α : Type u} {x : Ord α} [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {l : List α}
  {t : Std.DTreeMap.Internal.Impl α fun x => Unit} (h : t.WF),
  (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).toListModel.Perm
    (Std.Internal.List.insertListIfNewUnit t.toListModel l)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.πs'.congr_simp : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o₁ o₂ : Ordinal.{u}}
  (h : o₁ ≤ o₂), Profinite.NobelingProof.πs' C h = Profinite.NobelingProof.πs' C h
-- Mathlib.CategoryTheory.IsoCat
/-- The forward functor of an isomorphism of categories.  -/
CategoryTheory.IsoCat.functor : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.IsoCat C D → CategoryTheory.Functor C D
-- Mathlib.Data.Stream.Init
Stream'.nats_eq : Stream'.nats = Stream'.cons 0 (Stream'.map Nat.succ Stream'.nats)
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_1.eq_1 : ∀ {σ : Type u_1} (motive : σ × Bool → Sort u_2) (fst : σ) (checkSuccess : Bool)
  (h_1 : (fst : σ) → (checkSuccess : Bool) → motive (fst, checkSuccess)),
  (match (fst, checkSuccess) with
    | (fst, checkSuccess) => h_1 fst checkSuccess) =
    h_1 fst checkSuccess
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move_right_nth : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ) (i : ℤ),
  (Turing.Tape.move Turing.Dir.right T).nth i = T.nth (i + 1)
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type with `0` and `+` is `AddZeroClass` if `β` is a
`AddZeroClass`.  -/
FunLike.addZeroClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] → [inst_3 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → AddZeroClass F
-- Std.Http.Server.Config
/-- Maximum number of headers allowed per request.
 -/
Std.Http.Config.maxHeaders : Std.Http.Config → ℕ
-- Lean.Elab.Parallel
/-- Creates an iterator over a list of tasks that yields results in completion order.

Uses `IO.waitAny'` to wait for the next task to complete (whichever finishes first),
then yields that result and continues with the remaining tasks.

The iterator will terminate once all tasks have completed, but we don't provide a `Finite`
instance since we cannot prove termination from the available information.
In practice, if all tasks eventually complete, the iterator will be finite.

## Example
```lean
let tasks : List (Task Nat) ← [
  IO.asTask (pure 1),
  IO.asTask (pure 2),
  IO.asTask (pure 3)
]
let iter := IO.iterTasks tasks
for result in iter do
  IO.println s!"Got result: {result}"
```
 -/
_private.Lean.Elab.Parallel.0.IO.iterTasks : {α : Type} → List (Task α) → Std.IterM BaseIO α
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateProj!Impl : Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult : Type
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G`, this is the projective resolution of `k`
as a trivial `k`-linear `G`-representation given by periodic complex
`... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0` where `ρ` is
the left regular representation and `N` is the norm map.  -/
Rep.FiniteCyclicGroup.resolution : (k : Type u) →
  {G : Type u} →
    [inst : CommRing k] →
      [inst_1 : CommGroup G] →
        [Fintype G] →
          (g : G) → (∀ (x : G), x ∈ Subgroup.zpowers g) → CategoryTheory.ProjectiveResolution (Rep.trivial k G k)
-- Init.Meta.Defs
Array.mapSepElemsM : {m : Type → Type} → [Monad m] → Array Lean.Syntax → (Lean.Syntax → m Lean.Syntax) → m (Array Lean.Syntax)
-- Mathlib.RingTheory.MvPowerSeries.Order
_private.Mathlib.RingTheory.MvPowerSeries.Order.0.MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
  MvPowerSeries.weightedOrder w f < MvPowerSeries.weightedOrder w g →
    MvPowerSeries.weightedOrder w (f + g) = MvPowerSeries.weightedOrder w f
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYoneda.eq_1 : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F],
  Condensed.isoFinYoneda F =
    CategoryTheory.NatIso.ofComponents
      (fun X => Condensed.isoFinYonedaComponents F (FintypeCat.toProfinite.obj (Opposite.unop X))) ⋯
-- Mathlib.Algebra.Category.Ring.Topology
/-- `Hom(A/I, R)` is a closed subspace of `Hom(A, R)` if `R` is T1.  -/
CommRingCat.HomTopology.isClosedEmbedding_precomp_of_surjective : ∀ {R A B : CommRingCat} [inst : TopologicalSpace ↑R] [T1Space ↑R] (f : A ⟶ B),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsClosedEmbedding fun x => CategoryTheory.CategoryStruct.comp f x
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.divXPowOrder_pow : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R] [Nontrivial R] (φ : PowerSeries R) (n : ℕ),
  (φ ^ n).divXPowOrder = φ.divXPowOrder ^ n
-- Mathlib.CategoryTheory.Monad.Limits
/-- The algebra structure which will be the apex of the new limit cone for `D`.  -/
CategoryTheory.Monad.ForgetCreatesLimits.conePoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          (D : CategoryTheory.Functor J T.Algebra) →
            (c : CategoryTheory.Limits.Cone (D.comp T.forget)) → CategoryTheory.Limits.IsLimit c → T.Algebra
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero : ∀ {A : Type u_5} [inst : CommRing A] [IsDomain A] {ι : Type u_6} [inst_2 : DecidableEq ι] [inst_3 : Fintype ι]
  {M : Matrix ι ι A}, (Matrix.toBilin' M).Nondegenerate ↔ M.det ≠ 0
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits.eq_1 : Nat.digits 0 = Nat.digitsAux0
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
List.smul_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : MulOneClass N] [inst_2 : MulAction M N]
  [IsScalarTower M N N] [SMulCommClass M N N] (l : List N) (m : M),
  m ^ l.length • l.prod = (List.map (fun x => m • x) l).prod
-- Init.Data.List.MinMaxOn
List.apply_get_minOn?_le_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} {x : α} (h : x ∈ xs), f ((List.minOn? f xs).get ⋯) ≤ f x
-- Mathlib.Data.Finset.Insert
Multiset.toFinset_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), (a ::ₘ s).toFinset = insert a s.toFinset
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
SSet.horn.IsCompatible.δ_liftOfKanComplex : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  [inst : X.KanComplex] (hf : SSet.horn.IsCompatible f) (j : Fin (n + 2))
  (hj : autoParam (j ≠ i) SSet.horn.IsCompatible.δ_liftOfKanComplex._auto_1),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) hf.liftOfKanComplex = f j hj
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.minEntry?ₘ_eq_minEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered → l.minEntry?ₘ = Std.Internal.List.minEntry? l.toListModel
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] (a : α) (s : Finset α) (t : α → β),
  ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β}
  (h : t.Balanced),
  ↑(t.insertMany l h) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | ⟨k, v⟩ => Std.DTreeMap.Internal.Impl.insert! k v acc)
      t l
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  pos.find? p = some pos' ↔
    pos ≤ pos' ∧
      (∃ (h : pos' ≠ s.endPos), p (pos'.get h) = true) ∧
        ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), p (pos''.get ⋯) = false
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_filter : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] (s : Finset α) (p : α → Prop)
  [inst_2 : DecidablePred p], -{x ∈ s | p x} = {x ∈ -s | p (-x)}
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank_le_domain : ∀ {K : Type u} {V V₁ : Type v} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₁] [inst_4 : Module K V₁] (f : V →ₗ[K] V₁), f.rank ≤ Module.rank K V