mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- An induction principle for closure membership for predicates with two arguments.  -/
Subgroup.closure_induction₂ : ∀ {G : Type u_1} [inst : Group G] {k : Set G} {p : (x y : G) → x ∈ Subgroup.closure k → y ∈ Subgroup.closure k → Prop},
  (∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) →
    (∀ (x : G) (hx : x ∈ Subgroup.closure k), p 1 x ⋯ hx) →
      (∀ (x : G) (hx : x ∈ Subgroup.closure k), p x 1 hx ⋯) →
        (∀ (x y z : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k) (hz : z ∈ Subgroup.closure k),
            p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
          (∀ (y z x : G) (hy : y ∈ Subgroup.closure k) (hz : z ∈ Subgroup.closure k) (hx : x ∈ Subgroup.closure k),
              p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
            (∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x y hx hy → p x⁻¹ y ⋯ hy) →
              (∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x y hx hy → p x y⁻¹ hx ⋯) →
                ∀ {x y : G} (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x y hx hy
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.imageIsoRange_hom_subtype : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).hom
      (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype) =
    CategoryTheory.Limits.image.ι f
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
Finsupp.toFreeAbelianGroup.eq_1 : ∀ {X : Type u_1},
  Finsupp.toFreeAbelianGroup =
    Finsupp.liftAddHom fun x => (smulAddHom ℤ (FreeAbelianGroup X)).flip (FreeAbelianGroup.of x)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddOffset_3 : HAdd Std.Time.Timestamp Std.Time.Minute.Offset Std.Time.Timestamp
-- Mathlib.Data.Finsupp.AList
Finsupp.mem_toAlist : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {x : α}, x ∈ f.toAList ↔ f x ≠ 0
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Product of two diffeomorphisms.  -/
Diffeomorph.prodCongr : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {F : Type u_4} →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_5} →
                        [inst_7 : TopologicalSpace H] →
                          {H' : Type u_6} →
                            [inst_8 : TopologicalSpace H'] →
                              {G : Type u_7} →
                                [inst_9 : TopologicalSpace G] →
                                  {G' : Type u_8} →
                                    [inst_10 : TopologicalSpace G'] →
                                      {I : ModelWithCorners 𝕜 E H} →
                                        {I' : ModelWithCorners 𝕜 E' H'} →
                                          {J : ModelWithCorners 𝕜 F G} →
                                            {J' : ModelWithCorners 𝕜 F G'} →
                                              {M : Type u_9} →
                                                [inst_11 : TopologicalSpace M] →
                                                  [inst_12 : ChartedSpace H M] →
                                                    {M' : Type u_10} →
                                                      [inst_13 : TopologicalSpace M'] →
                                                        [inst_14 : ChartedSpace H' M'] →
                                                          {N : Type u_11} →
                                                            [inst_15 : TopologicalSpace N] →
                                                              [inst_16 : ChartedSpace G N] →
                                                                {N' : Type u_12} →
                                                                  [inst_17 : TopologicalSpace N'] →
                                                                    [inst_18 : ChartedSpace G' N'] →
                                                                      {n : WithTop ℕ∞} →
                                                                        Diffeomorph I I' M M' n →
                                                                          Diffeomorph J J' N N' n →
                                                                            Diffeomorph (I.prod J) (I'.prod J') (M × N)
                                                                              (M' × N') n
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_intCast : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Module R (Additive ℤˣ)] (u : ℤˣ) (z : ℤ), u ^ ↑z = u ^ z
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.mem_ofFixingAddSubgroup_insert_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {a : α}
  {s : Set ↥(SubAddAction.ofStabilizer M a)} {x : α},
  x ∈ SubAddAction.ofFixingAddSubgroup M (insert a ((fun x => ↑x) '' s)) ↔
    ∃ (hx : x ∈ SubAddAction.ofStabilizer M a),
      ⟨x, hx⟩ ∈ SubAddAction.ofFixingAddSubgroup (↥(AddAction.stabilizer M a)) s
-- Batteries.Data.Vector.Lemmas
Vector.getElem_scanl : ∀ {β : Type u_1} {α : Type u_2} {n i : ℕ} {init : β} {f : β → α → β} {as : Vector α n} (h : i < n + 1),
  (Vector.scanl f init as)[i] = Vector.foldl f init (as.take i)
-- Mathlib.Topology.MetricSpace.Completion
UniformSpace.Completion.dist_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : UniformSpace.Completion α), dist x x = 0
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_shift' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} [inst_7 : W.IsCompatibleWithShift M] {a : M}
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (n a' : M) (h : a + n = a'),
  (CategoryTheory.Localization.SmallHom.equiv W L) (f.shift n a' h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L n).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Localization.SmallHom.equiv W L) f))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso L a).hom.app Y))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a n a' h).inv.app (L.obj Y))
            ((CategoryTheory.Functor.commShiftIso L a').inv.app Y))))
-- Mathlib.GroupTheory.Finiteness
Group.closure_finite_fg : ∀ {G : Type u_3} [inst : Group G] (s : Set G) [Finite ↑s], Group.FG ↥(Subgroup.closure s)
-- Init.Data.SInt.Lemmas
Int32.ne_iff_toBitVec_ne : ∀ {a b : Int32}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Ring.lift_comp_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] (P : Type u_7) [inst_7 : NonAssocSemiring P] (g : (i : ι) → G i →+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι},
  (DirectLimit.Ring.lift G f P g Hg).comp (DirectLimit.Ring.of G f i) = g i
-- Mathlib.Data.Seq.Basic
Stream'.Seq.ofList.eq_1 : ∀ {α : Type u} (l : List α), ↑l = ⟨fun x => l[x]?, ⋯⟩
-- Init.Data.Vector.Extract
Vector.set_extract : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j k : ℕ} (h : k < min j n - i) {a : α},
  (xs.extract i j).set k a h = (xs.set (i + k) a ⋯).extract i j
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.IsRightContinuous.measurableSet : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {𝓕 : MeasureTheory.Filtration ι m}
  [𝓕.IsRightContinuous] {i : ι} {s : Set Ω}, MeasurableSet s → MeasurableSet s
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f : X.I → Y.I)
  (φ : (i : X.I) → X.obj i ⟶ Y.obj (f i)) (f_1 : X.I → Y.I) (φ_1 : (i : X.I) → X.obj i ⟶ Y.obj (f_1 i)),
  ({ f := f, φ := φ } = { f := f_1, φ := φ_1 }) = (f = f_1 ∧ φ ≍ φ_1)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.normal.sizeOf_spec : ∀ (promise : IO.Promise (Option Std.Http.Chunk)),
  sizeOf (Std.Http.Body.Channel.Consumer.normal✝ promise) = 1 + sizeOf promise
-- Mathlib.Data.Int.GCD
pow_intGCD_eq_one : ∀ {M : Type u_1} [inst : Group M] {a : M} {m n : ℤ}, a ^ m.gcd n = 1 ↔ a ^ m = 1 ∧ a ^ n = 1
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.mk.inj : ∀ {K : Type} {kDecidableEq : DecidableEq K} {kFin : Fintype K} {k₀ k₁ : K} {Γ : K → Type} {Λ : Type} {main : Λ}
  {ΛFin : Fintype Λ} {σ : Type} {initialState : σ} {σFin : Fintype σ} {Γk₀Fin : Fintype (Γ k₀)}
  {m : Λ → Turing.TM2.Stmt Γ Λ σ} {K_1 : Type} {kDecidableEq_1 : DecidableEq K_1} {kFin_1 : Fintype K_1}
  {k₀_1 k₁_1 : K_1} {Γ_1 : K_1 → Type} {Λ_1 : Type} {main_1 : Λ_1} {ΛFin_1 : Fintype Λ_1} {σ_1 : Type}
  {initialState_1 : σ_1} {σFin_1 : Fintype σ_1} {Γk₀Fin_1 : Fintype (Γ_1 k₀_1)}
  {m_1 : Λ_1 → Turing.TM2.Stmt Γ_1 Λ_1 σ_1},
  { K := K, kDecidableEq := kDecidableEq, kFin := kFin, k₀ := k₀, k₁ := k₁, Γ := Γ, Λ := Λ, main := main, ΛFin := ΛFin,
        σ := σ, initialState := initialState, σFin := σFin, Γk₀Fin := Γk₀Fin, m := m } =
      { K := K_1, kDecidableEq := kDecidableEq_1, kFin := kFin_1, k₀ := k₀_1, k₁ := k₁_1, Γ := Γ_1, Λ := Λ_1,
        main := main_1, ΛFin := ΛFin_1, σ := σ_1, initialState := initialState_1, σFin := σFin_1, Γk₀Fin := Γk₀Fin_1,
        m := m_1 } →
    K = K_1 ∧
      kDecidableEq ≍ kDecidableEq_1 ∧
        kFin ≍ kFin_1 ∧
          k₀ ≍ k₀_1 ∧
            k₁ ≍ k₁_1 ∧
              Γ ≍ Γ_1 ∧
                Λ = Λ_1 ∧
                  main ≍ main_1 ∧
                    ΛFin ≍ ΛFin_1 ∧
                      σ = σ_1 ∧ initialState ≍ initialState_1 ∧ σFin ≍ σFin_1 ∧ Γk₀Fin ≍ Γk₀Fin_1 ∧ m ≍ m_1
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveExprProps.mk.inj : ∀ {expr expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx}, { expr := expr } = { expr := expr_1 } → expr = expr_1
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
/-- A cochain complex `L` is K-injective if any morphism `K ⟶ L`
with `K` acyclic is homotopic to zero.  -/
CochainComplex.IsKInjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [inst_1 : CategoryTheory.Abelian C] → CochainComplex C ℤ → Prop
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- An invariant σ-finite measure is absolutely continuous with respect to a Haar measure in a
second countable group.  -/
MeasureTheory.Measure.absolutelyContinuous_isHaarMeasure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] [LocallyCompactSpace G] [SecondCountableTopology G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SigmaFinite μ] [μ.IsMulLeftInvariant] [ν.IsHaarMeasure], μ.AbsolutelyContinuous ν
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_fst'_eq_p₁ : ∀ {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.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) (hf₁.fst' f₂) =
    CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃
-- Mathlib.LinearAlgebra.Dimension.LinearMap
/-- **Alias** of `LinearMap.rank_finsetSum_le`. -/
LinearMap.rank_finset_sum_le : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] {η : Type u_1} (s : Finset η) (f : η → V →ₗ[K] V'),
  (∑ d ∈ s, f d).rank ≤ ∑ d ∈ s, (f d).rank
-- Init.Data.Fin.Lemmas
Fin.lt_succ : ∀ {n : ℕ} {a : Fin n}, a.castSucc < a.succ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_singleton_pow : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (n : ℕ),
  0 < n → ProjectiveSpectrum.zeroLocus 𝒜 {f ^ n} = ProjectiveSpectrum.zeroLocus 𝒜 {f}
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_le_apply_gfpApprox_of_lt : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}},
  a < b → OrdinalApprox.gfpApprox f x b ≤ f (OrdinalApprox.gfpApprox f x a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_inter!_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 : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter! m₂).get! k = default
-- Mathlib.Control.Functor
/-- The map operation of the `Const γ` functor.  -/
Functor.Const.map : {γ : Type u_1} → {α : Type u_2} → {β : Type u_3} → (α → β) → Functor.Const γ β → Functor.Const γ α
-- Lean.Meta.Sym.Arith.Types
/-- If this is a `OfSemiring.Q α` ring, this field contains the
`semiringId` for `α`.
 -/
Lean.Meta.Sym.Arith.CommRing.semiringId? : Lean.Meta.Sym.Arith.CommRing → Option ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_map : ∀ {n m : SimplexCategory} (f : n ⟶ m), SSet.yonedaEquiv (SSet.stdSimplex.map f) = SSet.stdSimplex.objEquiv.symm f
-- Mathlib.Analysis.Normed.Group.Uniform
abs_dist_sub_le_dist_add_add : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E),
  |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ + a₂) (b₁ + b₂)
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Equivalence $(M/W)^* \cong \operatorname{ann}(W)$. That is, there is a one-to-one
correspondence between the dual of `M ⧸ W` and those elements of the dual of `M` that
vanish on `W`.

The inverse of this is `Submodule.dualCopairing`.  -/
Submodule.dualQuotEquivDualAnnihilator : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (W : Submodule R M) → Module.Dual R (M ⧸ W) ≃ₗ[R] ↥W.dualAnnihilator
-- Mathlib.Order.Bounds.Basic
mem_upperBounds_iff_subset_Iic : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, a ∈ upperBounds s ↔ s ⊆ Set.Iic a
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_or_nontrivial : ∀ {α : Type u} (s : Set α), s.Subsingleton ∨ s.Nontrivial
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNonAssocSemiring : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [NonAssocSemiring β] → NonAssocSemiring (MeasureTheory.SimpleFunc α β)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_pos_of_nonneg : ∀ {p : ℝ} {x : ENNReal}, 0 < x → 0 ≤ p → 0 < x ^ p
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Complex.Basic
Complex.isClosedEmbedding_intCast : Topology.IsClosedEmbedding Int.cast
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.hom_map_lift : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] {N : Type u_5} [inst_1 : Monoid N] (g : M →* N) (f : α → M)
  (x : FreeMonoid α), g ((FreeMonoid.lift f) x) = (FreeMonoid.lift (⇑g ∘ f)) x
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vadd_vadd_le : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v v' : V) (p p' : P), dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofBitVec : ∀ {a : BitVec 64}, { toBitVec := a }.toNat = a.toNat
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_ric : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [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]
  [inst_4 : Std.PRange.Least? α] [inst_5 : LE α] [inst_6 : DecidableLE α] [inst_7 : Std.PRange.UpwardEnumerable α]
  [inst_8 : Std.Rxc.IsAlwaysFinite α] [inst_9 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_10 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_11 : Std.PRange.LawfulUpwardEnumerableLE α]
  {xs : Std.Ric α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Analysis.Normed.Group.Indicator
nnnorm_indicator_eq_indicator_nnnorm : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α),
  ‖s.indicator f a‖₊ = s.indicator (fun a => ‖f a‖₊) a
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasAbsLeftKanLift.commute : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [self : CategoryTheory.Bicategory.HasAbsLeftKanLift f g] {x : B} (h : x ⟶ c),
  CategoryTheory.Bicategory.LanLift.CommuteWith f g h
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_mul_two_pow : ∀ (x j i : ℕ), (x * 2 ^ i).testBit j = (decide (i ≤ j) && x.testBit (j - i))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_iff_isSome_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∈ m ↔ m[a]?.isSome = true
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.rightQuotientEquiv_apply : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {f : Quotient (QuotientGroup.rightRel H) → G}
  (hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q) (q : Quotient (QuotientGroup.rightRel H)),
  ↑(⋯.rightQuotientEquiv q) = f q
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Internal implementation detail of the iterator library.  -/
Std.IterM.Partial.instForIn' : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] →
          [MonadLiftT m n] →
            [Monad n] → ForIn' n (Std.IterM.Partial m β) β { mem := fun it out => it.it.IsPlausibleIndirectOutput out }
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_comp_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : CategoryTheory.ShortComplex.QuasiIso φ],
  CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔
    CategoryTheory.ShortComplex.QuasiIso φ'
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.integrableExpSet_eq_univ : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ProbabilityTheory.integrableExpSet X μ = Set.univ
-- Mathlib.Algebra.Lie.Basic
LieHom.mk.sizeOf_spec : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] [inst_5 : SizeOf R] [inst_6 : SizeOf L] [inst_7 : SizeOf L']
  (toLinearMap : L →ₗ[R] L')
  (map_lie' : ∀ {x y : L}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆),
  sizeOf { toLinearMap := toLinearMap, map_lie' := map_lie' } = 1 + sizeOf toLinearMap
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_7.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Mathlib.Algebra.Group.Basic
mul_div_mul_left_eq_div : ∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), c * a / (c * b) = a / b
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_minValue : Int8.minValue.toNatClampNeg = 0
-- Mathlib.Order.UpperLower.Prod
LowerSet.inf_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s₁ s₂ : LowerSet α) (t : LowerSet β),
  (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
-- Mathlib.Order.RelSeries
RelSeries.reverse_apply : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)), p.reverse.toFun i = p.toFun i.rev
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle._auto_1) {Z : C}
  (h_1 : HomologicalComplex.homology T.obj₁ n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.homologyδOfTriangle T n₀ n₁ h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ h)
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁) h_1)
-- Std.Internal.Do.WP.Basic
_private.Std.Internal.Do.WP.Basic.0.Std.Internal.Do.EStateM.wpInst.match_1.eq_1 : ∀ {ε σ α : Type} (motive : EStateM.Result ε σ α → Sort u_1) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (el : ε) → (s' : σ) → motive (EStateM.Result.error el s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error el s' => h_2 el s') =
    h_1 a s'
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.fg_adjoin_of_finite : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {t : Set E},
  t.Finite → (IntermediateField.adjoin F t).FG
-- Mathlib.Topology.Algebra.Group.Basic
mul_mem_connectedComponent_one : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : MulOneClass G] [ContinuousMul G] {g h : G},
  g ∈ connectedComponent 1 → h ∈ connectedComponent 1 → g * h ∈ connectedComponent 1
-- Init.Data.List.Nat.Range
List.pairwise_lt_range' : ∀ {s n : ℕ} (step : optParam ℕ 1),
  autoParam (0 < step) List.pairwise_lt_range'._auto_1 → List.Pairwise (fun x1 x2 => x1 < x2) (List.range' s n step)