mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- If `{Uᵢ}` covers `X`, the pre-`0`-hypercover `{Uᵢ ×[Z] Y}` of `X ×[Z] Y` is isomorphic
to the pullback of `{Uᵢ}` along the first projection.  -/
CategoryTheory.PreZeroHypercover.pullbackCoverOfLeftIsoPullback₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      (E : CategoryTheory.PreZeroHypercover X) →
        {Y Z : C} →
          (f : X ⟶ Z) →
            (g : Y ⟶ Z) →
              [inst_1 : CategoryTheory.Limits.HasPullback f g] →
                [inst_2 :
                    ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.fst f g) (E.f i)] →
                  [inst_3 :
                      ∀ (i : E.I₀),
                        CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] →
                    E.pullbackCoverOfLeft f g ≅
                      CategoryTheory.PreZeroHypercover.pullback₁ (CategoryTheory.Limits.pullback.fst f g) E
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.smulAntidiagonal_mono_right : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s : Set G} {t v : Set P} (a : P)
  (hst : (s.smulAntidiagonal t a).Finite) (hsv : (s.smulAntidiagonal v a).Finite),
  v ⊆ t → Finset.SMulAntidiagonal a hsv ⊆ Finset.SMulAntidiagonal a hst
-- Init.Data.List.Lemmas
List.getElem_tail : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i < l.tail.length), l.tail[i] = l[i + 1]
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsDecompositionField.algebraMap_ringEquiv_symm_apply : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (D : Type u_5) [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (D' : Type u_8) [inst_7 : Field D'] [inst_8 : Algebra D' L]
  [inst_9 : IsDecompositionField K L P D] [inst_10 : IsDecompositionField K L P D'] (x : D'),
  (algebraMap D L) ((IsDecompositionField.ringEquiv K L P D D').symm x) = (algebraMap D' L) x
-- Lean.Data.Position
Lean.instInhabitedPosition.default : Lean.Position
-- Mathlib.NumberTheory.NumberField.House
NumberField.one_le_house_of_isIntegral : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {α : K}, IsIntegral ℤ α → α ≠ 0 → 1 ≤ NumberField.house α
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.isIso_lanAdjunction_counit_app_iff : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  (G : CategoryTheory.Functor D H),
  CategoryTheory.IsIso ((L.lanAdjunction H).counit.app G) ↔
    G.IsLeftKanExtension (CategoryTheory.CategoryStruct.id (L.comp G))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi : ∀ {θ ψ : Real.Angle}, 2 • θ + 2 • ψ = ↑Real.pi → |θ.cos| = |ψ.sin|
-- Init.Data.Int.DivMod.Bootstrap
Int.add_emod_emod : ∀ (m n k : ℤ), (m + n % k) % k = (m + n) % k
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparison_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.snd =
    F.map CategoryTheory.Limits.prod.snd
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instReprMRefinePat.repr : Lean.Parser.Tactic.MRefinePat → ℕ → Std.Format
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.ext : ∀ {V : Type u_1} {M : Type u_2} {inst : SMul M V} {S : Type u_3} {_ι : S → M} {x y : Quiver.SchreierGraph V _ι},
  x.toVertex = y.toVertex → x = y
-- Mathlib.Algebra.Order.Ring.Abs
abs_lt_of_sq_lt_sq : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a ^ 2 < b ^ 2 → 0 ≤ b → |a| < b
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_σ_of_gt'_assoc : ∀ {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : SimplexCategory} (h : { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) h) =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (j.castLT ⋯))
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (i.pred ⋯)) h)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mk.congr_simp : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (carrier carrier_1 : Set M) (e_carrier : carrier = carrier_1)
  (smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier)
  (add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier),
  { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' } =
    { carrier := carrier_1, smul_mem' := ⋯, add_mem' := ⋯ }
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The discriminant of a quadratic form `Q : QuadraticForm R N` generalizes the discriminant
of a quadratic polynomial.  -/
QuadraticForm.discr : {R : Type u_3} →
  {N : Type u_5} →
    {n : Type w} →
      [Fintype n] →
        [DecidableEq n] →
          [inst : CommRing R] →
            [Invertible 2] →
              [inst_2 : AddCommGroup N] → [inst_3 : Module R N] → Module.Basis n R N → QuadraticForm R N → R
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.fst_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (self : A × B), (ContinuousMonoidHom.fst A B) self = self.1
-- Lean.Elab.DocString
Lean.Doc.CodeSuggestion.mk.inj : ∀ {role : Lean.Name} {args moreInfo : Option String} {role_1 : Lean.Name} {args_1 moreInfo_1 : Option String},
  { role := role, args := args, moreInfo := moreInfo } = { role := role_1, args := args_1, moreInfo := moreInfo_1 } →
    role = role_1 ∧ args = args_1 ∧ moreInfo = moreInfo_1
-- Mathlib.Algebra.RingQuot
/-- The `natCast` function for `RingQuot`.  -/
RingQuot.natCast : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → ℕ → RingQuot r
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The volume on the real line (as a particular case of the volume on a finite-dimensional
inner product space) coincides with the Stieltjes measure coming from the identity function.  -/
Real.volume_eq_stieltjes_id : MeasureTheory.volume = StieltjesFunction.id.measure
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.biInter_mem : ∀ {α : Type u_1} {C : Set (Set α)} {ι : Type u_2},
  MeasureTheory.IsSetRing C → ∀ {s : ι → Set α} (S : Finset ι), S.Nonempty → (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
-- Mathlib.Data.PFunctor.Multivariate.W
_private.Mathlib.Data.PFunctor.Multivariate.W.0.MvPFunctor.wMk'.match_1.splitter : {n : ℕ} →
  (P : MvPFunctor.{u_1} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      (motive : ↑P (α ::: P.W α) → Sort u_2) →
        (x : ↑P (α ::: P.W α)) → ((a : P.A) → (f : (P.B a).Arrow (α ::: P.W α)) → motive ⟨a, f⟩) → motive x
-- Mathlib.Data.Finset.Defs
Finset.wellFoundedLT : ∀ {α : Type u_1}, WellFoundedLT (Finset α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.CommRing.EqCnstr) →
      ((t : Lean.Meta.Grind.Arith.CommRing.EqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) → t.below → motive_2 t) → motive_1 t ×' t.below
-- Mathlib.GroupTheory.FreeGroup.Orbit
FreeGroup.startsWith.Injective : ∀ {α : Type u_1} [inst : DecidableEq α], Function.Injective FreeGroup.startsWith
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_mono_left : ∀ {α : Type u} [inst : CompleteLattice α], Monotone OrdinalApprox.gfpApprox
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.inf_subgroupOf_right : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), (H ⊓ K).subgroupOf K = H.subgroupOf K
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNormedAlgebra : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [inst_1 : CompactSpace α] →
      {𝕜 : Type u_4} →
        {γ : Type u_5} →
          [inst_2 : NormedField 𝕜] → [inst_3 : SeminormedRing γ] → [NormedAlgebra 𝕜 γ] → NormedAlgebra 𝕜 C(α, γ)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The connecting homomorphism from `t.eTruncGE` to the
shift by `1` of `t.eTruncLT`.  -/
CategoryTheory.Triangulated.TStructure.eTruncGEδLT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                t.eTruncGE ⟶
                  t.eTruncLT.comp ((CategoryTheory.Functor.whiskeringRight C C C).obj (CategoryTheory.shiftFunctor C 1))
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`.  -/
Subgroup.map_injective_of_ker_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) {H K : Subgroup G},
  f.ker ≤ H → f.ker ≤ K → Subgroup.map f H = Subgroup.map f K → H = K
-- Init.Data.Array.Find
Array.findFinIdx?_eq_some_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {i : Fin xs.size},
  Array.findFinIdx? p xs = some i ↔ p xs[i] = true ∧ ∀ (j : Fin xs.size) (hji : j < i), ¬p xs[j] = true
-- Mathlib.Topology.MetricSpace.Polish
TopologicalSpace.Opens.CompleteCopy.dist_val_le_dist : ∀ {α : Type u_1} [inst : MetricSpace α] {s : TopologicalSpace.Opens α} (x y : s.CompleteCopy), dist ↑x ↑y ≤ dist x y
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.instIsComm𝔾ₐ : ∀ {R : Type u_1} [inst : CommRing R], FormalGroup.𝔾ₐ.IsComm
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.binaryProductLimitCone_isLimit_lift : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair M N)),
  (M.binaryProductLimitCone N).isLimit.lift s =
    ModuleCat.ofHom
      ((ModuleCat.Hom.hom (s.π.app { as := CategoryTheory.Limits.WalkingPair.left })).prod
        (ModuleCat.Hom.hom (s.π.app { as := CategoryTheory.Limits.WalkingPair.right })))
-- Mathlib.Combinatorics.Additive.Energy
/-- The multiplicative energy of a finset `s` in a group is the number of quadruples
`(a₁, a₂, b₁, b₂) ∈ s × s × s × s` such that `a₁ * b₁ = a₂ * b₂`.  -/
Combinatorics.Additive.«termEₘ[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Equiv
/-- An equivalence of algebras (denoted as `A ≃ₐ[R] B`)
is an equivalence of rings commuting with the actions of scalars.  -/
«term_≃ₐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.Full.mapMon : ∀ {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} [inst_4 : F.Monoidal] [F.Full] [F.Faithful], F.mapMon.Full
-- Mathlib.RingTheory.PowerSeries.Trunc
/-- The `n`th truncation of a formal power series to a polynomial.  -/
PowerSeries.trunc : {R : Type u_1} → [inst : Semiring R] → ℕ → PowerSeries R →ₗ[R] Polynomial R
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.Const.maxEntry! : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap α (fun x => β) cmp → α × β
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_of_injective : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] [IsCyclic G'] (f : G →* G'),
  Function.Injective ⇑f → IsCyclic G
-- Mathlib.GroupTheory.HNNExtension
/-- The transversal of each subgroup  -/
HNNExtension.NormalWord.TransversalPair.set : {G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → HNNExtension.NormalWord.TransversalPair G A B → ℤˣ → Set G
-- Mathlib.Combinatorics.Graph.Basic
Graph.banana_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} {x u v : α} {e : β} {edgeSet : Set β},
  (Graph.banana u v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = u ∧ u = v
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.span_mono : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {s t : Set R}, s ⊆ t → TwoSidedIdeal.span s ≤ TwoSidedIdeal.span t
-- Mathlib.Algebra.Group.Prod
MulHom.comp_coprod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : CommSemigroup P] {Q : Type u_6}
  [inst_3 : CommSemigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P),
  h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_mod : ∀ {a b : ℕ} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32), UInt32.ofNatLT (a % b) ⋯ = UInt32.ofNatLT a ha % UInt32.ofNatLT b hb
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).op
      (CategoryTheory.Limits.colimitRightOpIsoUnopLimit F).inv =
    CategoryTheory.Limits.colimit.ι F.rightOp (Opposite.unop j)
-- Batteries.Util.Pickle
pickle.unsafe_1 : {α : Type} → α → Lean.ModuleData
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux.eq_1 : ∀ (b : ℕ) (h : 2 ≤ b), b.digitsAux h 0 = []
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w)
  (curr : ℕ) (acc : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs curr acc =
    if h : curr < w then
      if aig.isConstant (rhs.get curr h) false = true then
        Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs (curr + 1) acc
      else
        let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst aig { vec := lhs, distance := curr };
        let aig_1 := res.aig;
        let shifted := res.vec;
        have this := ⋯;
        have lhs_1 := lhs.cast this;
        let rhs_1 := rhs.cast this;
        let acc_1 := acc.cast this;
        let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd aig_1 { lhs := acc_1, rhs := shifted };
        let aig_2 := res.aig;
        let added := res.vec;
        have this_1 := ⋯;
        have lhs_2 := lhs_1.cast this_1;
        let rhs_2 := rhs_1.cast this_1;
        let acc_2 := acc_1.cast this_1;
        let res := Std.Sat.AIG.RefVec.ite aig_2 { discr := rhs_2.get curr h, lhs := added, rhs := acc_2 };
        let aig_3 := res.aig;
        have acc_3 := res.vec;
        have this := ⋯;
        have lhs := lhs_2.cast this;
        have rhs := rhs_2.cast this;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig_3 lhs rhs (curr + 1) acc_3
    else { aig := aig, vec := acc }
-- Init.Data.BitVec.Lemmas
/-- Sign extending to the same bitwidth is a no op.  -/
BitVec.signExtend_eq : ∀ {w : ℕ} (x : BitVec w), BitVec.signExtend w x = x
-- Init.Data.List.Basic
List.replicateTR_loop_replicate_eq : ∀ {α : Type u} {a : α} {m n : ℕ}, List.replicateTR.loop a n (List.replicate m a) = List.replicate (n + m) a
-- Mathlib.Data.Set.NAry
Set.image2_range : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} (f : α' → β' → γ) (g : α → α')
  (h : β → β'), Set.image2 f (Set.range g) (Set.range h) = Set.range fun x => f (g x.1) (h x.2)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.equivOfIsUnitDet.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] {f : M →ₗ[R] M} (h : IsUnit (LinearMap.det f)),
  LinearMap.equivOfIsUnitDet h =
    if hR : Nontrivial R then
      match ⋯.some with
      | ⟨ι, b⟩ =>
        have this := ⋯;
        have this := Fintype.ofFinite ι;
        have this_1 := Classical.typeDecidableEq ι;
        LinearEquiv.ofIsUnitDet ⋯
    else 1
-- Mathlib.CategoryTheory.Abelian.Basic
/-- In an abelian category, an epi is the cokernel of its kernel. More precisely:
If `f` is an epimorphism and `s` is some limit kernel cone on `f`, then `f` is a cokernel
of `fork.ι s`.  -/
CategoryTheory.Abelian.epiIsCokernelOfKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.Epi f] →
            (s : CategoryTheory.Limits.Fork f 0) →
              CategoryTheory.Limits.IsLimit s →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul_nc.go.induct_unfolding : ∀ (p₂ : Lean.Grind.CommRing.Poly)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k) acc (acc.combine (Lean.Grind.CommRing.Poly.mulConst k p₂))) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (acc.combine (Lean.Grind.CommRing.Poly.mulMon_nc k m p₂))
            (Lean.Grind.CommRing.Poly.mul_nc.go p₂ p (acc.combine (Lean.Grind.CommRing.Poly.mulMon_nc k m p₂))) →
          motive (Lean.Grind.CommRing.Poly.add k m p) acc
            (Lean.Grind.CommRing.Poly.mul_nc.go p₂ p (acc.combine (Lean.Grind.CommRing.Poly.mulMon_nc k m p₂)))) →
      ∀ (p₁ acc : Lean.Grind.CommRing.Poly), motive p₁ acc (Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ acc)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instMulZeroClassOfContinuousMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : MulZeroClass β] → [ContinuousMul β] → MulZeroClass (CompactlySupportedContinuousMap α β)
-- Mathlib.Data.Seq.Computation
Computation.LiftRelAux.ret_right : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (b : β) (ca : Computation α),
  Computation.LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ a ∈ ca, R a b
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.AtomIso.src : Mathlib.Tactic.BicategoryLike.AtomIso → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∏ j ∈ s, f j) (f i) κ μ
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.instIsIPCOfShapeOfIsIPCOfSmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
  [inst_2 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v_1, u_1} C] [CategoryTheory.Limits.IsIPC C]
  (ι : Type u_3) [Small.{w, u_3} ι] [inst_5 : CategoryTheory.Limits.HasProductsOfShape ι C],
  CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_1, u_1} ι C
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_norm_poly : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote' ctx p = Int.Internal.Linear.Poly.denote' ctx p' →
    Int.Internal.Linear.Poly.denote' ctx p = 0 → Int.Internal.Linear.Poly.denote' ctx p' = 0
-- Mathlib.Algebra.Lie.CartanSubalgebra
/-- Given a Lie module `M` of a Lie algebra `L`, `LieSubmodule.IsUcsLimit` is the proposition
that a Lie submodule `N ⊆ M` is the limiting value for the upper central series.

This is a characteristic property of Cartan subalgebras with the roles of `L`, `M`, `N` played by
`H`, `L`, `H`, respectively. See `LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit`.  -/
LieSubmodule.IsUcsLimit : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {M : Type u_1} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → LieSubmodule R L M → Prop
-- Mathlib.Topology.Instances.Irrational
Irrational.instNoMaxOrderSubtypeReal : NoMaxOrder { x // Irrational x }
-- Init.Data.Float.Float
instDecidableEqFloat.decEq : (x x_1 : Float) → Decidable (x = x_1)
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `p` is a formal multilinear series such that `p m = 0` for `n ≤ m`, then
`p.changeOriginSeriesTerm k l = 0` for `n ≤ k + l`.  -/
FormalMultilinearSeries.changeOriginSeriesTerm_bound : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
  (∀ (m : ℕ), n ≤ m → p m = 0) →
    ∀ (k l : ℕ) {s : Finset (Fin (k + l))} (hs : s.card = l), n ≤ k + l → p.changeOriginSeriesTerm k l s hs = 0
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.isMulCommutative_adjoin_singleton : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (a : A) [IsStarNormal a], IsMulCommutative ↥(NonUnitalStarAlgebra.adjoin R {a})
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- (Colimit) cofork which gives a presentation of a presheaf of modules `M` using
coproducts of free presheaves of modules on Yoneda presheaves.  -/
PresheafOfModules.freeYonedaCoproductsCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : PresheafOfModules R) → CategoryTheory.Limits.CokernelCofork M.toFreeYonedaCoproduct