mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Zip
Array.getElem?_zip_eq_some : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} {z : α × β} {i : ℕ},
  (as.zip bs)[i]? = some z ↔ as[i]? = some z.1 ∧ bs[i]? = some z.2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).maxKey! = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.mk.injEq : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (dom : L.Substructure M) (cod : L.Substructure N) (toEquiv : L.Equiv ↥dom ↥cod) (dom_1 : L.Substructure M)
  (cod_1 : L.Substructure N) (toEquiv_1 : L.Equiv ↥dom_1 ↥cod_1),
  ({ dom := dom, cod := cod, toEquiv := toEquiv } = { dom := dom_1, cod := cod_1, toEquiv := toEquiv_1 }) =
    (dom = dom_1 ∧ cod = cod_1 ∧ toEquiv ≍ toEquiv_1)
-- Mathlib.Analysis.Normed.Ring.Basic
norm_pow : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ), ‖a ^ n‖ = ‖a‖ ^ n
-- Std.Data.TreeSet.Iterator
Std.TreeMap.keys.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp), t.keys = t.inner.keys
-- Lean.Level
Lean.instHashableLevelMVarId.hash : Lean.LevelMVarId → UInt64
-- Init.Data.List.Attach
List.unattach_append : ∀ {α : Type u_1} {p : α → Prop} {l₁ l₂ : List { x // p x }}, (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach
-- Mathlib.Algebra.Algebra.Hom
AlgHomClass.toRingHomClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : FunLike F A B}
  [self : AlgHomClass F R A B], RingHomClass F A B
-- Std.Time.Format
/-- Parses a `String` in the dateTimeWithZone format and returns a `DateTime` object in the GMT time zone.
 -/
Std.Time.DateTime.fromDateTimeWithZoneString : String → Except String Std.Time.DateTime
-- Mathlib.Tactic.Widget.Calc
/-- Return the link text and inserted text above and below of the calc widget.  -/
suggestSteps : Array Lean.SubExpr.GoalsLocation →
  Lean.Expr → CalcParams → Lean.MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw))
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sup_support_list_prod_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
  [inst_3 : AddMonoid A] [inst_4 : AddMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (l : List (AddMonoidAlgebra R A)),
        l.prod.coeff.support.sup degb ≤ (List.map (fun f => f.coeff.support.sup degb) l).sum
-- Mathlib.Computability.Primrec.Basic
Primrec.fst : ∀ {α : Type u_2} {β : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec Prod.fst
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The direction of `⊥` is the submodule `⊥`.  -/
AffineSubspace.direction_bot : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], ⊥.direction = ⊥
-- Mathlib.Tactic.Linter.UpstreamableDecl
/-- If set to `true`, the `upstreamableDecl` linter will add warnings on private declarations.
 -/
Mathlib.Linter.linter.upstreamableDecl.private : Lean.Option Bool
-- Mathlib.Topology.Connected.LocallyConnected
connectedComponentIn_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α] {F : Set α} {x : α},
  F ∈ nhds x → connectedComponentIn F x ∈ nhds x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.proj_apply : ∀ {R : Type u_3} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {n : Type u_9} (i j : n) (x : n → A),
  (QuadraticMap.proj i j) x = x i * x j
-- Init.Data.UInt.Bitwise
UInt8.xor_right_inj : ∀ {a b : UInt8} (c : UInt8), c ^^^ a = c ^^^ b ↔ a = b
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.instInhabitedStartsWithResult : Inhabited Lean.Grind.AC.StartsWithResult✝
-- Aesop.Tree.Data
Aesop.GoalId.mk : ℕ → Aesop.GoalId
-- Mathlib.Algebra.Group.Basic
zpow_one_add : ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a ^ (1 + n) = a * a ^ n
-- Lean.Expr
/-- Given `a b : Prop`, returns `a = b`  -/
Lean.mkPropEq : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.zero : ∀ {M : Type u_1} {E : Type u_2} [inst : Bornology M] [inst_1 : Zero E] [inst_2 : SMulZeroClass M E] {s : Set E},
  0 ∈ s → Absorbs M s 0
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_of_not_ac : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  ¬μ.AbsolutelyContinuous ν → InformationTheory.klDiv μ ν = ⊤
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_comp_zero_cochain : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K 0) (m₁ : ℤ) (h₁ : n₁ + 1 = m₁),
  CochainComplex.HomComplex.δ n₁ m₁ (z₁.comp z₂ ⋯) =
    z₁.comp (CochainComplex.HomComplex.δ 0 1 z₂) h₁ + (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- Let `μ` be a σ-finite left invariant measure on `G`. Then `μ` is equal to the Haar measure
defined by `K₀` iff `μ K₀ = 1`.  -/
MeasureTheory.Measure.haarMeasure_eq_iff : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [SecondCountableTopology G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ]
  [μ.IsMulLeftInvariant], MeasureTheory.Measure.haarMeasure K₀ = μ ↔ μ ↑K₀ = 1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift_restrict : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] (f : FreeMonoid α →* M), FreeMonoid.lift (⇑f ∘ FreeMonoid.of) = f
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atTop_atBot_of_antitone : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → (∀ (b : β), ∃ a, f a ≤ b) → Filter.Tendsto f Filter.atTop Filter.atBot
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.instIsIdId : ∀ {M : Type u_1}, CompTriple.IsId id
-- Init.Data.String.Defs
String.append_left_inj : ∀ {s₁ s₂ : String} (t : String), s₁ ++ t = s₂ ++ t ↔ s₁ = s₂
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueSums.of_addOpposite : ∀ {G : Type u} [inst : Add G], TwoUniqueSums Gᵃᵒᵖ → TwoUniqueSums G
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w), (p.concat h).support = p.support ++ [w]
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.limitConeX_str : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat),
  (CategoryTheory.Cat.HasLimits.limitConeX F).str = inferInstance
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfRightIso_π_app_none : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g], (CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app none = f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.mk : List Lean.Expr → Lean.Meta.Grind.ParentSet
-- Mathlib.Data.Vector.Snoc
List.Vector.snoc.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : List.Vector α n) (x : α), xs.snoc x = xs ++ x ::ᵥ List.Vector.nil
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (l : α →₀ M),
  Finsupp.equivMapDomain f l =
    { support := Finset.map f.toEmbedding l.support, toFun := fun a => l (f.symm a), mem_support_toFun := ⋯ }
-- Mathlib.Algebra.Algebra.Hom
AlgHom.ext : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ₁ φ₂ : A →ₐ[R] B}, (∀ (x : A), φ₁ x = φ₂ x) → φ₁ = φ₂
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.instIsTrans : ∀ {M : Type u_1} [inst : Monoid M], IsTrans M Associated
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.head.eq_2 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 j k : ι) (_hne : j ≠ k)
  (w₁ : Monoid.CoprodI.NeWord M x j) (w₂ : Monoid.CoprodI.NeWord M k x_1), (w₁.append _hne w₂).head = w₁.head
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.brecOn : ∀ {R : Type u_1} [inst : Ring R]
  {motive : (M : Type u_2) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → IsFiniteLength R M → Prop}
  {M : Type u_2} {inst_1 : AddCommGroup M} {inst_2 : Module R M} (t : IsFiniteLength R M),
  (∀ (M : Type u_2) [inst_3 : AddCommGroup M] [inst_4 : Module R M] (t : IsFiniteLength R M),
      IsFiniteLength.below t → motive M t) →
    motive M t
-- Mathlib.Data.Int.ModEq
Int.ModEq.of_mul_right : ∀ {n a b : ℤ} (m : ℤ), a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n]
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.EMatchTheoremPtr : Type
-- Std.Sync.Notify
/-- Wait to be notified. Returns a task that completes when notify is called.
Note: if notify was called before wait, this will wait for the next notify call.
 -/
Std.Notify.wait : Std.Notify → IO (Std.Async.AsyncTask Unit)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mulVec_surjective_iff_isUnit : ∀ {m : Type u} [inst : DecidableEq m] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Fintype m] {A : Matrix m m R},
  Function.Surjective A.mulVec ↔ IsUnit A
-- Mathlib.Analysis.Convex.StrictConvexSpace
StrictConvexSpace.of_norm_add_ne_two : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2) → StrictConvexSpace ℝ E
-- Mathlib.RingTheory.LocalProperties.Injective
Module.injective_of_localization_maximal : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v, u} R]
  [IsNoetherianRing R],
  (∀ (I : Ideal R) (x : I.IsMaximal), Module.Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)) →
    Module.Injective R M
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `CompHausLike.LocallyConstant.functor` is left adjoint to the forgetful functor.
 -/
CompHausLike.LocallyConstant.adjunction : (P : TopCat → Prop) →
  [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    [inst : CompHausLike.HasProp P PUnit.{u + 1}] →
      [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
        [inst_2 : CompHausLike.HasExplicitPullbacks P] →
          (hs :
              ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
                CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
            [CompHausLike.HasExplicitFiniteCoproducts P] →
              CompHausLike.LocallyConstant.functor P hs ⊣
                (CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj
                  (Opposite.op (CompHausLike.of P PUnit.{u + 1}))
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.formula₂.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (r : L.Relations 2) (t₁ t₂ : L.Term α), r.formula₂ t₁ t₂ = r.formula ![t₁, t₂]
-- Init.Data.Int.Lemmas
Int.subNatNat_sub : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), Int.subNatNat (m - n) k = Int.subNatNat m (k + n)
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.zero_smul : ∀ {α : Type u_1} (𝕜 : Type u_3) {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (p : ENNReal)
  {q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp E q μ)), 0 • f = 0
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.loop.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Lean.Compiler.ExportAttr
_private.Lean.Compiler.ExportAttr.0.Lean.isValidCppName : Lean.Name → Bool
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_left_monotone : ∀ (o : Ordinal.{u_1}), Monotone fun x => Ordinal.veblen x o
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀)
  {Z : AlgebraicGeometry.Scheme} (h : 𝒰.affineRefinement.openCover.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f i)
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Cover.pullbackHom (𝒰.X i.fst).affineCover
        (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) i.snd)
      h
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.StrongCore.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η : F ⟶ G}
  {naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (η.app b)}
  {naturality_hom :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
      CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom._autoParam}
  {naturality_1 :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (η.app b)}
  {naturality_hom_1 :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality_1 f).hom = η.naturality f)
      CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom._autoParam},
  { naturality := naturality, naturality_hom := naturality_hom } =
      { naturality := naturality_1, naturality_hom := naturality_hom_1 } →
    naturality = naturality_1
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CnstrRHS.mk.inj : ∀ {levelNames : Array Lean.Name} {numMVars : ℕ} {expr : Lean.Expr} {levelNames_1 : Array Lean.Name} {numMVars_1 : ℕ}
  {expr_1 : Lean.Expr},
  { levelNames := levelNames, numMVars := numMVars, expr := expr } =
      { levelNames := levelNames_1, numMVars := numMVars_1, expr := expr_1 } →
    levelNames = levelNames_1 ∧ numMVars = numMVars_1 ∧ expr = expr_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f' f) g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.IsOpenPosMeasure.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X},
  (∀ (U : Set X), IsOpen U → U.Nonempty → μ U ≠ 0) → μ.IsOpenPosMeasure
-- Mathlib.Logic.Denumerable
Denumerable.nat : Denumerable ℕ
-- Std.Time.Zoned
/-- Converts a `PlainDate` to a `DateTime` using `TimeZone`.
 -/
Std.Time.DateTime.ofLocalDateWithZone : Std.Time.PlainDate → Std.Time.TimeZone → Std.Time.DateTime
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_isCycle₁_of_mem_fixedPoints : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A] (g : G),
  ∀ a ∈ MulAction.fixedPoints G A, groupHomology.IsCycle₁ fun₀ | g => a
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instMonoid : {G : Type u_1} → [inst : Add G] → {a : G} → Monoid (AddConstMap G G a a)
-- Init.Data.Option.Monadic
_private.Init.Data.Option.Monadic.0.Option.instForIn'InferInstanceMembershipOfMonad.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (r : β) (h_1 : (r : β) → motive (ForInStep.done r))
  (h_2 : (r : β) → motive (ForInStep.yield r)),
  (match ForInStep.done r with
    | ForInStep.done r => h_1 r
    | ForInStep.yield r => h_2 r) =
    h_1 r
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule : ∀ {ι : 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) [NeZero 2]
  [IsDomain R] [Module.IsTorsionFree R M] (q : Submodule R M),
  (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) →
    ∃ Φ, (∀ i ∈ Φ, ¬Disjoint q (R ∙ P.root i)) ∧ ∀ i ∉ Φ, q ≤ LinearMap.ker (P.coroot' i)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_indicator_iff : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasurableSet s → (MeasureTheory.IntegrableOn (s.indicator f) t μ ↔ MeasureTheory.IntegrableOn f (s ∩ t) μ)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.of_append_left : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w}, (p.append q).IsPath → p.IsPath
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.traceEMatchDiagsCompact : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo → Lean.Meta.Grind.GrindM Unit
-- Lean.Expr
/-- Given `a b : Int`, returns `a ∣ b`  -/
Lean.mkIntDvd : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.comp_inverse' : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
  {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f}, (f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function is continuous on the right at a point `a`, then its variations on `Ioi a` and
on `Ici a` coincide. We give a version relative to a set `s`.  -/
eVariationOn.eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {a : α},
  (nhdsWithin a (s ∩ Set.Ioi a)).NeBot →
    ContinuousWithinAt f (s ∩ Set.Ici a) a → eVariationOn f (s ∩ Set.Ioi a) = eVariationOn f (s ∩ Set.Ici a)
-- Lean.Elab.Tactic.Induction
/-- Applies syntactic alternative to alternative goal.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.applyAltStx : Lean.Meta.ElimInfo →
  Lean.Syntax →
    ℕ →
      Array Lean.FVarId →
        Array Lean.FVarId →
          Array (Lean.Ident × Lean.FVarId) →
            Array (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot) →
              Array Lean.Syntax → ℕ → Lean.Syntax → Lean.Elab.Tactic.ElimApp.Alt → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, s.Nonempty → t.Nonempty → 0 < s.addEnergy t
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Convenience shortcut for `ModuleCat.hom_bijective.surjective`.  -/
ModuleCat.hom_surjective : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}, Function.Surjective ModuleCat.Hom.hom
-- Mathlib.Data.Finset.Sups
Finset.compls_inter : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : DecidableEq α] (s t : Finset α),
  (s ∩ t).compls = s.compls ∩ t.compls
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.eq_of_superset_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {C C' : Set α}, M.IsCircuit C → M.IsCircuit C' → C' ⊆ C → C = C'
-- Mathlib.Order.LiminfLimsup
Filter.iSup_liminf_le_liminf_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : CompleteLattice α] {f : Filter β} {u : ι → β → α},
  ⨆ i, Filter.liminf (u i) f ≤ Filter.liminf (fun b => ⨆ i, u i b) f
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The underlying map between abelian presheaves of a morphism of `𝒪ₓ`-modules.  -/
AlgebraicGeometry.Scheme.Modules.Hom.mapPresheaf : {X : AlgebraicGeometry.Scheme} → {M N : X.Modules} → (M ⟶ N) → (M.presheaf ⟶ N.presheaf)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_lt_iff_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, a + -b < c ↔ a < c + b
-- Mathlib.Algebra.Category.CommAlgCat.Basic
instHasColimitsCommAlgCat : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.Limits.HasColimits (CommAlgCat R)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_not : ∀ {w : ℕ} {x : BitVec w}, (~~~x).toInt = (2 ^ w - 1 - ↑x.toNat).bmod (2 ^ w)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.colimitsOfShape_discrete_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) (J : Type w),
  T.colimitsOfShape (CategoryTheory.Discrete J) ≤ T.rlp.llp
-- Mathlib.Data.Nat.DvdSequence
/-- **Alias** of `IsDvdSequence`.

---

A function `f : α → β` is a divisibility sequence if `a ∣ b` implies `f a ∣ f b`.  -/
IsDivSequence : {α : Type u_1} → {β : Type u_2} → [Dvd α] → [Dvd β] → (α → β) → Prop
-- Init.Data.String.Basic
String.toList.eq_1 : ∀ (s : String), s.toList = (String.Internal.toArray s).toList
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.ext : ∀ {B : Type u_1} {x y : CoxeterMatrix B}, x.M = y.M → x = y
-- Mathlib.Analysis.Convex.Topology
Convex.openSegment_interior_closure_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ interior s → y ∈ closure s → openSegment 𝕜 x y ⊆ interior s
-- Mathlib.Algebra.Group.Invertible.Basic
/-- `invertibleOfMulInvertible` and `invertibleMul` as an equivalence.  -/
Invertible.mulRight : {α : Type u} → [inst : Monoid α] → (a : α) → {b : α} → Invertible b → Invertible a ≃ Invertible (a * b)
-- Mathlib.Order.Interval.Multiset
Multiset.right_notMem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ∉ Multiset.Ioo a b
-- Mathlib.Order.PFilter
/-- If a poset `P` admits arbitrary `Inf`s, then `principal` and `Inf` form a Galois coinsertion.  -/
Order.PFilter.infGi : {P : Type u_1} →
  [inst : CompleteSemilatticeInf P] →
    GaloisCoinsertion (fun x => OrderDual.toDual (Order.PFilter.principal x)) fun F => sInf ↑(OrderDual.ofDual F)
-- Mathlib.CategoryTheory.Whiskering
/-- If `α : G ⟶ H` then `whiskerRight α F : G ⋙ F ⟶ H ⋙ F` has components `F.map (α.app X)`.  -/
CategoryTheory.Functor.whiskerRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {G H : CategoryTheory.Functor C D} → (G ⟶ H) → (F : CategoryTheory.Functor D E) → G.comp F ⟶ H.comp F