mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Basic
List.isPrefixOf_cons₂ : ∀ {α : Type u} {as : List α} {b : α} {bs : List α} [inst : BEq α] {a : α},
  (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView!.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r'))
  (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  l = Std.DTreeMap.Internal.Impl.inner size k' v' l' r' →
    (match l with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') ≍
      h_2 size k' v' l' r'
-- Init.System.Uri
_private.Init.System.Uri.0.System.Uri.UriEscape.decodeUri.hexDigitToUInt8? : UInt8 → Option UInt8
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
NonUnitalAlgebra.adjoin_le_algebra_adjoin : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (s : Set A),
  NonUnitalAlgebra.adjoin R s ≤ (Algebra.adjoin R s).toNonUnitalSubalgebra
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.unop_le_unop : ∀ {α : Type u_1} [inst : Preorder α] {a b : αᵃᵒᵖ}, AddOpposite.unop a ≤ AddOpposite.unop b ↔ a ≤ b
-- Mathlib.Order.NonemptyFiniteChains
PartOrd.nonemptyFiniteChainsFunctor_obj_coe : ∀ (X : PartOrd), ↑(PartOrd.nonemptyFiniteChainsFunctor.obj X) = PartialOrder.NonemptyFiniteChains ↑X
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_diff_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiff.clm_prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₄},
  ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g →
    ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f →
      ContMDiff I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n fun x => (g x).prodMap (f x)
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- Map any coequalizer cofork to a cocone on the difference of the two morphisms.  -/
CategoryTheory.Preadditive.cokernelCoforkOfCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f g : X ⟶ Y} → CategoryTheory.Limits.Cofork f g → CategoryTheory.Limits.CokernelCofork (f - g)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.twoMore : ByteArray.utf8DecodeChar?.FirstByte
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
instExpCharAdjoinPthRoots : ∀ (k : Type u_1) [inst : Field k] (p : ℕ) [ExpChar k p], ExpChar (AdjoinPthRoots k) p
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_ne_zero_of_finite : ∀ {G : Type u} [inst : AddLeftCancelMonoid G] [Finite G], AddMonoid.exponent G ≠ 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_roo : ∀ {m n i fallback : ℕ}, (m<...n).toArray.getD i fallback = if i < n - (m + 1) then m + 1 + i else fallback
-- Mathlib.RingTheory.Localization.FractionRing
Submonoid.pos.congr_simp : ∀ (α : Type u_1) [inst : MulZeroOneClass α] [inst_1 : PartialOrder α] [inst_2 : PosMulStrictMono α]
  [inst_3 : ZeroLEOneClass α] [inst_4 : NeZero 1], Submonoid.pos α = Submonoid.pos α
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.eq_self_sdiff_zero : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension S A B = IsCyclotomicExtension (S \ {0}) A B
-- Mathlib.Logic.IsEmpty.Basic
Function.not_surjective_of_isEmpty_of_nonempty : ∀ {α : Type u_4} {β : Type u_5} [IsEmpty α] [Nonempty β] (f : α → β), ¬Function.Surjective f
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The duality isomorphism `S.P' ≅ Opposite.unop S.op.P`.  -/
CategoryTheory.ShortComplex.SnakeInput.P'IsoUnopOpP : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.P' ≅ Opposite.unop S.op.P
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey_modify_eq_minKey : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : β → β}
  {he : (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false},
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey he = t.minKey ⋯
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.ofClass_carrier : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SetLike S A] [inst_4 : NonUnitalSubsemiringClass S A] [inst_5 : SMulMemClass S R A]
  (s : S), ↑(NonUnitalSubalgebra.ofClass s) = ↑s
-- Mathlib.Tactic.Linarith.Parsing
/-- A scalar `z` is represented by a `Sum` with coefficient `z` and monomial `one`  -/
Mathlib.Tactic.Linarith.scalar : ℤ → Mathlib.Tactic.Linarith.Sum
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiAlgebraFin_apply : ∀ {R : Type uR} {n : ℕ} [inst : CommSemiring R] {A : Type u_1} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (m : Fin n → A), (MultilinearMap.mkPiAlgebraFin R n A) m = (List.ofFn m).prod
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- The character space of a topological algebra is the subset of elements of the weak dual that
are also algebra homomorphisms.  -/
WeakDual.characterSpace : (𝕜 : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : NonUnitalNonAssocSemiring A] →
              [inst_5 : TopologicalSpace A] → [inst_6 : Module 𝕜 A] → Set (WeakDual 𝕜 A)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.append : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
hasFPowerSeriesAt_clog_one_add : HasFPowerSeriesAt (fun x => Complex.log (1 + x)) (FormalMultilinearSeries.ofScalars ℂ fun n => -(-1) ^ n / ↑n) 0
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.charpoly_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.charpoly = ∏ i, (Polynomial.X - Polynomial.C ↑(hA.eigenvalues i))
-- Mathlib.Combinatorics.SimpleGraph.Operations
/-- Except possibly for itself, the neighbours of `t` in `G.replaceVertex s t` are the neighbours of
`s` in `G`.  -/
SimpleGraph.adj_replaceVertex_iff_of_ne_right : ∀ {V : Type u_1} (G : SimpleGraph V) (s : V) {t : V} [inst : DecidableEq V] {w : V},
  w ≠ t → ((G.replaceVertex s t).Adj t w ↔ G.Adj s w)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F] (a : A),
  CategoryTheory.CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a))
      (G.map ((L.pointwiseRightKanExtensionCounit F).app a)) =
    (L.pointwiseRightKanExtensionCounit (F.comp G)).app a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Init.Data.Option.Lemmas
Option.bind_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Option α) (f : α → Option β) (g : β → Option γ),
  (x.bind f).bind g = x.bind fun y => (f y).bind g
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A set of points is coplanar if their `vectorSpan` has dimension at most `2`.  -/
Coplanar : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} → [inst : DivisionRing k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → Set P → Prop
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf'_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Inv α] [inst_2 : SemilatticeInf β] {s : Finset α}
  (hs : s⁻¹.Nonempty) (f : α → β), s⁻¹.inf' hs f = s.inf' ⋯ fun x => f x⁻¹
-- Init.Data.UInt.Lemmas
UInt16.lt_iff_toBitVec_lt : ∀ {a b : UInt16}, a < b ↔ a.toBitVec < b.toBitVec
-- Mathlib.Topology.Sets.Closeds
/-- the carrier set, i.e. the points in this set  -/
TopologicalSpace.Clopens.carrier : {α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.Clopens α → Set α
-- Std.Data.DTreeMap.Raw.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.DTreeMap.Raw.filterMap : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      {cmp : α → α → Ordering} → ((a : α) → β a → Option (γ a)) → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α γ cmp
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.isEmpty_eq : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ → t₁.isEmpty = t₂.isEmpty
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
/-- The property of objects in the functor category `J ⥤ C`
which preserves finite limits.  -/
CategoryTheory.ObjectProperty.preservesFiniteLimits : {J : Type u_1} →
  {C : Type u_3} →
    [inst : CategoryTheory.Category.{v_3, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_5, u_3} C] → CategoryTheory.ObjectProperty (CategoryTheory.Functor J C)
-- Mathlib.Topology.MetricSpace.Polish
/-- An open subset of a Polish space is also Polish.  -/
IsOpen.polishSpace : ∀ {α : Type u_3} [inst : TopologicalSpace α] [PolishSpace α] {s : Set α}, IsOpen s → PolishSpace ↑s
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
prod_vanishing_of_summable_norm : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R},
  (Summable fun i => ‖f i‖) → ∀ {ε : ℝ}, 0 < ε → ∃ s₂, ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starMap.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : NonUnitalSemiring B] [inst_8 : StarRing B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] [inst_12 : StarModule R B] (φ φ_1 : A →⋆ₙₐ[R] B),
  φ = φ_1 → Unitization.starMap φ = Unitization.starMap φ_1
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} [inst_2 : SizeOf C] [inst_3 : (a : C) → SizeOf (P a)]
  [inst_4 : SizeOf J] (toLimitPresentation : CategoryTheory.Limits.LimitPresentation J X)
  (prop_diag_obj : ∀ (j : J), P (toLimitPresentation.diag.obj j)),
  sizeOf { toLimitPresentation := toLimitPresentation, prop_diag_obj := prop_diag_obj } = 1 + sizeOf toLimitPresentation
-- Mathlib.Order.Minimal
/-- **Alias** of the forward direction of `maximal_toDual`. -/
Maximal.of_dual : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α],
  Maximal (fun x => P (OrderDual.ofDual x)) (OrderDual.toDual x) → Minimal P x
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (toMonoidHom : G →* E)
  (rightInverse_rightHom : Function.RightInverse (↑toMonoidHom).toFun ⇑S.rightHom) (toMonoidHom_1 : G →* E)
  (rightInverse_rightHom_1 : Function.RightInverse (↑toMonoidHom_1).toFun ⇑S.rightHom),
  ({ toMonoidHom := toMonoidHom, rightInverse_rightHom := rightInverse_rightHom } =
      { toMonoidHom := toMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 }) =
    (toMonoidHom = toMonoidHom_1)
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.instConjExponentOfFactLeOfNat : ∀ {p : ENNReal} [Fact (1 ≤ p)], p.HolderConjugate p.conjExponent
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_equivSentence : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {α : Type u'} [inst_1 : (L.withConstants α).Structure M]
  [(L.lhomWithConstants α).IsExpansionOn M] (φ : L.Formula α),
  M ⊨ FirstOrder.Language.Formula.equivSentence φ ↔ φ.Realize fun a => ↑(L.con a)
-- Init.Data.UInt.Bitwise
USize.and_assoc : ∀ (a b c : USize), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.finite_torsion : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ},
  0 < n → {u | n • u = 0}.Finite
-- Mathlib.Order.Category.LinOrd
LinOrd.ofHom_id : ∀ {X : Type u} [inst : LinearOrder X],
  LinOrd.ofHom OrderHom.id = CategoryTheory.CategoryStruct.id { carrier := X, str := inst }
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- **Alias** of the reverse direction of `isUnit_iff_ne_zero`. -/
Ne.isUnit : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → IsUnit a
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.ForwardSliceSearcher.skipPrefix?_eq_some_iff : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.ForwardSliceSearcher.skipPrefix? pat s = some pos ↔ (s.sliceTo pos).copy = pat.copy
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSimple.instHasTrivialRadical : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSimple R L], LieAlgebra.HasTrivialRadical R L
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight.inj : ∀ {c₁ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr} {c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr}
  {c₁_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr} {c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.denote'.go.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (k : ℤ) (h_1 : Unit → motive (Lean.Grind.CommRing.Poly.num 0))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_3 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  (k = 0 → False) →
    (match Lean.Grind.CommRing.Poly.num k with
      | Lean.Grind.CommRing.Poly.num 0 => h_1 ()
      | Lean.Grind.CommRing.Poly.num k => h_2 k
      | Lean.Grind.CommRing.Poly.add k m p => h_3 k m p) =
      h_2 k
-- Init.Data.Option.Lemmas
Option.eq_none_iff_forall_ne_some : ∀ {α : Type u_1} {o : Option α}, o = none ↔ ∀ (a : α), o ≠ some a
-- Lean.Elab.Tactic.RCases
/-- Get the syntax node from which this pattern was parsed. Used for error messages  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.ref : Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Syntax
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.Equiv t₂ → ∀ (k : α) (f : β k → β k), (t₁.modify k f).Equiv (t₂.modify k f)
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel : ℕ → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.setLIntegral_condKernel_univ_left : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
  {f : β × Ω → ENNReal},
  Measurable f →
    ∀ {t : Set Ω},
      MeasurableSet t →
        ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.add : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [inst_2 : (i : ι) → Add (β i)]
  [∀ (i : ι), MeasurableAdd₂ (β i)],
  MeasureTheory.Adapted f u → MeasureTheory.Adapted f v → MeasureTheory.Adapted f (u + v)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Use the axiom of choice to extract explicit `WeakLimitCone F` from `HasWeakLimit F`.  -/
CategoryTheory.Limits.getWeakLimitCone : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        (F : CategoryTheory.Functor J C) →
          [CategoryTheory.Limits.HasWeakLimit F] → CategoryTheory.Limits.WeakLimitCone F
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.params : Lean.Meta.SizeOfSpecNested.Context → Array Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- The map on connected components induced by a graph homomorphism.  -/
SimpleGraph.ConnectedComponent.map : {V : Type u} →
  {V' : Type v} → {G : SimpleGraph V} → {G' : SimpleGraph V'} → G →g G' → G.ConnectedComponent → G'.ConnectedComponent
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_subsemigroup_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : Set R),
  NonUnitalSubsemiring.closure ↑(Subsemigroup.closure s) = NonUnitalSubsemiring.closure s
-- Mathlib.Algebra.Field.Defs
DivisionRing.toInv : {K : Type u_2} → [self : DivisionRing K] → Inv K
-- Mathlib.Analysis.Complex.Basic
Complex.le_of_eq_sum_of_eq_sum_norm : ∀ {ι : Type u_2} {a b : ℝ} (f : ι → ℂ) (s : Finset ι), 0 ≤ a → ↑a = ∑ i ∈ s, f i → ↑b = ∑ i ∈ s, ↑‖f i‖ → a ≤ b
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig.disallowedMethods? : Lean.Lsp.LogConfig → Option (Std.HashSet String)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φH =
    CategoryTheory.Limits.Fork.ι c
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.span_singleton_setGcd : ∀ (s : Set ℕ), Ideal.span {↑(Nat.setGcd s)} = Ideal.span (Nat.cast '' s)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C))
  (hom₁ : A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₁)
  (hom₂ : A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₂)
  (hom₃ : A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₃)
  (comm₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) hom₂ =
        CategoryTheory.CategoryStruct.comp hom₁ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_1)
  (comm₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) hom₃ =
        CategoryTheory.CategoryStruct.comp hom₂ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
          (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
        CategoryTheory.CategoryStruct.comp hom₃ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_5)
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorHomMk A B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₁ = hom₁.app j
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorph.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y},
  IsLocalHomeomorph (g ∘ f) → IsLocalHomeomorph g → Continuous f → IsLocalHomeomorph f
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h h_1 : Homotopy f g),
  h = h_1 → ∀ (e : c.Embedding c') [inst_3 : e.IsRelIff], h.extend e = h_1.extend e
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.YonedaSheafCondition.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
  (S : CategoryTheory.Sieve X),
  CategoryTheory.Presieve.YonedaSheafCondition P S =
    ∀ (f : S.functor ⟶ P), ∃! g, CategoryTheory.CategoryStruct.comp S.functorInclusion g = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_minKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).minKey?.isSome = true
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.withAlts.mkMinorType : Lean.Expr →
  Array Lean.Expr →
    Array Lean.Meta.Match.DiscrInfo → Array Lean.Expr → Lean.Meta.Match.AltLHS → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Nat.Totient
Nat.totient_eq_card_coprime : ∀ (n : ℕ), n.totient = {a ∈ Finset.range n | n.Coprime a}.card