mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂),
  ↑(h ∘SL f) = ↑h ∘ₛₗ ↑f
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.error.inj : ∀ {stx : Lean.TSyntax `tactic} {msg : Lean.MessageData} {stx_1 : Lean.TSyntax `tactic} {msg_1 : Lean.MessageData},
  Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝ stx msg =
      Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝ stx_1 msg_1 →
    stx = stx_1 ∧ msg = msg_1
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Ideal R}
  [inst_3 : p.IsPrime],
  p ∈ associatedPrimes R M →
    IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈
      associatedPrimes (Localization.AtPrime p) (LocalizedModule.AtPrime p M)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_filterM : ∀ {α β γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [inst_4 : Std.Internal.Do.Assertion Pred]
  [inst_5 : Std.Internal.Do.Assertion EPred] [inst_6 : Std.Internal.Do.WPMonad o Pred EPred] [inst_7 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_9 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_12 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → n (ULift.{w, 0} Bool)}
  {init : γ} {g : β → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.filterM f it) init g ⦃ Q; eQ ⦄
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.eq_iso_inv : ∀ (f : CategoryTheory.WalkingIso.one ⟶ CategoryTheory.WalkingIso.zero), f = CategoryTheory.WalkingIso.iso.inv
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.toDecomposition : {ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      {inst : DecidableEq ι} →
        {inst_1 : AddMonoid ι} →
          {inst_2 : Semiring A} →
            {inst_3 : SetLike σ A} →
              {inst_4 : AddSubmonoidClass σ A} → {𝒜 : ι → σ} → [self : GradedRing 𝒜] → DirectSum.Decomposition 𝒜
-- Mathlib.RingTheory.HahnSeries.PowerSeries
/-- The ring `R⟦ℕ⟧` is isomorphic to `PowerSeries R`.  -/
HahnSeries.toPowerSeries : {R : Type u_2} → [inst : Semiring R] → HahnSeries ℕ R ≃+* PowerSeries R
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.under_le_under_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I J : Ideal S}, Ideal.under R I ≤ Ideal.under R J ↔ I ≤ J
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.GrothendieckTopology.monotone_close : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C},
  Monotone J₁.close
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.isEqvAux.match_1.eq_2 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.DTreeMap.Raw.Const.unitOfList l cmp).getKeyD k' fallback = k
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffAt_diffeomorph_comp_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : M' → M},
  m ≤ n → ∀ {x : M'}, ContMDiffAt I' J m (⇑h ∘ f) x ↔ ContMDiffAt I' I m f x
-- Mathlib.Data.List.Basic
List.choose_mem : ∀ {α : Type u} (p : α → Prop) [inst : DecidablePred p] (l : List α) (hp : ∃ a ∈ l, p a), List.choose p l hp ∈ l
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_eq_zero : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G}, A.convolution B x = 0 ↔ x ∉ A * B
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofBitVec : ∀ {b : BitVec 16}, { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_div : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α] (s t : NonemptyInterval α),
  (s / t).toProd.2 = s.toProd.2 / t.toProd.1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- An element commutes with `cfcₙ f a` if it commutes with both `a` and `star a`.

If the base ring is `ℝ` or `ℝ≥0`, see `Commute.cfcₙ_real` or `Commute.cfcₙ_nnreal` which don't
require the `Commute (star a) b` hypothesis.  -/
Commute.cfcₙ : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A},
  Commute a b → Commute (star a) b → ∀ (f : 𝕜 → 𝕜), Commute (cfcₙ f a) b
-- Mathlib.Topology.Bases
Topology.IsEmbedding.secondCountableTopology : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : TopologicalSpace β]
  [SecondCountableTopology β], Topology.IsEmbedding f → SecondCountableTopology α
-- Mathlib.Topology.Sets.Closeds
/-- The equivalence between `IrreducibleCloseds α` and `{x : Set α // IsClosed x ∧ IsIrreducible x }`.
 -/
TopologicalSpace.IrreducibleCloseds.equivSubtype' : {α : Type u_2} →
  [inst : TopologicalSpace α] → TopologicalSpace.IrreducibleCloseds α ≃ { x // IsClosed x ∧ IsIrreducible x }
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_neg : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R} [IsOrderedRing R], ⌈-a⌉ = -⌊a⌋
-- Batteries.Data.List.Basic
/-- **Alias** of `List.idxsOf`.

---

`idxsOf a l s` is the list of all indexes of `a` in `l`,  added to an
optional parameter `s`. For example:
```
idxsOf b [a, b, a, a] = [1]
idxsOf a [a, b, a, a] 5 = [5, 7, 8]
```
 -/
List.indexesOf : {α : Type u_1} → [BEq α] → α → List α → optParam ℕ 0 → List ℕ
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates the current argument.
The argument `remainingArgs` is the number of arguments in the application after this one.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.mkArg : Bool →
  Lean.PrettyPrinter.Delaborator.ParamKind →
    Lean.PrettyPrinter.Delaborator.DelabM Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Mathlib.Order.Monotone.Basic
StrictAntiOn.compares : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → ∀ {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares b a
-- Init.Data.Vector.Lemmas
Vector.singleton_inj : ∀ {α : Type u_1} {a b : α}, #v[a] = #v[b] ↔ a = b
-- Mathlib.Algebra.Order.Antidiag.Nat
PNat.instHasAntidiagonal : Finset.HasAntidiagonal (Additive ℕ+)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction' : ∀ {ι : Type u_1} {κ : Type u_2} {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mY : (j : κ) → MeasurableSpace (Y j)} [inst_3 : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)]
  [∀ (j : κ), HasOuterApproxClosed (Y j)] [Finite ι] [Finite κ] {μ : MeasureTheory.Measure ((i : ι) → X i)}
  {ν : MeasureTheory.Measure ((j : κ) → Y j)} {ξ : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ),
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂ξ =
        (∫ (x : (i : ι) → X i), f x ∂μ) * ∫ (y : (j : κ) → Y j), g y ∂ν) →
    ξ = μ.prod ν
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.codisjoint_mrange_inl_mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  Codisjoint (AddMonoidHom.mrange AddMonoid.Coprod.inl) (AddMonoidHom.mrange AddMonoid.Coprod.inr)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Addition.
 -/
Std.Tactic.BVDecide.BVBinOp.add : Std.Tactic.BVDecide.BVBinOp
-- Init.Data.Range.Polymorphic.IntLemmas
Int.size_rco : ∀ {a b : ℤ}, (a...b).size = (b - a).toNat
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.self_trans_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), e.trans e.symm = MulEquiv.refl M
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.sub_nonneg_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  {a b : M}, 0 ≤ a - b ↔ b ≤ a
-- Mathlib.Algebra.Lie.Basic
LieAlgebra.mk : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [toModule : Module R L] → (∀ (t : R) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆) → LieAlgebra R L
-- Init.Data.Int.Pow
Int.pow_succ : ∀ (m : ℤ) (n : ℕ), m ^ n.succ = m ^ n * m
-- Mathlib.Data.Nat.Nth
Nat.nth_mem_anti : ∀ {p : ℕ → Prop} {a b : ℕ}, a ≤ b → p (Nat.nth p b) → p (Nat.nth p a)
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.lintegral_kernel_prod_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : β → α → ENNReal},
  Measurable (Function.uncurry f) → Measurable fun y => ∫⁻ (x : β), f x y ∂κ y
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.directLimitIsColimit_desc : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι] (G : ι → Type v)
  [inst_3 : (i : ι) → AddCommGroup (G i)] [inst_4 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_5 : DirectedSystem G fun i j h => ⇑(f i j h)]
  (s : CategoryTheory.Limits.Cocone (ModuleCat.directLimitDiagram G f)),
  (ModuleCat.directLimitIsColimit G f).desc s =
    ModuleCat.ofHom (Module.DirectLimit.lift R ι G f (fun i => ModuleCat.Hom.hom (s.ι.app i)) ⋯)
-- Mathlib.Data.Option.Basic
guard.congr_simp : ∀ {f : Type → Type v} [inst : Alternative f] (p p_1 : Prop),
  p = p_1 → ∀ {inst_1 : Decidable p} [inst_2 : Decidable p_1], guard p = guard p_1
-- Mathlib.Algebra.Group.Submonoid.Support
/-- **Alias** of the forward direction of `isPointed_iff_support_eq_bot`. -/
AddSubmonoid.IsPointed.support_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.IsPointed → M.support = ⊥
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn.eq : ∀ {ε : Type u} {α : Type v} {motive_1 : Lean.AsyncList ε α → Sort u_1}
  {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1}
  {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1}
  (t : Lean.AsyncList ε α) (F_1 : (t : Lean.AsyncList ε α) → t.below → motive_1 t)
  (F_2 : (t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t)
  (F_3 : (t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t)
  (F_4 : (t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_1 t (Lean.AsyncList.brecOn.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Order.CompactlyGenerated.Basic
iSupIndep_iff_supIndep_of_injOn : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {f : ι → α},
  Set.InjOn f {i | f i ≠ ⊥} → (iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsIsolated.eq_1 : ∀ {α : Type u_1} (H : Hypergraph α) (x : α), H.IsIsolated x = ∀ e ∈ H.edgeSet, x ∉ e
-- Init.Data.Array.Lemmas
Array.append_ne_empty_of_right_ne_empty : ∀ {α : Type u_1} {xs ys : Array α}, ys ≠ #[] → xs ++ ys ≠ #[]
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.d₁ : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (self : e₀₁.CompStruct e₁₂ e₀₂),
  (CategoryTheory.ConcreteCategory.hom
        (X.map
          (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
      self.simplex =
    e₀₂.edge
-- Mathlib.Algebra.Module.ZLattice.Basic
instModuleFree_of_discrete_submodule : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L], Module.Free ℤ ↥L
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.Space : {A : Type} → [inst : MetricSpace A] → GromovHausdorff.AuxGluingStruct A → Type
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_map_mul : ∀ {μ : MeasureTheory.Measure ℝ} (r t : ℝ),
  MeasureTheory.charFun (MeasureTheory.Measure.map (fun x => r * x) μ) t = MeasureTheory.charFun μ (r * t)
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedAlgebra.proj_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜] (i : ι) (r : A),
  (GradedAlgebra.proj 𝒜 i) r = ↑(((DirectSum.decompose 𝒜) r) i)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.toArray.size = t.size
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.min_le_mk_of_le_of_le : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {x y z : M},
  y ≤ x → x ≤ z → min (ArchimedeanClass.mk y) (ArchimedeanClass.mk z) ≤ ArchimedeanClass.mk x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskering.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J),
  CategoryTheory.Limits.Cone.whiskering E =
    { obj := fun c => CategoryTheory.Limits.Cone.whisker E c, map := fun {X Y} f => { hom := f.hom, w := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- Let `B` be a faithfully flat `A`-algebra, then `A` is a local ring if `B` is.  -/
Module.FaithfullyFlat.isLocalRing : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B] [IsLocalRing B], IsLocalRing A
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- The group structure on `DihedralGroup n`.
 -/
DihedralGroup.instGroup : {n : ℕ} → Group (DihedralGroup n)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ → σ → Γ) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stmts₁ (Turing.TM1.Stmt.write a q) = insert (Turing.TM1.Stmt.write a q) (Turing.TM1.stmts₁ q)
-- Batteries.Data.List.Lemmas
List.dropInfix?_eq_some_iff : ∀ {α : Type u_1} [inst : BEq α] {l i p s : List α},
  l.dropInfix? i = some (p, s) ↔
    (∃ i', l = p ++ i' ++ s ∧ (i' == i) = true) ∧
      ∀ (p' i' s' : List α), l = p' ++ i' ++ s' → (i' == i) = true → p'.length ≥ p.length
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F)
  (ψ : ↥q →L[R] F) (x : ↥q), (ContinuousLinearMap.ofIsTopCompl h φ ψ) ↑x = ψ x
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.ofFinsupp_algebraMap : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  { toFinsupp := (algebraMap R (AddMonoidAlgebra A ℕ)) r } = (algebraMap R (Polynomial A)) r
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.beqModel_congr : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : BEq β] {l₁ l₂ l₃ l₄ : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l₂ →
    l₁.Perm l₃ → l₂.Perm l₄ → Std.Internal.List.Const.beqModel l₁ l₂ = Std.Internal.List.Const.beqModel l₃ l₄
-- Lean.Attributes
/-- Low level attribute registration function.  -/
Lean.registerBuiltinAttribute : Lean.AttributeImpl → IO Unit
-- Mathlib.Topology.Category.CompHaus.Basic
/-- The fully faithful embedding of `CompHaus` in `TopCat`.  -/
compHausToTop : CategoryTheory.Functor CompHaus TopCat
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.of_val : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x : P.Cotangent), Algebra.Extension.Cotangent.of x.val = x
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
CategoryTheory.extensiveTopology.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C],
  CategoryTheory.extensiveTopology C = (CategoryTheory.extensiveCoverage C).toGrothendieck
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.append.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) →
    (x x_1 : RBTree.RBNode α) →
      ((x : RBTree.RBNode α) → motive RBTree.RBNode.nil x) →
        ((x : RBTree.RBNode α) → (x = RBTree.RBNode.nil → False) → motive x RBTree.RBNode.nil) →
          ((a : RBTree.RBNode α) →
              (x : α) →
                (b c : RBTree.RBNode α) →
                  (y : α) →
                    (d : RBTree.RBNode α) →
                      motive (RBTree.RBNode.node RBTree.RBColor.red a x b)
                        (RBTree.RBNode.node RBTree.RBColor.red c y d)) →
            ((a : RBTree.RBNode α) →
                (x : α) →
                  (b c : RBTree.RBNode α) →
                    (y : α) →
                      (d : RBTree.RBNode α) →
                        motive (RBTree.RBNode.node RBTree.RBColor.black a x b)
                          (RBTree.RBNode.node RBTree.RBColor.black c y d)) →
              ((l : RBTree.RBNode α) →
                  (v : α) →
                    (r b : RBTree.RBNode α) →
                      (x : α) →
                        (c : RBTree.RBNode α) →
                          motive (RBTree.RBNode.node RBTree.RBColor.black l v r)
                            (RBTree.RBNode.node RBTree.RBColor.red b x c)) →
                ((a : RBTree.RBNode α) →
                    (x : α) →
                      (b l : RBTree.RBNode α) →
                        (v : α) →
                          (r : RBTree.RBNode α) →
                            motive (RBTree.RBNode.node RBTree.RBColor.red a x b)
                              (RBTree.RBNode.node RBTree.RBColor.black l v r)) →
                  motive x x_1
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.HasLift.iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g), sq.HasLift ↔ ⋯.HasLift
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.codisjoint_iff_exists_add_eq : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M}, Codisjoint p p' ↔ ∀ (z : M), ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ {n : ℕ} {e : Fin n → S},
      CompleteOrthogonalIdempotents e →
        (∀ (i : Fin n), e i ∈ f.range) → ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.mk.injEq : ∀ {Γ : Type u} {Γ' : Type v} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Γ → Γ') (map_pt' : f default = default)
  (f_1 : Γ → Γ') (map_pt'_1 : f_1 default = default),
  ({ f := f, map_pt' := map_pt' } = { f := f_1, map_pt' := map_pt'_1 }) = (f = f_1)
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The underlying type of the colimit of a diagram in `CommRingCat`.
 -/
RingCat.Colimits.ColimitType : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J RingCat → Type v
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.land.eq_1 : Nat.land = Nat.bitwise and
-- Mathlib.Algebra.GradedMonoid
/-- The zeroth power will yield 1  -/
GradedMonoid.GMonoid.gnpow_zero' : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a : GradedMonoid A),
  GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpow 0 a.snd) = 1
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.isInvertible_restrict : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (pkg : u.FredholmPackage), (u.restrict ⋯).IsInvertible
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.renameEquiv_symm : ∀ {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (f : σ ≃ τ),
  (MvPolynomial.renameEquiv R f).symm = MvPolynomial.renameEquiv R f.symm
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of the identity on `s ∩ Icc a b` is `b - a`.  -/
eVariationOn_id : ∀ {a b : ℝ} {s : Set ℝ}, a ∈ s → b ∈ s → eVariationOn id (s ∩ Set.Icc a b) = ENNReal.ofReal (b - a)