mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- All objects that can be reached by exactly `n` extensions from objects in `P`.  -/
CategoryTheory.ObjectProperty.extensionProductIter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → ℕ → CategoryTheory.ObjectProperty C
-- Std.Sat.AIG.Basic
Std.Sat.AIG.BinaryInput.rhs : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.BinaryInput → aig.Ref
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff! m₂).get? k = none
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.iff : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
  0 < k → (IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1)
-- Mathlib.Topology.UniformSpace.Completion
/-- The Hausdorff completion as an abstract completion.  -/
UniformSpace.Completion.cPkg : {α : Type u_4} → [inst : UniformSpace α] → AbstractCompletion.{u_4, u_4} α
-- Mathlib.Analysis.Convex.PathConnected
segment_image_Ico : ∀ {x y : ℝ}, x < y → ⇑(Path.segment x y) '' Set.Ico 0 1 = Set.Ico x y
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.extendCocone_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone (F.comp G)),
  (CategoryTheory.Functor.Final.extendCocone.obj c).pt = c.pt
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_bounded_subset_le : ∀ {α : Type u} (s : Set α) (c : Cardinal.{u}),
  Cardinal.mk { t // t ⊆ s ∧ Cardinal.mk ↑t ≤ c } ≤ max (Cardinal.mk ↑s) Cardinal.aleph0 ^ c
-- Mathlib.Order.Basic
/-- **Alias** of `le_of_le_of_eq`. -/
LE.le.trans_eq : ∀ {α : Type u_1} {a b c : α} [inst : LE α], a ≤ b → b = c → a ≤ c
-- Init.Data.Float.Float
instMinFloat : Min Float
-- Mathlib.Data.Fintype.EquivFin
isEmpty_fintype : ∀ {α : Type u_4}, IsEmpty (Fintype α) ↔ Infinite α
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasProdLocallyUniformlyOn f g s` means that the (potentially infinite) product `∏' i, f i b`
for `b : β` converges locally uniformly on `s` to `g b` (in the sense of
`TendstoLocallyUniformlyOn`).  -/
HasProdLocallyUniformlyOn : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → (β → α) → Set β → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.addNewArg : Lean.Expr → Lean.Elab.Tactic.ElimApp.M✝ Unit
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore condition of a difference, expressed in terms of `oreMin` and `oreSubtra`.  -/
AddOreLocalization.add_ore_eq : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (r : R) (s : ↥S),
  ↑(AddOreLocalization.oreSubtra r s) + r = AddOreLocalization.oreMin r s + ↑s
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.hasKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology], CategoryTheory.Limits.HasKernel S.g
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_getLast : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) (h : optParam (p.vertices ≠ []) ⋯),
  p.vertices.getLast h = b
-- Mathlib.Algebra.Group.Units.Basic
LeftCancelMonoid.eq_one_of_mul_left : ∀ {α : Type u} [inst : LeftCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → b = 1
-- Mathlib.RingTheory.Invariant.Basic
/-- The isomorphism between `stabilizer G Q ⧸ inertia G Q` and the Galois group of the residue fields.
 -/
IsFractionRing.stabilizerQuotientInertiaEquiv : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (G : Type u_3) →
            [inst_3 : Group G] →
              [Finite G] →
                [inst_5 : MulSemiringAction G B] →
                  [SMulCommClass G A B] →
                    (P : Ideal A) →
                      (Q : Ideal B) →
                        [Q.IsPrime] →
                          [inst_8 : Q.LiesOver P] →
                            (K : Type u_4) →
                              (L : Type u_5) →
                                [inst_9 : Field K] →
                                  [inst_10 : Field L] →
                                    [inst_11 : Algebra (A ⧸ P) K] →
                                      [inst_12 : Algebra (B ⧸ Q) L] →
                                        [inst_13 : Algebra (A ⧸ P) L] →
                                          [IsScalarTower (A ⧸ P) (B ⧸ Q) L] →
                                            [inst_15 : Algebra K L] →
                                              [IsScalarTower (A ⧸ P) K L] →
                                                [Algebra.IsInvariant A B G] →
                                                  [IsFractionRing (A ⧸ P) K] →
                                                    [IsFractionRing (B ⧸ Q) L] →
                                                      ↥(MulAction.stabilizer G Q) ⧸
                                                          Ideal.inertia (↥(MulAction.stabilizer G Q)) Q ≃*
                                                        Gal(L/K)
-- Init.Data.Option.Basic
/-- Flattens nested optional values, preserving any value found.

This is analogous to `List.flatten`.

Examples:
* `none.join = none`
* `(some none).join = none`
* `(some (some v)).join = some v`
 -/
Option.join : {α : Type u_1} → Option (Option α) → Option α
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The path object obtained by switching the two projections.  -/
HomotopicalAlgebra.PathObject.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.PathObject A → HomotopicalAlgebra.PathObject A
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The centroid of two points, expressed directly as adding a vector
to a point.  -/
Finset.centroid_pair : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : DecidableEq ι] [Invertible 2] (p : ι → P) (i₁ i₂ : ι),
  Finset.centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
-- Mathlib.Topology.Algebra.Monoid
Pi.continuousAdd : ∀ {ι : Type u_1} {C : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (C i)] [inst_1 : (i : ι) → Add (C i)]
  [∀ (i : ι), ContinuousAdd (C i)], ContinuousAdd ((i : ι) → C i)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.checkInv : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.row_weak_of_le : ∀ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j1 j2 : ℕ}, j1 ≤ j2 → (i, j2) ∈ μ → T i j1 ≤ T i j2
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ElabHeaderResult.checkLevelNames : Array Lean.Elab.Command.PreElabHeaderResult → Lean.Elab.TermElabM Unit
-- Mathlib.Geometry.Euclidean.Sphere.Power
_private.Mathlib.Geometry.Euclidean.Sphere.Power.0.EuclideanGeometry.cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p : P},
  dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p →
    EuclideanGeometry.angle p₁ p p₂ = Real.pi →
      EuclideanGeometry.angle p₃ p p₄ = Real.pi →
        ¬Collinear ℝ {p₁, p, p₃} → EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄}
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.ofHom_comp : ∀ {R S T : Type u} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] (f : R →+* S)
  (g : S →+* T),
  CommSemiRingCat.ofHom (g.comp f) =
    CategoryTheory.CategoryStruct.comp (CommSemiRingCat.ofHom f) (CommSemiRingCat.ofHom g)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.OplaxTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a)
  {Z : a' ⟶ H.obj a}
  (h :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.id (H.obj a))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapId a))) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapId a) (θ.app a)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor (θ.app a)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor (θ.app a)).inv) h))
-- Mathlib.Analysis.Convex.Visible
/-- If `s` is a closed set, then any point `x` sees some point of `s` in any direction where there
is something to see.  -/
IsClosed.exists_wbtw_isVisible : ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {y : V} [inst_2 : TopologicalSpace V]
  [IsTopologicalAddGroup V] [ContinuousSMul ℝ V],
  IsClosed s → y ∈ s → ∀ (x : V), ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
-- Init.Prelude
instMonadStateOfMonadStateOf : (σ : Type u) → (m : Type u → Type v) → [MonadStateOf σ m] → MonadState σ m
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_symm_conj : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁'), e.symm.conj (e.conj f) = f
-- Lean.Parser.Basic
Lean.Syntax.forArgsM : {m : Type → Type u_1} → [Monad m] → Lean.Syntax → (Lean.Syntax → m Unit) → m Unit
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LipschitzOnWith.comp_locallyBoundedVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {F : Type u_3}
  [inst_2 : PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E},
  LipschitzOnWith C f t →
    ∀ {g : α → E} {s : Set α}, Set.MapsTo g s t → LocallyBoundedVariationOn g s → LocallyBoundedVariationOn (f ∘ g) s
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mem_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : Set α} {hs : IsClosed s} {x : α},
  x ∈ { carrier := s, isClosed' := hs } ↔ x ∈ s
-- Mathlib.Tactic.Translate.ToDual
/-- The `to_dual_insert_cast_fun` attribute is used to tag types that should not be unfolded in a
proof that is translated. Instead, a casting function is inserted. This casting function then may be
translated by the translation attribute.  -/
Mathlib.Tactic.ToDual.«commandTo_dual_insert_cast_fun_:=_,_» : Lean.ParserDescr
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.foldlAux.eq_def : ∀ {α : Type u} (f : α → Char → α) (s : String) (stopPos i : String.Pos.Raw) (a : α),
  String.Legacy.foldlAux f s stopPos i a =
    if h : i < stopPos then
      have this := ⋯;
      String.Legacy.foldlAux f s stopPos (String.Pos.Raw.next s i) (f a (String.Pos.Raw.get s i))
    else a
-- Mathlib.GroupTheory.Exponent
/-- In a group of exponent two, every element is its own inverse.  -/
inv_eq_self_of_exponent_two : ∀ {G : Type u} [inst : Group G], Monoid.exponent G = 2 → ∀ (x : G), x⁻¹ = x
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isCoveringMapOn_of_vadd_disjoint : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  Topology.IsQuotientMap f →
    ∀ [ContinuousConstVAdd G E],
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) →
        (∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g +ᵥ e = e) →
          IsCoveringMapOn f (f '' {e | AddAction.stabilizer G e = ⊥})
-- Mathlib.Tactic.Simps.Basic
/-- Syntax for making a projection non-default in `initialize_simps_projections`.  -/
Lean.Parser.Command.simpsRule.erase : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_log_of_pow_lt : ∀ {x y : ℝ} {n : ℕ}, 0 < x → x ^ n < y → ↑n * Real.log x < Real.log y
-- Mathlib.CategoryTheory.Types.Basic
/-- The type of morphisms in `Type`.  -/
TypeCat.Hom : Type u → Type u → Type u
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.ruleSetsFeature : Lean.ParserDescr
-- Init.Data.List.Monadic
List.flatMapM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : List (Subtype P)} {f : α → m (List β)},
  List.flatMapM f xs.unattach =
    List.flatMapM
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_3 : CategoryTheory.FinallySmall C],
  (CategoryTheory.FinallySmall.fromFilteredFinalModel C).Final
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteSpanningSetsIn.mk.inj : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} {set : ℕ → Set α}
  {set_mem : ∀ (i : ℕ), set i ∈ C} {finite : ∀ (i : ℕ), μ (set i) < ⊤} {spanning : ⋃ i, set i = Set.univ}
  {set_1 : ℕ → Set α} {set_mem_1 : ∀ (i : ℕ), set_1 i ∈ C} {finite_1 : ∀ (i : ℕ), μ (set_1 i) < ⊤}
  {spanning_1 : ⋃ i, set_1 i = Set.univ},
  { set := set, set_mem := set_mem, finite := finite, spanning := spanning } =
      { set := set_1, set_mem := set_mem_1, finite := finite_1, spanning := spanning_1 } →
    set = set_1
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.ext : ∀ {X : Type u_3} {inst : MetricSpace X} {x y : Delone.DeloneSet X},
  x.carrier = y.carrier → x.packingRadius = y.packingRadius → x.coveringRadius = y.coveringRadius → x = y
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  MeasureTheory.pdf.IsUniform X s ℙ μ → μ s = 0 ∨ μ s = ⊤ → MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- The maps `hσ' q n m hnm` are compatible with the application of additive functors.  -/
AlgebraicTopology.DoldKan.map_hσ' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (G : CategoryTheory.Functor C D) [G.Additive] (X : CategoryTheory.SimplicialObject C) (q n m : ℕ)
  (hnm : AlgebraicTopology.DoldKan.c.Rel m n),
  AlgebraicTopology.DoldKan.hσ' q n m hnm = G.map (AlgebraicTopology.DoldKan.hσ' q n m hnm)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.smul_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] {R : Type u_10}
  [inst_6 : Monoid R] [inst_7 : DistribMulAction R V2] [inst_8 : SMulCommClass k R V2] (t : R) (f : P1 →ᵃ[k] V2),
  (t • f).linear = t • f.linear
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_filterMapM : ∀ {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [inst_14 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_16 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.filterMapM f it) init g ⦃ Q; eQ ⦄
-- Std.Do.SPred.Laws
Std.Do.SVal.evalsTo_total : ∀ {σs : List (Type u_1)} {α : Type u_1} {P : Std.Do.SPred σs} (f : Std.Do.SVal σs α), P ⊢ₛ ∃ m, f.evalsTo m
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_f₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).f₃₄ = F.map sq.f₃₄
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.PGL.mk_smul_mk : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (g : GL ι K) {v : ι → K}
  (hv : v ≠ 0), Matrix.ProjGenLinGroup.mk g • Projectivization.mk K v hv = Projectivization.mk K (g • v) ⋯
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.inr_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N], Function.Injective ⇑Monoid.Coprod.inr
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.epi₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₃ = 0 → CategoryTheory.Epi T.mor₂
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedAddCommGroup.Subgroup.negGen_neg : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G] (H : AddSubgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsAddCyclic ↥H], LinearOrderedAddCommGroup.Subgroup.negGen H < 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharTwoJNeZeroNF_spec : ∀ {F : Type u_2} [inst : Field F] [CharP F 2] (W : WeierstrassCurve F) (ha₁ : W.a₁ ≠ 0),
  (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.isUnit : ∀ {A : Type u_1} [inst : LE A] [inst_1 : Monoid A] [inst_2 : Zero A] {a : A}, IsStrictlyPositive a → IsUnit a
-- Mathlib.Algebra.DirectSum.Module
/-- Two `LinearMap`s out of a direct sum are equal if they agree on the generators.

See note [partially-applied ext lemmas].  -/
DirectSum.linearMap_ext : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] {N : Type u₁} [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] ⦃ψ ψ' : (DirectSum ι fun i => M i) →ₗ[R] N⦄,
  (∀ (i : ι), ψ ∘ₗ DirectSum.lof R ι M i = ψ' ∘ₗ DirectSum.lof R ι M i) → ψ = ψ'
-- Init.Data.Nat.Basic
Nat.ne_of_lt : ∀ {a b : ℕ}, a < b → a ≠ b
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getKey?_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m₁.Equiv m₂ → m₁.getKey? k = m₂.getKey? k
-- Init.Data.SInt.Lemmas
ISize.div_one : ∀ {a : ISize}, a / 1 = a
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.zero_ne_addChar : ∀ {i : String.Pos.Raw} {c : Char}, 0 ≠ i + c
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getBitVecValue? : Lean.Expr → OptionT Id Lean.Meta.Sym.BitVecValue
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- Summing the count of `x` over a list filtered by some `p` is just `countP` applied to `p`  -/
List.sum_map_count_dedup_filter_eq_countP : ∀ {α : Type u_2} [inst : DecidableEq α] (p : α → Bool) (l : List α),
  (List.map (fun x => List.count x l) (List.filter p l.dedup)).sum = List.countP p l
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hom_ofHom : ∀ {M N : Type u} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N),
  AddCommMonCat.Hom.hom (AddCommMonCat.ofHom f) = f
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNNRat_mul : ∀ {α : Type u_1} [inst : Semiring α] {f : α → α → α} {a b : α} {na nb nc da db dc k : ℕ},
  f = HMul.hMul →
    Mathlib.Meta.NormNum.IsNNRat a na da →
      Mathlib.Meta.NormNum.IsNNRat b nb db →
        na.mul nb = k.mul nc → da.mul db = k.mul dc → Mathlib.Meta.NormNum.IsNNRat (f a b) nc dc
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.toPerm_apply : ∀ {G : Type u_1} [inst : Add G] {a : G} (self : AddConstEquiv G G a a), AddConstEquiv.toPerm self = self.toEquiv
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.injective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N), Function.Injective ⇑e
-- Mathlib.MeasureTheory.Measure.Haar.Basic
NNReal.toReal.eq_1 : NNReal.toReal = Subtype.val
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_δ : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 2)) (hi : autoParam (n + i = m) SimplexCategory.δ₀Iter_δ._auto_1),
  autoParam (↑j ≤ i) SimplexCategory.δ₀Iter_δ._auto_3 →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i hi) (SimplexCategory.δ j) =
      SimplexCategory.δ₀Iter (i + 1) ⋯
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.add_sub_mul_of_commute : ∀ {R : Type u_1} {p q : R} [inst : NonUnitalRing R] [inst_1 : StarRing R],
  Commute p q → IsStarProjection p → IsStarProjection q → IsStarProjection (p + q - p * q)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Run monadic function `f` on each element of the tree (in increasing order).  -/
RBTree.RBMap.forM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {m : Type u_1 → Type u_2} → [Monad m] → (α → β → m PUnit.{u_1 + 1}) → RBTree.RBMap α β cmp → m PUnit.{u_1 + 1}
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- A graph is connected if it's preconnected and contains at least one vertex.
This follows the convention observed by mathlib that something is connected iff it has
exactly one connected component.

There is a `CoeFun` instance so that `h u v` can be used instead of `h.Preconnected u v`.  -/
SimpleGraph.Connected : {V : Type u} → SimpleGraph V → Prop
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToJsonMessageKind.toJson : Lean.JsonRpc.MessageKind → Lean.Json