mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ - f₂` at `x` is the
trailing coefficient of the function with the lowest order.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_left_of_lt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₂ x →
    meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x →
      meromorphicTrailingCoeffAt (f₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x
-- Mathlib.RingTheory.Localization.Away.Lemmas
Ideal.eq_of_map_algebraMap_le : ∀ {R : Type u_2} (S : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S] {I J : Ideal R},
  Ideal.map (algebraMap R S) I = Ideal.map (algebraMap R S) J →
    (∀ (y : R), x * y ∈ I → y ∈ I) → (∀ (y : R), x * y ∈ J → y ∈ J) → I = J
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivWithinAt.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') s x
-- Mathlib.RingTheory.Nilpotent.Defs
IsUnit.isNilpotent_unit_mul_of_commute_iff : ∀ {R : Type u_1} [inst : MonoidWithZero R] {r u : R}, IsUnit u → Commute r u → (IsNilpotent (u * r) ↔ IsNilpotent r)
-- Init.Data.Nat.Lemmas
Nat.mod_two_ne_one : ∀ {n : ℕ}, n % 2 ≠ 1 ↔ n % 2 = 0
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.bornology : {ι : Type u_2} → (p : ENNReal) → (β : ι → Type u_5) → [(i : ι) → Bornology (β i)] → Bornology (PiLp p β)
-- Lean.Server.Utils
/-- Module name corresponding to `uri`.
We store the module name instead of recomputing it as needed to ensure that we can still
determine the original module name even when the file has been deleted in the mean-time.
 -/
Lean.Server.DocumentMeta.mod : Lean.Server.DocumentMeta → Lean.Name
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkIso.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (eₗ eₗ_1 : x.fst ≅ y.fst) (e_eₗ : eₗ = eₗ_1)
  (eᵣ eᵣ_1 : x.snd ≅ y.snd) (e_eᵣ : eᵣ = eᵣ_1)
  (w :
    CategoryTheory.CategoryStruct.comp (F.map eₗ.hom) y.iso.hom =
      CategoryTheory.CategoryStruct.comp x.iso.hom (G.map eᵣ.hom)),
  CategoryTheory.Limits.CategoricalPullback.mkIso eₗ eᵣ w = CategoryTheory.Limits.CategoricalPullback.mkIso eₗ_1 eᵣ_1 ⋯
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Hour.Ordinal n
-- Mathlib.Analysis.Complex.Basic
Complex.exists_norm_mul_eq_self : ∀ (z : ℂ), ∃ c, ‖c‖ = 1 ∧ c * ↑‖z‖ = z
-- Aesop.BaseM
Aesop.BaseM.State.mk.inj : ∀ {rulePatternCache : Aesop.RulePatternCache} {stats : Aesop.Stats} {rulePatternCache_1 : Aesop.RulePatternCache}
  {stats_1 : Aesop.Stats},
  { rulePatternCache := rulePatternCache, stats := stats } =
      { rulePatternCache := rulePatternCache_1, stats := stats_1 } →
    rulePatternCache = rulePatternCache_1 ∧ stats = stats_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcompose_obj_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Limits.Cone.postcompose α).obj c).π = CategoryTheory.CategoryStruct.comp c.π α
-- Mathlib.CategoryTheory.Limits.Final
/-- This is the small version of the more general lemma `Grothendieck.final_map` below.  -/
_private.Mathlib.CategoryTheory.Limits.Final.0.CategoryTheory.Grothendieck.final_map_small : ∀ {C : Type u₁} [inst : CategoryTheory.SmallCategory C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G)
  [hα : ∀ (X : C), (α.app X).toFunctor.Final], (CategoryTheory.Grothendieck.map α).Final
-- Init.Data.UInt.Lemmas
UInt32.ofNat_uSizeToNat : ∀ (n : USize), UInt32.ofNat n.toNat = n.toUInt32
-- Lean.Util.PtrSet
Lean.Ptr.value : {α : Type u} → Lean.Ptr α → α
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.instCategory : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.Category.{w, u} (CategoryTheory.ShrinkHoms.{u} C)
-- Aesop.Util.Basic
Aesop.forEachExprInLCtx' : {ω : Type} →
  {m : Type → Type} →
    [STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] →
          [MonadControlT Lean.MetaM m] → [MonadLiftT Lean.MetaM m] → Lean.MVarId → (Lean.Expr → m Bool) → m Unit
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_X_pow_succ : ∀ {F : Type u_1} [inst : Field F] (d k : ℕ), (Polynomial.X ^ k).hilbertPoly (d + 1) = Polynomial.preHilbertPoly F d k
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.num_pos : ∀ {a : ℚ}, 0 < a.num ↔ 0 < a
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `MulSemiringActionHomClass F M R S` states that `F` is a type of morphisms preserving
the ring structure and equivariant with respect to a `DistribMulAction` of `M` on `R` and `S`.
 -/
MulSemiringActionHomClass : (F : Type u_15) →
  {M : outParam (Type u_16)} →
    [inst : Monoid M] →
      (R : outParam (Type u_17)) →
        (S : outParam (Type u_18)) →
          [inst_1 : Semiring R] →
            [inst_2 : Semiring S] → [DistribMulAction M R] → [DistribMulAction M S] → [FunLike F R S] → Prop
-- Lean.Widget.InteractiveCode
Lean.Widget.CodeWithInfos.pretty : Lean.Widget.CodeWithInfos → String
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filter_||_» : Lean.TrailingParserDescr
-- Mathlib.Topology.UniformSpace.Closeds
monotone_hausdorffEntourage : ∀ {α : Type u_1}, Monotone hausdorffEntourage
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.smul.injEq : ∀ {A : Type u} {M : Type v} (a : A) (m : M) (a_1 : A) (m_1 : M),
  (Module.Presentation.tautological.R.smul a m = Module.Presentation.tautological.R.smul a_1 m_1) = (a = a_1 ∧ m = m_1)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.indepNum_compl : ∀ {α : Type u_3} {G : SimpleGraph α}, Gᶜ.indepNum = G.cliqueNum
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofFin : ∀ {n : Fin UInt8.size}, (UInt8.ofFin n).toUInt16 = UInt16.ofNatLT ↑n ⋯
-- Mathlib.Data.Finsupp.Lex
/-- The partial order on `Finsupp`s obtained by the lexicographic ordering.
See `Finsupp.Lex.linearOrder` for a proof that this partial order is in fact linear.  -/
Finsupp.Lex.partialOrder : {α : Type u_1} → {N : Type u_2} → [inst : Zero N] → [LinearOrder α] → [PartialOrder N] → PartialOrder (Lex (α →₀ N))
-- Mathlib.LinearAlgebra.Projection
Submodule.toLinearMap_symm_quotientEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), ↑(p.quotientEquivOfIsCompl q h).symm = p.mkQ ∘ₗ q.subtype
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of `SimpleGraph.minDegree_of_subsingleton`. -/
SimpleGraph.minDegree_of_isEmpty : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Subsingleton V], G.minDegree = 0
-- Mathlib.Algebra.Free
/-- Length of an element of free semigroup.  -/
FreeSemigroup.length : {α : Type u} → FreeSemigroup α → ℕ
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.preNormEDS'.match_1.eq_5 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : Unit → motive 4) (h_6 : (n : ℕ) → motive n.succ.succ.succ.succ.succ),
  (match 4 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | 4 => h_5 ()
    | n.succ.succ.succ.succ.succ => h_6 n) =
    h_5 ()
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet`.

---

Let `P` be a predicate on `Set J.obj` where `J : CardinalDirectedPoset κ`.
We assume that `Subtype P` is directed and nonempty, and that any `a : J.obj`
belongs to some `S : Set J.obj` satisfying `P`. Then, `J` is the colimit in the
category `CardinalDirectedPoset κ` of these subsets.  -/
CategoryTheory.CardinalFilteredPoset.isColimitCoconeOfPredicateSet : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    {J : CategoryTheory.CardinalDirectedPoset κ} →
      (P : Set ↑J.obj → Prop) →
        [IsDirectedOrder (Subtype P)] →
          [Nonempty (Subtype P)] →
            [inst_3 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] →
              (∀ (a : ↑J.obj), ∃ S, P S ∧ a ∈ S) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet P)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_sup_comap_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup N) (f : G →* N),
  Subgroup.comap f H ⊔ Subgroup.comap f K ≤ Subgroup.comap f (H ⊔ K)
-- Mathlib.Data.Matrix.Basic
Matrix.entryAddHom_apply : ∀ {m : Type u_2} {n : Type u_3} (α : Type u_11) [inst : Add α] (i : m) (j : n) (M : Matrix m n α),
  (Matrix.entryAddHom α i j) M = M i j
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.loopRef.eq_2 : ∀ (x : Lean.Meta.Grind.Action) (goal : Lean.Meta.Grind.Goal) (x_1 kp : Lean.Meta.Grind.ActionCont) (n_2 : ℕ),
  Lean.Meta.Grind.Action.loopRef n_2.succ x goal x_1 kp =
    x goal kp fun goal' => Lean.Meta.Grind.Action.loopRef n_2 x goal' kp kp
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.self_algebra_smul : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (c : MvPolynomial S R)
  (x : S), SMul.smul c x = (MvPolynomial.aeval id).toRingHom c * x
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {M N : CoalgCat R} {f g : M ⟶ N},
  f = g ↔ CoalgCat.Hom.toCoalgHom f = CoalgCat.Hom.toCoalgHom g
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A], Function.Injective NonUnitalStarSubalgebra.toNonUnitalSubalgebra
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.brecOn.go : {α : Type u} →
  {motive : RBTree.RBNode α → Sort u_1} →
    (t : RBTree.RBNode α) →
      ((t : RBTree.RBNode α) → RBTree.RBNode.below t → motive t) → motive t ×' RBTree.RBNode.below t
-- Init.Data.Array.Bootstrap
Array.toList_appendList : ∀ {α : Type u_1} {xs : Array α} {l : List α}, (xs ++ l).toList = xs.toList ++ l
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.sigma' : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α]
  [RegularSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α},
  Summable f → (∀ (b : β), Summable fun c => f ⟨b, c⟩) → Summable fun b => ∑' (c : γ b), f ⟨b, c⟩
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insert! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {k a : α} {v : β},
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.insert! k v t) a =
        if compare k a = Ordering.eq then v else Std.DTreeMap.Internal.Impl.Const.get! t a
-- Mathlib.Analysis.Normed.Group.Continuity
NormedGroup.toENormedMonoid : {F : Type u_7} → [inst : NormedGroup F] → ENormedMonoid F
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Add a single morphism to a `0`-hypercover.  -/
CategoryTheory.Precoverage.ZeroHypercover.add : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} →
        (E : J.ZeroHypercover S) →
          {T : C} → (f : T ⟶ S) → E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S → J.ZeroHypercover S
-- Init.Data.List.Nat.InsertIdx
List.length_le_length_insertIdx : ∀ {α : Type u} {l : List α} {x : α} {i : ℕ}, l.length ≤ (l.insertIdx i x).length
-- Mathlib.LinearAlgebra.Matrix.WithConv
instRingWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [Ring α] → Ring (WithConv (Matrix m n α))
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearEquiv.flip.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e e_1 : N ≃ₗ[R] Module.Dual R M),
  e = e_1 → e.flip = e_1.flip
-- Aesop.Tree.Check
Aesop.checkInvariantsIfEnabled : Aesop.TreeM Unit
-- Lean.Meta.StringLitProof
/-- Builds a proof of `String.ofList l₁ ≠ String.ofList l₂` for two distinct string literals.

The proof avoids both `String.decEq` (expensive UTF-8 byte array comparison) and full
`List Char` comparison. It reduces to `List Char` via `String.ofList_injective`, then
proves the lists differ using one of two strategies depending on whether the strings
share a common prefix of the shorter string's full length:

- **Different characters at position `i`**: Uses
  `congrArg (fun l => (List.get!Internal l i).toNat)` to project down to `Nat`, then
  `Nat.ne_of_beq_eq_false rfl` for a single `Nat.beq` comparison. This avoids `Decidable`
  instances entirely — the kernel only evaluates `Nat.beq` on two concrete natural numbers.

- **One string is a prefix of the other**: Uses `congrArg (List.drop n ·)` where `n` is the
  shorter string's length, then `List.cons_ne_nil` to prove the non-empty tail differs from `[]`.
  This avoids `decide` entirely since `cons_ne_nil` is a definitional proof.
 -/
Lean.Meta.mkStringLitNeProof : String → String → Lean.MetaM Lean.Expr
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_le_packingNumber : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.coveringNumber ε A ≤ Metric.packingNumber ε A
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitForward_counitBackward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
  (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A),
  CategoryTheory.OverPresheafAux.counitForward F s ∘ CategoryTheory.OverPresheafAux.counitBackward F s = id
-- Mathlib.Algebra.Order.Kleene
Pi.instIdemSemiring : {ι : Type u_3} → {π : ι → Type u_4} → [(i : ι) → IdemSemiring (π i)] → IdemSemiring ((i : ι) → π i)
-- Init.Data.List.Lemmas
List.getD_cons_zero : ∀ {α : Type u_1} {x : α} {xs : List α} {d : α}, (x :: xs).getD 0 d = x
-- Mathlib.Order.Cover
WithBot.bot_wcovBy_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ⊥ ⩿ ↑a ↔ IsMin a
-- Mathlib.Algebra.Algebra.Hom
AlgHom.addHomMk_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), { toFun := ⇑f, map_add' := ⋯ } = ↑f
-- Mathlib.Order.Monotone.Defs
Subsingleton.antitone' : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton β] (f : α → β), Antitone f
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_def : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : Sub G], MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_symm : ∀ {α : Type u_1}, SymAlg.sym.symm = SymAlg.unsym
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_bot : ∀ {V : Type u} {G : SimpleGraph V}, ⊥.verts = ∅
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.contract_one : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R}, Polynomial.contract 1 f = f
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse.Monoidal
-- Init.Data.Vector.Lemmas
Vector.any_beq : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {a : α}, (xs.any fun x => a == x) = xs.contains a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.liftH.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k k_1 : A ⟶ h.Q) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp k h.g' = 0), h.liftH k hk = h.liftH k_1 ⋯
-- Mathlib.Topology.Sheaves.Forget
TopCat.Presheaf.isSheaf_iff_isSheaf_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} D]
  (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits G] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheaf ↔ TopCat.Presheaf.IsSheaf (CategoryTheory.Functor.comp F G)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
MeasureTheory.lintegral_enorm_condExp_indicator : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} (hm : m ≤ m𝓧) {μ : MeasureTheory.Measure 𝓧}
  [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set 𝓧},
  MeasurableSet s →
    autoParam (μ s ≠ ⊤) MeasureTheory.lintegral_enorm_condExp_indicator._auto_1 →
      ∫⁻ (a : 𝓧), ‖μ[s.indicator 1 | m] a‖ₑ ∂μ = μ s
-- Mathlib.Algebra.Group.Units.Equiv
val_inv_unitsEquivProdSubtype_symm_apply : ∀ (α : Type u_2) [inst : Monoid α] (p : { p // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }),
  ↑((unitsEquivProdSubtype α).symm p)⁻¹ = (↑p).2
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.fullyFaithfulForget₂ToMonCat.eq_1 : GrpCat.fullyFaithfulForget₂ToMonCat =
  { preimage := fun {X Y} f => GrpCat.ofHom (MonCat.Hom.hom f),
    map_preimage := @GrpCat.fullyFaithfulForget₂ToMonCat._proof_1,
    preimage_map := @GrpCat.fullyFaithfulForget₂ToMonCat._proof_2 }
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- Constructs a Lie ideal from an invariant submodule of the dual space of a Cartan subalgebra.

Given a submodule `q` of the dual space `Dual K H` that is invariant under all root reflections,
this produces a Lie ideal by taking the sum of all `sl₂` subalgebras corresponding to roots
whose linear forms lie in `q`.  -/
LieAlgebra.IsKilling.invtSubmoduleToLieIdeal : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : CharZero K] →
        [inst_2 : LieRing L] →
          [inst_3 : LieAlgebra K L] →
            [inst_4 : FiniteDimensional K L] →
              [inst_5 : LieAlgebra.IsKilling K L] →
                {H : LieSubalgebra K L} →
                  [inst_6 : H.IsCartanSubalgebra] →
                    [inst_7 : LieModule.IsTriangularizable K (↥H) L] →
                      (q : Submodule K (Module.Dual K ↥H)) →
                        (∀ (i : ↥LieSubalgebra.root),
                            q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)) →
                          LieIdeal K L
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformly.exists : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], MultipliableLocallyUniformly f → ∃ g, HasProdLocallyUniformly f g
-- Mathlib.Order.SuccPred.Limit
IsMax.isPredPrelimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α], IsMax a → Order.IsPredPrelimit a
-- Init.Core
cast_eq : ∀ {α : Sort u} (h : α = α) (a : α), cast h a = a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.setTag.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (cidx : ℕ)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_9),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h) = 1 + sizeOf fvarId + sizeOf cidx + sizeOf h
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `Iio b` and
nonnegative on `Ioi b`. Then `f` attains its minimum on `ℝ` at `b`.  -/
isMinOn_univ_of_deriv : ∀ {f : ℝ → ℝ} {b : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Iio b) →
      DifferentiableOn ℝ f (Set.Ioi b) →
        (∀ x ∈ Set.Iio b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioi b, 0 ≤ deriv f x) → IsMinOn f Set.univ b
-- Mathlib.GroupTheory.Nilpotent
Group.IsNilpotent.nilpotent' : ∀ {G : Type u_2} {inst : Group G} [self : Group.IsNilpotent G], ∃ n, Subgroup.upperCentralSeries G n = ⊤
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.eqToIso.congr_simp : ∀ {α : Type u₁} {X Y : CategoryTheory.Discrete α} (h : X.as = Y.as),
  CategoryTheory.Discrete.eqToIso h = CategoryTheory.Discrete.eqToIso h
-- Mathlib.Data.List.Rotate
List.length_mem_cyclicPermutations : ∀ {α : Type u} {l' : List α} (l : List α), l' ∈ l.cyclicPermutations → l'.length = l.length
-- Lean.Meta.Sym.Pattern
/-- Attempts to assign an unassigned metavariable on either side.
Tries `t := s` first, then `s := t`. Returns `true` if either assignment succeeds.
Used as a fast path before more expensive unification strategies. Example: using
more expensive `isDefEqI` for instance arguments.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.tryAssignUnassigned : Lean.Expr → Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.S_smul_four : ∀ {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m), ModularGroup.S • ModularGroup.S • ModularGroup.S • ModularGroup.S • A = A
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_piecewise_zero : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  (f : MeasureTheory.SimpleFunc α F) (μ : MeasureTheory.Measure α) {s : Set α} (hs : MeasurableSet s),
  MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.piecewise s hs f 0) =
    MeasureTheory.SimpleFunc.integral (μ.restrict s) f
-- Init.Data.SInt.Lemmas
Int64.neg_mul : ∀ (a b : Int64), -a * b = -(a * b)
-- Mathlib.GroupTheory.Sylow
/-- The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup.  -/
Sylow.comapOfKerIsPGroup : {p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] →
      (P : Sylow p G) →
        {K : Type u_2} → [inst_1 : Group K] → (ϕ : K →* G) → IsPGroup p ↥ϕ.ker → ↑P ≤ ϕ.range → Sylow p K
-- Mathlib.Algebra.BigOperators.Finprod
/-- If the product of `f i` over `i ∈ s` is not equal to `1`, then there is some `x ∈ s` such that
`f x ≠ 1`.  -/
exists_ne_one_of_finprod_mem_ne_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
  ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1 → ∃ x ∈ s, f x ≠ 1
-- Init.Data.SInt.Bitwise
Int16.toBitVec_or : ∀ (a b : Int16), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, (m₁ ∩ m₂).getKeyD k fallback = if k ∈ m₂ then m₁.getKeyD k fallback else fallback
-- Init.Data.Float.Model.Float
/-- Converts a `UInt64` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofUInt64 : UInt64 → Float.Model