mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- Similar to `colimit` and `colim`, taking fiberwise colimits is a functor
`(Grothendieck F ⥤ H) ⥤ (C ⥤ H)` between functor categories.  -/
CategoryTheory.Limits.fiberwiseColim : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C CategoryTheory.Cat) →
      (H : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] →
            CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
              (CategoryTheory.Functor C H)
-- Mathlib.RingTheory.Ideal.Int
Int.cast_mem_ideal_iff : ∀ {R : Type u_1} [inst : Ring R] {I : Ideal R} {d : ℤ}, ↑d ∈ I ↔ ↑(Ideal.absNorm (Ideal.under ℤ I)) ∣ d
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.finSigmaFinEquiv.match_1.eq_2 : ∀ (motive : (m : ℕ) → {n : Fin m → ℕ} → Sort u_1) (m : ℕ) (n : Fin m.succ → ℕ) (h_1 : (n : Fin 0 → ℕ) → motive 0)
  (h_2 : (m : ℕ) → (n : Fin m.succ → ℕ) → motive m.succ),
  (match m.succ, n with
    | 0, n => h_1 n
    | m.succ, n => h_2 m n) =
    h_2 m n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_le_size_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t.size ≤ (t.insert k v).size
-- Mathlib.Tactic.Positivity.Core
/-- Each `positivity` extension is labelled with a collection of patterns
which determine the expressions to which it should be applied.  -/
Mathlib.Meta.Positivity.Entry : Type
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Prop.instMeasurableSpace : MeasurableSpace Prop
-- Mathlib.Data.Finset.Card
/-- Specialization of `Finset.card_nbij'` that automatically fills in most arguments.

See `Fintype.card_equiv` for the version where `s` and `t` are `univ`.  -/
Finset.card_equiv : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (e : α ≃ β),
  (∀ (i : α), i ∈ s ↔ e i ∈ t) → s.card = t.card
-- Mathlib.Algebra.DirectSum.Basic
/-- Coercion from a `DirectSum` to a pi type is an `AddMonoidHom`.  -/
DirectSum.coeFnAddMonoidHom : {ι : Type v} → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → (DirectSum ι fun i => β i) →+ (i : ι) → β i
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.infinite_not_isOfFinOrder : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {x : G}, ¬IsOfFinOrder x → {y | ¬IsOfFinOrder y}.Infinite
-- Mathlib.Topology.ContinuousMap.Polynomial
polynomialFunctions.le_equalizer : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] {A : Type u_2}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (s : Set R) (φ ψ : C(↑s, R) →ₐ[R] A),
  φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
    polynomialFunctions s ≤ φ.equalizer ψ
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.toRingEquiv_uniqueAlgEquiv : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : Unique M], ↑(MonoidAlgebra.uniqueAlgEquiv R M) = MonoidAlgebra.uniqueRingEquiv M
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₂_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.ShortComplex.SnakeInput.functorL₂.obj S = S.L₂
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- Recursion formula for the coefficients of the hypergeometric series.

This is mainly used to calculate the convergence radius.  -/
Complex.regularizedHGFunCoeff_add_one_div_self : ∀ {a b : Multiset ℂ} {n : ℕ},
  Complex.regularizedHGFunCoeff a b n ≠ 0 →
    Complex.regularizedHGFunCoeff a b (n + 1) / Complex.regularizedHGFunCoeff a b n =
      (Multiset.map (fun x => x + ↑n) a).prod / ((Multiset.map (fun x => x + ↑n) b).prod * (↑n + 1))
-- Mathlib.Data.Fin.Tuple.Curry
/-- `Equiv.curry` for `p`-ary heterogeneous functions.  -/
Function.FromTypes.curryEquiv : {n : ℕ} → {τ : Type u} → (p : Fin n → Type u) → (((i : Fin n) → p i) → τ) ≃ Function.FromTypes p τ
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
algebraicIndependent_of_set_of_finite : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (s : Set ι),
  (AlgebraicIndependent R fun i => x ↑i) →
    (∀ (t : Set ι),
        t.Finite →
          (AlgebraicIndependent R fun i => x ↑i) →
            ∀ i ∉ s, i ∉ t → Transcendental (↥(Algebra.adjoin R (x '' t))) (x i)) →
      AlgebraicIndependent R x
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The associativity axiom associated to an algebra.  -/
CategoryTheory.Monad.Algebra.assoc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) {Z : C}
  (h : self.A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T.μ.app self.A) (CategoryTheory.CategoryStruct.comp self.a h) =
    CategoryTheory.CategoryStruct.comp (T.map self.a) (CategoryTheory.CategoryStruct.comp self.a h)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.natCast_def : ∀ (R : Type u_1) {N₁ : Type u_8} [inst : Semiring R] (n : ℕ) [inst_1 : AddCommMonoid N₁] [inst_2 : Module R N₁],
  ↑n = (Module.toModuleEnd R N₁) n
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.size.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.size✝ x =
    match x with
    | Std.DTreeMap.Internal.Zipper.done => 0
    | Std.DTreeMap.Internal.Zipper.cons k v tree next => 1 + tree.treeSize + Std.DTreeMap.Internal.Zipper.size✝ next
-- Mathlib.Data.Num.ZNum
Num.div.eq_2 : ∀ (x : Num), (x = Num.zero → False) → x.div Num.zero = 0
-- Init.Prelude
/-- A byte position in a `String`, according to its UTF-8 encoding.

Character positions (counting the Unicode code points rather than bytes) are represented by plain
`Nat`s. Indexing a `String` by a `String.Pos.Raw` takes constant time, while character positions need to
be translated internally to byte positions, which takes linear time.

A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.rawEndPos` and `p` lies on a UTF-8
character boundary, see `String.Pos.IsValid`.

There is another type, `String.Pos`, which bundles the validity predicate. Using `String.Pos`
instead of `String.Pos.Raw` is recommended because it will lead to less error handling and fewer edge cases.
 -/
String.Pos.Raw : Type
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.toFinsuppAntidiag_injective : ∀ (n : ℕ), Function.Injective Nat.Partition.toFinsuppAntidiag
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces.saveLine.eq_def : ∀ (n : ℕ) {s : String} (it : s.Pos) (r : String),
  String.removeNumLeadingSpaces.saveLine✝ n it r =
    if h : it.IsAtEnd then r
    else
      if (it.get h == '\n') = true then String.removeNumLeadingSpaces.consumeSpaces✝ n n (it.next h) (r.push '\n')
      else String.removeNumLeadingSpaces.saveLine✝ n (it.next h) (r.push (it.get h))
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineIsometry.coe_toAffineIsometryEquiv : ∀ {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : NormedAddCommGroup V₁] [inst_2 : SeminormedAddCommGroup V₂] [inst_3 : NormedSpace 𝕜 V₁]
  [inst_4 : NormedSpace 𝕜 V₂] [inst_5 : MetricSpace P₁] [inst_6 : PseudoMetricSpace P₂] [inst_7 : NormedAddTorsor V₁ P₁]
  [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : FiniteDimensional 𝕜 V₁] [inst_10 : FiniteDimensional 𝕜 V₂]
  [inst_11 : Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : Module.finrank 𝕜 V₁ = Module.finrank 𝕜 V₂),
  ⇑(li.toAffineIsometryEquiv h) = ⇑li
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
borel.eq_1 : ∀ (α : Type u) [inst : TopologicalSpace α], borel α = MeasurableSpace.generateFrom {s | IsOpen s}
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.adjoin_rootSet : ∀ (n : ℕ) {K : Type u} [inst : Field K] (f : Polynomial K),
  f.natDegree = n → Algebra.adjoin K (f.rootSet (Polynomial.SplittingFieldAux n f)) = ⊤
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.extendDomain_symm : ∀ {α' : Type u_9} {β' : Type u_10} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p),
  Equiv.symm (e.extendDomain f) = Equiv.Perm.extendDomain (Equiv.symm e) f
-- Init.Data.Option.Lemmas
Option.get_join : ∀ {α : Type u_1} {x : Option (Option α)} {h : x.join.isSome = true}, x.join.get h = (x.get ⋯).get ⋯
-- Mathlib.Order.Bounds.Basic
/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` such that `x`
is not less than or equal to `y`. This version only assumes `Preorder` structure and uses
`¬(x ≤ y)`. A version for linear orders is called `not_bddBelow_iff`.  -/
not_bddBelow_iff' : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, ¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, ¬x ≤ y
-- Mathlib.Order.Fin.Basic
Fin.orderIsoSubtype_apply : ∀ {n : ℕ} (a : Fin n), Fin.orderIsoSubtype a = ⟨↑a, ⋯⟩
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- A chosen right Kan extension when `[HasRightKanExtension L F]` holds.  -/
CategoryTheory.Functor.rightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) → [L.HasRightKanExtension F] → CategoryTheory.Functor D H
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.eraseSimprocAttr : Lean.Meta.Simp.SimprocExtension → Lean.Name → Lean.AttrM Unit
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- Given a family of maps `f : K → (j ⟶ j')` in a `κ`-filtered category `J`,
with `HasCardinalLT K κ`, this is a morphism `j ⟶ coeq f hK` which is equal
to all compositions `f k ≫ coeqHom f hK` for `k : K`.  -/
CategoryTheory.IsCardinalFiltered.toCoeq : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [inst_1 : CategoryTheory.IsCardinalFiltered J κ] →
          {K : Type v'} →
            {j j' : J} → (f : K → (j ⟶ j')) → (hK : HasCardinalLT K κ) → j ⟶ CategoryTheory.IsCardinalFiltered.coeq f hK
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.rightCancelMonoid : {α : Type u} → [AddRightCancelMonoid α] → RightCancelMonoid (Multiplicative α)
-- Mathlib.RingTheory.LocalProperties.Projective
/-- A variant of `Module.projective_of_localization_maximal` that accepts `IsLocalizedModule`.
 -/
Module.projective_of_localization_maximal' : ∀ {R : Type u_1} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)]
  [inst_7 : (P : Ideal R) → [inst_7 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [∀ (P : Ideal R) [inst_9 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_10 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)],
  (∀ (I : Ideal R) (x : I.IsMaximal), Module.Projective (Rₚ I) (Mₚ I)) →
    ∀ [Module.FinitePresentation R M], Module.Projective R M
-- Mathlib.Order.Heyting.Basic
/-- A bounded linear order is a bi-Heyting algebra by setting
* `a ⇨ b = ⊤` if `a ≤ b` and `a ⇨ b = b` otherwise.
* `a \ b = ⊥` if `a ≤ b` and `a \ b = a` otherwise.  -/
LinearOrder.toBiheytingAlgebra : (α : Type u_2) → [inst : LinearOrder α] → [BoundedOrder α] → BiheytingAlgebra α
-- Std.Time.Time.Unit.Second
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Second.Ordinal.ofInt : {leap : Bool} → (data : ℤ) → 0 ≤ data ∧ data ≤ Int.ofNat (if leap = true then 60 else 59) → Std.Time.Second.Ordinal leap
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_sdiff_zero : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.closure (s \ {0}) = AddSubgroup.closure s
-- Mathlib.Order.Minimal
IsLeast.minimal : ∀ {α : Type u_2} {x : α} {s : Set α} [inst : Preorder α], IsLeast s x → Minimal (fun x => x ∈ s) x
-- Mathlib.Topology.Order.Basic
/-- A strictly monotone function between linear orders with order topology is a topological
embedding provided that the range of `f` is order-connected.  -/
StrictMono.isEmbedding_of_ordConnected : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : TopologicalSpace α]
  [h : OrderTopology α] [inst_3 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  StrictMono f → (Set.range f).OrdConnected → Topology.IsEmbedding f
-- Init.Data.BitVec.Bitblast
/-- Adding a bitvector to its own complement yields the all ones bitpattern  -/
BitVec.add_not_self : ∀ {w : ℕ} (x : BitVec w), x + ~~~x = BitVec.allOnes w
-- Std.Http.Data.URI.Basic
/-- Port component, preserving whether it is omitted (`example.com`),
explicitly empty (`example.com:`), or numeric (`example.com:443`).
 -/
Std.Http.URI.Authority.port : Std.Http.URI.Authority → Std.Http.URI.Port
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.toHomeomorph_symm_apply : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (e : α ≃ᵤ β),
  ⇑e.toHomeomorph.symm = ⇑e.symm
-- Init.System.IO
_private.Init.System.IO.0.IO.Process.Child.mk.injEq : ∀ {cfg : IO.Process.StdioConfig} (stdin : cfg.stdin.toHandleType) (stdout : cfg.stdout.toHandleType)
  (stderr : cfg.stderr.toHandleType) (stdin_1 : cfg.stdin.toHandleType) (stdout_1 : cfg.stdout.toHandleType)
  (stderr_1 : cfg.stderr.toHandleType),
  ({ stdin := stdin, stdout := stdout, stderr := stderr } =
      { stdin := stdin_1, stdout := stdout_1, stderr := stderr_1 }) =
    (stdin = stdin_1 ∧ stdout = stdout_1 ∧ stderr = stderr_1)
-- Mathlib.Algebra.Torsor.Basic
sub_add_vsub_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (v₁ v₂ : G) (p₁ p₂ : P),
  v₁ - v₂ + (p₁ -ᵥ p₂) = (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.noConfusionType : Sort v✝ → Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Γ' → Sort v✝
-- Lean.Meta.Tactic.Grind.Core
/-- Save asserted facts for pretty printing goal.  -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.storeFact : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.shadow_iterate_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (k : ℕ), Finset.shadow^[k] ∅ = ∅
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.map_commutator : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H₁ H₂ : Subgroup G) (f : G →* G'),
  Subgroup.map f ⁅H₁, H₂⁆ = ⁅Subgroup.map f H₁, Subgroup.map f H₂⁆
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f g : H → H'}, f =ᶠ[nhdsWithin x s] g → f x = g x → (P f s x ↔ P g s x)
-- Mathlib.Algebra.Polynomial.Eval.SMul
Polynomial.leval_apply : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R), (Polynomial.leval r) f = Polynomial.eval r f
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffWithinAt.prodMk : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F' : Type u_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {s : Set M} {x : M} {n : WithTop ℕ∞} {f : M → M'} {g : M → N'},
  ContMDiffWithinAt I I' n f s x →
    ContMDiffWithinAt I J' n g s x → ContMDiffWithinAt I (I'.prod J') n (fun x => (f x, g x)) s x
-- Mathlib.Combinatorics.Configuration
Configuration.HasPoints.lineCount_le_pointCount : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.HasPoints P L] {p : P} {l : L},
  p ∉ l → ∀ [hf : Finite { p // p ∈ l }], Configuration.lineCount L p ≤ Configuration.pointCount P l
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `nontrivialTopology_iff_exists_norm_ne_zero`. -/
NontrivialTopology.of_exists_norm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], (∃ x, ‖x‖ ≠ 0) → NontrivialTopology E
-- Mathlib.Order.BooleanSubalgebra
/-- The inf of two Boolean subalgebras is their intersection.  -/
BooleanSubalgebra.instInf : {α : Type u_2} → [inst : BooleanAlgebra α] → Min (BooleanSubalgebra α)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.δ_δ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f : i ⟶ j) (g : j ⟶ k) (h : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_δ._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.δ_δ._auto_3),
  CategoryTheory.CategoryStruct.comp (X.δ g h n₀ n₁ hn₁) (X.δ f g n₁ n₂ hn₂) = 0
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_ground_eq : ∀ {α : Type u_1} {β : Type u_2} (N : Matroid β) (f : α → β), (N.comap f).E = f ⁻¹' N.E
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given two multiforks with isomorphic components in such a way that the natural diagrams
commute, then one is a limit if and only if the other one is.  -/
CategoryTheory.Limits.Multifork.isLimitEquivOfIsos : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I I' : CategoryTheory.Limits.MulticospanIndex J C} →
        (c : CategoryTheory.Limits.Multifork I) →
          (c' : CategoryTheory.Limits.Multifork I') →
            (e : c.pt ≅ c'.pt) →
              (el : (i : J.L) → I.left i ≅ I'.left i) →
                (er : (i : J.R) → I.right i ≅ I'.right i) →
                  autoParam
                      (∀ (i : J.R),
                        CategoryTheory.CategoryStruct.comp (I.fst i) (er i).hom =
                          CategoryTheory.CategoryStruct.comp (el (J.fst i)).hom (I'.fst i))
                      CategoryTheory.Limits.Multifork.isLimitEquivOfIsos._auto_1 →
                    autoParam
                        (∀ (i : J.R),
                          CategoryTheory.CategoryStruct.comp (I.snd i) (er i).hom =
                            CategoryTheory.CategoryStruct.comp (el (J.snd i)).hom (I'.snd i))
                        CategoryTheory.Limits.Multifork.isLimitEquivOfIsos._auto_3 →
                      autoParam
                          (∀ (i : J.L),
                            CategoryTheory.CategoryStruct.comp e.hom (c'.ι i) =
                              CategoryTheory.CategoryStruct.comp (c.ι i) (el i).hom)
                          CategoryTheory.Limits.Multifork.isLimitEquivOfIsos._auto_5 →
                        CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit c'
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.eqnInfoExt : Lean.MapDeclarationExtension Lean.Elab.PartialFixpoint.EqnInfo
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.analyticAt_smul : ∀ {g : GL (Fin 2) ℝ},
  0 < (↑g).det → ∀ (τ : UpperHalfPlane), AnalyticAt ℂ (fun z => ↑(g • ↑UpperHalfPlane.ofComplex z)) ↑τ
-- Mathlib.Analysis.Analytic.Composition
/-- Only `0`-th coefficient of `q.comp p` depends on `q 0`.  -/
FormalMultilinearSeries.removeZero_comp_of_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
  0 < n → q.removeZero.comp p n = q.comp p n
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstField.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `opEquivalence`.  -/
HomologicalComplex.opFunctor : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          CategoryTheory.Functor (HomologicalComplex V c)ᵒᵖ (HomologicalComplex Vᵒᵖ c.symm)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Sheaf.toImage_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sheaf.toImage f) (CategoryTheory.Sheaf.imageι f) = f
-- Mathlib.CategoryTheory.Subobject.Basic
/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows.  -/
CategoryTheory.Subobject.mk_eq_mk_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g] (i : A₁ ≅ A₂),
  CategoryTheory.CategoryStruct.comp i.hom g = f → CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.minKey! = t.minKeyD default
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_some_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.min? = some (t.min he)