mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- The subfunctor associated to a functor of submonoids.  -/
CategoryTheory.SubmonoidFunctor.toSubfunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} →
      CategoryTheory.SubmonoidFunctor M → CategoryTheory.Subfunctor (M.comp (CategoryTheory.forget MonCat))
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
/-- Given a family of elements of an additive monoid, a member is said
to be indecomposable if it cannot be written as a sum of two others in a non-trivial way. -/
IsAddIndecomposable : {ι : Type u_1} → {M : Type u_2} → [AddMonoid M] → (ι → M) → Set ι → ι → Prop
-- Init.Data.List.Nat.Modify
List.getElem?_modifyHead_succ : ∀ {α : Type u_1} {l : List α} {f : α → α} {n : ℕ}, (List.modifyHead f l)[n + 1]? = l[n + 1]?
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k : α} {f : β → β} {hc : k ∈ t.modify k f}, (t.modify k f).getKey k hc = k
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleighQuotient_apply_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), T.rayleighQuotient 0 = 0
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.pow_period_add_smul : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (n : ℕ) (m : M) (a : α),
  m ^ (MulAction.period m a + n) • a = m ^ n • a
-- Mathlib.Data.Seq.Basic
Stream'.Seq.instLawfulFunctor : LawfulFunctor Stream'.Seq
-- Mathlib.Analysis.MellinTransform
hasMellin_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℝ → E} {s : ℂ},
  MellinConvergent f s → MellinConvergent g s → HasMellin (fun t => f t + g t) s (mellin f s + mellin g s)
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
IsOpenMap.coverPreserving : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)),
  CategoryTheory.CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) hf.functor
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_ofSliceTo : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : String.Slice.Pos.ofSliceTo p ≠ s.startPos},
  (String.Slice.Pos.ofSliceTo p).prev h = String.Slice.Pos.ofSliceTo (p.prev ⋯)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N} {S : AddSubsemigroup M} {y : N},
  y ∈ AddSubsemigroup.map f S ↔ ∃ x ∈ S, f x = y
-- Mathlib.Data.TwoPointing
TwoPointing.prod_snd : ∀ {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β), (p.prod q).toProd.2 = (p.toProd.2, q.toProd.2)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.uniformContinuous_closure : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous TopologicalSpace.Closeds.closure
-- Init.Data.Int.Gcd
Int.gcd_mul_right_left : ∀ (a b : ℤ), (b * a).gcd b = b.natAbs
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, (p * Polynomial.X ^ n).leadingCoeff = p.leadingCoeff
-- Lean.Meta.Tactic.Grind.Arith.Linear.Model
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Model.0.Lean.Meta.Grind.Arith.Linear.toQ? : Lean.Expr → Option Lean.Expr
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.right_notMem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → y ∉ s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)} {h : k' ∈ m.alter k f},
  (m.alter k f).get k' h = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The trivial continuous representation of a group `G` on a `R`-module `V`.  -/
ContRepresentation.trivial : (R : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] → [inst_5 : Module R V] → ContRepresentation R G V
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.mk : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsPathGraph3Compl v w₁ w₂ →
    v ∉ s →
      v ∉ t →
        w₁ ∉ s →
          w₂ ∉ t →
            G.IsNClique (r + 1) (insert v s) →
              G.IsNClique (r + 1) (insert w₁ s) →
                G.IsNClique (r + 1) (insert v t) →
                  G.IsNClique (r + 1) (insert w₂ t) → (s ∩ t).card = k → G.IsFiveWheelLike r k v w₁ w₂ s t
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.forall : Mathlib.Tactic.Push.Head
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- `true` if we require that each tag belongs to its own closed
box; the value `false` means that we only require that tags belong to the ambient box.  -/
BoxIntegral.IntegrationParams.bHenstock : BoxIntegral.IntegrationParams → Bool
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedMul.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [toExistsMulOfLE : ExistsMulOfLE α],
  (∀ (a b : α), a ≤ b * a) → (∀ (a b : α), a ≤ a * b) → CanonicallyOrderedMul α
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.objectEnd.sizeOf_spec : sizeOf Lean.Json.CompressWorkItemKind.objectEnd✝ = 1
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.instCategoryMatOfSemiring : (R : Type u) → [Semiring R] → CategoryTheory.Category.{u, u + 1} (CategoryTheory.Mat R)
-- Mathlib.RingTheory.PrincipalIdealDomain
DivisionSemiring.isPrincipalIdealRing : ∀ (K : Type u) [inst : DivisionSemiring K], IsPrincipalIdealRing K
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_pos_of_isNNRat : ∀ {e : ℝ} {d n : ℕ}, Mathlib.Meta.NormNum.IsNNRat e n d → decide (1 < ↑n / ↑d) = true → 0 < Real.log e
-- Std.Data.HashSet.Lemmas
Std.HashSet.any_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulHashable α] [EquivBEq α] {p : α → Bool},
  m.toList.any p = m.any p
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosure_of_normal : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] (K : IntermediateField F L)
  [Normal F ↥K], IntermediateField.normalClosure F (↥K) L = K
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceAddOpposite.eq_1 : ∀ {α : Type ua} [inst : UniformSpace α], instUniformSpaceAddOpposite = UniformSpace.comap AddOpposite.unop inst
-- Mathlib.Algebra.Group.Torsion
self_eq_inv : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {a : G}, a = a⁻¹ ↔ a = 1
-- Mathlib.RepresentationTheory.Intertwining
/-- If `z` is a central element of the monoid algebra `A[G]`, then this is the action of `z`,
considered as an intertwining map from any representation of `G` to itself.  -/
Representation.IntertwiningMap.centralAlgebraMul : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] →
              (ρ : Representation A G V) →
                {z : MonoidAlgebra A G} → z ∈ Submonoid.center (MonoidAlgebra A G) → ρ.IntertwiningMap ρ
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.eval₂_one_cyclotomic_prime : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Semiring S] (f : R →+* S) {p : ℕ} [Fact (Nat.Prime p)],
  Polynomial.eval₂ f 1 (Polynomial.cyclotomic p R) = ↑p
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side.  -/
InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y = 0 → Real.tan (InnerProductGeometry.angle x (x + y)) * ‖x‖ = ‖y‖
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P]
  {Φ :
    CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂})}
  (f g :
    CategoryTheory.Functor.LeftExtension.mk F.op.lan
        (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶
      Φ),
  f = g
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The angle between two nonzero vectors is `θ` if and only if the second vector is the first
rotated by `θ` and scaled by the ratio of the norms.  -/
Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • (o.rotation θ) x
-- Mathlib.Algebra.Order.Group.Synonym
isLeftRegular_ofColex : ∀ {α : Type u_1} [inst : Monoid α] {a : Colex α}, IsLeftRegular (ofColex a) ↔ IsLeftRegular a
-- Lean.Meta.Canonicalizer
/-- Given a hashcode `k` and `keyToExprs.find? h = some es`, we have that all `es` have hashcode `k`, and
are not definitionally equal modulo the transparency setting used.  -/
Lean.Meta.Canonicalizer.State.keyToExprs : Lean.Meta.Canonicalizer.State → Std.HashMap UInt64 (List Lean.Expr)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyπ_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.isoHomologyπ i j hi h).inv =
    CategoryTheory.CategoryStruct.id (K.cycles j)
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.paramNames : Lean.MetavarContext.LevelMVarToParam.State → Array Lean.Name
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
homeomorphSphereProd.congr_simp : ∀ (E : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (r : ℝ) (hr : 0 < r),
  homeomorphSphereProd E r hr = homeomorphSphereProd E r hr
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toMulEquiv_eq_coe : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (f : R ≃+* S),
  f.toMulEquiv = ↑f
-- Mathlib.Probability.Process.Stopping
MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [hf : f.IsRightContinuous],
  (∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}) →
    (∀ (i : ι), nhdsWithin i (Set.Ioi i) = ⊥ → MeasurableSet {ω | τ ω = ↑i}) → MeasureTheory.IsStoppingTime f τ
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.ofIso.eq_1 : ∀ {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.MonoidalLeftAction C D]
  {M : C} [inst_4 : CategoryTheory.AddMonObj M] {X : D} {N : C} [inst_5 : CategoryTheory.AddMonObj N] (e₁ : M ≅ N)
  [inst_6 : CategoryTheory.IsAddMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [inst_7 : CategoryTheory.AddModObj M X],
  CategoryTheory.AddModObj.ofIso e₁ e₂ =
    {
      vadd :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom e₁.inv e₂.inv)
          (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd e₂.hom),
      zero_vadd := ⋯, add_vadd := ⋯ }
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- A multilinear map is additive in every argument.  -/
MultilinearMap.map_update_add' : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (self : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι)
  (x y : M₁ i),
  self.toFun (Function.update m i (x + y)) = self.toFun (Function.update m i x) + self.toFun (Function.update m i y)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (r : A), ↑(ProjectiveSpectrum.basicOpen 𝒜 r) = (ProjectiveSpectrum.zeroLocus 𝒜 {r})ᶜ
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.c_mem_support : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], c ∈ Function.support ↑f
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Construct a new tree with one element `v`.  -/
RBTree.RBSet.single : {α : Type u_1} → {cmp : α → α → Ordering} → α → RBTree.RBSet α cmp
-- Init.MetaTypes
/-- The maximum number of subexpressions to visit when performing simplification.
The default is 100000.
 -/
Lean.Meta.Simp.Config.maxSteps : Lean.Meta.Simp.Config → ℕ
-- Mathlib.Order.CompleteBooleanAlgebra
iInf_sup_of_antitone : ∀ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} [inst_1 : Preorder ι] [IsDirectedOrder ι] {f g : ι → α},
  Antitone f → Antitone g → ⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i
-- Mathlib.Data.Seq.Basic
Stream'.Seq.ofStream_cons : ∀ {α : Type u} (a : α) (s : Stream' α), ↑(Stream'.cons a s) = Stream'.Seq.cons a ↑s
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.Scheme.IsGermInjective.Spec : ∀ {R : CommRingCat},
  (∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0) →
    (AlgebraicGeometry.Spec R).IsGermInjective
-- Mathlib.Data.Finset.Insert
Finset.instUniqueOfIsEmpty : {α : Type u_1} → [IsEmpty α] → Unique (Finset α)
-- Lean.Compiler.LCNF.Types
/-- `uint8` is an 8-bit unsigned integer.
 -/
Lean.Compiler.LCNF.ImpureType.uint8 : Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.induce_mono_right : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s s' : Set V}, s ⊆ s' → G'.induce s ≤ G'.induce s'
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_functor_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} (t : CategoryTheory.Limits.Cone K),
  (CategoryTheory.WithTerminal.coneEquiv.functor.obj t).pt = t.pt.left
-- Mathlib.Condensed.TopComparison
topCatToSheafCompHausLike_map_hom_app : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  {X Y : TopCat} (f : X ⟶ Y) (x : (CompHausLike P)ᵒᵖ),
  ((topCatToSheafCompHausLike P hs).map f).hom.app x = TypeCat.ofHom fun g => (TopCat.Hom.hom f).comp g
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combineC.eq_def : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly) (c : ℕ),
  p₁.combineC p₂ c =
    match p₁, p₂ with
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => Lean.Grind.CommRing.Poly.num ((k₁ + k₂) % ↑c)
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ =>
      (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂).addConstC k₁ c
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ =>
      (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁).addConstC k₂ c
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ =>
      match m₁.grevlex m₂ with
      | Ordering.eq =>
        have k := (k₁ + k₂) % ↑c;
        bif k == 0 then p₁.combineC p₂ c else Lean.Grind.CommRing.Poly.add k m₁ (p₁.combineC p₂ c)
      | Ordering.gt => Lean.Grind.CommRing.Poly.add k₁ m₁ (p₁.combineC (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂) c)
      | Ordering.lt => Lean.Grind.CommRing.Poly.add k₂ m₂ ((Lean.Grind.CommRing.Poly.add k₁ m₁ p₁).combineC p₂ c)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.cofibration_unop_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  {X Y : Cᵒᵖ} (f : X ⟶ Y), HomotopicalAlgebra.Cofibration f.unop ↔ HomotopicalAlgebra.Fibration f
-- Init.GrindInstances.Ring.Rat
Lean.Grind.instFieldRat : Lean.Grind.Field ℚ
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Nat.isLinearSet_iff_exists_matrix : ∀ {ι : Type u_3} {s : Set (ι → ℕ)}, IsLinearSet s ↔ ∃ v n A, s = {x | ∃ x_1, v + A.mulVec x_1 = x}
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.zpow_apply : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : Group N] (f : OneHom M N) (z : ℤ) (x : M), (f ^ z) x = f x ^ z
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  MonCat.FilteredColimits.colimitCoconeIsColimit F =
    { desc := MonCat.FilteredColimits.colimitDesc F, fac := ⋯, uniq := ⋯ }
-- Mathlib.Data.Sum.Order
Sum.inr_lt_inr_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : β}, Sum.inr a < Sum.inr b ↔ a < b
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_rid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {N' : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N'] (f : N →ₗ[R] N')
  (g : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.assoc R M R N') ∘ₗ TensorProduct.map (↑(TensorProduct.rid R M).symm) f ∘ₗ g =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R N).symm) ∘ₗ g
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comapₗ_apply : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {x : MeasurableSpace α} {x_1 : MeasurableSpace β} (f : α → β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) →
      ∀ (μ : MeasureTheory.Measure β), MeasurableSet s → ((MeasureTheory.Measure.comapₗ f) μ) s = μ (f '' s)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.maxValueSealed : Int32
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) {X_1 Y : SimplexCategoryᵒᵖ}
  (f : X_1 ⟶ Y),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.obj X).left.map f =
    X.map
      (match CategoryTheory.WithTerminal.incl.obj X_1, CategoryTheory.WithTerminal.incl.obj Y,
        CategoryTheory.WithTerminal.incl.map f with
      | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f =>
        CategoryTheory.WithInitial.down f
      | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x =>
        Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop))
      | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
        CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star))
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The space of affine maps taking values in an `R`-module is an `R`-module.  -/
AffineMap.instModule : {R : Type u_1} →
  {k : Type u_2} →
    {V1 : Type u_3} →
      {P1 : Type u_4} →
        {V2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : AddTorsor V1 P1] →
                [inst_3 : AddCommGroup V2] →
                  [inst_4 : Module k V1] →
                    [inst_5 : Module k V2] →
                      [inst_6 : Semiring R] → [inst_7 : Module R V2] → [SMulCommClass k R V2] → Module R (P1 →ᵃ[k] V2)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.Sign.minus : {v : Lean.Level} → {M : Q(Type v)} → Q(Field «$M») → Mathlib.Tactic.FieldSimp.Sign M
-- Lean.Meta.DiscrTree.Util
/-- Monadically fold over the values stored in a `DiscrTree`.
 -/
Lean.Meta.DiscrTree.foldValuesM : {m : Type u_1 → Type u_2} → {σ : Type u_1} → {α : Type} → [Monad m] → (σ → α → m σ) → σ → Lean.Meta.DiscrTree α → m σ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonFunctor_obj : ∀ (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.LaxMonoidalFunctor C D), (CategoryTheory.Functor.mapMonFunctor C D).obj F = F.mapMon
-- Mathlib.Algebra.Field.ULift
ULift.instRatCast : {α : Type u} → [RatCast α] → RatCast (ULift.{u_1, u} α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_div_thirty_two : Real.cos (Real.pi / 32) = √(2 + √(2 + √(2 + √2))) / 2
-- Mathlib.Algebra.Order.Group.Indicator
Function.support_sup : ∀ {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SemilatticeSup M] (f g : α → M),
  (Function.support fun x => f x ⊔ g x) ⊆ Function.support f ∪ Function.support g
-- Mathlib.RingTheory.Extension.Generators
/-- The extension `R[X₁,...,Xₙ] → S` given a family of generators.  -/
Algebra.Generators.toExtension : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Generators R S ι → Algebra.Extension R S
-- Init.Core
instDecidableIte : {c t e : Prop} → [dC : Decidable c] → [dT : Decidable t] → [dE : Decidable e] → Decidable (if c then t else e)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.inr_le_iff : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a b : A),
  autoParam (IsSelfAdjoint a) Unitization.inr_le_iff._auto_1 →
    autoParam (IsSelfAdjoint b) Unitization.inr_le_iff._auto_3 → (↑a ≤ ↑b ↔ a ≤ b)
-- Std.Time.Date.Unit.Day
Std.Time.Day.instAddOffset : Add Std.Time.Day.Offset
-- Mathlib.Data.Matrix.Mul
Matrix.mul_right_injective_iff_mulVec_injective : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m]
  [Nonempty n] {A : Matrix l m α}, (Function.Injective fun B => A * B) ↔ Function.Injective A.mulVec
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.castAddEmb m) (Finset.Ioc i j) = Finset.Ioc (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_const_pUnitAlgEquiv : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : MvPolynomial PUnit.{u_4 + 1} R}
  {φ : R →+* S} {a : S}, Polynomial.eval₂ φ a ((MvPolynomial.pUnitAlgEquiv R) f) = MvPolynomial.eval₂ φ (fun x => a) f