mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mk : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (toLinearMap : M →ₗ[R] N →ₗ[R] R) →
                    [isPerfPair_toLinearMap : toLinearMap.IsPerfPair] →
                      (root : ι ↪ M) →
                        (coroot : ι ↪ N) →
                          (∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2) →
                            (reflectionPerm : ι → ι ≃ ι) →
                              (∀ (i j : ι),
                                  root j - (toLinearMap (root j)) (coroot i) • root i = root ((reflectionPerm i) j)) →
                                (∀ (i j : ι),
                                    coroot j - (toLinearMap (root i)) (coroot j) • coroot i =
                                      coroot ((reflectionPerm i) j)) →
                                  RootPairing ι R M N
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) (CategoryTheory.Limits.biproduct.π g j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (p j)
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.Lex.isOrderedMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [MulLeftStrictMono α]
  [inst_3 : CommMonoid β] [inst_4 : Preorder β] [IsOrderedMonoid β], IsOrderedMonoid (Lex (α × β))
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousAt_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], UpperSemicontinuousAt (-f) a ↔ LowerSemicontinuousAt f a
-- Aesop.RuleTac.GoalDiff
Aesop.GoalDiff.mk.inj : ∀ {oldGoal newGoal : Lean.MVarId} {addedFVars removedFVars : Std.HashSet Lean.FVarId} {targetChanged : Bool}
  {oldGoal_1 newGoal_1 : Lean.MVarId} {addedFVars_1 removedFVars_1 : Std.HashSet Lean.FVarId} {targetChanged_1 : Bool},
  { oldGoal := oldGoal, newGoal := newGoal, addedFVars := addedFVars, removedFVars := removedFVars,
        targetChanged := targetChanged } =
      { oldGoal := oldGoal_1, newGoal := newGoal_1, addedFVars := addedFVars_1, removedFVars := removedFVars_1,
        targetChanged := targetChanged_1 } →
    oldGoal = oldGoal_1 ∧
      newGoal = newGoal_1 ∧ addedFVars = addedFVars_1 ∧ removedFVars = removedFVars_1 ∧ targetChanged = targetChanged_1
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsComonHom.hom_comul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.ComonObj M} {inst_3 : CategoryTheory.ComonObj N} (f : M ⟶ N)
  [self : CategoryTheory.IsComonHom f],
  CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, CategoryTheory.Sieve.generate ⊤ = ⊤
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` acts as a Galois group on `L/K` and the subgroup `H` acts as a Galois group on `L/B`,
then the fixing subgroup of `algebraMap B L` inside `G` equals `H`.
See `fixingSubgroup_range_algebraMap` for a more general version.  -/
IsGaloisGroup.fixingSubgroup_range_algebraMap' : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] [Finite G]
  (B : Type u_5) [inst_6 : CommSemiring B] [inst_7 : Algebra B L] [IsGaloisGroup (↥H) B L],
  fixingSubgroup G (Set.range ⇑(algebraMap B L)) = H
-- Init.Data.BitVec.Lemmas
BitVec.getElem_rotateLeft : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ} (h : i < w),
  (x.rotateLeft r)[i] = if h' : i < r % w then x[w - r % w + i] else x[i - r % w]
-- Lean.Elab.InfoTree.Types
Lean.Elab.DelabTermInfo.mk : Lean.Elab.TermInfo →
  Option Lean.DeclarationLocation → Option (Lean.PPContext → IO String) → Bool → Lean.Elab.DelabTermInfo
-- Init.Data.List.Sublist
List.Sublist.length_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → (l₁.length = l₂.length ↔ l₁ = l₂)
-- Lean.Declaration
Lean.Declaration.axiomDecl.sizeOf_spec : ∀ (val : Lean.AxiomVal), sizeOf (Lean.Declaration.axiomDecl val) = 1 + sizeOf val
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → ((d : ℕ) → motive (some d)) → (Unit → motive none) → motive x
-- Std.Http.Data.URI.Basic
/-- Returns the decoded username, or `none` if decoding fails UTF-8 validation.
 -/
Std.Http.URI.UserInfo.username? : Std.Http.URI.UserInfo → Option String
-- Mathlib.Order.Disjoint
Codisjoint.mono_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b c : α}, c ≤ b → Codisjoint a c → Codisjoint a b
-- Mathlib.Order.Birkhoff
LowerSet.supIrred_iff_of_finite : ∀ {α : Type u_1} [inst : PartialOrder α] {s : LowerSet α} [Finite α], SupIrred s ↔ ∃ a, LowerSet.Iic a = s
-- Mathlib.Order.Filter.Cocardinal
Filter.cocardinal.congr_simp : ∀ (α : Type u) {c c_1 : Cardinal.{u}} (e_c : c = c_1) (hreg : c.IsRegular),
  Filter.cocardinal α hreg = Filter.cocardinal α ⋯
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_singleton : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (b : α),
  AddAction.stabilizer G {b} = AddAction.stabilizer G b
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of `Set α`
on `Set β`.  -/
Set.mulAction : {α : Type u_2} → {β : Type u_3} → [inst : Monoid α] → [MulAction α β] → MulAction (Set α) (Set β)
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
FreeNonUnitalNonAssocAlgebra.lift_comp_of : ∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A]
  (F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A),
  (FreeNonUnitalNonAssocAlgebra.lift R) (⇑F ∘ FreeNonUnitalNonAssocAlgebra.of R) = F
-- Lean.DocString.Links
_private.Lean.DocString.Links.0.Lean.getManualRoot : Unit → String
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.instZeroHom_1 : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → {c : ComplexShape ι} → {C D : HomologicalComplex V c} → Zero (C ⟶ D)
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.ofBaseChangeAux_ι : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V) (v : V),
  (CliffordAlgebra.ofBaseChangeAux A Q) ((CliffordAlgebra.ι Q) v) =
    (CliffordAlgebra.ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd.congr_simp : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.toEnd R L M = LieModule.toEnd R L M
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SimplexCategory.toTopHomeo_naturality : ∀ {n m : SimplexCategory} (f : n ⟶ m),
  ⇑m.toTopHomeo ∘ ⇑(CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) =
    stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f) ∘ ⇑n.toTopHomeo
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.map_volume_mul_right : ∀ {a : ℝ},
  a ≠ 0 → MeasureTheory.Measure.map (fun x => x * a) MeasureTheory.volume = ENNReal.ofReal |a⁻¹| • MeasureTheory.volume
-- Mathlib.Analysis.ODE.Basic
/-- If `γ` is an integral curve at each `t ∈ s`, it is an integral curve on `s`.  -/
IsIntegralCurveAt.isIntegralCurveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ},
  (∀ t ∈ s, IsIntegralCurveAt γ v t) → IsIntegralCurveOn γ v s
-- Mathlib.Topology.Homotopy.HomotopyGroup
HomotopyGroup.auxGroup_indep : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i j : N),
  HomotopyGroup.auxGroup i = HomotopyGroup.auxGroup j
-- Mathlib.CategoryTheory.Yoneda
/-- A variant of the curried version of the Yoneda lemma with a raise in the universe level.  -/
CategoryTheory.uliftYonedaOpCompCoyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.uliftYoneda.{w, v₁, u₁}.op.comp CategoryTheory.coyoneda ≅
      (CategoryTheory.evaluation Cᵒᵖ (Type (max v₁ w))).comp
        ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type (max v₁ w))) (Type (max v₁ w))
              (Type (max (max w u₁) v₁))).obj
          CategoryTheory.uliftFunctor.{u₁, max v₁ w})
-- Std.Do.WP.Basic
_private.Std.Do.WP.Basic.0.Std.Do.EStateM.instWP.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_1 a s'
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.countPerms_filter_ne : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (m : Multiset α),
  m.countPerms = m.card.choose (Multiset.count a m) * (Multiset.filter (fun x => a ≠ x) m).countPerms
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.mem_of_mem_of_le : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE r.lower b → a ∈ b<...* → a ∈ r
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PathObject.RightHomotopy.weakEquivalence_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject Y)
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.weakEquivalences C).ContainsIdentities] {f₀ f₁ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁),
  HomotopicalAlgebra.WeakEquivalence f₀ ↔ HomotopicalAlgebra.WeakEquivalence f₁
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_vec_bit1_eq_alt1 : ∀ {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) (i : Fin (n + 1)),
  Matrix.vecCons x u (i + i + 1) = Matrix.vecAlt1 ⋯ (Matrix.vecAppend ⋯ (Matrix.vecCons x u) (Matrix.vecCons x u)) i
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
/-- If `V` is a finite `k`-module and `k` is finite, `ℙ k V` is finite.  -/
Projectivization.finite_of_finite : ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite V],
  Finite (Projectivization k V)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.sub : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] {i j k : ι}, b.IsPos i → j ∈ b.support → P.root k = P.root i - P.root j → b.IsPos k
-- Mathlib.Analysis.Convex.Quasiconvex
Antitone.quasilinearOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Antitone f → QuasilinearOn 𝕜 Set.univ f
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A category is called preadditive if `P ⟶ Q` is an abelian group such that composition is
linear in both variables.  -/
CategoryTheory.Preadditive : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Order.Cover
/-- **Alias** of the reverse direction of `ofDual_covBy_ofDual_iff`. -/
CovBy.ofDual : ∀ {α : Type u_1} [inst : LT α] {a b : αᵒᵈ}, b ⋖ a → OrderDual.ofDual a ⋖ OrderDual.ofDual b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_diff_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.Order.Concept
extentClosure_isClosed : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set α),
  (extentClosure r).IsClosed x = (lowerPolar r (upperPolar r x) = x)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.ofTwoCocycle_incl_apply : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] [inst_6 : LieRingModule L M]
  [inst_7 : LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : M),
  (LieAlgebra.Extension.ofTwoCocycle c).incl x = { carrier := (0, x) }
-- Init.Data.ToString.Extra
instToStringByteArray : ToString ByteArray
-- Mathlib.SetTheory.ZFC.PSet
PSet.subset_iff : ∀ {x y : PSet.{u_1}}, x ⊆ y ↔ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ y
-- Mathlib.Topology.Algebra.Order.Group
Filter.Tendsto.mabs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] {α : Type u_2} {l : Filter α} {f : α → G} {a : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => |f x|ₘ) l (nhds |a|ₘ)
-- Mathlib.Topology.UniformSpace.Defs
tendsto_right_nhds_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {a : α}, Filter.Tendsto (fun a' => (a', a)) (nhds a) (uniformity α)
-- Init.Data.String.Pattern.Basic
/-- Checks whether the slice ends with the pattern. If it does, the slice is returned with the
  suffix removed; otherwise the result is `none`.
   -/
String.Slice.Pattern.BackwardPattern.skipSuffix? : {ρ : Type} → (pat : ρ) → [self : String.Slice.Pattern.BackwardPattern pat] → (s : String.Slice) → Option s.Pos
-- Mathlib.Algebra.Order.Pi
Function.const_pos : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  0 < Function.const β a ↔ 0 < a
-- Mathlib.Analysis.Convex.Intrinsic
_private.Mathlib.Analysis.Convex.Intrinsic.0.aux : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (φ : α ≃ₜ β) (s : Set β),
  (interior s).Nonempty ↔ (interior (⇑φ ⁻¹' s)).Nonempty
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_ret_halt : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt) =
  Turing.TM2.Stmt.load (fun x => none) Turing.TM2.Stmt.halt
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.categoryAsType_comp : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  {X Y Z : CategoryTheory.FinCategory.AsType α} (f : Fin (Fintype.card (X ⟶ Y))) (g : Fin (Fintype.card (Y ⟶ Z))),
  CategoryTheory.CategoryStruct.comp f g =
    (Fintype.equivFin (X ⟶ Z))
      (CategoryTheory.CategoryStruct.comp ((Fintype.equivFin (X ⟶ Y)).symm f) ((Fintype.equivFin (Y ⟶ Z)).symm g))
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_functor_obj : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N) (a : CategoryTheory.SingleObj M),
  e.toSingleObjEquiv.functor.obj a = a
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.alterₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (f : Option (β a) → Option (β a)),
  m.alterₘ a f =
    if h : m.containsₘ a = true then
      let buckets' :=
        Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a fun l => Std.DHashMap.Internal.AssocList.alter a f l;
      have size' :=
        if Std.DHashMap.Internal.Raw₀.containsₘ ⟨Std.DHashMap.Internal.withComputedSize buckets', ⋯⟩ a = true then
          (↑m).size
        else (↑m).size - 1;
      ⟨{ size := size', buckets := buckets' }, ⋯⟩
    else
      match f none with
      | none => m
      | some b => (m.consₘ a b).expandIfNecessary
-- Mathlib.RingTheory.Derivation.DifferentialRing
Differential.mk : {R : Type u_1} → [inst : CommRing R] → Derivation ℤ R R → Differential R
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- The complex unit disc, denoted as `𝔻` within the Complex namespace  -/
Complex.UnitDisc.term𝔻 : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x''} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : (out : β) → out ∈ it → γ → m (ForInStep γ)},
  forIn' it init f =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let __do_lift ← f out ⋯ init
      match __do_lift with
        | ForInStep.yield c => forIn' it' c fun out_1 h'' acc => f out_1 ⋯ acc
        | ForInStep.done c => pure c
    | ⟨Std.IterStep.skip it', h⟩ => forIn' it' init fun out h' acc => f out ⋯ acc
    | ⟨Std.IterStep.done, property⟩ => pure init
-- Batteries.Util.ProofWanted
/-- Information returned by `classifyWantedRef`: the wrapper kind, the parameter-binder type
syntax to use when referencing it (a Π-type over `nm`'s user binders, ending in the appropriate
`.Stmt`/`.Val` accessor), a flag saying whether the recorded payload is a typeclass — the
generated parameter is then an instance binder — and the non-class dependencies to surface.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefInfo : Type
-- Lean.Message
Lean.MessageSeverity : Type
-- Mathlib.RingTheory.Int.Basic
prime_two_or_dvd_of_dvd_two_mul_pow_self_two : ∀ {m : ℤ} {p : ℕ}, Nat.Prime p → ↑p ∣ 2 * m ^ 2 → p = 2 ∨ p ∣ m.natAbs
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The isomorphism between
morphisms from the cone point of the colimit cocone for `F` to `W`
and cocones over `F` with cone point `W`
is natural in `F`.
 -/
CategoryTheory.Limits.colimCoyoneda : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] →
          CategoryTheory.Limits.colim.op.comp
              (CategoryTheory.coyoneda.comp
                ((CategoryTheory.Functor.whiskeringRight C (Type v) (Type (max v u₁))).obj
                  CategoryTheory.uliftFunctor.{u₁, v})) ≅
            CategoryTheory.cocones J C
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_get_MonadState_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {post : σ → Pred} {epost : EPred} [inst_4 : MonadStateOf σ m],
  Std.Internal.Do.wp get post epost = Std.Internal.Do.wp MonadStateOf.get post epost
-- Mathlib.Topology.Category.CompHaus.Basic
/-- The Stone-Cech compactification functor from topological spaces to compact Hausdorff spaces,
left adjoint to the inclusion functor.
 -/
topToCompHaus : CategoryTheory.Functor TopCat CompHaus
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.instFaithfulSMulSubtypeMem : ∀ {K : Type u} [inst : DivisionRing K] {X : Type u_1} [inst_1 : SMul K X] [FaithfulSMul K X] (F : Subfield K),
  FaithfulSMul (↥F) X
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X},
  (∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f) → R = S
-- Init.Data.Array.MinMax
Array.max?_eq_none_iff : ∀ {α : Type u_1} {xs : Array α} [inst : Max α], xs.max? = none ↔ xs = #[]
-- Lean.Expr
/-- Return `Not p`  -/
Lean.mkNot : Lean.Expr → Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `Ring` instance  -/
Lean.Meta.Grind.Arith.Linear.Struct.ringInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- An image map is a morphism `image f → image g` fitting into a commutative square and satisfying
the obvious commutativity conditions.  -/
CategoryTheory.Limits.ImageMap.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        [inst_2 : CategoryTheory.Limits.HasImage g.hom] →
          {sq : f ⟶ g} →
            CategoryTheory.Limits.ImageMap sq → (CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
-- Mathlib.Data.NNReal.Defs
/-- Extension for the `positivity` tactic: `Real.nnabs`  -/
Mathlib.Meta.Positivity.evalRealNNAbs : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of morphisms `f : W ⟶ Y` and
`g : W ⟶ Z` induces a morphism `coprod.map f g : W ⨿ X ⟶ Y ⨿ Z`.  -/
CategoryTheory.Limits.coprod.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] →
        [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z] → (W ⟶ Y) → (X ⟶ Z) → (W ⨿ X ⟶ Y ⨿ Z)
-- Mathlib.Order.Interval.Set.Basic
Set.eq_endpoints_or_mem_Ioo_of_mem_Icc : ∀ {α : Type u_1} [inst : PartialOrder α] {a b x : α}, x ∈ Set.Icc a b → x = a ∨ x = b ∨ x ∈ Set.Ioo a b
-- Init.PropLemmas
left_eq_dite_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x : α} {y : ¬p → α},
  (x = if h : p then x else y h) ↔ ∀ (h : ¬p), x = y h
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the third point with the midpoint of the segment
between the second point and that point.  -/
EuclideanGeometry.oangle_midpoint_rev_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), EuclideanGeometry.oangle p₁ p₂ (midpoint ℝ p₂ p₃) = EuclideanGeometry.oangle p₁ p₂ p₃
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.mk.inj : ∀ {p : Lean.Grind.CommRing.Poly} {h : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof} {sugar id : ℕ}
  {p_1 : Lean.Grind.CommRing.Poly} {h_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof} {sugar_1 id_1 : ℕ},
  { p := p, h := h, sugar := sugar, id := id } = { p := p_1, h := h_1, sugar := sugar_1, id := id_1 } →
    p = p_1 ∧ h = h_1 ∧ sugar = sugar_1 ∧ id = id_1
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.instInhabitedCaseArraySizesSubgoal : Inhabited Lean.Meta.CaseArraySizesSubgoal
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instNontrivial : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [Nontrivial M], Nontrivial (LieSubmodule R L M)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualEquivDual_apply : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Subspace K V}
  (φ : Module.Dual K ↥W), W.dualEquivDual φ = ⟨W.dualLift φ, ⋯⟩
-- Mathlib.Tactic.Widget.StringDiagram
/-- The horizontal position of the strand in the string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.Strand.hPos : Mathlib.Tactic.Widget.StringDiagram.Strand → ℕ