mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Congruence.Defs
Con.mk.inj : ∀ {M : Type u_1} {inst : Mul M} {toSetoid : Setoid M}
  {mul' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w * y) (x * z)} {toSetoid_1 : Setoid M}
  {mul'_1 : ∀ {w x y z : M}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w * y) (x * z)},
  { toSetoid := toSetoid, mul' := mul' } = { toSetoid := toSetoid_1, mul' := mul'_1 } → toSetoid = toSetoid_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrKey.mk.inj : ∀ {enodes : Lean.Meta.Grind.ENodeMap} {e e_1 : Lean.Expr}, { e := e } = { e := e_1 } → e = e_1
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaUnique_symm_apply : ∀ {α : Type u_10} {β : α → Type u_9} [inst : (a : α) → Unique (β a)] (x : α),
  (Equiv.sigmaUnique α β).symm x = ⟨x, default⟩
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.Limits.IsTerminal.isCardinalFiltered : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X)
  (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular], CategoryTheory.IsCardinalFiltered J κ
-- Init.Core
Relation.TransGen.brecOn : ∀ {α : Sort u} {r : α → α → Prop} {a : α} {motive : (a_1 : α) → Relation.TransGen r a a_1 → Prop} {a_1 : α}
  (t : Relation.TransGen r a a_1),
  (∀ (a_2 : α) (t : Relation.TransGen r a a_2), Relation.TransGen.below t → motive a_2 t) → motive a_1 t
-- Mathlib.Analysis.Analytic.Order
/-- **Alias** of `AnalyticOnNhd.codiscreteWithin_setOfPred_analyticOrderAt_eq_zero_or_top`.

---

The set where an analytic function has zero or infinite order is discrete within its domain of
analyticity.
 -/
AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U → {u | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤} ∈ Filter.codiscreteWithin U
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List ((a : α) × β a)},
  Std.ExtDTreeMap.ofList l cmp = ∅.insertMany l
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hom_ext_iff : ∀ {X Y : AddGrpCat} {f g : X ⟶ Y}, f = g ↔ AddGrpCat.Hom.hom f = AddGrpCat.Hom.hom g
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk''.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : D} [inst_5 : CategoryTheory.AddModObj A M]
  [inst_6 : CategoryTheory.AddModObj A N] (f : M ⟶ N)
  (smul_hom :
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
        CategoryTheory.AddModObj.vadd),
  CategoryTheory.AddMod.Hom.mk'' f smul_hom = { hom := f, isAddModHom := ⋯ }
-- Mathlib.Tactic.CrossRefAttribute
/-- The parenthesizer for Wikidata identifier syntax.  -/
Lean.PrettyPrinter.Parenthesizer.wikidataIdAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Environment
_private.Lean.Environment.0.Lean.RealizationContext.mk : NonScalar → Lean.Options → IO.Ref (Lean.NameMap NonScalar) → Lean.RealizationContext✝
-- Mathlib.Order.Filter.Pointwise
Filter.mem_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β} {t : Set β},
  t ∈ f +ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ +ᵥ t₂ ⊆ t
-- Std.Time.Date.Basic
Std.Time.instHAddOffset_5 : HAdd Std.Time.Day.Offset Std.Time.Day.Offset Std.Time.Day.Offset
-- Init.Data.String.Basic
List.isPrefix_of_utf8Encode_append_eq_utf8Encode : ∀ {l m : List Char} (b : ByteArray), l.utf8Encode ++ b = m.utf8Encode → l <+: m
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.comp_zero : ∀ {E : Type u_3} {F : Type u_4} [inst : Group E] [inst_1 : Group F] (p : GroupSeminorm E), p.comp 1 = 0
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.isHomological_of_localization : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.HasShift C ℤ] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.HasShift D ℤ]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_7 : CategoryTheory.Pretriangulated D] [inst_8 : CategoryTheory.Category.{v_3, u_3} A]
  [inst_9 : CategoryTheory.Limits.HasZeroObject C] [inst_10 : CategoryTheory.Preadditive C]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_12 : CategoryTheory.Pretriangulated C]
  [inst_13 : CategoryTheory.Abelian A] (L : CategoryTheory.Functor C D) [inst_14 : L.CommShift ℤ] [L.IsTriangulated]
  [L.mapArrow.EssSurj] (F : CategoryTheory.Functor D A) (G : CategoryTheory.Functor C A) (e : L.comp F ≅ G)
  [G.IsHomological], F.IsHomological
-- Mathlib.Order.BoundedOrder.Basic
Subtype.mk_bot : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : OrderBot (Subtype p)]
  (hbot : p ⊥), ⟨⊥, hbot⟩ = ⊥
-- Init.Data.Vector.Lemmas
Vector.findRev?_mk : ∀ {α : Type} {n : ℕ} {xs : Array α} (h : xs.size = n) (f : α → Bool),
  Vector.findRev? f (Vector.mk xs h) = Array.findRev? f xs
-- Lean.Elab.Quotation.Util
Lean.Elab.Term.Quotation.getPatternsVars : Array Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.inv_op_smul_finset_distrib₀ : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : DecidableEq α] (a : α) (s : Finset α),
  (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.EStateM.tryCatch.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)) (h_2 : (ok : EStateM.Result ε σ α) → motive ok),
  (match EStateM.Result.error e s with
    | EStateM.Result.error e s => h_1 e s
    | ok => h_2 ok) =
    h_1 e s
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the `n`th denominator is greater than or equal to the `n + 1`th fibonacci number,
that is `Nat.fib (n + 1) ≤ Bₙ`.  -/
GenContFract.succ_nth_fib_le_of_nth_den : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K],
  n = 0 ∨ ¬(GenContFract.of v).TerminatedAt (n - 1) → ↑(Nat.fib (n + 1)) ≤ (GenContFract.of v).dens n
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.mk.congr_simp : ∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] (toEquiv toEquiv_1 : α ≃ β)
  (e_toEquiv : toEquiv = toEquiv_1) (uniformContinuous_toFun : UniformContinuous toEquiv.toFun)
  (uniformContinuous_invFun : UniformContinuous toEquiv.invFun),
  { toEquiv := toEquiv, uniformContinuous_toFun := uniformContinuous_toFun,
      uniformContinuous_invFun := uniformContinuous_invFun } =
    { toEquiv := toEquiv_1, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.cases.sizeOf_spec : ∀ (target : Aesop.CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool)
  (ctorNames : Array Aesop.CtorNames),
  sizeOf (Aesop.RuleTacDescr.cases target md isRecursiveType ctorNames) =
    1 + sizeOf target + sizeOf md + sizeOf isRecursiveType + sizeOf ctorNames
-- Qq.ForLean.ToExpr
toExprExpr : Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Normed.Group.Basic
/-- The nonnegative norm seen as an `ENNReal` and then as a `Real` is equal to the norm.  -/
toReal_coe_nnnorm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), (↑‖a‖₊).toReal = ‖a‖
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_toSubring : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (p : MvPowerSeries σ R) (T : Subring R)
  (hp : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) p ∈ T), (MvPowerSeries.map T.subtype) (p.toSubring T hp) = p
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.instIsAddCommutative_closure : ∀ (M : Type u_1) [inst : AddMonoid M] {S : Type u_2} [inst_1 : SetLike S M] [inst_2 : AddMemClass S M] (s : S)
  [IsAddCommutative ↥s], IsAddCommutative ↥(AddSubmonoid.closure ↑s)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Exhibit a bijection between `Fin n` and the index set of a certain basis of an `n`-dimensional
inner product space `E`.  This should not be accessed directly, but only via the subsequent API.  -/
DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv : {ι : Type u_7} →
  {𝕜 : Type u_8} →
    [inst : RCLike 𝕜] →
      {E : Type u_9} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [Fintype ι] →
              [FiniteDimensional 𝕜 E] →
                {n : ℕ} →
                  Module.finrank 𝕜 E = n →
                    [inst_5 : DecidableEq ι] →
                      {V : ι → Submodule 𝕜 E} →
                        DirectSum.IsInternal V →
                          (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) →
                            (i : ι) × Fin (Module.finrank 𝕜 ↥(V i)) ≃ Fin n
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.id_whisker_right : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsTrivialBlock.smul_iff : ∀ {M : Type u_3} {α : Type u_4} [inst : Group M] [inst_1 : MulAction M α] {B : Set α} (g : M),
  MulAction.IsTrivialBlock (g • B) ↔ MulAction.IsTrivialBlock B
-- Mathlib.ModelTheory.Order
FirstOrder.Language.dlo_age : ∀ (M : Type w') [inst : FirstOrder.Language.order.Structure M] [Mdlo : M ⊨ FirstOrder.Language.order.dlo] [Nonempty M],
  FirstOrder.Language.order.age M = {M | Finite ↑M ∧ ↑M ⊨ FirstOrder.Language.order.linearOrderTheory}
-- Mathlib.Algebra.Group.Defs
/-- A `Group` which `IsMulCommutative` is a `CommGroup`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instCommGroup : {G : Type u_2} → [inst : Group G] → [IsMulCommutative G] → CommGroup G
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `(⊥ : SubAlgebra A B) = ⊤`, then `IsCyclotomicExtension {1} A B`.  -/
IsCyclotomicExtension.singleton_one_of_bot_eq_top : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  ⊥ = ⊤ → IsCyclotomicExtension {1} A B
-- Batteries.Recycling.RBTree.Basic
/-- Asserts that `t₁` and `t₂` have the same number of elements in the same order,
and `R` holds pairwise between them. The tree structure is ignored.
 -/
RBTree.RBMap.all₂ : {α : Type u} →
  {β : Type v} →
    {γ : Type u_1} →
      {δ : Type u_2} →
        {cmpα : α → α → Ordering} →
          {cmpγ : γ → γ → Ordering} → (α × β → γ × δ → Bool) → RBTree.RBMap α β cmpα → RBTree.RBMap γ δ cmpγ → Bool
-- Batteries.Data.List.Perm
List.Perm.subperm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₁.Subperm l₂
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instNonUnitalNonAssocRingOfIsTopologicalRing : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalNonAssocRing β] →
          [IsTopologicalRing β] → NonUnitalNonAssocRing (CompactlySupportedContinuousMap α β)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.compl_inj : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] [inst_2 : Zero α] [inst_3 : One α]
  {A B : Matrix V V α}, A.IsAdjMatrix → B.IsAdjMatrix → (A.compl = B.compl ↔ A = B)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.Inv_divided_by_X_pow_order_leftInv : ∀ {k : Type u_2} [inst : Field k] {f : PowerSeries k} (hf : f ≠ 0),
  PowerSeries.Inv_divided_by_X_pow_order hf * f.divXPowOrder = 1
-- Aesop.Rule
Aesop.NormSimpRule.instBEq : BEq Aesop.NormSimpRule
-- Mathlib.Data.Multiset.Sum
Multiset.zero_disjSum : ∀ {α : Type u_1} {β : Type u_2} (t : Multiset β), Multiset.disjSum 0 t = Multiset.map Sum.inr t
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The yoneda embedding of `FormalCoproduct.{w} C` into `max w v`-presheaves.  -/
CategoryTheory.Limits.FormalCoproduct.uliftYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) (CategoryTheory.Functor Cᵒᵖ (Type (max w v)))
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_inv_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A] (X : CategoryTheory.Functor Cᵒᵖ A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId C A).inv.app X).app X_1 =
    CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findSome?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- Linear disjointness is symmetric in a commutative ring.  -/
Submodule.LinearDisjoint.symm : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M N : Submodule R S}, M.LinearDisjoint N → N.LinearDisjoint M
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStronglyProgressive.stronglyAdapted_stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStoppingTime f τ → MeasureTheory.StronglyAdapted f (MeasureTheory.stoppedProcess u τ)
-- Mathlib.Order.SupIndep
iSupIndep_ne_bot : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α}, (iSupIndep fun i => t ↑i) ↔ iSupIndep t
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.subsingleton_two_sylow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → Subsingleton (Sylow 2 ↥(alternatingGroup α))
-- Init.Data.List.Find
List.IsPrefix.findIdx?_eq_none : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <+: l₂ → List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zag.of_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ : J} (f : j₂ ⟶ j₁), CategoryTheory.Zag j₁ j₂
-- Mathlib.Tactic.Tauto
_private.Mathlib.Tactic.Tauto.0.Mathlib.Tactic.Tauto.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.Tauto.Config
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
AlgebraicTopology.instPreservesMonomorphismsTopCatChainComplexNatObjFunctorSingularChainComplexFunctorOfHasPullbacks : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasPullbacks C] {X : C},
  ((AlgebraicTopology.singularChainComplexFunctor C).obj X).PreservesMonomorphisms
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_eq_get_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he = t.minKey?.get ⋯
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.take : ∀ {l m r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → ∀ (n : ℕ), Substring.Raw.ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)
-- Mathlib.Order.Concept
/-- Note that if `r'` is the `≤` relation, this theorem will often not be true!  -/
Concept.disjoint_extent_intent : ∀ {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [Std.Irrefl r'], Disjoint c'.extent c'.intent
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.step_take.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_intCast : ∀ {R : Type u} [inst : Ring R] (z : ℤ), { toFinsupp := ↑z } = ↑z
-- Init.Data.UInt.Lemmas
USize.mul_neg : ∀ (a b : USize), a * -b = -(a * b)
-- Mathlib.Algebra.GradedMonoid
SetLike.coe_gMul : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Mul R] [inst_2 : Add ι] (A : ι → S)
  [inst_3 : SetLike.GradedMul A] {i j : ι} (x : ↥(A i)) (y : ↥(A j)), ↑(GradedMonoid.GMul.mul x y) = ↑x * ↑y
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The singleton operation as a `MonoidHom`.  -/
Set.singletonMonoidHom : {α : Type u_2} → [inst : MulOneClass α] → α →* Set α
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The maximal number of vertices of an independent set in a graph `G`.  -/
SimpleGraph.indepNum : {α : Type u_3} → SimpleGraph α → ℕ
-- Batteries.Data.List.Lemmas
List.forIn_eq_bindList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β))
  (l : List α) (init : β), forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_rev : ∀ {w : ℕ} {x : BitVec w} {i : Fin w}, x[i.rev] = x.getMsbD ↑i
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.extract.eq_1 : ∀ (x x_1 : String.Pos.Raw) (s : String) (b e : String.Pos.Raw),
  { str := s, startPos := b, stopPos := e }.extract x x_1 =
    if x ≥ x_1 then { str := "", startPos := 0, stopPos := 0 }
    else { str := s, startPos := e.min (x.offsetBy b), stopPos := e.min (x_1.offsetBy b) }
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.str : (self : ωCPO) → OmegaCompletePartialOrder self.carrier
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_bijective : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F],
  Function.Bijective ContinuousLinearMapWOT.ofCLM
-- Mathlib.Data.Set.Opposite
Set.opEquiv_symm_apply : ∀ {α : Type u_1} (s : Set αᵒᵖ), Set.opEquiv.symm s = s.unop
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoLeftHomology_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hf : S.f = 0),
  CategoryTheory.CategoryStruct.comp (S.cyclesIsoLeftHomology hf).inv S.leftHomologyπ =
    CategoryTheory.CategoryStruct.id S.leftHomology
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example (P : Matrix (Fin 2) (Fin 3) α → Prop) :
  (∃ x, P x) ↔ ∃ a b c d e f, P !![a, b, c; d, e, f] :=
(exists_iff _).symm
```
 -/
Matrix.exists_iff : ∀ {α : Type u_1} {m n : ℕ} (P : Matrix (Fin m) (Fin n) α → Prop), Matrix.Exists P ↔ ∃ x, P x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.lt_iff : ∀ {X : SSet} {A : X.Subcomplex} {x y : A.N}, x < y ↔ x.toN < y.toN
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mkSpanSingleton'_apply_self : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (x : E) (y : F)
  (H : ∀ (c : R), c • x = 0 → σ c • y = 0) (h : x ∈ (LinearPMap.mkSpanSingleton' x y H).domain),
  ↑(LinearPMap.mkSpanSingleton' x y H) ⟨x, h⟩ = y
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.mk.inj : ∀ {G : Type u_6} {inst : Group G} {toGroupSeminorm : GroupSeminorm G}
  {eq_one_of_map_eq_zero' : ∀ (x : G), toGroupSeminorm.toFun x = 0 → x = 1} {toGroupSeminorm_1 : GroupSeminorm G}
  {eq_one_of_map_eq_zero'_1 : ∀ (x : G), toGroupSeminorm_1.toFun x = 0 → x = 1},
  { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' } =
      { toGroupSeminorm := toGroupSeminorm_1, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 } →
    toGroupSeminorm = toGroupSeminorm_1
-- Mathlib.Data.Set.Image
Set.preimage_mono : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_inter_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.modifyₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [Hashable α] →
        [LawfulBEq α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → (β a → β a) → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.comp_commShiftIso_inv_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [inst_3 : AddMonoid A]
  [inst_4 : CategoryTheory.HasShift C A] [inst_5 : CategoryTheory.HasShift D A] [inst_6 : CategoryTheory.HasShift E A]
  [inst_7 : F.CommShift A] [inst_8 : G.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (F.comp G) a).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G a).inv.app (F.obj X))
      (G.map ((CategoryTheory.Functor.commShiftIso F a).inv.app X))
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.smul_def : ∀ {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : DecidableEq ιA]
  [inst_5 : DecidableEq ιB] [inst_6 : GradedMonoid.GMonoid A] [inst_7 : DirectSum.Gmodule A M]
  (x : DirectSum ιA fun i => A i) (y : DirectSum ιB fun i => M i),
  x • y = ((DirectSum.Gmodule.smulAddMonoidHom A M) x) y
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_mod : ∀ {a b : ℕ} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8), UInt8.ofNatLT (a % b) ⋯ = UInt8.ofNatLT a ha % UInt8.ofNatLT b hb
-- Mathlib.Data.Finset.Sort
Finset.coe_orderIsoOfFin_apply : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k),
  ↑((s.orderIsoOfFin h) i) = (s.orderEmbOfFin h) i
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSpace_iSup_eq : ∀ {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α),
  ⨆ n, m n = MeasurableSpace.generateFrom {s | ∃ n, MeasurableSet s}
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_one_nnnorm' : ∀ {E : Type u_2} [inst : SeminormedGroup E], LipschitzWith 1 nnnorm
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_sub_cancel : ∀ (a b : Ordinal.{u_4}), a + b - a = b