mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t ≠ ∅ → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ e₁_1 : T₁.obj₁ ≅ T₂.obj₁) (e_e₁ : e₁ = e₁_1)
  (e₂ e₂_1 : T₁.obj₂ ≅ T₂.obj₂) (e_e₂ : e₂ = e₂_1)
  (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁),
  CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm =
    CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁_1 e₂_1 ⋯
-- Mathlib.Data.Sum.Order
/-- The lexicographical bottom of a sum is the bottom of the left component.  -/
Sum.Lex.orderBot : {α : Type u_1} → {β : Type u_2} → [inst : LE α] → [OrderBot α] → [inst_2 : LE β] → OrderBot (α ⊕ₗ β)
-- Mathlib.GroupTheory.Nilpotent
AddGroup.nilpotencyClass_def : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G], AddGroup.nilpotencyClass G = Nat.find ⋯
-- Mathlib.SetTheory.ZFC.PSet
/-- The pre-set separation operation `{x ∈ a | p x}`  -/
PSet.sep : (PSet.{u_1} → Prop) → PSet.{u_1} → PSet.{u_1}
-- Mathlib.Logic.Equiv.Functor
Functor.mapEquiv_refl : ∀ {α : Type u} (f : Type u → Type v) [inst : Functor f] [inst_1 : LawfulFunctor f],
  Functor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_le_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km kmi : α},
  t.max? = some km → (t.insert k).max?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.bind₁_zero_wittPolynomial : ∀ {p : ℕ} {R : Type u} [inst : CommRing R] [Fact (Nat.Prime p)] (n : ℕ),
  (MvPolynomial.bind₁ 0) (wittPolynomial p R n) = 0
-- Std.Sat.AIG.CNF
/-- We say that a cache extends another by an index when it doesn't invalidate any entry and has an
entry for that index.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy : {aig : Std.Sat.AIG ℕ} →
  {cnf1 cnf2 : Std.Sat.CNF ℕ} →
    Std.Sat.AIG.toCNF.Cache✝ aig cnf1 → Std.Sat.AIG.toCNF.Cache✝ aig cnf2 → (new : ℕ) → new < aig.decls.size → Prop
-- Mathlib.Data.Num.Basic
ZNum.pos.injEq : ∀ (a a_1 : PosNum), (ZNum.pos a = ZNum.pos a_1) = (a = a_1)
-- Init.Data.UInt.Lemmas
UInt64.toNat_toUInt8 : ∀ (x : UInt64), x.toUInt8.toNat = x.toNat % 2 ^ 8
-- Mathlib.Algebra.Notation.Defs
SMul.ext : ∀ {M : Type u} {α : Type v} {x y : SMul M α}, SMul.smul = SMul.smul → x = y
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.comp_toThinSkeleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  F.comp (CategoryTheory.toThinSkeleton D) = (CategoryTheory.toThinSkeleton C).comp (CategoryTheory.ThinSkeleton.map F)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.homogeneousHull_toIdeal_eq_self : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] (I : HomogeneousIdeal 𝒜),
  Ideal.homogeneousHull 𝒜 I.toIdeal = I
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_add_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {β : Type u_5} [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s + t).inf f = s.inf fun x => t.inf fun x_1 => f (x + x_1)
-- Lean.Elab.SyntheticMVars
/-- Try to elaborate `stx` that was postponed by an elaboration method using `Exception.postpone`.
It returns `true` if it succeeded, and `false` otherwise.
It is used to implement `synthesizeSyntheticMVars`.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.resumePostponed : Lean.Elab.Term.SavedContext → Lean.Syntax → Lean.MVarId → Bool → Lean.Elab.TermElabM Bool
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.one_lt_omega0 : 1 < Ordinal.omega0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.inv_nonneg_of_nonneg : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : PartialOrder A]
  [inst_4 : Algebra NNReal A] [ContinuousFunctionalCalculus NNReal A fun x => 0 ≤ x] (a : Aˣ),
  autoParam (0 ≤ ↑a) CFC.inv_nonneg_of_nonneg._auto_1 → 0 ≤ ↑a⁻¹
-- Mathlib.Analysis.RCLike.Basic
RCLike.one_re : ∀ {K : Type u_1} [inst : RCLike K], RCLike.re 1 = 1
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.mk.sizeOf_spec : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : Star R] [inst_2 : SizeOf R] (toSubsemiring : Subsemiring R)
  (star_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → star a ∈ toSubsemiring.carrier),
  sizeOf { toSubsemiring := toSubsemiring, star_mem' := star_mem' } = 1 + sizeOf toSubsemiring
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.separatingLeft_toBilin_iff : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {M : Matrix ι ι R₂} (b : Module.Basis ι R₂ M₂),
  LinearMap.SeparatingLeft ((Matrix.toBilin b) M) ↔ M.SeparatingLeft
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys.isEmpty = t.isEmpty
-- Mathlib.GroupTheory.OrderOfElement
orderOf_dvd_of_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, x ^ n = 1 → orderOf x ∣ n
-- Init.Data.List.Lemmas
List.filter_map : ∀ {β : Type u_1} {α : Type u_2} {f : β → α} {p : α → Bool} {l : List β},
  List.filter p (List.map f l) = List.map f (List.filter (p ∘ f) l)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_lieSpan_submodule_eq_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {p : Submodule R L},
  (LieSubalgebra.lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_bot : ∀ {α : Type u_1} [inst : MeasurableSpace α], ↑⊥ = ⊥
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
/-- The morphism on cochain complexes indexed by `ℤ` that is induced by
an (heterogeneous) morphism of injective resolutions.  -/
CategoryTheory.InjectiveResolution.Hom.hom' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X : C} →
        {R : CategoryTheory.InjectiveResolution X} →
          {X' : C} →
            {R' : CategoryTheory.InjectiveResolution X'} →
              {f : X ⟶ X'} → R.Hom R' f → (R.cochainComplex ⟶ R'.cochainComplex)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.tensor_comp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁)
  (g₂ : Y₂ ⟶ Z₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
      (CategoryTheory.CategoryStruct.comp f₂ g₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂)
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivWithinAt.const_smul : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasFDerivWithinAt f f' s x → ∀ (c : R), HasFDerivWithinAt (c • f) (c • f') s x
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.AnalyzeResult.maxS? : FBinopElab.AnalyzeResult✝ → Option FBinopElab.SRec
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.Contradiction.Config : Type
-- Mathlib.Algebra.Order.Sub.Basic
tsub_self_add : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] (a b : α), a - (a + b) = 0
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_compRight`. -/
BilinForm.toMatrix_compRight : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁),
  (LinearMap.BilinForm.toMatrix b) (B.compRight f) = (LinearMap.BilinForm.toMatrix b) B * (LinearMap.toMatrix b b) f
-- Lean.Meta.TryThis
/-- Optional info to be printed immediately after replacement text in a widget.  -/
Lean.Meta.Tactic.TryThis.Suggestion.postInfo? : Lean.Meta.Tactic.TryThis.Suggestion → Option String
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_add_op : ∀ {α : Type u_2} [inst : MeasurableSpace α], Measurable AddOpposite.op
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.lt_pure_iff : ∀ {α : Type u} {f : Filter α} {a : α}, f < pure a ↔ f = ⊥
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  (F : CategoryTheory.Functor C H), (L.lan.obj F).IsLeftKanExtension (L.lanUnit.app F)
-- Mathlib.Order.Antisymmetrization
instWellFoundedLTAntisymmetrizationLe : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedLT α], WellFoundedLT (Antisymmetrization α fun x1 x2 => x1 ≤ x2)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.sumFrom.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (n lo : ℕ) (f : ℕ → R),
  BirdDet.sumFrom n lo f = if lo < n then f lo + BirdDet.sumFrom n (lo + 1) f else 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Y) (g : X ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) =
    CategoryTheory.CategoryStruct.comp g
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h))
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_rankPos : ∀ {α : Type u_1} {E I : Set α}, I ⊆ E → I.Nonempty → (Matroid.uniqueBaseOn I E).RankPos
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_ediv_of_mul_dvd : ∀ {a b c : ℤ}, a * b ∣ c → b ∣ c / a
-- Mathlib.Data.Finset.Insert
Finset.instLawfulSingleton : ∀ {α : Type u_1} [inst : DecidableEq α], LawfulSingleton α (Finset α)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.const.inj : ∀ {a : Lean.Name} {a_1 : ℕ} {a_2 : Lean.Name} {a_3 : ℕ},
  Lean.Meta.DiscrTree.Key.const a a_1 = Lean.Meta.DiscrTree.Key.const a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Data.Multiset.Bind
Multiset.prod_bind : ∀ {α : Type u_1} {β : Type v} [inst : CommMonoid β] (s : Multiset α) (t : α → Multiset β),
  (s.bind t).prod = (Multiset.map (fun a => (t a).prod) s).prod
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.isoEquivAlgEquiv_symm_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Algebra R X] [inst_3 : CommRing Y]
  [inst_4 : Algebra R Y] (e : X ≃ₐ[R] Y), CommAlgCat.isoEquivAlgEquiv.symm e = CommAlgCat.isoMk e
-- Mathlib.GroupTheory.Finiteness
AddMonoid.closure_finset_fg : ∀ {M : Type u_1} [inst : AddMonoid M] (s : Finset M), AddMonoid.FG ↥(AddSubmonoid.closure ↑s)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- Recursion principle for the complement sequence for a normalised EDS: if we have
* `P 0`, `P 1`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
  `P (m + 4)`, and `P (m + 5)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
  and `P (m + 4)`,

then we have `P n` for all `n : ℕ`.  -/
complEDSRec : {P : ℕ → Sort u_4} →
  P 0 →
    P 1 →
      ((m : ℕ) → P (m + 1) → P (2 * (m + 1))) → ((m : ℕ) → P (m + 1) → P (m + 2) → P (2 * (m + 1) + 1)) → (n : ℕ) → P n
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_not : ∀ {w k : ℕ} {x : BitVec w}, k ≤ w → BitVec.setWidth k (~~~x) = ~~~BitVec.setWidth k x
-- Lean.Meta.PPGoal
_private.Lean.Meta.PPGoal.0.Lean.Meta.ppGoal.ppVars : ℤ →
  Bool →
    List Lean.Name →
      Option Lean.Expr → Std.Format → Lean.LocalDecl → Lean.MetaM (List Lean.Name × Option Lean.Expr × Std.Format)
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.AssocListIterator.ext_iff : ∀ {α : Type u} {β : α → Type v} {x y : Std.DHashMap.Internal.AssocList.AssocListIterator α β}, x = y ↔ x.l = y.l
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.isomorphisms C).IsMultiplicative
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_mul_monomial : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {p : MvPolynomial σ R}
  (f : R →+* S₁) (g : σ → S₁) {s : σ →₀ ℕ} {a : R},
  MvPolynomial.eval₂ f g (p * (MvPolynomial.monomial s) a) = MvPolynomial.eval₂ f g p * f a * s.prod fun n e => g n ^ e
-- Mathlib.Tactic.Abel
/-- Interpret the sum of two expressions in `abel`'s normal form.
 -/
Mathlib.Tactic.Abel.evalAdd : Mathlib.Tactic.Abel.NormalExpr →
  Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)
-- Mathlib.NumberTheory.Dioph
Poly.sumsq.eq_def : ∀ {α : Type u_1} (x : List (Poly α)),
  Poly.sumsq x =
    match x with
    | [] => 0
    | p :: ps => p * p + Poly.sumsq ps
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Forgetting that a monomorphism over `X` is a monomorphism, then taking its image,
is the identity functor.
 -/
CategoryTheory.MonoOver.forgetImage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      [inst_1 : CategoryTheory.Limits.HasImages C] →
        (CategoryTheory.MonoOver.forget X).comp CategoryTheory.MonoOver.image ≅
          CategoryTheory.Functor.id (CategoryTheory.MonoOver X)
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.toFinsupp_single_tmul : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (c : A) (z : L), (LieAlgebra.LoopAlgebra.toFinsupp R A L) (AddMonoidAlgebra.single c 1 ⊗ₜ[R] z) = fun₀ | c => z
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_zero_eq_empty : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {j : Topology.RelCWComplex.cell C 0}, Topology.RelCWComplex.cellFrontier 0 j = ∅
-- Mathlib.RepresentationTheory.Basic
/-- The free `k[G]`-module on a type `α` is isomorphic to the representation `free k G α`.  -/
Representation.finsuppLEquivFreeAsModule : (k : Type u_1) →
  (G : Type u_2) →
    [inst : CommSemiring k] →
      [inst_1 : Monoid G] →
        (α : Type u_6) → (α →₀ MonoidAlgebra k G) ≃ₗ[MonoidAlgebra k G] (Representation.free k G α).asModule
-- Init.Prelude
/-- Unsigned 32-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 32-bit value
rather than wrapping a `BitVec 32`.
 -/
UInt32 : Type
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_1 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt isLt_1 : 0 < n + 1 + 1)
  (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_2 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨0, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_1 isLt isLt_1 x
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyMap_exact₁_of_distTriang : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
  (hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyMap_exact₁_of_distTriang._auto_1),
  { X₁ := HomologicalComplex.homology T.obj₃ n₀, X₂ := HomologicalComplex.homology T.obj₁ n₁,
      X₃ := HomologicalComplex.homology T.obj₂ n₁, f := CochainComplex.homologyδOfTriangle T n₀ n₁ h,
      g := HomologicalComplex.homologyMap T.mor₁ n₁, zero := ⋯ }.Exact
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processParserCategory : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.trans.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S') {E'' : Type u_5} [inst_4 : AddGroup E''] {S'' : AddGroupExtension N E'' G}
  (equiv' : S'.Equiv S''),
  equiv.trans equiv' = { toAddEquiv := equiv.trans equiv'.toAddEquiv, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Mathlib.Combinatorics.SetFamily.LYM
Finset.slice_union_shadow_falling_succ : ∀ {α : Type u_2} [inst : DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)),
  𝒜.slice k ∪ (Finset.falling (k + 1) 𝒜).shadow = Finset.falling k 𝒜
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n+1`-th iterated derivative can be obtained by differentiating the `n`-th
iterated derivative.  -/
iteratedDeriv_succ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F}, iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)
-- Init.Data.List.Lemmas
List.filterMap_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : α → Option β},
  List.filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂
-- Init.Data.BitVec.Lemmas
BitVec.twoPow_and : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), BitVec.twoPow w i &&& x = if x.getLsbD i = true then BitVec.twoPow w i else 0#w
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mk.inj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} A}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {inst_2 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {fst : A} {snd : C} {iso : F.obj fst ≅ G.obj snd}
  {fst_1 : A} {snd_1 : C} {iso_1 : F.obj fst_1 ≅ G.obj snd_1},
  { fst := fst, snd := snd, iso := iso } = { fst := fst_1, snd := snd_1, iso := iso_1 } →
    fst = fst_1 ∧ snd = snd_1 ∧ iso ≍ iso_1
-- Mathlib.Analysis.Complex.HasPrimitives
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.mem_closedBall_aux : ∀ {c z : ℂ} {r y : ℝ},
  z ∈ Metric.closedBall c r → y ∈ Set.uIoc c.im z.im → ↑z.re + ↑y * Complex.I ∈ Metric.closedBall c r
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_intCast : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A} (n : ℤ), (↑n).val = ↑n
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g f) g) =
    Set.range ⇑g ∩ Set.range ⇑f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.ExtDHashMap α β)
  (e_m : m = m_1) (a : α) (h : a ∈ m), m.get a h = m_1.get a ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- The discrete convolution of `f` and `g` using bilinear map `L`:
`(f ⋆[L] g) x = ∑' (a, b) : mulFiber x, L (f a) (g b)`.  -/
DiscreteConvolution.convolution : {M : Type u_1} →
  {S : Type u_2} →
    {E : Type u_3} →
      {E' : Type u_4} →
        {F : Type u_6} →
          [Monoid M] →
            [inst : CommSemiring S] →
              [inst_1 : AddCommMonoid E] →
                [inst_2 : AddCommMonoid E'] →
                  [inst_3 : AddCommMonoid F] →
                    [inst_4 : Module S E] →
                      [inst_5 : Module S E'] →
                        [inst_6 : Module S F] → [TopologicalSpace F] → (E →ₗ[S] E' →ₗ[S] F) → (M → E) → (M → E') → M → F
-- Lean.Elab.Do.InferControlInfo
/-- Infer the `ControlInfo` of a single doElem.  -/
Lean.Elab.Do.inferControlInfoElem : Lean.DoElem → Lean.Elab.TermElabM Lean.Elab.Do.ControlInfo
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).inv
      (CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) =
    CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F