mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.inr_f_descShortComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (n : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr S.f).f n)
      ((CochainComplex.mappingCone.descShortComplex S).f n) =
    S.g.f n
-- Mathlib.Data.Finset.Sym
Finset.sym2_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (s : Finset α),
  (Finset.image f s).sym2 = Finset.image (Sym2.map f) s.sym2
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instDefinableOfDefinable₁ : (f : ZFSet.{u_1} → ZFSet.{u_1}) →
  [ZFSet.Definable₁ f] →
    (n : ℕ) → (g : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) → [ZFSet.Definable n g] → ZFSet.Definable n fun s => f (g s)
-- Mathlib.Analysis.SpecificLimits.RCLike
RCLike.tendsto_ofReal_cobounded_cobounded : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜], Filter.Tendsto RCLike.ofReal (Bornology.cobounded ℝ) (Bornology.cobounded 𝕜)
-- Mathlib.Order.Hom.Lattice
SupHom.dual_id : ∀ {α : Type u_2} [inst : Max α], SupHom.dual (SupHom.id α) = InfHom.id αᵒᵈ
-- Init.Data.List.Lemmas
List.any_insert : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {f : α → Bool} {l : List α} {a : α},
  (List.insert a l).any f = (f a || l.any f)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_3 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.getFunIndInfo? : Bool → Bool → Lean.Name → Lean.CoreM (Option Lean.Meta.FunIndInfo)
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure.eq_1 : ∀ (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicClosure 𝕜 s = Subtype.val '' closure (Subtype.val ⁻¹' s)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.sConvexComb_convexCombPair : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1)
  (w w' : Convexity.StdSimplex R M),
  Convexity.sConvexComb (Convexity.convexCombPair s t hs ht hst w w') =
    Convexity.convexCombPair s t hs ht hst (Convexity.sConvexComb w) (Convexity.sConvexComb w')
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage : ∀ {X : AlgebraicGeometry.Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat)
  (α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F)
  (H : CategoryTheory.NatTrans.Coequifibered α) (U : X.AffineZariskiSite),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData H).toBase.base).obj ↑U =
    AlgebraicGeometry.Scheme.Hom.opensRange
      ((AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData H).cover.f U)
-- Lean.SubExpr
/-- A location within a goal state. It identifies a specific goal together with a `GoalLocation`
within it.  -/
Lean.SubExpr.GoalsLocation : Type
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableAt.smul_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜}
  {s : (x : B) → E x} {x₀ : B}, MDiffAt f x₀ → MDiffAt (T% s) x₀ → (MDiffAt fun x => ⟨x, (f • s) x⟩) x₀
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapId'_eq_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (b : B), F.mapId' (CategoryTheory.CategoryStruct.id b) ⋯ = F.mapId b
-- Mathlib.Tactic.Push
/-- `resolvePushId?` is a version of `resolveId?` that also supports notations like `_ ∈ _`,
`∃ x, _` and `∑ x, _`.  -/
Mathlib.Tactic.Push.resolvePushId? : Lean.Term → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.isClosedEmbedding_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [ContinuousMul B] [T2Space B],
  Topology.IsClosedEmbedding ContinuousMonoidHom.toContinuousMap
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.inf_iInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
  [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M), q ⊓ ⨅ i, p i = ⨅ i, q ⊓ p i
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.mk : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          {𝒜 : ι → σ} →
            {x : Submonoid A} →
              (deg : ι) → ↥(𝒜 deg) → (den : ↥(𝒜 deg)) → ↑den ∈ x → HomogeneousLocalization.NumDenSameDeg 𝒜 x
-- Mathlib.LinearAlgebra.Matrix.Permutation
/-- the permutation matrix associated with an `Equiv.Perm`  -/
Equiv.Perm.permMatrix : {n : Type u_1} → (R : Type u_2) → [DecidableEq n] → Equiv.Perm n → [Zero R] → [One R] → Matrix n n R
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_pow : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (k : ℕ), Lean.Grind.CommRing.Poly.denote ctx (p.pow k) = Lean.Grind.CommRing.Poly.denote ctx p ^ k
-- Mathlib.Tactic.Use
/-- Use the `args` to refine the goals `gs` in order, but whenever there is a single
goal remaining then first try applying a single constructor if it's for a single-constructor
inductive type. In `eager` mode, instead we always first try to refine, and if that fails we
always try to apply such a constructor no matter if it's the last goal.

Returns the remaining explicit goals `gs`, any goals `acc` due to `refine`, and a sublist of these
of instance arguments that we should try synthesizing after the loop.
The new set of goals should be `gs ++ acc`.  -/
Mathlib.Tactic.useLoop : Bool →
  List Lean.MVarId →
    List Lean.Term →
      List Lean.MVarId → List Lean.MVarId → Lean.Elab.TermElabM (List Lean.MVarId × List Lean.MVarId × List Lean.MVarId)
-- Mathlib.Tactic.Sat.FromLRAT
/-- Returns `a` and `pr : reify v f a` given a formula `f`  -/
Mathlib.Tactic.Sat.buildReify.reifyFmla : ℕ → Lean.Expr → Lean.Expr × Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.ofHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsAddMonHom f], CategoryTheory.AddGrp.ofHom f = CategoryTheory.AddGrp.homMk f
-- Mathlib.Analysis.LocallyConvex.Basic
Absorbs.eventually_nhds_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s t : Set E}, Absorbs 𝕜 s t → 0 ∈ s → ∀ᶠ (c : 𝕜) in nhds 0, Set.MapsTo (fun x => c • x) t s
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- On a set of unique differentiability, the second derivative is obtained by taking the
derivative of the derivative.  -/
iteratedFDerivWithin_two_apply' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  (f : E → F) {z : E},
  UniqueDiffOn 𝕜 s →
    z ∈ s → ∀ (v w : E), (iteratedFDerivWithin 𝕜 2 f s z) ![v, w] = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) v) w
-- Mathlib.Tactic.TacticAnalysis
/-- `continue` means to accumulate the current tactic, but not yet run the test on it.  -/
Mathlib.TacticAnalysis.TriggerCondition.continue : {ctx : Type u_1} → ctx → Mathlib.TacticAnalysis.TriggerCondition ctx
-- Mathlib.Analysis.Convex.Basic
convex_list_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {l : List (Set E)}, (∀ i ∈ l, Convex 𝕜 i) → Convex 𝕜 l.sum
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_over_two_pow : ∀ (n : ℕ), Real.cos (Real.pi / 2 ^ (n + 1)) = Real.sqrtTwoAddSeries 0 n / 2
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_const_mul_self : ∀ {a : EReal}, (LinearGrowth.linearGrowthInf fun n => a * ↑n) = a
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.full_of_comp_essSurj : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor D E) (L : CategoryTheory.Functor C D) [L.EssSurj],
  (∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ) → F.Full
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsGeneratedBy.mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  G.IsGeneratedBy x → ∀ (i : ι), x i ∈ G.obj (X i)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadIso.mk_inv_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (f : M.toFunctor ≅ N.toFunctor)
  (f_ε :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X)
      CategoryTheory.ComonadIso.mk._auto_1)
  (f_δ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) =
          CategoryTheory.CategoryStruct.comp (M.δ.app X)
            (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X))))
      CategoryTheory.ComonadIso.mk._auto_3),
  (CategoryTheory.ComonadIso.mk f f_ε f_δ).inv.toNatTrans = f.inv
-- Mathlib.Algebra.Algebra.Equiv
/-- `AlgEquivClass F R A B` states that `F` is a type of algebra structure preserving
equivalences. You should extend this class when you extend `AlgEquiv`.  -/
AlgEquivClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] → [inst_2 : Semiring B] → [Algebra R A] → [Algebra R B] → [EquivLike F A B] → Prop
-- Mathlib.Order.Directed
directedOn_singleton : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] (a : α), DirectedOn r {a}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `Y`-coordinate of a representative of `2 • P` for a Jacobian point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Jacobian.dblY : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → R
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_smul`. -/
SkewMonoidAlgebra.toFinsupp_smul : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : SMulZeroClass S k] (a : S)
  (b : SkewMonoidAlgebra k G), (a • b).coeff = a • b.coeff
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₃` is the cokernel of `v₁₂ : L₁ ⟶ L₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (self : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ self.v₂₃ ⋯)
-- Mathlib.MeasureTheory.Measure.DiracProba
BoundedContinuousFunction.mkOfBound.congr_simp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (f f_1 : C(α, β)) (e_f : f = f_1)
  (C C_1 : ℝ) (e_C : C = C_1) (h : ∀ (x y : α), dist (f x) (f y) ≤ C),
  BoundedContinuousFunction.mkOfBound f C h = BoundedContinuousFunction.mkOfBound f_1 C_1 ⋯
-- Mathlib.CategoryTheory.Action.Monoidal
CategoryTheory.Functor.mapAction_δ_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {W : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} W] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [inst_5 : F.OplaxMonoidal]
  (X Y : Action V G),
  (CategoryTheory.Functor.OplaxMonoidal.δ (F.mapAction G) X Y).hom = CategoryTheory.Functor.OplaxMonoidal.δ F X.V Y.V
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The `AddEquiv` between two `AddMonoid`s with a unique element.  -/
ContinuousAddEquiv.ofUnique : {M : Type u_3} →
  {N : Type u_4} →
    [Unique M] →
      [Unique N] →
        [inst : Add M] → [inst_1 : Add N] → [inst_2 : TopologicalSpace M] → [inst_3 : TopologicalSpace N] → M ≃ₜ+ N
-- Mathlib.Data.Sym.Basic
Sym.filterNe.eq_1 : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (a : α) (m : Sym α n),
  Sym.filterNe a m = ⟨⟨Multiset.count a ↑m, ⋯⟩, ⟨Multiset.filter (fun x => a ≠ x) ↑m, ⋯⟩⟩
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.ofSet_toPartialEquiv : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} (hs : IsOpen s),
  (OpenPartialHomeomorph.ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s
-- Init.Data.UInt.IntToBitVec
UInt64.toBitVec64_toUSize : ∀ (n : UInt64) (h : System.Platform.numBits = 64), n.toUSize.toBitVec64 h = n.toBitVec
-- Mathlib.Algebra.Group.Irreducible.Lemmas
Irreducible.of_map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] {f : F} {x : M}
  [inst_2 : FunLike F M N] [MonoidHomClass F M N] [IsLocalHom f], Irreducible (f x) → Irreducible x
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.composableArrows₅_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS₁ : S₁.ShortExact) (i j : ι)
  (hij : c.Rel i j), (HomologicalComplex.HomologySequence.composableArrows₅ hS₁ i j hij).Exact
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- The set of leading terms of zero and polynomials within a set `B` is equal to the set of
zero and leading terms of polynomials within `B`.
 -/
MonomialOrder.image_leadingTerm_insert_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (B : Set (MvPolynomial σ R)),
  m.leadingTerm '' insert 0 B = insert 0 (m.leadingTerm '' B)
-- Init.Data.Vector.Attach
Vector.unattach_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.attach.unattach = xs
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.length_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).keys.length = (↑m).size
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isPreconnected_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K L : TopologicalSpace.NonemptyCompacts α},
  IsPreconnected ↑L → IsPreconnected (Set.Ioc K L)
-- Mathlib.Order.Comparable
IncompRel.rfl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {a : α}, IncompRel r a a
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_sub_div_left : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), z ≠ 0 → z ∣ y → (z * x - y) / z = x - y / z
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- The product is the pullback over the terminal object.  -/
isPullbackOfIsTerminalIsProduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (h : W ⟶ X) →
            (k : W ⟶ Y) →
              (H₁ : CategoryTheory.Limits.IsTerminal Z) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk h k) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k ⋯)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_le_foldr_max : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : Zero N] [inst_2 : LinearOrder N] (f : M → N),
  f 0 ≤ 0 → (∀ (x y : M), f (x + y) ≤ max (f x) (f y)) → ∀ (l : List M), f l.sum ≤ List.foldr max 0 (List.map f l)
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.algebra : (A : Type u_2) →
  [inst : Ring A] →
    [inst_1 : UniformSpace A] →
      [inst_2 : IsUniformAddGroup A] →
        [inst_3 : IsTopologicalRing A] →
          (R : Type u_3) →
            [inst_4 : CommSemiring R] →
              [inst_5 : Algebra R A] → [UniformContinuousConstSMul R A] → Algebra R (UniformSpace.Completion A)
-- Init.System.IO
IO.FS.SystemTime.mk.inj : ∀ {sec : ℤ} {nsec : UInt32} {sec_1 : ℤ} {nsec_1 : UInt32},
  { sec := sec, nsec := nsec } = { sec := sec_1, nsec := nsec_1 } → sec = sec_1 ∧ nsec = nsec_1
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- If `n ≠ m`, then `(cyclotomic n ℚ)` and `(cyclotomic m ℚ)` are coprime.  -/
Polynomial.cyclotomic.isCoprime_rat : ∀ {n m : ℕ}, n ≠ m → IsCoprime (Polynomial.cyclotomic n ℚ) (Polynomial.cyclotomic m ℚ)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- If a measurable space admits a countable separating family of measurable sets,
there is a countably generated coarser space which still separates points.  -/
MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated : ∀ (α : Type u_1) [m : MeasurableSpace α] [h : MeasurableSpace.CountablySeparated α],
  ∃ m', MeasurableSpace.CountablyGenerated α ∧ MeasurableSpace.SeparatesPoints α ∧ m' ≤ m
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.eq_1 : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] (u : ι → TopologicalSpace.Opens X),
  TopologicalSpace.IsOpenCover u = (iSup u = ⊤)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.toFun_eq_coe : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f : M →ₛₗ[σ] M₃}, f.toFun = ⇑f
-- Mathlib.Order.Hom.Basic
/-- `Equiv.prodAssoc` promoted to an order isomorphism.  -/
OrderIso.prodAssoc : (α : Type u_6) →
  (β : Type u_7) → (γ : Type u_8) → [inst : LE α] → [inst_1 : LE β] → [inst_2 : LE γ] → (α × β) × γ ≃o α × β × γ
-- Mathlib.Computability.Language
Language.instMulLeftMono : ∀ {α : Type u_1}, MulLeftMono (Language α)
-- Mathlib.Algebra.Group.Translate
translate_sub_right : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] [inst_1 : Sub α] (a : G) (f g : G → α),
  translate a (f - g) = translate a f - translate a g
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeSomeUsingDefaultPrio.visit : ℕ → List Lean.MVarId → List Lean.MVarId → Lean.Elab.TermElabM Bool
-- Mathlib.Logic.Basic
dite_eq_or_eq : ∀ {α : Sort u_1} (P : Prop) [inst : Decidable P] {A : P → α} {B : ¬P → α},
  (∃ (h : P), dite P A B = A h) ∨ ∃ (h : ¬P), dite P A B = B h
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult : Type
-- Batteries.CodeAction.Attr
/-- An entry in the tactic code actions extension, containing the attribute arguments.  -/
Batteries.CodeAction.TacticCodeActionEntry : Type
-- Init.Data.Array.Zip
Array.of_mem_zip : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {as : Array α} {bs : Array β}, (a, b) ∈ as.zip bs → a ∈ as ∧ b ∈ bs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a fallback : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).getKeyD a fallback =
        if compare k a = Ordering.eq then k else t.getKeyD a fallback
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatTrans_comp : ∀ {C D : CategoryTheory.Cat} {F G H : C ⟶ D} (η₁ : F ⟶ G) (η₂ : G ⟶ H),
  (CategoryTheory.CategoryStruct.comp η₁ η₂).toNatTrans = CategoryTheory.CategoryStruct.comp η₁.toNatTrans η₂.toNatTrans
-- Mathlib.Order.CompleteLattice.Basic
iSup_Prop_eq : ∀ {ι : Sort u_4} {p : ι → Prop}, ⨆ i, p i = ∃ i, p i
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.instAddCommGroupH1Cotangent : {R : Type u_2} →
  {S : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Extension R S} → AddCommGroup P.H1Cotangent
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.image_eq_preimage_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) (s : Set P₁), ⇑e '' s = ⇑e.symm ⁻¹' s
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj.homEquiv_symm_apply : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {C : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_3} C]
  (F : V ⥤rq C), CategoryTheory.ReflQuiv.adj.homEquiv.symm F = CategoryTheory.Cat.FreeRefl.lift F
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- Turn a left exact functor into an additive functor.  -/
CategoryTheory.AdditiveFunctor.ofLeftExact : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            [CategoryTheory.Limits.HasZeroObject C] →
              [CategoryTheory.Limits.HasZeroObject D] →
                [CategoryTheory.Limits.HasBinaryBiproducts C] → CategoryTheory.Functor (C ⥤ₗ D) (C ⥤+ D)
-- Init.Data.List.Lemmas
List.getLast_append : ∀ {α : Type u_1} {l' l : List α} (h : l ++ l' ≠ []),
  (l ++ l').getLast h = if h' : l'.isEmpty = true then l.getLast ⋯ else l'.getLast ⋯
-- Aesop.Script.Tactic
Aesop.Script.Tactic.mk.inj : ∀ {uTactic : Aesop.Script.UTactic} {sTactic? : Option Aesop.Script.STactic} {uTactic_1 : Aesop.Script.UTactic}
  {sTactic?_1 : Option Aesop.Script.STactic},
  { uTactic := uTactic, sTactic? := sTactic? } = { uTactic := uTactic_1, sTactic? := sTactic?_1 } →
    uTactic = uTactic_1 ∧ sTactic? = sTactic?_1
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint over `F` and `A ⊔ B = E`, then the `Module.finrank` of
`E` over `A` is equal to the `Module.finrank` of `B` over `F`.
 -/
IntermediateField.LinearDisjoint.finrank_left_eq_finrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [Module.Finite F ↥A], A.LinearDisjoint ↥B → A ⊔ B = ⊤ → Module.finrank (↥A) E = Module.finrank F ↥B
-- Mathlib.Data.Set.Card
Set.encard_eq_three : ∀ {α : Type u_1} {s : Set α}, s.encard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_mul_eq_left : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] {f g : α → M},
  Disjoint (Function.mulSupport f) (Function.mulSupport g) → (Function.mulSupport f).mulIndicator (f * g) = f