mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_10 : ∀ {C : Type u} (T Y₁ W : CategoryTheory.FreeMonoidalCategory C) (f : Y₁.Hom W),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft T f) =
    CategoryTheory.Discrete.natTrans fun x =>
      match x with
      | { as := X } => (CategoryTheory.FreeMonoidalCategory.normalizeMapAux f).app { as := T.normalizeObj X }
-- Mathlib.RingTheory.Unramified.LocalRing
/-- [Stacks Tag 02FM](https://stacks.math.columbia.edu/tag/02FM) -/
Algebra.FormallyUnramified.of_map_maximalIdeal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : IsLocalRing S] [inst_5 : IsLocalHom (algebraMap R S)] [Algebra.EssFiniteType R S]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)],
  Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S → Algebra.FormallyUnramified R S
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `AddLECancellable.tsub_eq_of_eq_add'` for a version assuming that `a = c + b` itself is
cancellable rather than `b`.  -/
AddLECancellable.tsub_eq_of_eq_add : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable b → a = c + b → a - b = c
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.unique : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x gradf gradg : F},
  HasGradientAt f gradf x → HasGradientAt f gradg x → gradf = gradg
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
_private.Lean.Meta.Tactic.Simp.Arith.Int.Simp.0.Int.Internal.Linear.Poly.gcdAll.go : ℕ → Int.Internal.Linear.Poly → ℕ
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.instHasLeftCalculusOfFractionsIsoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.isoModSerre.HasLeftCalculusOfFractions
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.contains.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k' : α) (v : β k')
  (l r : 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)),
  (match Std.DTreeMap.Internal.Impl.inner size k' v l r 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
-- Mathlib.Logic.IsEmpty.Defs
Quot.instIsEmpty : ∀ {α : Sort u} [IsEmpty α] {r : α → α → Prop}, IsEmpty (Quot r)
-- Mathlib.Order.Defs.PartialOrder
/-- **Alias** of `not_le_of_gt`. -/
LT.lt.not_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ -x + y` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_neg_add : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [ν.IsAddLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => -p.1 + p.2) (μ.prod ν) ν
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxo.Iterator.toArray_eq_match : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  {it : Std.Iter α},
  it.toArray =
    match it.internalState.next with
    | none => #[]
    | some a =>
      if a < it.internalState.upperBound then
        #[a] ++ { internalState := { next := Std.PRange.succ? a, upperBound := it.internalState.upperBound } }.toArray
      else #[]
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.algebraMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] {x : A},
  IsIntegral R x → IsIntegral R ((algebraMap A B) x)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balanceR.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1) (r r_1 : Std.DTreeMap.Internal.Impl α β) (e_r : r = r_1)
      (hlb : l.Balanced) (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size),
      Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceR k v_1 l_1 r_1 ⋯ ⋯ ⋯
-- Init.Data.String.Subslice
String.Slice.Subslice.startInclusive_extendLeft : ∀ {s : String.Slice} {sl : s.Subslice} {newStart : s.Pos} {h : newStart ≤ sl.startInclusive},
  (sl.extendLeft newStart h).startInclusive = newStart
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k}, ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v
-- Lean.Syntax
Lean.Syntax.Range.stop : Lean.Syntax.Range → String.Pos.Raw
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.symm_toPartialEquiv : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (f : Equidecomp X G),
  f.symm.toPartialEquiv = f.symm
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.coe_linearMapAt_of_mem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ⇑(Bundle.Pretrivialization.linearMapAt R e b) = fun y => (↑e ⟨b, y⟩).2
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the first inclusion  -/
CategoryTheory.Functor.PushoutObjObj.inl : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₂ Y₂ : C₂} → {f₂ : X₂ ⟶ Y₂} → (self : F.PushoutObjObj f₁ f₂) → (F.obj Y₁).obj X₂ ⟶ self.pt
-- Mathlib.Order.Disjoint
/-- A complemented bounded lattice is one where every element has a (not necessarily unique)
complement.  -/
ComplementedLattice : (α : Type u_2) → [inst : Lattice α] → [BoundedOrder α] → Prop
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p p' : Submodule R M}
  {x : ↥(p ⊔ p')}, (LinearMap.quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ ↑x ∈ p'
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimAltInfo.numFields : Lean.Meta.ElimAltInfo → ℕ
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.disjoint_vadd_set_left : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s t : Set β} {a : α},
  Disjoint (a +ᵥ s) t ↔ Disjoint s (-a +ᵥ t)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.subtype_comp_inclusion : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  [inst_3 : LE S] [inst_4 : IsConcreteLE S G] {H K : S} (h : H ≤ K), (↑K).comp (AddSubgroupClass.inclusion h) = ↑H
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The Grothendieck construction is functorial: a strong natural transformation `α : F ⟶ G`
induces a functor `Grothendieck.map : ∫ F ⥤ ∫ G`.  -/
CategoryTheory.Pseudofunctor.Grothendieck.map : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      (F ⟶ G) → CategoryTheory.Functor F.Grothendieck G.Grothendieck
-- Mathlib.Data.DFinsupp.BigOperators
Trunc.lift.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} (f f_1 : α → β) (e_f : f = f_1) (c : ∀ (a b : α), f a = f b) (a a_1 : Trunc α),
  a = a_1 → Trunc.lift f c a = Trunc.lift f_1 ⋯ a_1
-- Aesop.Options.Public
/-- The transparency used by the `destructProducts` builtin rule. The rule splits
a hypothesis `h : T` if `T` is defeq to a product-like type (e.g. `T ≡ A ∧ B`
or `T ≡ A × B`) at the given transparency.

Note: we can index this rule only if the transparency is `.reducible`. With
any other transparency, the rule becomes unindexed and is applied to every
goal.
 -/
Aesop.Options.destructProductsTransparency : Aesop.Options → Lean.Meta.TransparencyMode
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.mkOfConeMorphism_lift : ∀ {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} {t : CategoryTheory.Limits.Cone F}
  (lift : (s : CategoryTheory.Limits.Cone F) → s ⟶ t) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.IsWeakLimit.mkOfConeMorphism lift).lift s = (lift s).hom
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.MorphismProperty.Q_inverts : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C), W.IsInvertedBy W.Q
-- Mathlib.Data.PEquiv
/-- Creates a `PEquiv` that is the identity on `s`, and `none` outside of it.  -/
PEquiv.ofSet : {α : Type u} → (s : Set α) → [DecidablePred fun x => x ∈ s] → α ≃. α
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.IsReduced.take : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {ω : List B},
  cs.IsReduced ω → ∀ (j : ℕ), cs.IsReduced (List.take j ω)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- `padicValRat` coincides with `padicValNat`.  -/
padicValRat_of_nat : ∀ {p : ℕ} (n : ℕ), ↑(padicValNat p n) = padicValRat p ↑n
-- Mathlib.Topology.Category.TopCat.ULift
/-- Given `X : TopCat.{u}`, this is the homeomorphism `X ≃ₜ uliftFunctor.{v}.obj X`.  -/
TopCat.uliftFunctorObjHomeo : (X : TopCat) → ↑X ≃ₜ ↑(TopCat.uliftFunctor.obj X)
-- Mathlib.Data.Matrix.Basis
Matrix.single_apply_same : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (c : α), Matrix.single i j c i j = c
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  {Y x : (Finset (CategoryTheory.Discrete α))ᵒᵖ} (h : Y ⟶ x),
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F).map h =
    CategoryTheory.Limits.Pi.lift fun y => CategoryTheory.Limits.Pi.π (fun x => F.obj ↑x) ⟨↑y, ⋯⟩
-- Mathlib.NumberTheory.Multiplicity
Int.sq_mod_four_eq_one_of_odd : ∀ {x : ℤ}, Odd x → x ^ 2 % 4 = 1
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvector_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, f.HasEigenvector μ x ↔ x ∈ f.eigenspace μ ∧ x ≠ 0
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.uniformContinuous_closure : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous closure
-- Std.Http.Internal.IndexMultiMap
/-- Inserts a new key-value pair into the map.
If the key already exists, appends the value to existing values.
 -/
Std.Internal.IndexMultiMap.insert : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [EquivBEq α] → [LawfulHashable α] → Std.Internal.IndexMultiMap α β → α → β → Std.Internal.IndexMultiMap α β
-- Mathlib.Order.Interval.Finset.Defs
/-- A constructor from a definition of `Finset.Ici` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderTop.ofIci'`, this one requires `PartialOrder` but
only `DecidableEq`.  -/
LocallyFiniteOrderTop.ofIci : (α : Type u_1) →
  [inst : PartialOrder α] →
    [DecidableEq α] → (finsetIci : α → Finset α) → (∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x) → LocallyFiniteOrderTop α
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_list_prod_right_iff : ∀ {k : ℕ} {l : List ℕ}, k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.coe_unzero : ∀ {α : Type u} {x : WithZero α} (hx : x ≠ 0), ↑(WithZero.unzero hx) = x
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.v : {R : Type u} →
  {inst : Ring R} →
    {Γ₀ : outParam (Type v)} → {inst_1 : LinearOrderedCommGroupWithZero Γ₀} → [self : Valued R Γ₀] → Valuation R Γ₀
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq : ∀ {ι : Type uι} {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] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s)
  [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M] (x : M),
  ∑ᶠ (i : ι), (fs.toSmoothPartitionOfUnity i) x = 1 - ∏ᶠ (i : ι), (1 - ↑(fs.toFun i) x)
-- Mathlib.Data.Fin.Basic
/-- Converting an in-range number to `Fin (n + 1)` produces a result
whose value is the original number.  -/
Fin.val_cast_of_lt : ∀ {n : ℕ} [inst : NeZero n] {a : ℕ}, a < n → ↑↑a = a
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.liftRingHom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  [inst_2 : IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m),
  IsAdicComplete.liftRingHom I f hf = (↑(AdicCompletion.ofAlgEquiv I).symm).comp (AdicCompletion.liftRingHom I f ⋯)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.proj_symm_apply' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} {x : F},
  b ∈ e.baseSet → proj (↑e.symm (b, x)) = b
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_comp_eq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G)
  (β : G ⟶ H),
  CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.map β)
-- Init.Data.Iterators.Basic
Std.Iterators.Productive.of_productivenessRelation : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (r : Std.Iterators.ProductivenessRelation α m), Std.Iterators.Productive α m
-- Init.Data.SInt.Bitwise
ISize.neg_eq_not_add : ∀ (a : ISize), -a = ~~~a + 1
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, StrictConvexOn 𝕜 s f → StrictConcaveOn 𝕜 s g → StrictConvexOn 𝕜 s (f - g)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Prod.isIsometricVAdd' : ∀ {M : Type u} {N : Type u_2} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd M M] [inst_3 : Add N]
  [inst_4 : PseudoEMetricSpace N] [IsIsometricVAdd N N], IsIsometricVAdd (M × N) (M × N)
-- Mathlib.Data.Set.Function
Set.MapsTo.mono_left : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s₁ t → s₂ ⊆ s₁ → Set.MapsTo f s₂ t
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.quotientKerEquivOfSurjective.congr_simp : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} (hf : Function.Surjective ⇑f),
  RingHom.quotientKerEquivOfSurjective hf = RingHom.quotientKerEquivOfSurjective hf
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.ensureNoMinIndexable : Bool → Lean.MetaM Unit
-- Init.Data.UInt.Lemmas
UInt16.toUSize_toUInt8 : ∀ (n : UInt16), n.toUInt8.toUSize = n.toUSize % 256
-- Mathlib.Topology.Defs.Induced
Topology.isQuotientMap_iff : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Topology.IsQuotientMap f ↔ Topology.IsCoinducing f ∧ Function.Surjective f
-- Init.Data.Iterators.Combinators.Monadic.Take
/-- Internal implementation detail of the iterator library  -/
Std.Iterators.Types.Take.inner : {α : Type w} →
  {m : Type w → Type w'} → {β : Type w} → [inst : Std.Iterator α m β] → Std.Iterators.Types.Take α m → Std.IterM m β
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instIsNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {f : Polynomial R}, IsNoetherianRing (AdjoinRoot f)
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzOnWith_iff_norm_sub_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {f : E → F}
  {C : NNReal} {s : Set E}, LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
-- Mathlib.RingTheory.WittVector.WittPolynomial
bind₁_xInTermsOfW_wittPolynomial : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] (k : ℕ),
  (MvPolynomial.bind₁ (xInTermsOfW p R)) (wittPolynomial p R k) = MvPolynomial.X k
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.constructors.sizeOf_spec : ∀ (constructorNames : Array Lean.Name) (md : Lean.Meta.TransparencyMode),
  sizeOf (Aesop.RuleTacDescr.constructors constructorNames md) = 1 + sizeOf constructorNames + sizeOf md
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.instMulActionWithZero : {M : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Zero A] →
        [inst_1 : Zero B] → [inst_2 : MonoidWithZero M] → [MulActionWithZero M B] → MulActionWithZero M (ZeroHom A B)
-- Init.Data.Bool
Bool.bne_true : ∀ (b : Bool), (b != true) = !b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {inv : Bool} (aig : Std.Sat.AIG α)
  (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig) (start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig input).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.mk : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      (toModuleCat : ModuleCat R) →
        [topologicalSpace : TopologicalSpace ↑toModuleCat] →
          [isTopologicalAddGroup : IsTopologicalAddGroup ↑toModuleCat] →
            [continuousSMul : ContinuousSMul R ↑toModuleCat] → TopModuleCat R
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algEquivOfTranscendental.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f), RatFunc.algEquivOfTranscendental f h = RatFunc.algEquivOfTranscendental f h
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {X Y Z : J.OneHypercover S} (f : X.Hom Y) (g : Y.Hom Z) (a : X.I₀),
  (CategoryTheory.CategoryStruct.comp f g).s₀ a = g.s₀ (f.s₀ a)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b c d p : M}, a ≡ b [PMOD p] → c ≡ d [PMOD p] → a + c ≡ b + d [PMOD p]
-- Mathlib.Data.Bool.Count
List.IsChain.length_div_two_le_count_bool : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → ∀ (b : Bool), l.length / 2 ≤ List.count b l
-- Mathlib.Order.Filter.Pointwise
Filter.pure_vadd_pure : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {a : α} {b : β}, pure a +ᵥ pure b = pure (a +ᵥ b)
-- Lean.Meta.Basic
/-- Return `true` if `e` is a synthetic (or synthetic opaque) metavariable  -/
Lean.Meta.isSyntheticMVar : Lean.Expr → Lean.MetaM Bool
-- Aesop.Stats.File
Aesop.StatsFileRecord.goalSolved : Aesop.StatsFileRecord → Bool
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_ne_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ {f : MvPolynomial σ R}, (MvPolynomial.expand p) f ≠ 0 ↔ f ≠ 0
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_of_nonneg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], 0 ≤ a → |a| = a
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.mvarId : Lean.Meta.GeneralizeIndicesSubgoal → Lean.MVarId
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the map
`(A ⊗ (α →₀ k[G]))_G →ₗ[k] (α →₀ A)` sending
`⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)).`  -/
Rep.coinvariantsTensorFreeToFinsupp : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        (α : Type u) →
          [DecidableEq α] →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.free k G α)).ρ.Coinvariants →ₗ[k] α →₀ ↑A
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.π_comp_eqToHom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {j j' : J} (hj : j = j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.Limits.limit.π F j'
-- Mathlib.Algebra.GroupWithZero.Prod
WithZero.ofClass_withZeroUnitsEquiv : ∀ (M₀ : Type u_1) [inst : GroupWithZero M₀] [inst_1 : DecidablePred fun x => x = 0],
  MonoidWithZeroHom.ofClass WithZero.withZeroUnitsEquiv = WithZero.lift' (Units.coeHom M₀)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightEquiv_comp_toLin : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (x y : P.Equiv P),
  RootPairing.Equiv.coweightEquiv P P (x.comp y) =
    RootPairing.Equiv.coweightEquiv P P x ≪≫ₗ RootPairing.Equiv.coweightEquiv P P y
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.tuple.sizeOf_spec : ∀ (args : List Lean.Parser.Tactic.MCasesPat), sizeOf (Lean.Parser.Tactic.MCasesPat.tuple args) = 1 + sizeOf args
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The right arrow of the walking cospan.  -/
CategoryTheory.Limits.WalkingCospan.Hom.inr : CategoryTheory.Limits.WalkingCospan.right ⟶ CategoryTheory.Limits.WalkingCospan.one
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq_spec : ∀ (x x_1 : Int.Internal.Linear.Poly),
  (x == x_1) =
    match x, x_1 with
    | Int.Internal.Linear.Poly.num a, Int.Internal.Linear.Poly.num b => a == b
    | Int.Internal.Linear.Poly.add a a_1 a_2, Int.Internal.Linear.Poly.add b b_1 b_2 =>
      a == b && (a_1 == b_1 && a_2 == b_2)
    | x, x_2 => false