mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value is nonarchimedean  -/
IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b), IsNonarchimedean ⇑(v.adicAbv hb)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The negation of a linear map is linear.  -/
LinearMap.instNeg : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {N₂ : Type u_12} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommGroup N₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ N₂] → {σ₁₂ : R₁ →+* R₂} → Neg (M →ₛₗ[σ₁₂] N₂)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Option.isSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (val : α) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Lean.Language.Basic
Lean.Language.Snapshot.instInhabitedDiagnostics.default : Lean.Language.Snapshot.Diagnostics
-- Mathlib.Analysis.Normed.Group.Hom
/-- The function underlying a `NormedAddGroupHom`  -/
NormedAddGroupHom.toFun : {V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] → [inst_1 : SeminormedAddCommGroup W] → NormedAddGroupHom V W → V → W
-- Mathlib.Data.Finset.Card
Finset.card_filter_le : ∀ {α : Type u_1} (s : Finset α) (p : α → Prop) [inst : DecidablePred p], (Finset.filter p s).card ≤ s.card
-- Mathlib.Data.Seq.Computation
Computation.length_thinkN : ∀ {α : Type u} (s : Computation α) [_h : s.Terminates] (n : ℕ), (s.thinkN n).length = s.length + n
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Reinterpret an `AffineIsometryEquiv` as a `Homeomorph`.  -/
AffineIsometryEquiv.toHomeomorph : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P ≃ᵃⁱ[𝕜] P₂) → P ≃ₜ P₂
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.natGenerator.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  (v : IsDedekindDomain.HeightOneSpectrum R),
  Rat.HeightOneSpectrum.natGenerator v =
    (Submodule.IsPrincipal.generator (Ideal.map (Rat.IsIntegralClosure.intEquiv R) v.asIdeal)).natAbs
-- Mathlib.Data.Set.Basic
Set.inter_subset_right : ∀ {α : Type u} {s t : Set α}, s ∩ t ⊆ t
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a * x) ⁻¹' Set.Icc b c = Set.Icc (b / a) (c / a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_le_nsmul_iff_left : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] {a : M} {m n : ℕ},
  0 < a → (m • a ≤ n • a ↔ m ≤ n)
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumCompl_symm_apply_compl : ∀ {α : Type u_3} {s : Set α} [inst : DecidablePred fun x => x ∈ s] (x : ↑sᶜ), (Equiv.Set.sumCompl s).symm ↑x = Sum.inr x
-- Mathlib.Analysis.Convex.Slope
/-- If `f` is convex on a set `s` in a linearly ordered field, and `f y < f x` for two points
`x < y` in `s`, then `f` is strictly antitone on `s ∩ (∞, x]`.  -/
ConvexOn.strictAntiOn : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f → ∀ {x y : 𝕜}, y ∈ s → x < y → f y < f x → StrictAntiOn f (s ∩ Set.Iic x)
-- Init.Data.BitVec.Lemmas
BitVec.one_eq_zero_iff : ∀ {w : ℕ}, 1#w = 0#w ↔ w = 0
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_P : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  (D₁ D₂ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) (a : J),
  (D₁.sup D₂).P a = (D₁.P ⊔ D₂.P) a
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `p` is prime, then `J(a | p)` is `-1` iff `a` is not a square modulo `p`.  -/
ZMod.nonsquare_iff_jacobiSym_eq_neg_one : ∀ {a : ℤ} {p : ℕ} [inst : Fact (Nat.Prime p)], jacobiSym a p = -1 ↔ ¬IsSquare ↑a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_toArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp},
  t₁.Equiv t₂ ↔ (Std.DTreeMap.Raw.Const.toArray t₁).Perm (Std.DTreeMap.Raw.Const.toArray t₂)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.interSnd_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (x : (E.inter F).I₀),
  (E.interSnd F).h₀ x =
    CategoryTheory.Limits.pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x).fst)
      (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x).snd)
-- Mathlib.CategoryTheory.Action.Concrete
Action.FintypeCat.quotientToQuotientOfLE_hom_mk : ∀ {G : Type u_1} [inst : Group G] (H N : Subgroup G) [inst_1 : Fintype (G ⧸ N)] [inst_2 : Fintype (G ⧸ H)] (h : N ≤ H)
  (x : G), (CategoryTheory.ConcreteCategory.hom (Action.FintypeCat.quotientToQuotientOfLE H N h).hom) ⟦x⟧ = ⟦x⟧
-- Init.Data.Iterators.PostconditionMonad
/-- The actual monadic operation. Its return value is bundled together with a proof that
it satisfies `Property`.
 -/
Std.Iterators.PostconditionT.operation : {m : Type w → Type w'} → {α : Type w} → (self : Std.Iterators.PostconditionT m α) → m (Subtype self.Property)
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.explainStuckTypeclassProblem : Lean.Expr → Lean.Elab.TermElabM (Option Lean.MessageData)
-- Mathlib.Order.Category.BddLat
_private.Mathlib.Order.Category.BddLat.0.BddLat.Hom.mk.inj : ∀ {X Y : BddLat} {hom' hom'_1 : BoundedLatticeHom ↑X.toLat ↑Y.toLat},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Topology.Category.Profinite.CofilteredLimit
LocallyConstant.unflip.congr_simp : ∀ {X : Type u_5} {α : Type u_6} {β : Type u_7} [inst : Finite α] [inst_1 : TopologicalSpace X]
  (f f_1 : α → LocallyConstant X β), f = f_1 → LocallyConstant.unflip f = LocallyConstant.unflip f_1
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.cast.congr_simp : ∀ {n m : ℕ} (c c_1 : Composition m), c = c_1 → ∀ (hmn : m = n), c.cast hmn = c_1.cast hmn
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp_id_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A.X A.X))
      CategoryTheory.MonObj.mul
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_perm_eq_self_power : ∀ {α : Type u} [Infinite α], Cardinal.mk (Equiv.Perm α) = Cardinal.mk α ^ Cardinal.mk α
-- Mathlib.LinearAlgebra.Lagrange
/-- Lagrange interpolation: given a finset `s : Finset ι`, a nodal map `v : ι → F` injective on
`s` and a value function `r : ι → F`, `interpolate s v r` is the unique
polynomial of degree `< #s` that takes value `r i` on `v i` for all `i` in `s`.  -/
Lagrange.interpolate : {F : Type u_1} → [inst : Field F] → {ι : Type u_2} → [DecidableEq ι] → Finset ι → (ι → F) → (ι → F) →ₗ[F] Polynomial F
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_dirac : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {x : X} {v : V},
  (MeasureTheory.VectorMeasure.dirac x v).variation = ‖v‖ₑ • MeasureTheory.Measure.dirac x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (i : ι), DFinsupp.erase i 0 = 0
-- Mathlib.Data.List.Basic
List.filterMap_none : ∀ {α : Type u} {β : Type v} (l : List α), List.filterMap (fun x => none) l = []
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ : ι}
  (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₁ n₂ n₃ : ℤ),
  autoParam ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0)
      CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃._auto_1 →
    ∀ (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃._auto_3)
      (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃._auto_5),
      CategoryTheory.IsIso
        (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)
-- Mathlib.RepresentationTheory.Homological.Resolution
CategoryTheory.SimplicialObject.augment.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C)
  (f : X.obj (Opposite.op { len := 0 }) ⟶ X₀)
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f),
  X.augment X₀ f w =
    { left := X, right := X₀,
      hom :=
        { app := fun x => CategoryTheory.CategoryStruct.comp (X.map ({ len := 0 }.const (Opposite.unop x) 0).op) f,
          naturality := ⋯ } }
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₂_inv_comp_iCocycles : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).inv (groupCohomology.iCocycles A 2) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.i
      (groupCohomology.cochainsIso₂ A).inv
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.eq_restrict_removeLoops : ∀ {α : Type u_1} (M : Matroid α), M.removeLoops.restrict M.E = M
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : A ⟶ B)
  [CategoryTheory.IsIso η], CategoryTheory.Limits.IsIndObject A → CategoryTheory.Limits.IsIndObject B
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.get' : Lean.Meta.Grind.GoalM Lean.Meta.Grind.Arith.Cutsat.State
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.subset_bipolar : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  s ⊆ B.flip.polar (B.polar s)
-- Init.Data.List.Nat.Range
List.fst_eq_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {l : List α} {k : ℕ} (h : x ∈ l.zipIdx k), x.1 = l[x.2 - k]
-- Mathlib.Order.Category.DistLat
DistLat.dualEquiv_functor : DistLat.dualEquiv.functor = DistLat.dual
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.State.mk : List Lean.MVarId → Lean.Elab.Tactic.State
-- Mathlib.Order.Heyting.Hom
BiheytingHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
  [inst_2 : FunLike F α β] [toLatticeHomClass : LatticeHomClass F α β],
  (∀ (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b) → (∀ (f : F) (a b : α), f (a \ b) = f a \ f b) → BiheytingHomClass F α β
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData.userName : ProofWidgets.ExprPresentationData → String
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_eq_encard_iff_encard_sdiff_eq_encard_sdiff`. -/
Set.encard_eq_encard_iff_encard_diff_eq_encard_diff : ∀ {α : Type u_1} {s t : Set α}, (s ∩ t).Finite → (s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of an additive monoid homomorphism
`Mᵃᵒᵖ →+ Nᵃᵒᵖ`. Inverse to `AddMonoidHom.op`.  -/
AddMonoidHom.unop : {M : Type u_3} → {N : Type u_4} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (Mᵃᵒᵖ →+ Nᵃᵒᵖ) ≃ (M →+ N)
-- Mathlib.Algebra.Order.Floor.Div
FloorDiv.mk : {α : Type u_2} →
  {β : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : PartialOrder α] →
        [inst_2 : AddCommMonoid β] →
          [inst_3 : PartialOrder β] →
            [inst_4 : SMulZeroClass α β] →
              (floorDiv : β → α → β) →
                (∀ ⦃a : α⦄, 0 < a → GaloisConnection (fun x => a • x) fun x => floorDiv x a) →
                  (∀ ⦃a : α⦄, a ≤ 0 → ∀ (b : β), floorDiv b a = 0) → (∀ (a : α), floorDiv 0 a = 0) → FloorDiv α β
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fmod.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc m, Int.ofNat n => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_4 m n
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.msgSent : Std.Internal.UV.System.RUsage → UInt64
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.tryCasesS.getUnusedCtorNames : Array Aesop.CtorNames → Lean.LocalContext → Array Aesop.CtorNames
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.domRestrict_ofUnitHom : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_3} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ)
  (S : Submonoid R),
  MulChar.domRestrict S (MulChar.ofUnitHom f) =
    MulChar.ofUnitHom ((f.domRestrict S.units).comp ↑S.unitsEquivUnitsType.symm)
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, the closure of a finite set is a compact set.  -/
Set.Finite.isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] {s : Set X}, s.Finite → IsCompact (closure s)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A variant of `Sieve.functor` with universe lifting.  -/
CategoryTheory.Sieve.uliftFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Sieve X → CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))
-- Mathlib.Order.Monotone.Monovary
antivary_toDual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Antivary (⇑OrderDual.toDual ∘ f) g ↔ Monovary f g
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {V : (x : M') → TangentSpace I' x} {c : 𝕜},
  VectorField.mpullbackWithin I I' f (c • V) s = c • VectorField.mpullbackWithin I I' f V s
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instHasZeroObject : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V],
  CategoryTheory.Limits.HasZeroObject (HomologicalComplex V c)
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.hasDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜}, HasDerivAt (⇑f) (f.linear 1) x
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Given two bundle trivializations `e`, `e'` over disjoint sets, `e.disjoint_union e' H` is the
bundle trivialization over the union of the base sets that agrees with `e` and `e'` over their
base sets.  -/
Bundle.Trivialization.disjointUnion : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              (e e' : Bundle.Trivialization F proj) → Disjoint e.baseSet e'.baseSet → Bundle.Trivialization F proj
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rii_eq_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α}, Std.Rii.Sliceable.mkSlice xs *...* = Std.Rci.Sliceable.mkSlice xs 0...*
-- Lean.Expr
Lean.instHashableLiteral : Hashable Lean.Literal
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.isIntegral_iff : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K),
  WeierstrassCurve.IsIntegral R W ↔ ∃ W_int, W = W_int.baseChange K
-- Mathlib.Data.Nat.EvenOddRec
/-- Strong recursion principle on even and odd numbers: if for all `i : ℕ` we can prove `P (2 * i)`
from `P j` for all `j < 2 * i` and we can prove `P (2 * i + 1)` from `P j` for all `j < 2 * i + 1`,
then we have `P n` for all `n : ℕ`.  -/
Nat.evenOddStrongRec : {P : ℕ → Sort u_1} →
  ((n : ℕ) → ((k : ℕ) → k < 2 * n → P k) → P (2 * n)) →
    ((n : ℕ) → ((k : ℕ) → k < 2 * n + 1 → P k) → P (2 * n + 1)) → (n : ℕ) → P n
-- Mathlib.Order.Interval.Set.Defs
/-- `Ioo a b` is the left-open right-open interval $(a, b)$.  -/
Set.Ioo : {α : Type u_1} → [Preorder α] → α → α → Set α
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E], Dense ↑T.domain → T.graph.adjoint.toLinearPMap = T.adjoint
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
          (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
            (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i)
            (CategoryTheory.CategoryStruct.comp g i))
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h
-- Mathlib.Topology.Separation.Profinite
/-- A totally disconnected compact Hausdorff space is totally separated.  -/
instTotallySeparatedSpaceOfTotallyDisconnectedSpace : ∀ {H : Type u_3} [inst : TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
  TotallySeparatedSpace H
-- Batteries.Recycling.RBTree.Alter
/-- Asserts that property `p` holds on the root of the tree, if any.  -/
RBTree.RBNode.OnRoot : {α : Type u_1} → (α → Prop) → RBTree.RBNode α → Prop
-- Init.Data.BitVec.Basic
/-- Count the number of bits with value `1` downward from the `pos`-th bit to the
`0`-th bit of `x`, storing the result in `acc`.  -/
BitVec.cpopNatRec : {w : ℕ} → BitVec w → ℕ → ℕ → ℕ
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_mul_transpose_apply_of_adj : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : Fintype (Sym2 α)] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] [inst_3 : Semiring R] {a b : α},
  G.Adj a b → (SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G).transpose) a b = 1
-- Lean.Elab.DocString
/-- Built-in docstring commands, for bootstrapping.
 -/
Lean.Doc.builtinDocCommands : IO.Ref (Lean.NameMap (Array (Lean.Name × Lean.Doc.DocCommandExpander)))
-- Std.Data.DHashMap.Basic
/-- Compares two hash maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DHashMap.beq : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [LawfulBEq α] → [(k : α) → BEq (β k)] → Std.DHashMap α β → Std.DHashMap α β → Bool
-- Lean.DeclarationRange
Lean.declRangeExt : Lean.MapDeclarationExtension Lean.DeclarationRanges
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_bind_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t.min?.bind t.get? = t.min?
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mem_genEigenspace_nat : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ} {x : M}, x ∈ (f.genEigenspace μ) ↑k ↔ x ∈ ((f - μ • 1) ^ k).ker
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instOrderBot : {α : Type u_1} → [inst : TopologicalSpace α] → OrderBot (TopologicalSpace.Compacts α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.map_injective : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Affine R} [inst_4 : DecidableEq F] [inst_5 : DecidableEq K]
  [inst_6 : Algebra R S] [inst_7 : Algebra R F] [inst_8 : Algebra S F] [inst_9 : IsScalarTower R S F]
  [inst_10 : Algebra R K] [inst_11 : Algebra S K] [inst_12 : IsScalarTower R S K] (f : F →ₐ[S] K),
  Function.Injective ⇑(WeierstrassCurve.Affine.Point.map f)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.linkAux.eq_1 : ∀ (self : Array Batteries.UFNode) (x y : Fin self.size),
  Batteries.UnionFind.linkAux self x y =
    if ↑x = ↑y then self
    else
      let nx := self[↑x];
      have ny := self[↑y];
      if ny.rank < nx.rank then self.set ↑y { parent := ↑x, rank := ny.rank } ⋯
      else
        let arr₁ := self.set ↑x { parent := ↑y, rank := nx.rank } ⋯;
        if nx.rank = ny.rank then arr₁.set ↑y { parent := ny.parent, rank := ny.rank + 1 } ⋯ else arr₁