mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Except.map.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (v : α) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.ok v with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_2 v
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_dvd : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {x y : Polynomial R},
  x ∣ y → Polynomial.map f x ∣ Polynomial.map f y
-- Mathlib.Order.Interval.Set.Basic
IsTop.Iic_eq : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsTop a → Set.Iic a = Set.univ
-- Mathlib.Lean.MessageData.ForExprs
/-- Find the expression in a message on which `f` does not return `none`.  -/
Lean.MessageData.firstExpr? : {α : Type} → Lean.MessageData → (Lean.Expr → Lean.MetaM (Option α)) → IO (Option α)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Indep.exists_isBasis_subset_union_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I X J : Set α},
  M.Indep I → I ⊆ X → M.IsBasis J X → ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertListIfNewₘ.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (hd : (a : α) × β a) (tl : List ((a : α) × β a)),
  m.insertListIfNewₘ (hd :: tl) = (m.insertIfNew hd.fst hd.snd).insertListIfNewₘ tl
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A functor `F : T ⥤ D` induces a functor `Over X ⥤ Over (F.obj X)` in the obvious way.  -/
CategoryTheory.Over.post : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          (F : CategoryTheory.Functor T D) →
            CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over (F.obj X))
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
if `h` is an additive-to-multiplicative homomorphism.
This is a more specialized version of `Finsupp.prod_add_index` with simpler hypotheses.  -/
Finsupp.prod_add_index' : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : CommMonoid N] {f g : α →₀ M}
  {h : α → M → N},
  (∀ (a : α), h a 0 = 1) →
    (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) → (f + g).prod h = f.prod h * g.prod h
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasis'_dim : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic), (AdjoinRoot.powerBasis' hg).dim = g.natDegree
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_map_mul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CancelCommMonoid α] (s : Finset α) (a : α),
  mulRothNumber (Finset.map (mulRightEmbedding a) s) = mulRothNumber s
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_subsingleton : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [Subsingleton R] (A : Matrix m n R), A.cRank = 1
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pushforward_def : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A)
  [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E] [inst_12 : IsTopologicalGroup C]
  [inst_13 : LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E) (c : C),
  ((H.pushforward μA) f) c = ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- If
```
(f 0)
(0 g)
```
is invertible, then `g` is invertible.
 -/
CategoryTheory.isIso_right_of_isIso_biprod_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
  [CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)], CategoryTheory.IsIso g
-- Mathlib.RingTheory.Ideal.Span
/-- A ring is a principal ideal ring if all (left) ideals are principal.  -/
IsPrincipalIdealRing : (R : Type u) → [Semiring R] → Prop
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.toPreOneHypercover_I₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (x x_1 : E.I₀), E.toPreOneHypercover.I₁ x x_1 = PUnit.{u_2 + 1}
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.trans : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w u : AbsoluteValue R S}, v.IsEquiv w → w.IsEquiv u → v.IsEquiv u
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.currySum_apply_inl_inr : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X) (p : ↑(GenLoop (M ⊕ N) X x))
  (y : M ⊕ N → ↑unitInterval), ((GenLoop.currySum x p) (y ∘ Sum.inl)) (y ∘ Sum.inr) = p y
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {c : ℕ}, m.WF → (m.Equiv (Std.HashMap.Raw.emptyWithCapacity c) ↔ m.isEmpty = true)
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The abelianization-forgetful adjunction from `Group` to `CommGroup`.  -/
GrpCat.abelianizeAdj : GrpCat.abelianize ⊣ CategoryTheory.forget₂ CommGrpCat GrpCat
-- Init.Prelude
/-- Implementation of `TSyntaxArray.mk`.  -/
Lean.TSyntaxArray.mkImpl : {ks : Lean.SyntaxNodeKinds} → Array Lean.Syntax → Lean.TSyntaxArray ks
-- Mathlib.Topology.Constructions
interior_pi_set : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {I : Set ι},
  I.Finite → ∀ {s : (i : ι) → Set (A i)}, interior (I.pi s) = I.pi fun i => interior (s i)
-- Std.Http.Protocol.H1
/-- Direction-dispatched message-head validation.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.checkMessageHead : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Message.Head dir → Except Std.Http.Protocol.H1.Error Std.Http.Protocol.H1.Machine.BodyMode✝
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.ext_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {E F : Topology.RelCWComplex.Subcomplex C}, E = F ↔ ∀ (x : X), x ∈ E ↔ x ∈ F
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.div_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (x / a)) (c * a)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_add : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ_[p]), ↑(z1 + z2) = ↑z1 + ↑z2
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Any linear map on a finite-dimensional space over a complete field is continuous.  -/
LinearMap.continuous_of_finiteDimensional : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [inst_5 : AddCommGroup F']
  [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [IsTopologicalAddGroup F'] [ContinuousSMul 𝕜 F']
  [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F'), Continuous ⇑f
-- Mathlib.Order.Hom.Basic
OrderEmbedding.coe_id : ∀ {α : Type u_2} [inst : LE α], ⇑(OrderEmbedding.id α) = id
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.ofLinearEquiv_toSolution : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (pres : Module.Presentation A M) {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (e : M ≃ₗ[A] N),
  (pres.ofLinearEquiv e).toSolution = pres.postcomp ↑e
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.List.alternatingSum.match_1.eq_3 : ∀ {G : Type u_1} (motive : List G → Sort u_2) (g h : G) (t : List G) (h_1 : Unit → motive [])
  (h_2 : (g : G) → motive [g]) (h_3 : (g h : G) → (t : List G) → motive (g :: h :: t)),
  (match g :: h :: t with
    | [] => h_1 ()
    | [g] => h_2 g
    | g :: h :: t => h_3 g h t) =
    h_3 g h t
-- Std.Http.Data.Body.Empty
/-- Builds a response with no body.
 -/
Std.Http.Response.Builder.empty : Std.Http.Response.Builder → Std.Async.Async (Std.Http.Response Std.Http.Body.Empty)
-- Lean.Parser.Extra
Lean.Parser.ppDedentIfGrouped.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.mkNatTrans.congr_simp : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor V.HomotopyCategory D}
  (φ φ_1 :
    (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })) →
      F.obj (SSet.Truncated.HomotopyCategory.mk x) ⟶ G.obj (SSet.Truncated.HomotopyCategory.mk x))
  (e_φ : φ = φ_1)
  (hφ :
    ∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
      (e : SSet.Truncated.Edge x y),
      CategoryTheory.CategoryStruct.comp (F.map (SSet.Truncated.HomotopyCategory.homMk e)) (φ y) =
        CategoryTheory.CategoryStruct.comp (φ x) (G.map (SSet.Truncated.HomotopyCategory.homMk e))),
  SSet.Truncated.HomotopyCategory.mkNatTrans φ hφ = SSet.Truncated.HomotopyCategory.mkNatTrans φ_1 ⋯
-- Mathlib.Data.Set.Image
Set.range_sdiff_image_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.range f \ f '' s ⊆ f '' sᶜ
-- Mathlib.Order.CompleteLattice.Basic
iSup_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_8} {f : β → γ} {g : γ → α} {t : Set β},
  ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.get! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → [Std.LawfulEqCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → [Inhabited (β a)] → β a
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.continuous_toPOUFun : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι),
  Continuous (f.toPOUFun i)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.fixpoint : Unit → Lean.Elab.Term.MutualClosure.FixPoint.M Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  (Std.DHashMap.filterMap f m).isEmpty = false ↔
    ∃ k, ∃ (h : k ∈ m), (f (m.getKey k h) (Std.DHashMap.Const.get m k h)).isSome = true
-- Aesop.Forward.SlotIndex
Aesop.instInhabitedSlotIndex : Inhabited Aesop.SlotIndex
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreCompInclusionIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : CategoryTheory.Core C),
  F.coreCompInclusionIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X.of)
-- Mathlib.Topology.Order.Basic
exists_Ico_subset_of_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  s ∈ nhds a → (∃ l, a < l) → ∃ l, a < l ∧ Set.Ico a l ⊆ s
-- Lean.Linter.Util
_private.Lean.Linter.Util.0.Lean.Linter.collectMacroExpansions?.go : {m : Type → Type u_1} →
  [Monad m] → Lean.Syntax.Range → Lean.Elab.InfoTree → m (Option (Option (List Lean.Elab.MacroExpansionInfo)))
-- Mathlib.GroupTheory.GroupAction.Pointwise
image_smul_setₛₗ : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : SMul M α]
  [inst_1 : SMul N β] [inst_2 : FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : M) (s : Set α),
  ⇑f '' (c • s) = σ c • ⇑f '' s
-- Aesop.Tree.Data
Aesop.RappId : Type
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.Quasicategory₂.fill32 : ∀ {X : SSet.Truncated 2} [self : X.Quasicategory₂]
  {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₂₃ : SSet.Truncated.Edge x₂ x₃}
  {e₀₂ : SSet.Truncated.Edge x₀ x₂} {e₁₃ : SSet.Truncated.Edge x₁ x₃} {e₀₃ : SSet.Truncated.Edge x₀ x₃}
  (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃),
  Nonempty (e₀₁.CompStruct e₁₃ e₀₃)
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
trailing coefficient of `f₁ + f₂` at `x` is the sum of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_add_eq_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x →
        meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0 →
          meromorphicTrailingCoeffAt (fun z => f₁ z + f₂ z) x =
            meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_coe_orderAddMonoidHom : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), ⇑↑f = ⇑f
-- Init.PropLemmas
ne_of_mem_of_not_mem' : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s t : β} {a : α}, a ∈ s → a ∉ t → s ≠ t
-- Mathlib.SetTheory.Ordinal.Rank
Acc.mem_range_rank_of_le : ∀ {α : Type u} {a : α} {r : α → α → Prop} {o : Ordinal.{u}} (ha : Acc r a),
  o ≤ ha.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
-- Mathlib.Data.List.Forall2
List.rel_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop},
  Relator.LiftFun (Relator.LiftFun R (Option.Rel P)) (Relator.LiftFun (List.Forall₂ R) (List.Forall₂ P)) List.filterMap
    List.filterMap
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3],
  W.twoTorsionPolynomial = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a fallback : α}, (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ofList_cons : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} {v : β} {tl : List (α × β)},
  Std.TreeMap.ofList ((k, v) :: tl) cmp = (∅.insert k v).insertMany tl
-- Init.Data.Array.Sort.Lemmas
/-- This merge sort algorithm is stable,
in the sense that breaking ties in the ordering function using the position in the array
has no effect on the output.

That is, elements which are equal with respect to the ordering function will remain
in the same order in the output array as they were in the input array.

See also:
* `sublist_mergeSort`: if `c <+ l` and `c.Pairwise le`, then `c <+ (mergeSort le l).toList`.
* `pair_sublist_mergeSort`: if `[a, b] <+ l` and `le a b`, then `[a, b] <+ (mergeSort le l).toList`)
 -/
Array.mergeSort_zipIdx : ∀ {α : Type u_1} {le : α → α → Bool} {xs : Array α},
  Array.map (fun x => x.1)
      ((Array.map
            (fun x =>
              match x with
              | (a, i) => (a, i))
            xs.zipIdx).mergeSort
        (List.zipIdxLE le)) =
    xs.mergeSort le
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function is even.
 -/
ValueDistribution.logCounting_even : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {e : WithTop E},
  Function.Even (ValueDistribution.logCounting f e)
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex : ∀ {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.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
  {K₁ L₁ : CochainComplex C₁ ℤ} (f : K₁ ⟶ L₁), CategoryTheory.NatTrans.CommShift (F.map₂CochainComplex.map f) ℤ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ)
  {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y),
  ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.obj F).map f = ((Opposite.unop F).map f.unop).op
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.mk.inj : ∀ {S : Type u_1} {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S}
  {X Y : CategoryTheory.DifferentialObject S C} {f : X.obj ⟶ Y.obj}
  {comm :
    autoParam
      (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) =
        CategoryTheory.CategoryStruct.comp f Y.d)
      CategoryTheory.DifferentialObject.Hom.comm._autoParam}
  {f_1 : X.obj ⟶ Y.obj}
  {comm_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f_1) =
        CategoryTheory.CategoryStruct.comp f_1 Y.d)
      CategoryTheory.DifferentialObject.Hom.comm._autoParam},
  { f := f, comm := comm } = { f := f_1, comm := comm_1 } → f = f_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k fallback : α}, k ∈ t → t.getKeyD k fallback = k
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.polar_ball_subset_closedBall_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜},
  1 < ‖c‖ → ∀ {r : ℝ}, 0 < r → StrongDual.polar 𝕜 (Metric.ball 0 r) ⊆ Metric.closedBall 0 (‖c‖ / r)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- The refinement morphism of the lifted cover.  -/
AlgebraicGeometry.QuasiCompactCover.uliftHom : {S : AlgebraicGeometry.Scheme} →
  (𝒰 : CategoryTheory.PreZeroHypercover S) →
    [inst : AlgebraicGeometry.QuasiCompactCover 𝒰] → (AlgebraicGeometry.QuasiCompactCover.ulift 𝒰).Hom 𝒰
-- Mathlib.NumberTheory.Divisors
Nat.mem_divisors_prime_pow : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ) {x : ℕ}, x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j
-- Mathlib.Order.Category.Lat
Lat_dual_comp_forget_to_partOrd : Lat.dual.comp (CategoryTheory.forget₂ Lat PartOrd) = (CategoryTheory.forget₂ Lat PartOrd).comp PartOrd.dual
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
/-- The complex arctangent, defined via the complex logarithm.  -/
Complex.arctan : ℂ → ℂ
-- Mathlib.RingTheory.Localization.Integral
/-- If the `S`-multiples of `a` are contained in some `R`-span, then `Frac(S)`-multiples of `a`
are contained in the equivalent `Frac(R)`-span.  -/
IsFractionRing.ideal_span_singleton_map_subset : ∀ (R : Type u_1) [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {K : Type u_4}
  {L : Type u_5} [IsDomain R] [IsDomain S] [inst_5 : Field K] [inst_6 : Field L] [inst_7 : Algebra R K]
  [inst_8 : Algebra R L] [inst_9 : Algebra S L] [Algebra.IsAlgebraic R S] [IsFractionRing S L] [inst_12 : Algebra K L]
  [IsScalarTower R S L] [IsScalarTower R K L] {a : S} {b : Set S},
  Function.Injective ⇑(algebraMap R L) →
    ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b) →
      ↑(Ideal.span {(algebraMap S L) a}) ⊆ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofMultiset_apply : ∀ {R : Type u} [inst : CommRing R] (s : Multiset R),
  Polynomial.ofMultiset s = (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod
-- Init.Data.Nat.Basic
Nat.le_zero : ∀ {i : ℕ}, i ≤ 0 ↔ i = 0
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_span_singleton : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (g : M),
  (R ∙ g).annihilator = (LinearMap.toSpanSingleton R M g).ker
-- Init.Notation
Lean.instCoeOutTSyntaxSyntax : {ks : Lean.SyntaxNodeKinds} → CoeOut (Lean.TSyntax ks) Lean.Syntax
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.injective : ∀ {𝕜 : 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),
  Function.Injective ↑I
-- Mathlib.Order.IsNormal
Order.IsNormal.map_sSup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLinearOrder β],
  Order.IsNormal f → ∀ {s : Set α}, s.Nonempty → BddAbove s → f (sSup s) = sSup (f '' s)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.op : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → α}, Summable f L → Summable (MulOpposite.op ∘ f) L
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.tr.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (q : Λ),
  Turing.TM0to1.tr M (Turing.TM0to1.Λ'.normal q) =
    Turing.TM1.Stmt.branch (fun a x => (M q a).isNone) Turing.TM1.Stmt.halt
      (Turing.TM1.Stmt.goto fun a x =>
        match M q a with
        | none => default
        | some (q', s) => Turing.TM0to1.Λ'.act s q')
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg' : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A] [CStarRing A]
  [inst_4 : NormedSpace ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A} (b : A),
  autoParam (IsSelfAdjoint b) CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg'._auto_1 →
    autoParam (0 ≤ a) CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg'._auto_3 → ‖b * a * b‖ = ‖b * CFC.sqrt a‖ ^ 2
-- Mathlib.Computability.DFA
DFA.accepts_union : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2), (M1.union M2).accepts = M1.accepts + M2.accepts
-- Mathlib.Data.Nat.PrimeFin
/-- The only prime divisor of positive prime power `p^k` is `p` itself  -/
Nat.primeFactors_prime_pow : ∀ {k p : ℕ}, k ≠ 0 → Nat.Prime p → (p ^ k).primeFactors = {p}
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.coe_of : ∀ (R : Type u) [inst : CommRing R], ↑(CommRingCat.of R) = R