mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `eq f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of object
which admits a morphism `eqHom f f' : eq f f' ⟶ j` such that
`eq_condition : eqHom f f' ≫ f = eqHom f f' ≫ f'`.
Its existence is ensured by `IsCofiltered`.
 -/
CategoryTheory.IsCofiltered.eq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofilteredOrEmpty C] → {j j' : C} → (j ⟶ j') → (j ⟶ j') → C
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (CategoryTheory.Functor.id C) =
    CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Init.Tactics
/-- `mrevert` is like `revert`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by
  mintro ⟨HP, HQ, HR⟩
  mrevert HR
  mrevert HP
  mintro HP'
  mintro HR'
  mexact HR'
```
 -/
Lean.Parser.Tactic.mrevertMacro : Lean.ParserDescr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_eq_getLast?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.max? = t.toList.getLast?
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X : ∀ {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.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ : I₂),
  ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)
-- Init.Data.BitVec.Basic
BitVec.zero_eq : ∀ {n : ℕ}, BitVec.zero n = 0#n
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.mk.inj : ∀ {X : Type u} {toTwoPointing : TwoPointing X} {X_1 : Type u} {toTwoPointing_1 : TwoPointing X_1},
  { X := X, toTwoPointing := toTwoPointing } = { X := X_1, toTwoPointing := toTwoPointing_1 } →
    X = X_1 ∧ toTwoPointing ≍ toTwoPointing_1
-- Lean.Parser.Term
Lean.Parser.Term.throwNamedErrorAtMacro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.cmp_veblen : ∀ {o₁ o₂ a b : Ordinal.{u}},
  cmp (Ordinal.veblen o₁ a) (Ordinal.veblen o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (Ordinal.veblen o₂ b)
    | Ordering.gt => cmp (Ordinal.veblen o₁ a) b
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder : {X : AlgebraicGeometry.Scheme} → PartialOrder X.IdealSheafData
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv_symm_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : CategoryTheory.Functor C (Type (max w v₁))}
  (x : F.obj (Opposite.unop X)) (Y : C),
  (CategoryTheory.uliftCoyonedaEquiv.symm x).app Y =
    TypeCat.ofHom fun y => (CategoryTheory.ConcreteCategory.hom (F.map y.down)) x
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_hom_toFunctor_obj_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.flippingIso.hom.toFunctor.obj F).obj k).map f = (F.map f).app k
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- Given a type `$t`, if there is an assumption `[i : MeasurableSpace $t]`, then try to prove
`[BorelSpace $t]` and replace `i` with `borel $t`. Otherwise, add instances
`borel $t : MeasurableSpace $t` and `⟨rfl⟩ : BorelSpace $t`.  -/
Mathlib.Tactic.Borelize.borelize : Lean.Term → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.PartitionOfUnity
/-- The support of a partition of unity at a point `x₀` as a `Finset`.
This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i x₀ ≠ 0`.  -/
PartitionOfUnity.finsupport : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → PartitionOfUnity ι X s → X → Finset ι
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.continuous_op : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous MulOpposite.op
-- Mathlib.Data.Num.Basic
instOnePosNum : One PosNum
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.CommRingCat.Colimits.descFunLift.match_1.splitter : {J : Type u_1} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      (motive : CommRingCat.Colimits.Prequotient F → Sort u_2) →
        (x : CommRingCat.Colimits.Prequotient F) →
          ((j : J) → (x : ↑(F.obj j)) → motive (CommRingCat.Colimits.Prequotient.of j x)) →
            (Unit → motive CommRingCat.Colimits.Prequotient.zero) →
              (Unit → motive CommRingCat.Colimits.Prequotient.one) →
                ((x : CommRingCat.Colimits.Prequotient F) → motive x.neg) →
                  ((x y : CommRingCat.Colimits.Prequotient F) → motive (x.add y)) →
                    ((x y : CommRingCat.Colimits.Prequotient F) → motive (x.mul y)) → motive x
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The object in the category of representations associated to a type equipped a representation.
This is the preferred way to construct a term of `Rep k G`.  -/
Rep.of : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] →
        {X : Type w} → [inst_2 : AddCommGroup X] → [inst_3 : Module k X] → Representation k G X → Rep.{w, u, v} k G
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_pow : ∀ {p m n : ℕ}, Nat.Prime p → emultiplicity p (m ^ n) = ↑n * emultiplicity p m
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.congr : ∀ {α : Type u} {β : Type v} [inst : LE β] {l : Filter α} {f f' g g' : α → β},
  f ≤ᶠ[l] g → f =ᶠ[l] f' → g =ᶠ[l] g' → f' ≤ᶠ[l] g'
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → LowerSet α),
  ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_empty : ∀ {α : Type u_1} (f : α → ℕ), Nat.multinomial ∅ f = 1
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Icc_intCast : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α],
  ⋃ n, Set.Icc (↑n) (↑n + 1) = Set.univ
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.stdSymm : Std.Symm Nat.Coprime
-- Init.Data.String.Basic
/-- Returns the character at position `p` of a string. Returns `(default : Char)`, which is `'A'`, if
`p` is not a valid position.

Requires evidence, `h`, that `p` is within bounds instead of performing a run-time bounds check as
in `String.get`.

A typical pattern combines `get'` with a dependent `if`-expression to avoid the overhead of an
additional bounds check. For example:
```
def getInBounds? (s : String) (p : String.Pos) : Option Char :=
  if h : s.atEnd p then none else some (s.get' p h)
```
Even with evidence of `¬ s.atEnd p`, `p` may be invalid if a byte index points into the middle of a
multi-byte UTF-8 character. For example, `"L∃∀N".get' ⟨2⟩ (by decide) = (default : Char)`.

This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos` or another means of obtaining a `String.Pos`.

Examples:
* `"abc".get' 0 (by decide) = 'a'`
* `let lean := "L∃∀N"; lean.get' (0 |> lean.next |> lean.next) (by decide) = '∀'`
 -/
String.Pos.Raw.get' : (s : String) → (p : String.Pos.Raw) → ¬String.Pos.Raw.atEnd s p = true → Char
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k a : α}, (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
-- Mathlib.Data.EReal.Basic
EReal.coe_le_coe_iff : ∀ {x y : ℝ}, ↑x ≤ ↑y ↔ x ≤ y
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {fallback : α}, t.getD (t.min he) fallback = t.min he
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Law of sines** (sine rule), vector angle form.  -/
InnerProductGeometry.sin_angle_mul_norm_eq_sin_angle_mul_norm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  Real.sin (InnerProductGeometry.angle x y) * ‖x‖ = Real.sin (InnerProductGeometry.angle y (x - y)) * ‖x - y‖
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ_δ₀Iter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 2)) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.δ_δ₀Iter._auto_1),
  autoParam (↑j ≤ i) CategoryTheory.SimplicialObject.δ_δ₀Iter._auto_3 →
    CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ₀Iter i hi) = X.δ₀Iter (i + 1) ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.skipWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.copy.skipWhile pat = (pos.skipWhile pat).copy
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_zero : ∀ {𝕜 : 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'},
  VectorField.mpullback I I' f 0 = 0
-- Lean.Meta.ExprLens
/-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e`  -/
Lean.Core.viewBinders : {M : Type → Type} → [Monad M] → [Lean.MonadError M] → Lean.SubExpr.Pos → Lean.Expr → M (Array (Lean.Name × Lean.Expr))
-- Mathlib.Topology.UniformSpace.Basic
uniformity_mulOpposite : ∀ {α : Type ua} [inst : UniformSpace α],
  uniformity αᵐᵒᵖ = Filter.comap (fun q => (MulOpposite.unop q.1, MulOpposite.unop q.2)) (uniformity α)
-- Mathlib.Algebra.Module.Submodule.Order
/-- A submodule of an ordered cancellative additive monoid is an ordered cancellative additive
monoid.  -/
Submodule.toIsOrderedCancelAddMonoid : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelAddMonoid M] [inst_4 : Module R M] (S : Submodule R M), IsOrderedCancelAddMonoid ↥S
-- Mathlib.Data.Part
Part.bind_le : ∀ {β α : Type u_2} (x : Part α) (f : α → Part β) (y : Part β), x >>= f ≤ y ↔ ∀ a ∈ x, f a ≤ y
-- Mathlib.Algebra.Group.Basic
right_ne_add : ∀ {M : Type u_4} [inst : AddMonoid M] [IsRightCancelAdd M] {a b : M}, b ≠ a + b ↔ a ≠ 0
-- Lean.ResolveName
/-- Finds an efficient name that unambiguously resolves to the given name `n₀`, if possible.
If not, it returns `n₀`. (See `unresolveNameGlobal?`, which returns `none` instead.)
 -/
Lean.unresolveNameGlobal : {m : Type → Type} →
  [inst : Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] →
              Lean.Name →
                optParam Bool false →
                  optParam Bool false → (optParam (Lean.Name → m Bool) fun x => pure true) → m Lean.Name
-- Mathlib.Order.Hom.Set
/-- Two order embeddings on a well-order are equal provided that their ranges are equal.  -/
OrderEmbedding.range_inj : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : Preorder β] {f g : α ↪o β},
  Set.range ⇑f = Set.range ⇑g ↔ f = g
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the continuants `⟨Aₙ₋₁, Bₙ₋₁⟩` of `g`.  -/
GenContFract.contsAux : {K : Type u_2} → [DivisionRing K] → GenContFract K → Stream' (GenContFract.Pair K)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropEndWhile_append_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [String.Slice.Pattern.Model.PatternModel pat] [inst : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.LawfulBackwardPattern pat] {s : String.Slice},
  (s.dropEndWhile pat).copy ++ (s.takeEndWhile pat).copy = s.copy
-- Mathlib.Data.EReal.Operations
EReal.neg_strictAnti : StrictAnti fun x => -x
-- Mathlib.Order.Filter.Lift
Filter.lift_lift_same_eq_lift : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Set α → Filter β},
  (∀ (s : Set α), Monotone fun t => g s t) →
    (∀ (t : Set α), Monotone fun s => g s t) → (f.lift fun s => f.lift (g s)) = f.lift fun s => g s s
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂RingHom'_apply : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S)
  (hf : ∀ (a : R), Commute (f a) x) (p : Polynomial R), (Polynomial.eval₂RingHom' f x hf) p = Polynomial.eval₂ f x p
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.mk.eq_1 : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f : A} {d : ι} (hf : f ∈ 𝒜 d) (n : ℕ) (x : A) (hx : x ∈ 𝒜 (n • d)),
  HomogeneousLocalization.Away.mk 𝒜 hf n x hx =
    HomogeneousLocalization.mk { deg := n • d, num := ⟨x, hx⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Auxiliary definition for `CofibrantObject.HoCat.adj`.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor.id (HomotopicalAlgebra.BifibrantObject.HoCat C) ⟶
        HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.comp
          HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_injOn : Set.InjOn Real.arccos (Set.Icc (-1) 1)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.hasLimit_iff_small_sections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat),
  CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget TopCat)).sections
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.card_torsion_le_of_isSMulRegular_int : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) (n : ℤ), n ≠ 0 → IsSMulRegular 𝕜 n → {x | n • x = 0}.encard ≤ ↑n.natAbs
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.ι_fromNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] (U : ↑Y.affineOpens),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.normalizationOpenCover f).f U)
      (AlgebraicGeometry.Scheme.Hom.fromNormalization f) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map ((AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap f).app (Opposite.op ↑U)))
      (AlgebraicGeometry.IsAffineOpen.fromSpec ⋯)
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.mk : {α : Type u_5} → {ι : Type u_6} → (idxFun : ι → Option α) → (∃ i, idxFun i = none) → Combinatorics.Line α ι
-- Mathlib.Order.Filter.Finite
Filter.iInter_mem : ∀ {α : Type u} {f : Filter α} {β : Sort v} {s : β → Set α} [Finite β], ⋂ i, s i ∈ f ↔ ∀ (i : β), s i ∈ f
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.unop_id_op : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : C},
  (CategoryTheory.CategoryStruct.id (Opposite.op X)).unop = CategoryTheory.CategoryStruct.id X
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_finset : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α),
  MeasureTheory.Measure.count ↑s = ↑s.card
-- Mathlib.Data.Set.Lattice
Set.iInter_sigma : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : Sigma γ → Set β), ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_norm_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.Integrable (fun a => ‖f a‖) μ ↔ MeasureTheory.Integrable f μ)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α}, a +ᵥ s = ∅ ↔ s = ∅
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` and `N` are isomorphic as additive monoid objects, then `X ⟶ M` and `X ⟶ N`
are isomorphic additive monoids.  -/
CategoryTheory.Hom.addEquivCongrRight : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M N : C} →
        [inst_2 : CategoryTheory.AddMonObj M] →
          [inst_3 : CategoryTheory.AddMonObj N] →
            (e : M ≅ N) → [CategoryTheory.IsAddMonHom e.hom] → (X : C) → (X ⟶ M) ≃+ (X ⟶ N)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.head!_le_of_lt : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : Inhabited I] {q l : Profinite.NobelingProof.Products I},
  q < l → ↑q ≠ [] → (↑q).head! ≤ (↑l).head!
-- Lean.Parser.Syntax
Lean.Parser.Command.identPrec : Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.mk : {α : Type u} →
  [inst : Ord α] →
    {β : α → Type v} →
      {k : α → Ordering} →
        (inner : Option ((a : α) × β a)) →
          (∀ [Std.OrientedOrd α] (p : (a : α) × β a), inner = some p → k p.fst = Ordering.eq) →
            Std.DTreeMap.Internal.Cell α β k
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The family of elements given by `x : FirstObj P S` is compatible iff `firstMap` and `secondMap`
map it to the same point.
 -/
CategoryTheory.Equalizer.Presieve.compatible_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) [inst_1 : R.HasPairwisePullbacks] (x : CategoryTheory.Equalizer.FirstObj P R),
  CategoryTheory.Presieve.FamilyOfElements.Compatible
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.firstObjEqFamily P R).hom) x) ↔
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.firstMap P R)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.secondMap P R)) x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_assoc : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] {M₄ : Type u_8} [inst_9 : TopologicalSpace M₄]
  [inst_10 : AddCommMonoid M₄] [inst_11 : Module R₁ M₁] [inst_12 : Module R₂ M₂] [inst_13 : Module R₃ M₃]
  [inst_14 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_9} [inst_15 : Semiring R₄] [inst_16 : Module R₄ M₄]
  {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [inst_17 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_18 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_19 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄)
  (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂), (h ∘SL g) ∘SL f = h ∘SL g ∘SL f
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.reverse_inv_prod_mul_prod : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n]
  (L : List (Matrix.TransvectionStruct n R)),
  (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.inv) L.reverse).prod *
      (List.map Matrix.TransvectionStruct.toMatrix L).prod =
    1
-- Init.Notation
/-- `a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. -/
«term_*_» : Lean.TrailingParserDescr
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ext_getKey?_unit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m₁ m₂ : Std.ExtHashMap α Unit}, (∀ (k : α), m₁.getKey? k = m₂.getKey? k) → m₁ = m₂
-- Mathlib.Analysis.InnerProductSpace.LinearMap
ContinuousLinearMap.toLinearMap_innerSL_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v : E), ↑((innerSL 𝕜) v) = (innerₛₗ 𝕜) v
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.map_eq_map : ∀ (σ : Type u) {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : MvPolynomial σ R)
  (f : R →+* S), AddMonoidAlgebra.map (↑f) p = (MvPolynomial.map f) p
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_pointwise_smul : ∀ {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S] (r : R) (I : Ideal R) (f : R →+* S),
  Ideal.map f (r • I) = f r • Ideal.map f I
-- Mathlib.NumberTheory.Pell
/-- Any nonnegative solution is a power with nonnegative exponent of a fundamental solution.  -/
Pell.IsFundamental.eq_pow_of_nonneg : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d}, Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 0 < a.x → 0 ≤ a.y → ∃ n, a = a₁ ^ n
-- Mathlib.LinearAlgebra.FreeModule.PID
eq_bot_of_generator_maximal_submoduleImage_eq_zero : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_1}
  {N O : Submodule R M} (b : Module.Basis ι R ↥O),
  N ≤ O →
    ∀ {ϕ : ↥O →ₗ[R] R},
      (∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N) →
        ∀ [inst_3 : (ϕ.submoduleImage N).IsPrincipal], Submodule.IsPrincipal.generator (ϕ.submoduleImage N) = 0 → N = ⊥
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_singleton_iff : ∀ {k m n : ℕ}, (m...n).toArray = #[k] ↔ n = m + 1 ∧ m = k
-- Mathlib.Data.Int.Log
Int.clog_one_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ), Int.clog b 1 = 0
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_intCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) [inst_3 : IntCast F] (z : ℤ), HasDerivWithinAt (↑z) 0 s x
-- Init.Data.Option.Lemmas
Option.min_le_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Min α], (∀ (x y : α), x ⊓ y ≤ y) → ∀ {a b : Option α}, a ⊓ b ≤ b
-- Init.Data.Vector.Lemmas
Vector.foldl_empty : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {init : β}, Vector.foldl f init #v[] = init