mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.PredTrans.pushOption.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The maps to the cocone point of a multicofork from the objects on the right.  -/
CategoryTheory.Limits.Multicofork.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      {I : CategoryTheory.Limits.MultispanIndex J C} →
        (K : CategoryTheory.Limits.Multicofork I) → (b : J.R) → I.right b ⟶ K.pt
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip_le_size_of_le_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len x : ℕ} (aig : Std.Sat.AIG α)
  (input : aig.BinaryRefVec len) (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func]
  [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α func],
  x ≤ aig.decls.size → x ≤ (Std.Sat.AIG.RefVec.zip aig input func).aig.decls.size
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.braiding_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Prod.braiding C D).inverse = CategoryTheory.Prod.swap D C
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Preorder α} {inst_1 : Preorder β} {l : α → β} {u : β → α}
  {choice : (x : β) → x ≤ l (u x) → α} {gc : GaloisConnection l u} {u_l_le : ∀ (x : α), u (l x) ≤ x}
  {choice_eq : ∀ (a : β) (h : a ≤ l (u a)), choice a h = u a} {choice_1 : (x : β) → x ≤ l (u x) → α}
  {gc_1 : GaloisConnection l u} {u_l_le_1 : ∀ (x : α), u (l x) ≤ x}
  {choice_eq_1 : ∀ (a : β) (h : a ≤ l (u a)), choice_1 a h = u a},
  { choice := choice, gc := gc, u_l_le := u_l_le, choice_eq := choice_eq } =
      { choice := choice_1, gc := gc_1, u_l_le := u_l_le_1, choice_eq := choice_eq_1 } →
    choice = choice_1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- If `R` is commutative, Ore localization and monoid localization are isomorphic.  -/
OreLocalization.equivMonoidLocalization : (R : Type u_1) → [inst : CommMonoid R] → (S : Submonoid R) → Localization S ≃* OreLocalization S R
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofNatClamp_of_le : ∀ {n : ℕ}, UInt32.size ≤ n → (UInt32.ofNatClamp n).toFin = ⟨UInt32.size - 1, UInt32.toFin_ofNatClamp_of_le._proof_1⟩
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {x : ι → Filter α} {y : Filter β},
  Filter.Tendsto f (⨆ i, x i) y ↔ ∀ (i : ι), Filter.Tendsto f (x i) y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKey! k' = k
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquiv_refl : ∀ {α : Sort u_1} {p : α → Prop} (h : optParam (∀ (a : α), p a ↔ p ((Equiv.refl α) a)) ⋯),
  (Equiv.refl α).subtypeEquiv h = Equiv.refl { a // p a }
-- Lean.Elab.ConfigEval.Basic
_private.Lean.Elab.ConfigEval.Basic.0.Lean.Elab.ConfigEval.stripParens : Lean.Term → Lean.Term
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.projVandermonde_apply_zero_right : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {v w : Fin (n + 1) → R} {i : Fin (n + 1)},
  w i = 0 → Matrix.projVandermonde v w i = Pi.single (Fin.last n) (v i ^ n)
-- Mathlib.Topology.Homotopy.Equiv
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousMap.HomotopyEquiv.Simps.apply : {X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → ContinuousMap.HomotopyEquiv X Y → X → Y
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.alterₘ.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (a : α) →
      (motive : Option (β a) → Sort u_2) →
        (x : Option (β a)) → (Unit → motive none) → ((b : β a) → motive (some b)) → motive x
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.instNonempty : ∀ {α : Type u_1} [Nonempty α], Nonempty (Topology.WithLawson α)
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.instCommShiftOppositeFunctorOpOpEquivalenceInt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → (CategoryTheory.opOpEquivalence C).functor.CommShift ℤ
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.MatchUnifyResult.mk : List Lean.Level → Array Lean.Expr → Array Lean.MVarId → Lean.Meta.Sym.MatchUnifyResult
-- Mathlib.Order.CompleteLattice.Basic
iSup_psigma : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) ×' κ i → α),
  ⨆ ij, f ij = ⨆ i, ⨆ j, f ⟨i, j⟩
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Coercion to `ℂ`.  -/
Complex.UnitDisc.coe : Complex.UnitDisc → ℂ
-- Mathlib.Topology.Algebra.Group.Torsor
/-- The map `v ↦ v • p` as a homeomorphism between `V` and `P`.  -/
Homeomorph.smulConst : {V : Type u_1} →
  {P : Type u_2} →
    [inst : Group V] →
      [inst_1 : TopologicalSpace V] →
        [inst_2 : Torsor V P] → [inst_3 : TopologicalSpace P] → [IsTopologicalTorsor P] → P → V ≃ₜ P
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments by prepending `ℕ` and duplicating the first argument. Used for `nsmul`.  -/
Simps.nsmulArgs : Simps.findArgType
-- Mathlib.Data.NNReal.Defs
NNReal.div_le_of_le_mul : ∀ {a b c : NNReal}, a ≤ b * c → a / c ≤ b
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.mk.inj : ∀ {R : Type u_1} {inst : SeminormedCommRing R} {S : Type u_2} {inst_1 : Ring S} {inst_2 : Algebra R S}
  {toMulRingNorm : MulRingNorm S} {smul' : ∀ (a : R) (x : S), toMulRingNorm.toFun (a • x) = ‖a‖ * toMulRingNorm.toFun x}
  {toMulRingNorm_1 : MulRingNorm S}
  {smul'_1 : ∀ (a : R) (x : S), toMulRingNorm_1.toFun (a • x) = ‖a‖ * toMulRingNorm_1.toFun x},
  { toMulRingNorm := toMulRingNorm, smul' := smul' } = { toMulRingNorm := toMulRingNorm_1, smul' := smul'_1 } →
    toMulRingNorm = toMulRingNorm_1
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_add_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ⌊a + 1⌋ = ⌊a⌋ + 1
-- Lean.Elab.ConfigEval.Basic
/-- Interprets `cfg` as configuration item or list of configuration items.

Items are interpreted in a way that allows user-defined configurations.
Nearly anything that looks like configuration items or lists of configuration items
will be interpreted. We're expecting an item that has one of the following formats:
- `"(" ident/atom ":=" syntax ")"`
- `"+" ident/atom`
- `"-" ident/atom`

The specification:
- A null node is a list of configurations
- A one-argument node is considered to be a wrapper like `optConfig` or `configItem`.
- A node with at two arguments starting with a "+"/"-" atom and whose second
  argument is an ident or atom is a `posConfigItem`/`negConfigItem`
- A node with at most five arguments starting with a "(" atom and whose second argument
  is an ident or atom is a `valConfigItem`. The fourth argument is the value,
  and it is allowed to have arbitary syntax (it does not need to be a `Term`).
- A bare atom is considered to be a `"+"` option.

We trust that any atoms are valid as idents. The atom will be parsed using `String.toName`
to form the name. (Small optimization: if the name doesn't contain `.`, we use `Name.mkSimple`
to skip parsing. Atoms must not contain numerals or `«»` escapes.)

On interpretation error, `onErr` is called with the current configuration object and the offending
syntax item. It may process the item itself or otherwise throw an error. We leave it to `onErr`
to decide what to do for items containing `Syntax.missing`.
 -/
Lean.Elab.ConfigEval.foldConfigM : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadRef m] → α → Lean.Syntax → (α → Lean.Elab.ConfigEval.ConfigItem → m α) → (α → Lean.Syntax → m α) → m α
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Topology.Basic.0.TopModuleCat.Hom.ofHom'.sizeOf_spec : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : TopModuleCat R} [inst_2 : SizeOf R]
  (hom' : ↑X.toModuleCat →L[R] ↑Y.toModuleCat), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hV5 : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Monoid G] (self : TopRep k G),
  ContinuousSMul k ↑self
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.iSup : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [inst_2 : SupSet β] [Countable ι]
  (hf : ∀ (i : ι), AEMeasurable (f i) μ), (∀ᵐ (x : α) ∂μ, p x fun n => f n x) → ⨆ n, aeSeq hf p n =ᵐ[μ] ⨆ n, f n
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.ker_comp_eq_of_commute_of_disjoint_ker : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {f g : V →ₗ[K] V}, Commute f g → Disjoint f.ker g.ker → (f ∘ₗ g).ker = f.ker ⊔ g.ker
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_inf : ∀ {R : Type u} [inst : NonAssocSemiring R] (p p' : Subsemiring R), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_comm : ∀ {α : Type u_3} [inst : NonAssocRing α] (n : ℤ) (x : α), ↑n * x = x * ↑n
-- Mathlib.Analysis.Distribution.Support
/-- The complement of the support is the largest open set on which `f` vanishes.  -/
Distribution.dsupport_compl_eq : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V},
  (Distribution.dsupport f)ᶜ = ⋃₀ {a | Distribution.IsVanishingOn f a ∧ IsOpen a}
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.instHasHomologyUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ) [S.HasHomology], S.unop.HasHomology
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
IsStrictlyPositive.ringInverse : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  {a : A}, IsStrictlyPositive a → IsStrictlyPositive (Ring.inverse a)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The equivalence from the lattice generated by a pair of periods to `ℤ × ℤ`.  -/
PeriodPair.latticeEquivProd : (L : PeriodPair) → ↥L.lattice ≃ₗ[ℤ] ℤ × ℤ
-- Mathlib.Data.Set.Finite.Lattice
/-- An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but
finitely many are empty.  -/
Set.finite_iUnion_iff : ∀ {α : Type u} {ι : Type u_1} {s : ι → Set α},
  (Pairwise fun i j => Disjoint (s i) (s j)) →
    ((⋃ i, s i).Finite ↔ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite)
-- Mathlib.Topology.Separation.Basic
/-- A topology inducing map from a T₀ space is a topological embedding.  -/
Topology.IsInducing.isEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T0Space X] {f : X → Y},
  Topology.IsInducing f → Topology.IsEmbedding f
-- Lean.Elab.Util
Lean.Elab.MacroStackElem.mk : Lean.Syntax → Lean.Syntax → Lean.Elab.MacroStackElem
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulForwardPatternModel.skipPrefix?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.ForwardPattern pat}
  {inst_1 : String.Slice.Pattern.Model.PatternModel pat}
  [self : String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice} (pos : s.Pos),
  String.Slice.Pattern.ForwardPattern.skipPrefix? pat s = some pos ↔ String.Slice.Pattern.Model.IsLongestMatch pat pos
-- Mathlib.GroupTheory.OrderOfElement
image_range_addOrderOf : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] {x : G} [inst_2 : DecidableEq G],
  Finset.image (fun i => i • x) (Finset.range (addOrderOf x)) = (↑(AddSubgroup.zmultiples x)).toFinset
-- Init.Data.Option.Lemmas
Option.min_join_left : ∀ {α : Type u_1} [inst : Min α] {o : Option (Option α)} {o' : Option α}, o.join ⊓ o' = (o ⊓ some o').join
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, Std.ExtDHashMap.Const.get? (m.insert k v) k = some v
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of two `C^n` functions is `C^n`.  -/
ContDiff.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F}, ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n (f • g)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_roc' : ∀ {m n k : ℕ}, List.map (fun x => k + x) (m<...=n).toList = ((k + m)<...=k + n).toList
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.right.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {a a_1 : D}, CategoryTheory.Join.right a = CategoryTheory.Join.right a_1 → a = a_1
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.rTensorEquiv_tmulAlgEquiv : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : CommMonoid M] (a : A) (p : MonoidAlgebra B M),
  (MonoidAlgebra.rTensorEquivAlgEquiv R S A B) (a ⊗ₜ[R] p) =
    a • (MonoidAlgebra.mapAlgHom M Algebra.TensorProduct.includeRight) p
-- Mathlib.Order.Filter.Pointwise
Filter.instZero.eq_1 : ∀ {α : Type u_2} [inst : Zero α], Filter.instZero = { zero := pure 0 }
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
AffineBasis.isUnit_toMatrix_iff : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : Fintype ι] [inst_5 : DecidableEq ι]
  [Nontrivial k] (p : ι → P), IsUnit (b.toMatrix p) ↔ AffineIndependent k p ∧ affineSpan k (Set.range p) = ⊤
-- Mathlib.Algebra.Opposites
MulOpposite.instIsEmpty : ∀ {α : Type u_1} [IsEmpty α], IsEmpty αᵐᵒᵖ
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.orderDualEquivalence_functor_obj : ∀ (X : Type u) [inst : Preorder X] (x : Xᵒᵈ),
  (CategoryTheory.orderDualEquivalence X).functor.obj x = Opposite.op (OrderDual.ofDual x)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.oddKernel.eq_1 : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.oddKernel a x = ⋯.lift a
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left_eq : ∀ (a c d p x : ℤ) (h₁ : p ≤ a * x), Int.Cooper.resolve_left a c d p x = ↑(Int.Cooper.resolve_left' a c d p x h₁)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α},
  Std.ExtDTreeMap.Const.get! (t₁ ∩ t₂) k = if k ∈ t₂ then Std.ExtDTreeMap.Const.get! t₁ k else default
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_hom_snd_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
        (CategoryTheory.Limits.pullback.fst f₃ f₄)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
      (CategoryTheory.Limits.pullback.snd f₁ f₂)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.isQuotientMap_mkQL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (S : Submodule R M), Topology.IsQuotientMap ⇑S.mkQL
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.const.injEq : ∀ (declName declName_1 : Lean.Name),
  (Lean.Lsp.CompletionIdentifier.const declName = Lean.Lsp.CompletionIdentifier.const declName_1) =
    (declName = declName_1)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instMul.eq_1 : ∀ {α : Type u},
  FreeGroup.instMul =
    { mul := fun x y => Quot.liftOn x (fun L₁ => Quot.liftOn y (fun L₂ => FreeGroup.mk (L₁ ++ L₂)) ⋯) ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentHighlight.toJson : Lean.Lsp.DocumentHighlight → Lean.Json
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 0 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₂ f₁ f₂).obj 0)
-- Lean.Parser.Extension
Lean.Parser.addParserTokens : Lean.Parser.TokenTable → Lean.Parser.ParserInfo → Except String Lean.Parser.TokenTable
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_ineq : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (b : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_left_split ctx p₁ p₂ p₃ d k →
    Int.Internal.Linear.cooper_dvd_left_split_ineq_cert p₁ p₂ (↑k) b p' = true →
      Int.Internal.Linear.Poly.denote' ctx p' ≤ 0
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- If `E : C ≌ D` is an equivalence, this expresses the compatibility of `CommShift`
structures on `E.functor` and `E.inverse`.
 -/
CategoryTheory.Equivalence.CommShift : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (E : C ≌ D) →
          (A : Type u_3) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] → [E.functor.CommShift A] → [E.inverse.CommShift A] → Prop
-- Mathlib.Topology.Separation.SeparatedNhds
Set.hasSeparatingCover_empty_right : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), HasSeparatingCover s ∅
-- Mathlib.Order.Lattice
Pi.inf_def : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Min (α' i)] (f g : (i : ι) → α' i), f ⊓ g = fun i => f i ⊓ g i
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.ext_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s s' : S.Splitting), s.s = s'.s → s = s'
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.reindex_points : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (a : Fin (n + 1)),
  (s.reindex e).points a = (s.points ∘ ⇑e.symm) a
-- Mathlib.Algebra.Ring.Basic
/-- Right multiplication by an element of a type with distributive multiplication is an `AddHom`.  -/
AddHom.mulRight : {R : Type u_1} → [inst : Distrib R] → R → R →ₙ+ R
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The torsion ideal of `x`, containing all `a` such that `a • x = 0`.  -/
Ideal.torsionOf : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → M → Ideal R
-- Mathlib.Tactic.Abel
/-- The normalization style for `abel_nf`.  -/
Mathlib.Tactic.Abel.AbelMode : Type
-- Mathlib.Order.Filter.CountableInter
countable_bInter_mem : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable → ∀ {s : (i : ι) → i ∈ S → Set α}, ⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
-- Mathlib.Data.NNReal.Defs
NNReal.coe_one : ↑1 = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.eraseManyEntries! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {ρ : Type u_1} [inst : ForIn Id ρ ((a : α) × β a)] {l : ρ}
  {t : Std.DTreeMap.Internal.Impl α β}, t.WF → (↑(t.eraseManyEntries! l)).WF
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshRef.ref : ProofWidgets.RefreshComponent.RefreshRef → IO.Ref ProofWidgets.RefreshComponent.RefreshState
-- Mathlib.Order.WithBotTop
WithTopBot.eq_1 : ∀ (ι : Type u_1), WithTopBot ι = WithTop (WithBot ι)
-- Plausible.Random
Plausible.Random.instBool : {m : Type → Type u_1} → [Monad m] → Plausible.Random m Bool
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- Assigns terms in the goal that satisfy `isTarget`.
Recall that not all terms are communicated to `linarith` and `cutsat` modules if they do not appear in relevant constraints.
The idea is to assign unused integer values that have not been used in the model and do not falsify equalities and disequalities
in core.
 -/
_private.Lean.Meta.Tactic.Grind.Arith.ModelUtil.0.Lean.Meta.Grind.Arith.assignUnassigned : Lean.Meta.Grind.Goal →
  (Lean.Meta.Grind.ENode → Lean.MetaM Bool) → Std.HashMap Lean.Expr ℚ → Lean.MetaM (Std.HashMap Lean.Expr ℚ)
-- Mathlib.Data.Int.Cast.Lemmas
AddMonoidHom.ext_int_iff : ∀ {A : Type u_5} [inst : AddMonoid A] {f g : ℤ →+ A}, f = g ↔ f 1 = g 1
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.iff_of_le_of_exists_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (N : Submonoid R),
  M ≤ N → (∀ n ∈ N, ∃ m ∈ M, n ∣ m) → (IsLocalization M S ↔ IsLocalization N S)
-- Lean.Parser.Term
Lean.Parser.Term.nomatch.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.homEquiv_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  (e : F.RepresentableBy Y) {X : C} (f : X ⟶ Y),
  e.homEquiv f = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (e.homEquiv (CategoryTheory.CategoryStruct.id Y))
-- Mathlib.Data.Fintype.Sets
Set.toFinset_nontrivial : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s], s.toFinset.Nontrivial ↔ s.Nontrivial
-- Lean.Elab.DeclModifiers
/-- Adds attribute `attr` in `modifiers`  -/
Lean.Elab.Modifiers.addAttr : Lean.Elab.Modifiers → Lean.Elab.Attribute → Lean.Elab.Modifiers