mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.left = sq.f₁₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k a : α} {v : β} {h₁ : a ∈ t.insert k v}, (t.insert k v)[a] = if h₂ : cmp k a = Ordering.eq then v else t[a]
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedAddHom.congr_simp : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Field β] [inst_4 : ConditionallyCompleteLinearOrder β] [inst_5 : IsStrictOrderedRing β]
  [inst_6 : Archimedean α],
  ConditionallyCompleteLinearOrderedField.inducedAddHom α β = ConditionallyCompleteLinearOrderedField.inducedAddHom α β
-- Mathlib.Order.Antichain
IsAntichain.insert_of_symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  IsAntichain r s → ∀ [Std.Symm r], (∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b) → IsAntichain r (insert a s)
-- Batteries.Data.AssocList
/-- `O(n)`. Replace the first entry in the list
with key equal to `a` to have key `a` and value `b`.
 -/
Batteries.AssocList.replace : {α : Type u_1} → {β : Type u_2} → [BEq α] → α → β → Batteries.AssocList α β → Batteries.AssocList α β
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumDiffSubset_symm_apply_of_mem : ∀ {α : Type u_3} {s t : Set α} (h : s ⊆ t) [inst : DecidablePred fun x => x ∈ s] {x : ↑t} (hx : ↑x ∈ s),
  (Equiv.Set.sumDiffSubset h).symm x = Sum.inl ⟨↑x, hx⟩
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isLocal.HasTwoOutOfThreeProperty
-- Mathlib.FieldTheory.Finite.Polynomial
/-- Over a field, this is the indicator function as an `MvPolynomial`.  -/
MvPolynomial.indicator : {K : Type u_1} → {σ : Type u_2} → [Fintype K] → [Fintype σ] → [inst : CommRing K] → (σ → K) → MvPolynomial σ K
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X₀ : C₀)
  (i : (data (F.obj X₀)).I₀) {Z : A} (h : G₀.obj.obj (Opposite.op ((data (F.obj X₀)).X i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv data G₀ X₀)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ (F.obj X₀) i) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i)) h
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ι_D₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') = K.d₂ c₁₂ i₁ i₂ i₁₂'
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.add_iff_right` -/
DifferentiableOn.fun_add_iff_right : ∀ {𝕜 : 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 g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → (DifferentiableOn 𝕜 (fun i => f i + g i) s ↔ DifferentiableOn 𝕜 g s)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.homMk.congr_simp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X}
  (f f_1 : U.left ⟶ V.left) (e_f : f = f_1) (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom),
  CategoryTheory.Over.homMk f w = CategoryTheory.Over.homMk f_1 ⋯
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ NonemptyFinLinOrd FinPartOrd
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- The absolute value of a bounded continuous `ℝ`-valued function as a bounded
continuous `ℝ≥0`-valued function.  -/
BoundedContinuousFunction.nnnorm : {α : Type u} → [inst : TopologicalSpace α] → BoundedContinuousFunction α ℝ → BoundedContinuousFunction α NNReal
-- Mathlib.Algebra.Module.StablyFree.Basic
_private.Mathlib.Algebra.Module.StablyFree.Basic.0.Module.IsStablyFree.mk : ∀ {R : Type u} [inst : Ring R] {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (∃ N x x_1, ∃ (_ : Module.Finite R N) (_ : Module.Free R N), Module.Free R (M × N)) → Module.IsStablyFree R M
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMonoid : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → Monoid (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] → Monoid (DirectLimit G f)
-- Mathlib.Data.Set.Lattice
Set.subset_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β) (i : ι), s i ⊆ ⋃ i, s i
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_affineSubspace : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : AffineSubspace k P},
  (↑s).Nonempty → asymptoticCone k ↑s = closure ↑s.direction
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_mul_X : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (p : Polynomial R),
  (⇑Polynomial.derivative)^[n] (p * Polynomial.X) =
    (⇑Polynomial.derivative)^[n] p * Polynomial.X + n • (⇑Polynomial.derivative)^[n - 1] p
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.homeomorphOfUnit_symm_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (T : (M₁ →L[R₁] M₁)ˣ) (a : M₁), (ContinuousLinearMap.homeomorphOfUnit T).symm a = ↑T⁻¹ a
-- Init.Core
Relation.TransGen.below.single : ∀ {α : Sort u} {r : α → α → Prop} {a : α} {motive : (a_1 : α) → Relation.TransGen r a a_1 → Prop} {b : α} (a_1 : r a b),
  Relation.TransGen.below ⋯
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.comap_cotangentIdeal : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), Ideal.comap (Ideal.Quotient.mk (I ^ 2)) I.cotangentIdeal = I
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
selfAdjoint.unitarySelfAddISMul_coe : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a : ↥(selfAdjoint A))
  (ha_norm : ‖a‖ ≤ 1), ↑(selfAdjoint.unitarySelfAddISMul a ha_norm) = ↑a + Complex.I • CFC.sqrt (1 - ↑a ^ 2)
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mker_mapRangeAddMonoidHom : ∀ {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [inst : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_1 : (i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i),
  AddMonoidHom.mker (DFinsupp.mapRange.addMonoidHom f) =
    AddSubmonoid.comap DFinsupp.coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i => AddMonoidHom.mker (f i))
-- Mathlib.Data.Stream.Defs
Stream'.unfolds : {α : Type u} → {β : Type v} → (α → β) → (α → α) → α → Stream' β
-- Lean.Elab.Tactic.Simp
/-- Implements the effect of the `*` attribute.  -/
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.applyStarArg : Lean.Meta.Simp.Context → Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.FieldTheory.SeparablyGenerated
MvPolynomial.toPolynomialAdjoinImageCompl.eq_1 : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (F : MvPolynomial ι k) (a : ι → K) (i : ι),
  F.toPolynomialAdjoinImageCompl a i =
    (Polynomial.mapAlgHom (MvPolynomial.aeval fun j => ⟨a ↑j, ⋯⟩))
      ((MvPolynomial.optionEquivLeft k { b // b ≠ i }) ((MvPolynomial.renameEquiv k (Equiv.optionSubtypeNe i).symm) F))
-- Init.Data.Nat.Gcd
Nat.gcd_sub_mul_left_left : ∀ {m n k : ℕ}, m * k ≤ n → (n - m * k).gcd m = n.gcd m
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- `setToFun` applied to the sum `T + T'` of two operators is the sum of the corresponding
`setToFun`. See also `setToFun_add_left'` for a version varying the reference measures.  -/
MeasureTheory.setToFun_add_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C''),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) →
    ∀ (f : α → E),
      MeasureTheory.setToFun μ T'' hT'' f = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T' hT' f
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.WithBot.inf : {ι : Type u_1} → Min (WithBot (BoxIntegral.Box ι))
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.op_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), h.op.g' = h.f'.op
-- Init.Data.UInt.Bitwise
UInt64.xor_zero : ∀ {a : UInt64}, a ^^^ 0 = a
-- Aesop.Script.TacticState
Aesop.Script.TacticState.invisibleGoals : Aesop.Script.TacticState → Std.HashSet Lean.MVarId
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.AdeleRing.algebraMap_fst_apply : ∀ (R : Type u_1) (K : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : K) (v : NumberField.InfinitePlace K),
  ((algebraMap K (NumberField.AdeleRing R K)) x).1 v = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
-- Lean.Util.LeanOptions
Lean.instEmptyCollectionLeanOptions : EmptyCollection Lean.LeanOptions
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.commMonoid.eq_1 : ∀ {α : Type u_2} [inst : CommMonoid α], Set.commMonoid = { toMonoid := Set.monoid, mul_comm := ⋯ }
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.coe_of : ∀ (R : Type u) [inst : CommSemiring R], ↑(CommSemiRingCat.of R) = R
-- Mathlib.RingTheory.LocalRing.Subring
/-- If in a sub(semi)ring `R` of a local (semi)ring `S` every element is either
invertible or a zero divisor, then `R` is local.  -/
IsLocalRing.of_subring : ∀ {S : Type u_1} [inst : Semiring S] [IsLocalRing S] {R : Subsemiring S},
  (∀ a ∈ nonZeroDivisors ↥R, IsUnit a) → IsLocalRing ↥R
-- Mathlib.Analysis.Convex.Side
Wbtw.wSameSide₃₂ : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, Wbtw R x y z → x ∈ s → s.WSameSide z y
-- Init.Data.List.Lemmas
List.foldl_add_const : ∀ {α : Type u_1} {l : List α} {a b : ℕ}, List.foldl (fun x x_1 => x + a) b l = b + a * l.length
-- Mathlib.Order.Basic
/-- **Alias** of `ge_of_eq`. -/
Eq.ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → b ≤ a
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₁_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥), RatFunc.Luroth.Q₁✝ h ≠ 0
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.SPolResult.mk : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Mon → ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.SPolResult
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddGrpCat.instBraidedForgetAddMonoidHomCarrier : (CategoryTheory.forget AddGrpCat).Braided
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- proof that this section is `C^n`  -/
ContMDiffSection.contMDiff_toFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] (self : ContMDiffSection I F n V),
  ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, self.toFun x⟩
-- Init.Data.List.Sublist
List.Sublist.map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {l₁ l₂ : List α}, l₁.Sublist l₂ → (List.map f l₁).Sublist (List.map f l₂)
-- Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
/-- If `R` is a normed commutative ring and `f₁` and `f₂` are two power-multiplicative `R`-algebra
norms on `S`, then if `f₁` and `f₂` are equivalent on every subring `R[y]` for `y : S`, it
follows that `f₁ = f₂` [BGR, Proposition 3.1.5/1][bosch-guntzer-remmert].  -/
eq_of_powMul_faithful : ∀ {R : Type u_1} {S : Type u_2} [inst : NormedCommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f₁ : AlgebraNorm R S),
  IsPowMul ⇑f₁ →
    ∀ (f₂ : AlgebraNorm R S),
      IsPowMul ⇑f₂ →
        (∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x) →
          f₁ = f₂
-- Mathlib.Algebra.Category.Grp.Basic
MulEquiv.toCommGrpIso_inv : ∀ {X Y : CommGrpCat} (e : ↑X ≃* ↑Y), e.toCommGrpIso.inv = CommGrpCat.ofHom e.symm.toMonoidHom
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The centroid of two points indexed by `Fin 2`, expressed directly
as adding a vector to the first point.  -/
Finset.centroid_pair_fin : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [Invertible 2] (p : Fin 2 → P), Finset.centroid k Finset.univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UnifIntegrable.ae_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f g : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifIntegrable f p μ → (∀ (n : ι), f n =ᵐ[μ] g n) → MeasureTheory.UnifIntegrable g p μ
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instNeg : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Neg (SlashInvariantForm Γ k)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.any_eq_forIn : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.any p it =
    (forIn it false fun x x_1 => if p x = true then pure (ForInStep.done true) else pure (ForInStep.yield false)).run
-- Mathlib.Data.Set.Card
ENat.card_coe_set_eq : ∀ {α : Type u_1} (s : Set α), ENat.card ↑s = s.encard
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive], CategoryTheory.NatTrans.CommShift (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom ℤ
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_nodal_derivative_eval_node_eq : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [inst_1 : DecidableEq ι] {i : ι},
  i ∈ s →
    Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)) =
      Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.z_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ),
  FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      ↑⋯.unit ^ 2 * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) =
    (hζ.toInteger - 1) * FermatLastTheoremForThreeGen.Solution.z✝ S
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isTop.injEq : ∀ (idx idx_1 : ℕ),
  (Mathlib.Tactic.Order.AtomicFact.isTop idx = Mathlib.Tactic.Order.AtomicFact.isTop idx_1) = (idx = idx_1)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F] [T2Space F] {f' : E → E →L[𝕜] F}, (∀ (x : E), HasFDerivAt f (f' x) x) → fderiv 𝕜 f = f'
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isAffine_affineOpenCover : ∀ (X : AlgebraicGeometry.Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.openCover.X i)
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_inter : ∀ {α : Type u_1} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
-- Lean.Language.Basic
Lean.Language.Snapshot.instInhabitedDiagnostics : Inhabited Lean.Language.Snapshot.Diagnostics
-- Aesop.Tree.Data
Aesop.Goal.normalizationState : Aesop.Goal → Aesop.NormalizationState
-- Mathlib.Tactic.NormNum.DivMod
/-- Given a result for evaluating `a b` in `ℤ` where `b > 0`, evaluate `a / b`.  -/
_private.Mathlib.Tactic.NormNum.DivMod.0.Mathlib.Meta.NormNum.evalIntDiv.core : (a na : Q(ℤ)) →
  ℤ →
    Q(Mathlib.Meta.NormNum.IsInt «$a» «$na») →
      (b : Q(ℤ)) →
        (nb : Q(ℕ)) →
          Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb») → ℤ × (q : Q(ℤ)) × Q(Mathlib.Meta.NormNum.IsInt («$a» / «$b») «$q»)
-- Init.Data.List.Lemmas
List.set_tail : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α}, l.tail.set i a = (l.set (i + 1) a).tail
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → Array.map Prod.fst m.toArray = m.keysArray
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.instHasMapBifunctorObjIntShiftFunctor : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) [K₁.HasMapBifunctor K₂ F],
  ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).HasMapBifunctor K₂ F
-- Mathlib.Data.Fintype.Card
Fintype.card_of_finset' : ∀ {α : Type u_1} {p : Set α} (s : Finset α),
  (∀ (x : α), x ∈ s ↔ x ∈ p) → ∀ [inst : Fintype ↑p], Fintype.card ↑p = s.card
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (a : R), MvPowerSeries.constantCoeff (MvPowerSeries.C a) = a
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSumLocallyUniformly_aux : ∀ (L : PeriodPair) (f : ↥L.lattice → ℂ → ℂ) (u : ℝ → ↥L.lattice → ℝ),
  (∀ r > 0, Summable (u r)) →
    (∀ r > 0, ∀ᶠ (R : ℝ) in Filter.atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l) →
      HasSumLocallyUniformly f fun x => ∑' (j : ↥L.lattice), f j x
-- Lean.Parser.Extra
Lean.Parser.mkAntiquot.formatter : String → Lean.SyntaxNodeKind → optParam Bool true → optParam Bool false → Lean.PrettyPrinter.Formatter
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_eq_getKey_getValue : ∀ {α : Type u} [inst : BEq α] {β : Type v} {l : List ((_ : α) × β)} {a : α}
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getEntry a l h = ⟨Std.Internal.List.getKey a l h, Std.Internal.List.getValue a l h⟩
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isBasis_loops_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.IsBasis I M.loops ↔ I = ∅
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_zpow_iff_log_le : ∀ {x y : ℝ} {n : ℤ}, 0 < x → 0 < y → (x ≤ y ^ n ↔ Real.log x ≤ ↑n * Real.log y)
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_self_add_right : ∀ {m n : ℕ}, m.Coprime (m + n) ↔ m.Coprime n
-- Mathlib.Algebra.Quaternion
Quaternion.star_add_self' : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), star a + a = ↑(2 * a.re)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_antidiagonal_of_finset : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  (f g : SkewMonoidAlgebra k G) (x : G) (s : Finset (G × G)),
  (∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) → (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntUInt32UintOfNatNat : Lean.Grind.ToInt UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isIso_ιTruncLE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ),
  CategoryTheory.IsIso (K.ιTruncLE n) ↔ K.IsStrictlyLE n
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mono₁ : ∀ {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 ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₃ = 0 → CategoryTheory.Mono T.mor₁
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_open_point : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E}
  {x : E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E], Convex ℝ s → IsOpen s → x ∉ s → ∃ f, ∀ a ∈ s, RCLike.re (f a) < RCLike.re (f x)
-- Init.Data.Array.Basic
/-- Removes the element at a given index from an array. Panics if the index is out of bounds.

This function takes worst-case `O(n)` time because it back-shifts all elements at positions
greater than `i`.
 -/
Array.eraseIdx! : {α : Type u} → Array α → ℕ → Array α
-- Lean.Server.Utils
/-- Meta-Data of a document.  -/
Lean.Server.DocumentMeta : Type