mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.step_flatMapAfterM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : LawfulMonad m]
  [inst_3 : WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ]
  {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β} {it₂ : Option (Std.IterM m γ)},
  (Std.Iter.flatMapAfterM f it₁ it₂).step =
    match hit : it₂ with
    | none =>
      match it₁.step with
      | ⟨Std.IterStep.yield it₁' b, h⟩ => do
        let fx ← MonadAttach.attach (f b)
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.flatMapAfterM f it₁' (some ↑fx)) ⋯))
      | ⟨Std.IterStep.skip it₁', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.flatMapAfterM f it₁' it₂) ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
    | some it₂_1 => do
      let __do_lift ← it₂_1.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₂' out, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.Iter.flatMapAfterM f it₁ (some it₂')) out ⋯))
        | ⟨Std.IterStep.skip it₂', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.flatMapAfterM f it₁ (some it₂')) ⋯))
        | ⟨Std.IterStep.done, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.flatMapAfterM f it₁ none) ⋯))
-- Init.Control.Except
Except.map_id : ∀ {ε : Type u} {α : Type u_1}, Except.map id = id
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  CategoryTheory.CategoryStruct.comp S.abelianImageToKernel (CategoryTheory.Limits.kernel.ι S.g) =
    CategoryTheory.Abelian.image.ι S.f
-- Mathlib.Topology.JacobsonSpace
/-- The class of Jacobson spaces, i.e.
spaces such that the set of closed points are dense in every closed subspace.  -/
JacobsonSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.rangeFactorization : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → IsUniformInducing (Set.rangeFactorization f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k km : α} (hc : t.contains k = true), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.valuationSubring_isPrincipalIdealRing : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
  [IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup],
  IsPrincipalIdealRing ↥v.valuationSubring
-- Mathlib.Order.Lattice
max_max_max_comm : ∀ {α : Type u} [inst : LinearOrder α] (a b c d : α), max (max a b) (max c d) = max (max a c) (max b d)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.liftₐ_coe_toRingHom : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (c : RingCon M) (f : M →ₐ[R] P) (H : c ≤ RingCon.ker f.toRingHom),
  (c.liftₐ f H).toRingHom = c.lift (↑f) H
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesLT.lt_iff : ∀ {α : Type u_1} {β : Type u_2} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.UpwardEnumerable β}
  {inst_2 : LT α} {inst_3 : LT β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesLT] {a b : α},
  a < b ↔ f.toFun a < f.toFun b
-- Lean.Elab.Tactic.RCases
/-- The `obtain` tactic in the no-target case. Given a type `T`, create a goal `|- T` and
and pattern match `T` against the given pattern. Returns the list of goals, with the assumed goal
first followed by the goals produced by the pattern match.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.obtainNone : Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Syntax → Lean.MVarId → Lean.Elab.TermElabM (List Lean.MVarId)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₂.sizeOf_spec : ∀ (a : List ℕ) (a_1 : Turing.ToPartrec.Cont), sizeOf (Turing.ToPartrec.Cont.cons₂ a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toListRev_keysIter : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keysIter.toListRev = m.keys.reverse
-- Mathlib.RingTheory.LinearDisjoint
/-- If `B/R` is integral, such that `A` and `B'` are linearly disjoint for all subalgebras `B'`
of `B` which are finitely generated `R`-modules, then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_linearDisjoint_finite_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Algebra.IsIntegral R ↥B], (∀ B' ≤ B, ∀ [Module.Finite R ↥B'], A.LinearDisjoint B') → A.LinearDisjoint B
-- Lean.Compiler.ExternAttr
_private.Lean.Compiler.ExternAttr.0.Lean.expandExternPatternAux.match_1.eq_1 : ∀ (pattern : String) (it₁ : pattern.Pos) (motive : (pattern.sliceFrom it₁).Pos × ℕ → Sort u_1)
  (it₂ : (pattern.sliceFrom it₁).Pos) (j : ℕ) (h_1 : (it₂ : (pattern.sliceFrom it₁).Pos) → (j : ℕ) → motive (it₂, j)),
  (match (it₂, j) with
    | (it₂, j) => h_1 it₂ j) =
    h_1 it₂ j
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.mul_coe_eq_bind : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {b : α},
  b ≠ 0 → ∀ (a : WithBot α), a * ↑b = Option.bind a fun a => some (a * b)
-- Init.Data.Array.Lemmas
Array.all_congr : ∀ {α : Type u_1} {start₁ start₂ stop₁ stop₂ : ℕ} {xs ys : Array α},
  xs = ys →
    ∀ {p q : α → Bool},
      (∀ (a : α), p a = q a) → start₁ = start₂ → stop₁ = stop₂ → xs.all p start₁ stop₁ = ys.all q start₂ stop₂
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- If a property holds for all points in closed balls of arbitrarily large radii, then it holds for
all points.  -/
Metric.forall_of_forall_mem_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] (p : α → Prop) (x : α),
  (∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.closedBall x R, p y) → ∀ (y : α), p y
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
LinearMap.BilinMap.tmul.eq_1 : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₁]
  [inst_5 : AddCommMonoid N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁]
  [inst_9 : Module R N₁] [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : SMulCommClass R A N₁] [inst_14 : IsScalarTower R A N₁] [inst_15 : Module R M₂] [inst_16 : Module R N₂]
  (B₁ : LinearMap.BilinMap A M₁ N₁) (B₂ : LinearMap.BilinMap R M₂ N₂),
  B₁.tmul B₂ = (LinearMap.BilinMap.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Two n-simplices among cospherical points in n-space have the same
circumradius.  -/
EuclideanGeometry.circumradius_eq_of_cospherical : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V],
  Module.finrank ℝ V = n →
    EuclideanGeometry.Cospherical ps →
      ∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
        Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumradius = sx₂.circumradius
-- Mathlib.Data.Set.Operations
/-- Range of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  -/
Set.range : {α : Type u} → {ι : Sort u_1} → (ι → α) → Set α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.kerAdjunction_unit_app : ∀ (Y : AlgebraicGeometry.Scheme) (I : Y.IdealSheafData), Y.kerAdjunction.unit.app I = CategoryTheory.eqToHom ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Associator
LinearMap.lTensor_rTensor_comp_assoc : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P] (x : M →ₗ[R] N),
  LinearMap.lTensor P (LinearMap.rTensor Q x) ∘ₗ ↑(TensorProduct.assoc R P M Q) =
    ↑(TensorProduct.assoc R P N Q) ∘ₗ LinearMap.rTensor Q (LinearMap.lTensor P x)
-- Mathlib.CategoryTheory.Sites.Sheaf
_private.Mathlib.CategoryTheory.Sites.Sheaf.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.L) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.left i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_1 i
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_le_add_iff_right : ∀ {a b : Ordinal.{u_4}} (n : ℕ), a + ↑n ≤ b + ↑n ↔ a ≤ b
-- Mathlib.Algebra.Module.LinearMap.Star
/-- The notation `M ≃ₗ⋆[R] M₂` denotes the type of star-linear equivalences between `M` and `M₂`
over the `⋆` endomorphism of the underlying starred ring `R`.  -/
«term_≃ₗ⋆[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.homEquivOfIsLeftKanExtension_symm_apply : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G),
  (F'.homEquivOfIsLeftKanExtension α G).symm β = F'.descOfIsLeftKanExtension α G β
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- Elements of the cone hull are expressible as conical combination of elements from s.  -/
PointedCone.mem_hull_set : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {x : E} {s : Set E},
  x ∈ PointedCone.hull R s ↔ ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r => r • m) = x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.card_nsmulAddMonoidHom_ker : ∀ (G : Type u_2) [inst : AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ),
  Nat.card ↥(nsmulAddMonoidHom d).ker = (Nat.card G).gcd d
-- Init.Data.Vector.OfFn
Vector.mem_ofFn : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α} {a : α}, a ∈ Vector.ofFn f ↔ ∃ i, f i = a
-- Init.Data.Vector.Zip
Vector.unzip_eq_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector (α × β) n},
  xs.unzip = (Vector.map Prod.fst xs, Vector.map Prod.snd xs)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective ⇑(FreeMonoid.map f) ↔ Function.Surjective f
-- Mathlib.Order.Monotone.Defs
monotoneOn_iff_forall_lt : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a ≤ f b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w curr : ℕ} {aig : Std.Sat.AIG α} {cin : aig.Ref}
  {lhs rhs : aig.RefVec w} (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.instOrderTopOfCompactSpaceOfNonempty : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → [Nonempty α] → OrderTop (TopologicalSpace.PositiveCompacts α)
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `limsup` of a function `u` along a filter `f` is the greatest cluster point of `u` along
`f`.  -/
isGreatest_mapClusterPt_limsup : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {u : β → α} {f : Filter β} [f.NeBot],
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) isGreatest_mapClusterPt_limsup._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) isGreatest_mapClusterPt_limsup._auto_3 →
      IsGreatest {x | MapClusterPt x f u} (Filter.limsup u f)
-- Mathlib.CategoryTheory.Sums.Associator
/-- Characterizing the composition of the inverse of the associator and the left inclusion.  -/
CategoryTheory.sum.inlCompInverseAssociator : (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] →
            (CategoryTheory.Sum.inl_ C (D ⊕ E)).comp (CategoryTheory.sum.inverseAssociator C D E) ≅
              (CategoryTheory.Sum.inl_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)
-- Mathlib.Algebra.Order.Floor.Ring
Int.abs_one_sub_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R} [IsOrderedRing R],
  |1 - Int.fract a| = 1 - Int.fract a
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Construct a morphism in `P.Arrow Q W` from a morphism in `Arrow T`.  -/
CategoryTheory.MorphismProperty.Arrow.Hom.mk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q W : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        [inst_2 : W.IsMultiplicative] →
          {A B : P.Arrow Q W} →
            (f :
                (CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj A ⟶
                  (CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj B) →
              Q (CategoryTheory.Arrow.Hom.left f) → W (CategoryTheory.Arrow.Hom.right f) → (A ⟶ B)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.StableUnderInverse.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ},
  P.StableUnderInverse → P.unop.StableUnderInverse
-- Mathlib.Algebra.Module.NatInt
map_natCast_smul : ∀ {M : Type u_3} {M₂ : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {F : Type u_5}
  [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [inst_4 : Semiring R]
  [inst_5 : Semiring S] [inst_6 : Module R M] [inst_7 : Module S M₂] (x : ℕ) (a : M), f (↑x • a) = ↑x • f a
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- If `PreservesColimit₂ K₁ K₂ G`, obtain that `G.mapCocone₂ c₁ c₂` is a colimit cocone
whenever c₁ c₂ are colimit cocones.  -/
CategoryTheory.Limits.isColimitOfPreserves₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    {K₁ : CategoryTheory.Functor J₁ C₁} →
                      {K₂ : CategoryTheory.Functor J₂ C₂} →
                        (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                          [CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] →
                            {c₁ : CategoryTheory.Limits.Cocone K₁} →
                              CategoryTheory.Limits.IsColimit c₁ →
                                {c₂ : CategoryTheory.Limits.Cocone K₂} →
                                  CategoryTheory.Limits.IsColimit c₂ →
                                    CategoryTheory.Limits.IsColimit (G.mapCocone₂ c₁ c₂)
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.instInhabitedApplyKey : Inhabited Mathlib.Tactic.ClickSuggestions.ApplyKey
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_eval_zero : ∀ (S : Type u) [inst : Semiring S] {n : ℕ}, Polynomial.eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.eq_5 : ∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (n₁ : Lean.Name) (k₁ : ℕ) (n₂ : Lean.Name) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (match Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ with
    | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
    | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
    | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
    | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
    | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
    h_5 n₁ k₁ n₂ k₂
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.instIsAccessibleCategoryOfIsLocallyPresentable : ∀ (C : Type u) [hC : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsLocallyPresentable.{w, v, u} C],
  CategoryTheory.IsAccessibleCategory.{w, v, u} C
-- Mathlib.Algebra.Homology.ImageToKernel
/-- The canonical morphism `imageSubobject f ⟶ kernelSubobject g` when `f ≫ g = 0`.
 -/
imageToKernel : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {A B C : V} →
        (f : A ⟶ B) →
          [inst_2 : CategoryTheory.Limits.HasImage f] →
            (g : B ⟶ C) →
              [inst_3 : CategoryTheory.Limits.HasKernel g] →
                CategoryTheory.CategoryStruct.comp f g = 0 →
                  (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶
                    CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g))
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.zpow_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : DivInvMonoid β] (z : ℤ)
  (f : MeasureTheory.SimpleFunc α β) (a : α), (f ^ z) a = f a ^ z
-- Mathlib.Algebra.Quaternion
/-- Space of quaternions over a type, denoted as `ℍ[R]`.
Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`.  -/
Quaternion : (R : Type u_1) → [Zero R] → [One R] → [Neg R] → Type u_1
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `N` is normal and `IsGaloisGroup N B C`, the action `smulOfNormal G B C` satisfies
`SMulDistribClass G B C`.  -/
IsGaloisGroup.smulDistribClass_smulOfNormal : ∀ (G : Type u_1) [inst : Group G] (B : Type u_3) (C : Type u_4) [inst_1 : Semiring C] [inst_2 : MulSemiringAction G C]
  (N : Subgroup G) [inst_3 : CommSemiring B] [inst_4 : Algebra B C] [inst_5 : N.Normal]
  [inst_6 : IsGaloisGroup (↥N) B C], SMulDistribClass G B C
-- Init.MetaTypes
Lean.Meta.ExtractLetsConfig.mk.injEq : ∀
  (proofs types implicits descend underBinder usedOnly merge useContext onlyGivenNames preserveBinderNames lift proofs_1
    types_1 implicits_1 descend_1 underBinder_1 usedOnly_1 merge_1 useContext_1 onlyGivenNames_1 preserveBinderNames_1
    lift_1 : Bool),
  ({ proofs := proofs, types := types, implicits := implicits, descend := descend, underBinder := underBinder,
        usedOnly := usedOnly, merge := merge, useContext := useContext, onlyGivenNames := onlyGivenNames,
        preserveBinderNames := preserveBinderNames, lift := lift } =
      { proofs := proofs_1, types := types_1, implicits := implicits_1, descend := descend_1,
        underBinder := underBinder_1, usedOnly := usedOnly_1, merge := merge_1, useContext := useContext_1,
        onlyGivenNames := onlyGivenNames_1, preserveBinderNames := preserveBinderNames_1, lift := lift_1 }) =
    (proofs = proofs_1 ∧
      types = types_1 ∧
        implicits = implicits_1 ∧
          descend = descend_1 ∧
            underBinder = underBinder_1 ∧
              usedOnly = usedOnly_1 ∧
                merge = merge_1 ∧
                  useContext = useContext_1 ∧
                    onlyGivenNames = onlyGivenNames_1 ∧ preserveBinderNames = preserveBinderNames_1 ∧ lift = lift_1)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The multilinear version of `LinearMap.comp_codRestrict`  -/
LinearMap.compMultilinearMap_codRestrict : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃)
  (f : MultilinearMap R M₁ M₂) (p : Submodule R M₃) (h : ∀ (c : M₂), g c ∈ p),
  (LinearMap.codRestrict p g h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, k ∈ Std.DTreeMap.Internal.Impl.insert! k v t
-- Mathlib.NumberTheory.NumberField.Basic
/-- A ℤ-basis of the ring of integers of `K`.  -/
NumberField.RingOfIntegers.basis : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Module.Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℤ (NumberField.RingOfIntegers K)
-- Mathlib.Geometry.Manifold.HasGroupoid
HasGroupoid.mk : ∀ {H : Type u_5} [inst : TopologicalSpace H] {M : Type u_6} [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H},
  (∀ {e e' : OpenPartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G) → HasGroupoid M G
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' : ∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    Summable f →
      (Summable fun x => ‖g x‖) →
        Summable g →
          (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n =
            ∑' (n : ℕ), ∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, f kl.1 * g kl.2