mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Ring.Basic
/-- Applies `Int.cast` to an int monomial to produce a monomial in `α`.

* `↑c = c` if `c` is a numeric literal
* `↑(a ^ n * b) = ↑a ^ n * ↑b`
 -/
Mathlib.Tactic.Ring.ExProd.evalIntCast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          (sβ : Q(CommSemiring «$β»)) →
            {a : Q(ℤ)} →
              (rα : Q(CommRing «$α»)) →
                Mathlib.Tactic.Ring.ExProd sβ a →
                  Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.ExProd sα) q(↑«$a»))
-- Init.Data.Nat.Lemmas
Nat.eq_one_of_mul_eq_one_left : ∀ {m n : ℕ}, m * n = 1 → n = 1
-- Mathlib.Data.List.AList
/-- Given `l : List (Sigma β)`, create a term of type `AList β` by removing
entries with duplicate keys.  -/
List.toAList : {α : Type u} → [DecidableEq α] → {β : α → Type v} → List (Sigma β) → AList β
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_periodic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), Function.Periodic (toIcoMod hp a) p
-- Mathlib.RingTheory.Perfectoid.BDeRham
_private.Mathlib.RingTheory.Perfectoid.BDeRham.0.«term_♭» : Lean.TrailingParserDescr
-- Aesop.Forward.State
/-- Add a hypothesis to the cluster state. `hyp.subst` must be the substitution
that results from applying `h` to `slot`.  -/
Aesop.ClusterState.addHyp : Aesop.ClusterState → Aesop.Slot → Aesop.Hyp → Aesop.ClusterState.AddM Aesop.ClusterState
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- To check whether two maps are equalized by both maps of a trident, it suffices to check it for
the first map  -/
CategoryTheory.Limits.Trident.equalizer_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J]
  (s : CategoryTheory.Limits.Trident f) {W : C} {k l : W ⟶ s.pt},
  CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι →
    ∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
      CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- `legendreSym p a = -1` iff `a` is a nonsquare mod `p`.  -/
legendreSym.eq_neg_one_iff : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℤ}, legendreSym p a = -1 ↔ ¬IsSquare ↑a
-- Mathlib.Order.Category.Lat
Lat.hom_inv_apply : ∀ {X Y : Lat} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Std.Async.Signal
Std.Async.Signal.sigterm.sizeOf_spec : sizeOf Std.Async.Signal.sigterm = 1
-- Mathlib.RingTheory.RingHom.Flat
CommRingCat.inr_injective_of_flat : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    (CommRingCat.Hom.hom g).Flat →
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inr f g))
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.toEdge_eq_toEdge_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {v w : V} (h : M.IsMatching) (ha : M.Adj v w),
  h.toEdge ⟨v, ⋯⟩ = h.toEdge ⟨w, ⋯⟩
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf_zero : Nat.zeckendorf 0 = []
-- Mathlib.Algebra.Order.Sub.Defs
le_add_tsub_swap : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α}
  [AddLeftReflectLE α], a ≤ b + a - b
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_sdiff_singleton_zero : ∀ {R : Type u} [inst : CommSemiring R] (s : Set R), PrimeSpectrum.zeroLocus (s \ {0}) = PrimeSpectrum.zeroLocus s
-- Mathlib.Order.Filter.Extr
IsExtrFilter.filter_mono : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
  IsExtrFilter f l a → l' ≤ l → IsExtrFilter f l' a
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal] (X Y : D),
  CategoryTheory.Functor.LaxMonoidal.μ G X Y =
    (adj.homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y))
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)))
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp.eq_1 : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F)
  (U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ),
  AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.lift
        ((AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp.comp
          ((CategoryTheory.evaluation
                (TopologicalSpace.Opens
                    ↑(CategoryTheory.Limits.colimit (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))))ᵒᵖ
                C).obj
            ((TopologicalSpace.Opens.map
                    (CategoryTheory.Limits.colimit.desc (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
                      ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).op.obj
              U)))
        { pt := s.pt.presheaf.obj U,
          π :=
            {
              app := fun j =>
                CategoryTheory.CategoryStruct.comp ((s.ι.app (Opposite.unop j)).c.app U)
                  ((F.obj (Opposite.unop j)).presheaf.map (CategoryTheory.eqToHom ⋯)),
              naturality := ⋯ } })
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation
          (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp
          ((TopologicalSpace.Opens.map
                  (CategoryTheory.Limits.colimit.desc (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
                    ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).op.obj
            U)).inv
-- Mathlib.Topology.Instances.NNReal.Lemmas
tendsto_real_toNNReal_atTop : Filter.Tendsto Real.toNNReal Filter.atTop Filter.atTop
-- Aesop.Stats.Basic
Aesop.ForwardRuleStateStats.clusterStateStats : Aesop.ForwardRuleStateStats → Array Aesop.ForwardClusterStateStats
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.op_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂), ψ.op.φH = ψ.φH.op
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) ⁻¹' Set.Ioc b c = Set.Ico (a / c) (a / b)
-- Init.Grind.Ring.OfScientific
Lean.Grind.LawfulOfScientific.mk : ∀ {α : Type u} [inst : Lean.Grind.Field α] [inst_1 : OfScientific α],
  (∀ {m : ℕ} {s : Bool} {e : ℕ}, OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e) →
    Lean.Grind.LawfulOfScientific α
-- Init.Data.Array.Lemmas
Array.set_set : ∀ {α : Type u_1} (a : α) {b : α} {xs : Array α} {i : ℕ} (h : i < xs.size), (xs.set i a h).set i b ⋯ = xs.set i b h
-- Mathlib.SetTheory.Ordinal.Family
not_injective_of_ordinal : ∀ {α : Type u_1} [Small.{u, u_1} α] (f : Ordinal.{u} → α), ¬Function.Injective f
-- Std.Data.Internal.List.Associative
Std.Internal.List.forall_mem_iff_forall_contains_getValueCast : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)}
  {p : (a : α) → β a → Prop},
  Std.Internal.List.DistinctKeys l →
    ((∀ x ∈ l, p x.fst x.snd) ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true), p a (Std.Internal.List.getValueCast a l h))
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff_eq_or_lt_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin b → (Order.pred b < a ↔ a = b ∨ b < a)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.isSome_next_of_isPlausibleIndirectOutput : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it : Std.Iter α}
  {out : α}, it.IsPlausibleIndirectOutput out → it.internalState.next.isSome = true
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.le_of_le_subset : ∀ {α : Type u_1} {β : Type u_2} {G H K : Graph α β}, K ≤ G → K.vertexSet ⊆ H.vertexSet → H.IsInducedSubgraph G → K ≤ H
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ShiftTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (vec : aig.RefVec w)
  (distance : ℕ) (vec_1 : aig.RefVec w) (distance_1 : ℕ),
  ({ vec := vec, distance := distance } = { vec := vec_1, distance := distance_1 }) =
    (vec = vec_1 ∧ distance = distance_1)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.matchesAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos → String.Slice.Pattern.Model.MatchesAt pat startPos
-- Init.Data.SInt.Basic
/-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`.  -/
Int8.ofBitVec : BitVec 8 → Int8
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterM m α → Sort u_3)
  (h_1 : Unit → motive { internalState := { list := [] } })
  (h_2 : (x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }),
  (match { internalState := { list := [] } } with
    | { internalState := { list := [] } } => h_1 ()
    | { internalState := { list := x :: xs } } => h_2 x xs) =
    h_1 ()
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.coe_id : ∀ (α : Type u_2) [inst : Bornology α], ⇑(LocallyBoundedMap.id α) = id
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.isIso_π_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n i : ℤ),
  i ≤ n → CategoryTheory.IsIso ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π✝ f n).f i)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The auxiliary sequence for a normalised EDS `W : ℕ → R`, with initial values
`W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d` and extra parameter `b`.  -/
preNormEDS' : {R : Type u_1} → [CommRing R] → R → R → R → ℕ → R
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- If `t` is a non-empty open subset of `H`,
every chart of `t` is the restriction of some chart on `H`.  -/
TopologicalSpace.Opens.chart_eq' : ∀ {H : Type u} [inst : TopologicalSpace H] {t : TopologicalSpace.Opens H} (ht : Nonempty ↥t)
  {e' : OpenPartialHomeomorph (↥t) H}, e' ∈ atlas H ↥t → ∃ x, e' = (chartAt H ↑x).subtypeRestr ht
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂)
  (h₂ : i₂ < j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.ofCocone c) i₁ i₂ h₁₂ ⋯ =
    CategoryTheory.Arrow.mk (F.map (CategoryTheory.homOfLE h₁₂))
-- Mathlib.Topology.Algebra.UniformMulAction
/-- The action of `Semiring.toModule` is uniformly continuous.  -/
Ring.uniformContinuousConstSMul : ∀ (R : Type u) [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R] [ContinuousMul R],
  UniformContinuousConstSMul R R
-- Std.Data.ExtTreeSet.Basic
/-- Partitions a tree set into two tree sets based on a predicate.  -/
Std.ExtTreeSet.partition : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → (α → Bool) → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp × Std.ExtTreeSet α cmp
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_add_monomial_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff (m + n)) ((MvPowerSeries.monomial m) a * φ) = a * (MvPowerSeries.coeff n) φ
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.mk.injEq : ∀ {V : Type u} {G : SimpleGraph V} (parts : Set (Set V)) (isPartition : Setoid.IsPartition parts)
  (independent : ∀ s ∈ parts, IsAntichain G.Adj s) (parts_1 : Set (Set V)) (isPartition_1 : Setoid.IsPartition parts_1)
  (independent_1 : ∀ s ∈ parts_1, IsAntichain G.Adj s),
  ({ parts := parts, isPartition := isPartition, independent := independent } =
      { parts := parts_1, isPartition := isPartition_1, independent := independent_1 }) =
    (parts = parts_1)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.fieldName.injEq : ∀ (ref : Lean.Syntax) (name : String) (levels : List Lean.Level) (suffix? : Option Lean.Name)
  (fullRef ref_1 : Lean.Syntax) (name_1 : String) (levels_1 : List Lean.Level) (suffix?_1 : Option Lean.Name)
  (fullRef_1 : Lean.Syntax),
  (Lean.Elab.Term.LVal.fieldName ref name levels suffix? fullRef =
      Lean.Elab.Term.LVal.fieldName ref_1 name_1 levels_1 suffix?_1 fullRef_1) =
    (ref = ref_1 ∧ name = name_1 ∧ levels = levels_1 ∧ suffix? = suffix?_1 ∧ fullRef = fullRef_1)
-- Mathlib.SetTheory.Ordinal.Basic
/-- Convert an element of `α.toType` to the corresponding `Ordinal`  -/
Ordinal.ToType.toOrd : {o : Ordinal.{u_1}} → o.ToType → ↑(Set.Iio o)
-- Mathlib.Data.Set.Finite.Basic
Set.toFinite_toFinset : ∀ {α : Type u} (s : Set α) [inst : Fintype ↑s], ⋯.toFinset = s.toFinset
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_zero' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], (MvPolynomial.eval fun x => 0) = MvPolynomial.constantCoeff
-- Mathlib.Data.Fin.Basic
Fin.add_one_le_of_lt : ∀ {n : ℕ} {a b : Fin (n + 1)}, a < b → a + 1 ≤ b
-- Init.Prelude
/-- The word size of the current platform, which may be 64 or 32 bits.
 -/
System.Platform.numBits : ℕ
-- Lean.Elab.MutualDef
Lean.Elab.Command.elabMutualDef : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Init.Core
or_comm : ∀ {a b : Prop}, a ∨ b ↔ b ∨ a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.coeff_degree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.Monic f → MvPolynomial.coeff (m.degree f) f = 1
-- Mathlib.Data.TypeVec
TypeVec.dropFun_toSubtype : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)),
  TypeVec.dropFun (TypeVec.toSubtype p) = TypeVec.toSubtype fun i => p i.fs
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_lineMap_left : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist ((AffineMap.lineMap p₁ p₂) c) p₁ = ‖c‖ * dist p₁ p₂
-- Mathlib.Data.Finset.Lattice.Prod
Finset.inf_product_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β)
  (t : Finset γ) (f : β × γ → α), (s ×ˢ t).inf f = t.inf fun i' => s.inf fun i => f (i, i')
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatch.State.mk : Lean.Meta.Grind.EMatchTheoremsArray →
  ℕ →
    Lean.PArray Lean.Meta.Grind.EMatchTheorem →
      Lean.PArray Lean.Meta.Grind.EMatchTheorem →
        ℕ →
          ℕ →
            ℕ →
              Lean.Meta.Grind.PreInstanceSet →
                ℕ →
                  Lean.PHashSet Lean.Name →
                    Lean.PHashMap Lean.Meta.Sym.ExprPtr (List Lean.Meta.Grind.DelayedTheoremInstance) →
                      Lean.Meta.Grind.EMatch.State
-- Mathlib.CategoryTheory.Shift.Quotient
CategoryTheory.Quotient.LiftCommShift.iso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) (r : HomRel C) {A : Type w} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : r.IsCompatibleWithShift A]
  [inst_6 : F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A),
  CategoryTheory.Quotient.LiftCommShift.iso F r hF a =
    CategoryTheory.Quotient.natIsoLift r
      (((CategoryTheory.Quotient.functor r).associator (CategoryTheory.shiftFunctor (CategoryTheory.Quotient r) a)
            (CategoryTheory.Quotient.lift r F hF)).symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight
            (CategoryTheory.Functor.commShiftIso (CategoryTheory.Quotient.functor r) a).symm
            (CategoryTheory.Quotient.lift r F hF) ≪≫
          (CategoryTheory.shiftFunctor C a).associator (CategoryTheory.Quotient.functor r)
              (CategoryTheory.Quotient.lift r F hF) ≪≫
            (CategoryTheory.shiftFunctor C a).isoWhiskerLeft (CategoryTheory.Quotient.lift.isLift r F hF) ≪≫
              CategoryTheory.Functor.commShiftIso F a ≪≫
                CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Quotient.lift.isLift r F hF).symm
                    (CategoryTheory.shiftFunctor D a) ≪≫
                  (CategoryTheory.Quotient.functor r).associator (CategoryTheory.Quotient.lift r F hF)
                    (CategoryTheory.shiftFunctor D a))
-- Mathlib.RingTheory.Adjoin.Field
minpoly_algebraMap_sub_splits : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (r : K),
  (Polynomial.map (algebraMap K L) (minpoly K x)).Splits →
    (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap K L) r - x))).Splits
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Hom.vadd_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} [inst_3 : CategoryTheory.AddModObj M X] (Y : C) (m : Y ⟶ M) (x : Y ⟶ X),
  m +ᵥ x =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift m x) CategoryTheory.AddModObj.vadd
-- Lean.Meta.Tactic.Simp.Main
/-- Auxiliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
This is the `dsimp` equivalent of the approach used at `visitApp`.
Recall that we fold orphan raw Nat literals.
 -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.doNotVisitOfNat : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_iInf : ∀ {X Y : SSet} {ι : Type u_1} (A : ι → X.Subcomplex) (p : Y ⟶ X), (⨅ i, A i).preimage p = ⨅ i, (A i).preimage p
-- Lean.Meta.Sym.Pattern
/-- Structural definitional equality for `forall` and `lambda` binders.
Opens all binders simultaneously, then checks domain equality and body equality.
This approach avoids repeated `withLCtx` calls for each binder.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqBindingS : Lean.Expr → Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_congr_perm : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (v : ι → M)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (σ : Equiv.Perm ι), g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ)
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.Polynomial.exists_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f' : (i j : ι) → i ≤ j → G i →+* G j} [Nonempty ι] [IsDirectedOrder ι]
  (q : Polynomial (Ring.DirectLimit G fun i j h => ⇑(f' i j h))),
  ∃ i p, Polynomial.map (Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i) p = q
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapAddMon_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapAddMon.counitIso =
    CategoryTheory.Functor.mapAddMonCompIso.symm ≪≫
      CategoryTheory.Functor.mapAddMonNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapAddMonIdIso
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Polynomial.Chebyshev.sumZeroes_smul : ∀ (n : ℕ) (c : ℝ) (P : Polynomial ℝ), Polynomial.Chebyshev.sumZeroes n (c • P) = c * Polynomial.Chebyshev.sumZeroes n P
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.lifts_iff_coeffs_subset_range : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} (p : Polynomial S),
  p ∈ Polynomial.lifts f ↔ ↑p.coeffs ⊆ Set.range ⇑f
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j),
  (E.toSaturateOfHasPullbacks.s₁ k).obj = CategoryTheory.Limits.pullback (E.f i) (E.f j)
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorLeft_apply_tmul_apply : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) {α : Type w'} [inst_6 : DecidableEq α] (f : α →₀ V) (w : W) (i : α),
  ((σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w)) i = f i ⊗ₜ[k] w
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_l_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] {X Y : C} (f : X ⟶ Y)
  (hf : W f) (g : X ⟶ Z) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.ιLeft f hf g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.l W Z) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_le_ediam : ∀ {α : Type u_1} {G : SimpleGraph α} {u : α}, G.eccent u ≤ G.ediam
-- Init.Data.Int.Order
Int.max_eq_left : ∀ {a b : ℤ}, b ≤ a → max a b = a
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
/-- A `1`-approximate subgroup is the same thing as a subgroup.  -/
isApproximateSubgroup_one : ∀ {G : Type u_1} [inst : Group G] {A : Set G}, IsApproximateSubgroup 1 A ↔ ∃ H, ↑H = A
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const.opObjOp_hom_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) (x : Jᵒᵖ),
  (CategoryTheory.Functor.const.opObjOp X).hom.app x =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X)).obj x)