mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.BisimO.match_1.eq_2 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (s s' : Computation α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_1 : α ⊕ Computation α) → motive x x_1),
  (match Sum.inr s, Sum.inr s' with
    | Sum.inl a, Sum.inl a' => h_1 a a'
    | Sum.inr s, Sum.inr s' => h_2 s s'
    | x, x_1 => h_3 x x_1) =
    h_2 s s'
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseClause : Std.Internal.Parsec.ByteArray.Parser (Array ℤ)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.srange_eq_top_iff_surjective : ∀ {M : Type u_1} [inst : Add M] {N : Type u_5} [inst_1 : Add N] {f : M →ₙ+ N}, f.srange = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.comapEquiv_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (e : R ≃+* S) (p : PrimeSpectrum R),
  (PrimeSpectrum.comapEquiv e) p = PrimeSpectrum.comap e.symm.toRingHom p
-- Mathlib.Algebra.Group.Defs
/-- `a / b := a * b⁻¹`  -/
DivInvMonoid.div_eq_mul_inv : ∀ {G : Type u} [self : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
/-- This is a choice of structure `F.DenseAt Y` when `F : C ⥤ D`
is dense, and `Y : D`.  -/
CategoryTheory.Functor.denseAt : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [F.IsDense] → (Y : D) → F.DenseAt Y
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Ioi_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo b a ⊆ Set.Ioi b
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BiconeMorphism.wπ_assoc : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) {Z : C} (h : F j ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (B.π j) h) =
    CategoryTheory.CategoryStruct.comp (A.π j) h
-- Mathlib.Data.Multiset.Filter
Multiset.filter_true : ∀ {α : Type u_1} (s : Multiset α), Multiset.filter (fun x => True) s = s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n d : aig.RefVec w) (wn wr : ℕ)
  (q r : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig 0 n d wn wr q r = { aig := aig, q := q, r := r, hle := ⋯ }
-- Lean.Elab.Command
Lean.Elab.Command.State.ngen : Lean.Elab.Command.State → Lean.NameGenerator
-- Mathlib.RingTheory.Teichmuller
Perfection.coeff_quotientMulEquiv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] (x : Perfection R p) (n : ℕ),
  (Perfection.coeff (R ⧸ I) p n) ((Perfection.quotientMulEquiv p I) x) =
    (Ideal.Quotient.mk I) ((Perfection.coeffMonoidHom R p n) x)
-- Mathlib.RingTheory.Congruence.Basic
/-- Congruence relations equal the smallest congruence relation in which they are contained.  -/
RingCon.ringConGen_of_ringCon : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (c : RingCon R), ringConGen ⇑c = c
-- Mathlib.Analysis.Analytic.Linear
/-- `fst` is analytic  -/
analyticAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
  AnalyticAt 𝕜 (fun p => p.1) p
-- Aesop.Search.Main
/-- This function detects whether the search has made progress, meaning that the
remaining goals after safe prefix expansion are different from the initial goal.
We approximate this by checking whether, after safe prefix expansion, either
of the following statements is true.

- There is a safe rapp.
- A subgoal of the preprocessing rule has been modified during normalisation.

This is an approximation because a safe rule could, in principle, leave the
initial goal unchanged.
 -/
Aesop.treeHasProgress : Aesop.TreeM Bool
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.instReprGuessLexRel : Repr Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_inj_real : ∀ {r₁ r₂ s : ℝ}, (↑r₁).IsSt s → (↑r₂).IsSt s → r₁ = r₂
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagramIso_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J × D.J),
  (D.diagramIso F).app (CategoryTheory.Limits.WalkingMultispan.left i) =
    CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.left i))
-- Mathlib.Order.InitialSeg
PrincipalSeg.trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsTrans γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) (a : α),
  (f.trans g).toRelEmbedding a = g.toRelEmbedding (f.toRelEmbedding a)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SMul.ofStabilizer.eq_1 : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] (s : Set α),
  SMul.ofStabilizer G α s = { smul := fun g x => ⟨g • ↑x, ⋯⟩ }
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.startsWith_eq_false_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.startsWith pat = false ↔ ¬String.Slice.Pattern.Model.MatchesAt pat s.startPos
-- Init.Data.SInt.Lemmas
Int64.mul_assoc : ∀ (a b c : Int64), a * b * c = a * (b * c)
-- Batteries.Data.Array.Match
Array.Matcher.instFiniteIterator : ∀ {n : Type u_1 → Type u_2} {α σ : Type u_1} [inst : Monad n] [inst_1 : BEq α] (m : Array.Matcher α)
  [inst_2 : Std.Iterator σ n α] [inst_3 : Std.Iterators.Finite σ n],
  Std.Iterators.Finite (Array.Matcher.Iterator σ n α m) n
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_compare : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α),
  UniformContinuous (pkg.compare pkg')
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.semilatticeSup : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasImages C] →
      [CategoryTheory.Limits.HasBinaryCoproducts C] → {B : C} → SemilatticeSup (CategoryTheory.Subobject B)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The canonical morphism `K.restriction e ⟶ K.truncGE' e`.  -/
HomologicalComplex.restrictionToTruncGE' : {ι : 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.IsTruncGE] → [inst_3 : ∀ (i' : ι'), K.HasHomology i'] → K.restriction e ⟶ K.truncGE' e
-- Mathlib.Algebra.GroupWithZero.Action.Defs
MulActionWithZero.subsingleton : ∀ (M₀ : Type u_2) (A : Type u_7) [inst : MonoidWithZero M₀] [inst_1 : Zero A] [MulActionWithZero M₀ A]
  [Subsingleton M₀], Subsingleton A
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.LaxBraided.toLaxMonoidal : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {D : Type u₂} →
          {inst_3 : CategoryTheory.Category.{v₂, u₂} D} →
            {inst_4 : CategoryTheory.MonoidalCategory D} →
              {inst_5 : CategoryTheory.BraidedCategory D} →
                {F : CategoryTheory.Functor C D} → [self : F.LaxBraided] → F.LaxMonoidal
-- Mathlib.Combinatorics.Tiling.Tile
/-- The group elements under which this tile is an image.  -/
DiscreteTiling.PlacedTile.groupElts : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] →
          {ps : DiscreteTiling.Protoset G X ιₚ} →
            (self : DiscreteTiling.PlacedTile ps) →
              G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps self.index)).subtype (↑ps self.index).symmetries
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.iterate_mod_apply : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → ∀ (m : ℕ), f^[m % n] x = f^[m] x
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformContinuous_singleton : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous fun x => {x}
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.lift.eq_1 : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1),
  PadicInt.lift f_compat =
    { toFun := PadicInt.limNthHom f_compat, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι'),
  ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_union_le : ∀ {x y : ZFSet.{u}}, (x ∪ y).card ≤ x.card + y.card
-- Init.Data.Nat.Lemmas
Nat.div_mul_div_le_div : ∀ (a b c : ℕ), a / c * b / a ≤ b / c
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.instTypeNameFunInfoEnvCacheKey : TypeName Lean.Meta.FunInfoEnvCacheKey✝
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Graph homomorphisms induce a contravariant function on subgraphs.  -/
SimpleGraph.Subgraph.comap : {V : Type u} → {W : Type v} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G →g G' → G'.Subgraph → G.Subgraph
-- Mathlib.RingTheory.AdicCompletion.Completeness
AdicCompletion.ofValEqZero.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {x x_1 : AdicCompletion I M} (e_x : x = x_1) (hxn : ↑x n = 0),
  AdicCompletion.ofValEqZero I hxn = AdicCompletion.ofValEqZero I ⋯
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.equivFunOnFinite_symm_sum : ∀ {α : Type u_1} {M : Type u_8} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f : α → M),
  ((Finsupp.equivFunOnFinite.symm f).sum fun x n => n) = ∑ a, f a
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- If a set is not bounded above, its supremum is by convention `sSup ∅`.  -/
ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove : ∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrder α] (s : Set α), ¬BddAbove s → sSup s = sSup ∅
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IntermediateField.isPurelyInseparable_tower_top : ∀ (F : Type u) [inst : Field F] (K : Type w) [inst_1 : Field K] [inst_2 : Algebra F K] (M : IntermediateField F K)
  [IsPurelyInseparable F K], IsPurelyInseparable (↥M) K
-- Init.Data.List.Find
List.findIdx?_eq_fst_find?_zipIdx : ∀ {α : Type u_1} {xs : List α} {p : α → Bool},
  List.findIdx? p xs =
    Option.map (fun x => x.2)
      (List.find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        xs.zipIdx)
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- Shows that the recurrence relation (`convs`) and direct evaluation (`convs'`) of the
generalized continued fraction coincide at position `n` if the sequence of fractions contains
strictly positive values only.
Requiring positivity of all values is just one possible condition to obtain this result.
For example, the dual - sequences with strictly negative values only - would also work.

In practice, one most commonly deals with regular continued fractions, which satisfy the
positivity criterion required here. The analogous result for them
(see `ContFract.convs_eq_convs'`) hence follows directly from this theorem.
 -/
GenContFract.convs_eq_convs' : ∀ {K : Type u_1} {n : ℕ} {g : GenContFract K} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K],
  (∀ {gp : GenContFract.Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
-- Mathlib.CategoryTheory.Enriched.HomCongr
CategoryTheory.Iso.eHomCongr.eq_1 : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C}
  (α : X ≅ X₁) (β : Y ≅ Y₁),
  CategoryTheory.Iso.eHomCongr V α β =
    {
      hom :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V α.inv Y)
          (CategoryTheory.eHomWhiskerLeft V X₁ β.hom),
      inv :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V α.hom Y₁)
          (CategoryTheory.eHomWhiskerLeft V X β.inv),
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.instBEqSign.beq.eq_1 : ∀ (x y : Float.Model.UnpackedFloat.Sign), Float.Model.UnpackedFloat.instBEqSign.beq x y = (x.ctorIdx == y.ctorIdx)
-- Mathlib.Data.Rat.Cast.Order
NNRat.one_lt_cast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0}, 1 < ↑p ↔ 1 < p
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelf_inv_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.RightLift f g),
  t.whiskerOfIdCompIsoSelf.inv.left = (CategoryTheory.Bicategory.leftUnitor t.lift).inv
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → IsOpenMap f
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.block_command.intro : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.sInf_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedGT ι] (s : Set (Colex ((i : ι) → α i))) (i : ι), sInf s i = ⨅ e, ↑e i
-- Mathlib.Order.WellFounded
/-- **Alias** of the forward direction of `WellFounded.wellFoundedGT_iff_exists_maximal`. -/
WellFoundedGT.exists_maximal : ∀ {α : Type u_1} [inst : Preorder α], WellFoundedGT α → ∀ (s : Set α), s.Nonempty → ∃ m, Maximal (fun x => x ∈ s) m
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.pad : ℕ → ℤ → optParam Bool false → String
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.append.sizeOf_spec : ∀ {l r w : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr l) (rhs : Std.Tactic.BVDecide.BVExpr r) (h : w = l + r),
  sizeOf (lhs.append rhs h) = 1 + sizeOf l + sizeOf r + sizeOf w + sizeOf lhs + sizeOf rhs + sizeOf h
-- Std.Async.UDP
Std.Async.UDP.Membership.leaveGroup : Std.Async.UDP.Membership
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- **Alias** of `Topology.RelCWComplex.finite_of_finite_cells`.

---

If the collection of all cells (of any dimension) of a relative CW complex `C` is finite, then
`C` is finite as a CW complex.  -/
Topology.CWComplex.finite_of_finite_cells : ∀ {X : Type u_2} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D],
  Finite ((n : ℕ) × Topology.RelCWComplex.cell C n) → Topology.RelCWComplex.Finite C
-- Lean.Meta.AppBuilder
Lean.Meta.mkEqRec : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2.eq_def : ∀ (ctorVal : Lean.ConstructorVal) (useEq : Bool) (args1 : Array Lean.Expr) (resultType : Lean.Expr)
  (k : Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Option Lean.Expr)) (i : ℕ) (type : Lean.Expr)
  (args2 args2New : Array Lean.Expr),
  Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2✝ ctorVal useEq args1 resultType k i type args2 args2New =
    if h : i < args1.size then do
      let __x ← Lean.Meta.whnf type
      match __x with
        | Lean.Expr.forallE n d b binderInfo =>
          have arg1 := args1[i];
          do
          let __do_lift ← Lean.getLCtx
          if Lean.Meta.occursOrInType __do_lift arg1 resultType = true then
              Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2✝ ctorVal useEq args1 resultType k (i + 1)
                (b.instantiate1 arg1) (args2.push arg1) args2New
            else
              Lean.Meta.withLocalDecl n (if useEq = true then Lean.BinderInfo.default else Lean.BinderInfo.implicit) d
                fun arg2 =>
                Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2✝ ctorVal useEq args1 resultType k (i + 1)
                  (b.instantiate1 arg2) (args2.push arg2) (args2New.push arg2)
        | x =>
          Lean.throwError
            (Lean.toMessageData "unexpected constructor type for `" ++ Lean.toMessageData ctorVal.name ++
              Lean.toMessageData "`")
    else k args2 args2New
-- Mathlib.Order.Disjointed
disjointed.eq_1 : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α) (i : ι), disjointed f i = f i \ (Finset.Iio i).sup f
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- The property of morphisms that is satisfied by `𝟙 X` for any `X`.  -/
CategoryTheory.MorphismProperty.identities : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.ofEq_rfl : ∀ {R : Type u_1} {M₁ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
  {B : LinearMap.BilinForm R M₁}, LinearMap.BilinForm.Isometry.ofEq ⋯ = LinearMap.BilinForm.Isometry.id B
-- Mathlib.Data.Multiset.UnionInter
Multiset.cons_inter_of_neg : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α), a ∉ t → (a ::ₘ s) ∩ t = s ∩ t
-- Init.Data.Function
Function.Injective.comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} {f : α → β},
  Function.Injective g → Function.Injective f → Function.Injective (g ∘ f)
-- Mathlib.Analysis.CStarAlgebra.Spectrum
CStarAlgebra.sqrt_toReal_spectralRadius_self_mul_star_eq_norm : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A), √(spectralRadius ℂ (a * star a)).toReal = ‖a‖
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.mk : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {R : Type u_10} →
            [inst_2 : Semiring R] →
              [inst_3 : MulSemiringAction M R] →
                {S : Type u_12} →
                  [inst_4 : Semiring S] →
                    [inst_5 : MulSemiringAction N S] →
                      (toDistribMulActionHom : R →ₑ+[φ] S) →
                        toDistribMulActionHom.toFun 1 = 1 →
                          (∀ (x y : R),
                              toDistribMulActionHom.toFun (x * y) =
                                toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y) →
                            R →ₑ+*[φ] S
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.revMatchAt?_eq : ∀ {s : String.Slice} {pos : s.Pos} {p : Char → Prop} [inst : DecidablePred p],
  String.Slice.Pattern.Model.revMatchAt? p pos =
    if h₀ : ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) then some (pos.prev ⋯) else none
-- Init.Data.UInt.Lemmas
UInt32.instLawfulOrderLT : Std.LawfulOrderLT UInt32
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan_eq_centralBinom_div : ∀ (n : ℕ), catalan n = n.centralBinom / (n + 1)
-- Aesop.Tracing
_private.Aesop.Tracing.0.Aesop.isFullyQualifiedGlobalName : Lean.Name → Lean.MacroM Bool
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.smul_congr : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (n : ℕ) (a : α) (a' : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.toQ a = a' → Lean.Grind.IntModule.OfNatModule.toQ (n • a) = n • a'
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp) (e_t : t = t_1)
  (h : t ≠ ∅), t.max h = t_1.max ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isCharTwoJEqZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2], W.c₆ = 0
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.updateRIn.congr_simp : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f f_1 : SmoothBumpFunction I c) (e_f : f = f_1) (r r_1 : ℝ) (e_r : r = r_1) (hr : r ∈ Set.Ioo 0 f.rOut),
  f.updateRIn r hr = f_1.updateRIn r_1 ⋯
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«priority-_» : Lean.ParserDescr
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The map `E → F` when `E` is an intermediate field contained in the intermediate field `F`.

This is the intermediate field version of `Subalgebra.inclusion`.  -/
IntermediateField.inclusion : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → {E F : IntermediateField K L} → E ≤ F → ↥E →ₐ[K] ↥F
-- Mathlib.Algebra.Group.Hom.Instances
/-- If `G` is a group, then so is `OneHom M G`.  -/
OneHom.instGroup : {M : Type uM} → {N : Type uN} → [inst : One M] → [inst_1 : Group N] → Group (OneHom M N)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonUnitalNonAssocSemiring : {R : Type u_1} → [NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring Rᵃᵒᵖ
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc.trans_left_one : ∀ {n : ℕ} {i j k : Fin n} [NeZero n], i ≤ j → ⇑(j.cycleIcc i) ∘ ⇑(i.cycleIcc k) = ⇑(i.cycleIcc k)
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of the reverse direction of `wellFounded_liftOn₂'_iff`. -/
WellFounded.quotient_liftOn₂' : ∀ {α : Type u_1} {s : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁ → s a₂ b₂ → r a₁ a₂ = r b₁ b₂},
  WellFounded r → WellFounded fun x y => x.liftOn₂' y r H
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing : {α : Type u_5} → [self : NonUnitalSeminormedCommRing α] → NonUnitalSeminormedRing α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SizedBalancedTree.toBalancedTree.eq_1 : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} (t : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β lb ub),
  t.toBalancedTree = { impl := t.impl, balanced_impl := ⋯ }
-- Mathlib.CategoryTheory.Shift.Basic
/-- The shift autoequivalence, moving objects and morphisms 'up'.  -/
CategoryTheory.shiftFunctor : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → A → CategoryTheory.Functor C C