mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.lift_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = 0) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift f k h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Data.Set.Function
Equiv.bijOn_symm_image : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α}, Set.BijOn (⇑e.symm) (⇑e '' s) s
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.neg_le_neg_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommGroup M]
  [inst_2 : PartialOrder M] [IsOrderedAddMonoid M] [inst_4 : IsTopologicalAddGroup M]
  (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
  MeasurableSet i → ((-w).restrict i ≤ (-v).restrict i ↔ v.restrict i ≤ w.restrict i)
-- Std.Http.Data.Status
Std.Http.Status.loopDetected.sizeOf_spec : sizeOf Std.Http.Status.loopDetected = 1
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.zero₃_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.zero₃._auto_1) {Z : C}
  (h_1 : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h))
      (CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.FieldTheory.Galois.Basic
/-- See `InfiniteGalois.fixedField_fixingSubgroup` for the infinite case,
i.e. without the `[FiniteDimensional F E]` assumption.  -/
IsGalois.fixedField_fixingSubgroup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  [FiniteDimensional F E] [h : IsGalois F E], IntermediateField.fixedField K.fixingSubgroup = K
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueNum.eq_1 : ∀ {α : Type u_3} (G : SimpleGraph α), G.cliqueNum = sSup {n | ∃ s, G.IsNClique n s}
-- Mathlib.Algebra.Group.Subgroup.Basic
sub_mem_comm_iff : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_6} {H : S} [inst_1 : SetLike S G] [AddSubgroupClass S G] {a b : G},
  a - b ∈ H ↔ b - a ∈ H
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.toMulHom_injective : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N], Function.Injective MonoidHom.toMulHom
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_setInterior_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {I : Set k} {n : ℕ} {s : Affine.Simplex k P n} {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ Affine.Simplex.setInterior I s ↔
      ∀ (i : Fin (n + 1)), w i ∈ I)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.of_vsub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β},
  (s -ᵥ t).Nonempty → t.Nonempty
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.lift_lt_univ : ∀ (c : Cardinal.{u}), Cardinal.lift.{u + 1, u} c < Cardinal.univ.{u, u + 1}
-- Mathlib.CategoryTheory.Extensive
/-- (Implementation) An auxiliary lemma for the proof that `TopCat` is finitary extensive.  -/
CategoryTheory.finitaryExtensiveTopCatAux : (Z : TopCat) →
  (f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) →
    CategoryTheory.Limits.IsColimit
      (CategoryTheory.Limits.BinaryCofan.mk
        (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
        (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr))
-- Lean.Parser.Module
Lean.Parser.ModuleParserState.mk.injEq : ∀ (pos : String.Pos.Raw) (recovering hasLeading : Bool) (pos_1 : String.Pos.Raw) (recovering_1 hasLeading_1 : Bool),
  ({ pos := pos, recovering := recovering, hasLeading := hasLeading } =
      { pos := pos_1, recovering := recovering_1, hasLeading := hasLeading_1 }) =
    (pos = pos_1 ∧ recovering = recovering_1 ∧ hasLeading = hasLeading_1)
-- Mathlib.Topology.Algebra.MulAction
Prod.continuousVAdd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [inst_4 : VAdd M Y] [ContinuousVAdd M X] [ContinuousVAdd M Y],
  ContinuousVAdd M (X × Y)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_add_three : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α] {a b c d e f : α},
  a ≤ d → b ≤ e → c ≤ f → a + b + c ≤ d + e + f
-- Lean.Meta.Sym.SymM
/-- Returns the `AlphaShareCommon` context with the checks enabled by the current configuration.  -/
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.checkedShareCtx : Lean.Meta.Sym.SymM Lean.Meta.Sym.AlphaShareCommon.Context
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of two unit vectors is less than or equal to `1`.  -/
real_inner_le_one_of_norm_eq_one : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  ‖x‖ = 1 → ‖y‖ = 1 → inner ℝ x y ≤ 1
-- Init.Data.Char.Order
Char.instLawfulOrderLT : Std.LawfulOrderLT Char
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.congr_eq_2 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) (x : Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  x = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) ≍
      h_2 ()
-- Mathlib.Data.List.Cycle
Cycle.empty_eq : ∀ {α : Type u_1}, ∅ = Cycle.nil
-- Mathlib.FieldTheory.AbelRuffini
/-- **Abel-Ruffini Theorem** (one direction): An irreducible polynomial with a `solvableByRad` root
has a solvable Galois group.  -/
isSolvable_gal_of_irreducible : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ solvableByRad F E → ∀ {q : Polynomial F}, Irreducible q → (Polynomial.aeval x) q = 0 → Group.IsSolvable q.Gal
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulRightMono.toMulPosMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulRightMono α], MulPosMono α
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The canonical (surjective) linear map `(relations.G →₀ A) →ₗ[A] relations.Quotient`.  -/
Module.Relations.toQuotient : {A : Type u} → [inst : Ring A] → (relations : Module.Relations A) → (relations.G →₀ A) →ₗ[A] relations.Quotient
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_rio_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ}, (Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
-- Std.Internal.Do.Triple.SpecLemmas
/-- Construct an invariant from a loop invariant `inv` and a break condition `onBreak`.

`inv` holds at the end of every loop iteration (including the breaking one), and `onBreak` holds in
addition to `inv` once the loop is done. For a normal `while` loop `onBreak` can be taken as the
negation of the loop condition.
 -/
Std.Internal.Do.RepeatInvariant.ofInvariantAndBreak : {α Pred : Type u} →
  [Std.Internal.Do.Assertion Pred] → (α → Pred) → (α → Pred) → Std.Internal.Do.RepeatInvariant α α Pred
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseClause : Std.Internal.Parsec.ByteArray.Parser (Array ℤ)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (self : CategoryTheory.Oplax.StrongTrans F G) →
            {a b : B} →
              (f : a ⟶ b) →
                CategoryTheory.CategoryStruct.comp (F.map f) (self.app b) ≅
                  CategoryTheory.CategoryStruct.comp (self.app a) (G.map f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDerivWithin_sinh_Icc : ∀ (n : ℕ) {a b : ℝ},
  a < b → ∀ {x : ℝ}, x ∈ Set.Icc a b → iteratedDerivWithin n Real.sinh (Set.Icc a b) x = iteratedDeriv n Real.sinh x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constGet?_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α},
  m₁.WF → m₂.WF → m₁.Equiv m₂ → Std.DHashMap.Raw.Const.get? m₁ k = Std.DHashMap.Raw.Const.get? m₂ k
-- Mathlib.Algebra.Order.Floor.Div
ceilDiv_one : ∀ {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : MulActionWithZero α β] [inst_5 : CeilDiv α β] [IsOrderedRing α] [Nontrivial α]
  (b : β), b ⌈/⌉ 1 = b
-- Lean.Parser.Extension
Lean.Parser.registerParserAttributeHook : Lean.Parser.ParserAttributeHook → IO Unit
-- Mathlib.Order.Atoms
/-- A lattice is coatomic iff every element other than `⊤` has a coatom above it.  -/
IsCoatomic : (α : Type u_2) → [inst : PartialOrder α] → [OrderTop α] → Prop
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_star : ∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : AddMonoid A] [inst_2 : StarAddMonoid A] (r : R),
  Unitization.inl (star r) = star (Unitization.inl r)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_zero : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂], LinearMap.range 0 = ⊥
-- Mathlib.LinearAlgebra.Span.Basic
/-- **Alias** of `Submodule.span_preimage_le`.

---

See also `Submodule.span_preimage_eq`.  -/
LinearMap.span_preimage_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  (f : M →ₛₗ[σ₁₂] M₂) (s : Set M₂), Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)
-- Mathlib.GroupTheory.HNNExtension
/-- The product of a `ReducedWord` as an element of the `HNNExtension`  -/
HNNExtension.NormalWord.ReducedWord.prod : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → (φ : ↥A ≃* ↥B) → HNNExtension.NormalWord.ReducedWord G A B → HNNExtension G A B φ
-- Mathlib.Geometry.Euclidean.Simplex
/-- The distance from a vertex to its `faceOppositeCentroid` equals `(n + 1)` times the distance
from the `centroid` to that `faceOppositeCentroid`.  -/
Affine.Simplex.dist_point_faceOppositeCentroid : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  dist (s.points i) (s.faceOppositeCentroid i) = (↑n + 1) * dist s.centroid (s.faceOppositeCentroid i)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.scoped.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Lean.Name) (a_1 : α),
  sizeOf (Lean.ScopedEnvExtension.Entry.scoped a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.mulInitial_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)],
  (CategoryTheory.Limits.mulInitial X).hom = CategoryTheory.Limits.prod.snd
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_zero_iff : ∀ {x : ℝ}, Chebyshev.psi x = 0 ↔ x < 2
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_sSup_of_directedOn : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.RingTheory.Etale.Field
IsArtinianRing.primeSpectrumEquivMaximalSpectrum.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsArtinianRing R],
  IsArtinianRing.primeSpectrumEquivMaximalSpectrum = IsArtinianRing.primeSpectrumEquivMaximalSpectrum
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil_append_of_mem_left : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] {x : V} (p : G.Walk u v) (q : G.Walk v w)
  (hx : x ∈ p.support), (p.append q).takeUntil x ⋯ = p.takeUntil x hx
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i'],
  K.truncLE' e = (K.op.truncGE' e.op).unop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) {Z : C}
  (h : I.right b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) =
    CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)
-- Std.Sat.AIG.Lemmas
_private.Std.Sat.AIG.Lemmas.0.Std.Sat.AIG.isConstant.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (h_1 : Unit → motive Std.Sat.AIG.Decl.false)
  (h_2 : (x : Std.Sat.AIG.Decl α) → motive x),
  (match Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_ne_top : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ 0 → x / y ≠ ⊤
-- Batteries.Recycling.RBTree.Lemmas
/-- The set `{x | cut x = .gt}` is upward-closed.  -/
RBTree.RBNode.IsCut.le_gt_trans : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} [self : RBTree.RBNode.IsCut cmp cut] {x y : α}
  [Std.TransCmp cmp], cmp x y ≠ Ordering.gt → cut y = Ordering.gt → cut x = Ordering.gt
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The norm of a `NonUnitalSeminormedRing` as a `RingSeminorm`.  -/
normRingSeminorm : (R : Type u_2) → [inst : NonUnitalSeminormedRing R] → RingSeminorm R
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Equivalence.enoughInjectives_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : C ≌ D),
  CategoryTheory.EnoughInjectives C ↔ CategoryTheory.EnoughInjectives D
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, m.size ≤ (m.erase k).size + 1
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.eventually_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u → ∃ a, ∀ᶠ (x : β) in f, u x ≤ a
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_range : ∀ {β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  {xs : Std.Legacy.Range} {init : β} {f : (a : ℕ) → a ∈ xs → β → m (ForInStep β)}
  (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List ℕ) (cur : ℕ) (suff : List ℕ) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry.expr : Lean.Meta.GeneralizeTelescope.Entry → Lean.Expr
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsFlat.loops_subset : ∀ {α : Type u_1} {M : Matroid α} {F : Set α}, M.IsFlat F → M.loops ⊆ F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).minKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.minKey?
-- Lean.Parser.Extra
Lean.Parser.withoutPosition.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.Vector.Lemmas
Vector.map_set : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {i : ℕ} {h : i < n} {a : α},
  Vector.map f (xs.set i a h) = (Vector.map f xs).set i (f a) h
-- Mathlib.Data.List.Basic
List.sublist_singleton : ∀ {α : Type u} {l : List α} {a : α}, l.Sublist [a] ↔ l = [] ∨ l = [a]
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoDiv hp (a + ↑m * p) b = toIcoDiv hp a b - ↑m
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.size_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.size = t₂.size
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.coe_comap : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F] [inst_6 : Module R F] (f : E →ₗ[R] F)
  (C : PointedCone R F), ↑(PointedCone.comap f C) = ⇑f ⁻¹' ↑C
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instZero : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} → [inst : SMul M X] → [inst_1 : Zero Y] → [inst_2 : SMulZeroClass N Y] → Zero (X →ₑ[σ] Y)
-- Init.Data.List.MinMax
List.max_cons_cons_nil : ∀ {α : Type u_1} [inst : Max α] {a b : α}, [a, b].max ⋯ = a ⊔ b
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_tprod_le_of_forall_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : NNReal},
  (∀ (i : ι), ‖f i‖₊ ≤ C) → ‖∏' (i : ι), f i‖₊ ≤ C
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_le_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x y : K), A.valuation x ≤ A.valuation y ↔ ∃ a, ↑a * y = x
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The short root `α`.  -/
RootPairing.EmbeddedG2.shortRoot : {ι : 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) → [P.EmbeddedG2] → M
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {km : α}, t.minKey? = some km → t.getKey! km = km
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => ‖f x‖ₑ) p μ
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.isCompletionInEmptyTacticBlock : Lean.FileMap → String.Pos.Raw → Lean.Syntax → Option String.Pos.Raw → Bool
-- Mathlib.FieldTheory.Galois.Basic
isGalois_bot : ∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], IsGalois F ↥⊥
-- Mathlib.Data.List.Sort
List.sortedGE_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, (List.map (⇑OrderDual.toDual) l).SortedGE ↔ l.SortedLE
-- Mathlib.Analysis.Normed.Ring.Basic
RingHomIsometric.nnnorm_map : ∀ {R₁ : Type u_5} {R₂ : Type u_6} [inst : SeminormedRing R₁] [inst_1 : SeminormedRing R₂] (σ : R₁ →+* R₂)
  [RingHomIsometric σ] (x : R₁), ‖σ x‖₊ = ‖x‖₊
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- Applying the compression makes the set smaller in colex. This is intuitive since a portion of
the set is being "shifted down" as `max U < max V`.  -/
Finset.UV.toColex_compress_lt_toColex : ∀ {α : Type u_1} [inst : LinearOrder α] {s U V : Finset α} {hU : U.Nonempty} {hV : V.Nonempty},
  U.max' hU < V.max' hV → UV.compress U V s ≠ s → toColex (UV.compress U V s) < toColex s
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
contDiffWithinAt_ext_coord_change : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] [IsManifold I n M] (x x' : M) {y : E},
  y ∈ ((extChartAt I x').symm.trans (extChartAt I x)).source →
    ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑(extChartAt I x').symm) (Set.range ↑I) y
-- Mathlib.Algebra.Group.Basic
/-- Version of `mul_left_iterate` that is fully applied, for `rw`.  -/
mul_left_iterate_apply : ∀ {M : Type u_4} [inst : Monoid M] {n : ℕ} (a b : M), (fun x => a * x)^[n] b = a ^ n * b
-- Lean.Meta.Tactic.Grind.Types
/-- A delayed theorem instantiation is an instantiation that includes one or more guards.
See `TheoremGuard`.
 -/
Lean.Meta.Grind.DelayedTheoremInstance : Type
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_univ : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  (MeasureTheory.Measure.pi μ) Set.univ = ∏ i, (μ i) Set.univ
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_mul_right' : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Finset β)
  (f : β → α) (a : α), Associated (s.gcd fun x => f x * a) (s.gcd f * a)