mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_3),
  (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f =
    CategoryTheory.Limits.biprod.desc ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂))
      (X.δ f₁₂ f₃ n₀ n₁ ⋯)
-- Mathlib.Tactic.Linter.HaveLetLinter
/-- find the `have` syntax.  -/
_private.Mathlib.Tactic.Linter.HaveLetLinter.0.Mathlib.Linter.haveLet.isHave? : Lean.Syntax → Bool
-- Mathlib.Algebra.GroupWithZero.Subgroup
Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ : ∀ {G₀ : Type u_1} {G : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Group G] [inst_2 : MulDistribMulAction G₀ G]
  {a : G₀}, a ≠ 0 → ∀ (S : Subgroup G) (x : G), x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.op_symm_apply_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (a : β),
  (MulEquiv.op.symm f).symm a = (MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op) a
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_lhs_prefix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' ≠ Lean.Grind.AC.Seq.denote ctx rhs₂
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColim_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (H : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  {X Y : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} (α : X ⟶ Y) (c : C),
  ((CategoryTheory.Limits.fiberwiseColim F H).map α).app c =
    CategoryTheory.Limits.colim.map ((CategoryTheory.Grothendieck.ι F c).whiskerLeft α)
-- Init.Data.Vector.Range
Vector.self_mem_range_succ : ∀ {n : ℕ}, n ∈ Vector.range (n + 1)
-- Mathlib.Algebra.DirectSum.Internal
/-- Build a `DirectSum.GCommRing` instance for a collection of additive submonoids.  -/
SetLike.gcommRing : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : AddCommMonoid ι] →
        [inst_1 : CommRing R] →
          [inst_2 : SetLike σ R] →
            [inst_3 : AddSubgroupClass σ R] →
              (A : ι → σ) → [SetLike.GradedMonoid A] → DirectSum.GCommRing fun i => ↥(A i)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasStrictFDerivAt_multiset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] [inst_3 : DecidableEq ι] [Finite ι] {u : Multiset ι} {x : ι → 𝔸'},
  HasStrictFDerivAt (fun x => (Multiset.map x u).prod)
    (Multiset.map (fun i => (Multiset.map x (u.erase i)).prod • ContinuousLinearMap.proj i) u).sum x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Inv_cast : ∀ {aig1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {assign : Std.Tactic.BVDecide.BVExpr.Assignment}
  {aig2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (cache : Std.Tactic.BVDecide.BVExpr.Cache aig1)
  (hpref : Std.Sat.AIG.IsPrefix aig1.decls aig2.decls),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig1 cache →
    Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig2 (cache.cast ⋯)
-- Mathlib.RingTheory.Localization.Integral
/-- If `t` is integral over `R[1/t]`, then it is integral over `R`.  -/
isIntegral_of_isIntegral_adjoin_of_mul_eq_one : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] (t s : S),
  s * t = 1 → IsIntegral (↥R[s]) t → IsIntegral R t
-- Mathlib.Data.Num.Basic
PosNum.instSub : Sub PosNum
-- Std.Time.Date.Unit.Month
Std.Time.Month.instInhabitedOffset : Inhabited Std.Time.Month.Offset
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.TreeMap.getEntryLE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap α β cmp → α → α × β
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.encoding_decode : ∀ {L : FirstOrder.Language} {α : Type u'} (l : List (α ⊕ (i : ℕ) × L.Functions i)),
  FirstOrder.Language.Term.encoding.decode l =
    (do
        let a ← (FirstOrder.Language.Term.listDecode l).head?
        pure (some a)).join
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.isoHom_inv_id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (e : X ≅ Y), CategoryTheory.CategoryStruct.comp e.hom.hom e.inv.hom = CategoryTheory.CategoryStruct.id X.obj
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquivSubtype_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {p : W'.Point → Prop} (p0 : p WeierstrassCurve.Affine.Point.zero),
  (WeierstrassCurve.Affine.pointEquivSubtype p0) ⟨WeierstrassCurve.Affine.Point.zero, p0⟩ = none
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.reduceNatEqExpr : Lean.Expr → Lean.Expr → Lean.Meta.SimpM (Option Nat.EqResult✝)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_ofBitVec : ∀ (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 64),
  (ISize.ofBitVec n).toBitVec64 h = BitVec.cast h n
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- `autMap` is uniquely characterized by making the canonical diagram commute.  -/
CategoryTheory.PreGaloisCategory.autMap_unique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f : A ⟶ B) (σ : CategoryTheory.Aut A) (τ : CategoryTheory.Aut B),
  CategoryTheory.CategoryStruct.comp f τ.hom = CategoryTheory.CategoryStruct.comp σ.hom f →
    CategoryTheory.PreGaloisCategory.autMap f σ = τ
-- Mathlib.Topology.Algebra.Constructions
Units.instDiscreteTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M] [DiscreteTopology M], DiscreteTopology Mˣ
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_sub : ∀ {α : Type u_12} {β : Type u_13} {M : Type u_14} [inst : AddCommGroup M] {v₁ v₂ : α →₀ M} {f : α → β},
  Finsupp.mapDomain f (v₁ - v₂) = Finsupp.mapDomain f v₁ - Finsupp.mapDomain f v₂
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.d.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (n m : ℕ) (h_1 : (n m : ℕ) → motive (Int.ofNat n) (Int.ofNat m))
  (h_2 : (n m : ℕ) → motive (Int.negSucc n) (Int.negSucc m)) (h_3 : Unit → motive (Int.negSucc 0) (Int.ofNat 0))
  (h_4 : (a a_1 : ℕ) → motive (Int.ofNat a) (Int.negSucc a_1))
  (h_5 : (a a_1 : ℕ) → motive (Int.negSucc a) (Int.ofNat a_1)),
  (match Int.negSucc n, Int.negSucc m with
    | Int.ofNat n, Int.ofNat m => h_1 n m
    | Int.negSucc n, Int.negSucc m => h_2 n m
    | Int.negSucc 0, Int.ofNat 0 => h_3 ()
    | Int.ofNat a, Int.negSucc a_1 => h_4 a a_1
    | Int.negSucc a, Int.ofNat a_1 => h_5 a a_1) =
    h_2 n m
-- Mathlib.Data.TwoPointing
/-- The two-pointing of constant functions.  -/
TwoPointing.pi : (α : Type u_1) → {β : Type u_2} → TwoPointing β → [Nonempty α] → TwoPointing (α → β)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.toInfHom : {α : Type u_6} →
  {β : Type u_7} → [inst : Min α] → [inst_1 : Min β] → [inst_2 : Top α] → [inst_3 : Top β] → InfTopHom α β → InfHom α β
-- Mathlib.Algebra.Group.Action.End
MulDistribMulAction.toMulAut_apply : ∀ (G : Type u_1) (M : Type u_2) [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulDistribMulAction G M] (x : G),
  (MulDistribMulAction.toMulAut G M) x = MulDistribMulAction.toMulEquiv M x
-- Mathlib.Data.PNat.Interval
PNat.map_subtype_embedding_Ioc : ∀ (a b : ℕ+), Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.isIso_iff_isIso_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {A B : CategoryTheory.MonoOver X} (f : A ⟶ B),
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso (CategoryTheory.Over.Hom.left f.hom)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKey?_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).maxKey? = some k ↔
        (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.isCoprime_scaleRoots : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
  IsUnit r → IsCoprime p q → IsCoprime (p.scaleRoots r) (q.scaleRoots r)
-- Mathlib.Algebra.Group.Basic
eq_add_of_add_neg_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a + -c = b → a = b + c
-- Aesop.Tree.Data
Aesop.NodeState.proven.sizeOf_spec : sizeOf Aesop.NodeState.proven = 1
-- Mathlib.Algebra.Order.Monovary
Monovary.mul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Monovary f g₁ → Monovary f g₂ → Monovary f (g₁ * g₂)
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype : ∀ (X : FinBoolAlg), (CategoryTheory.HasForget₂.forget₂.obj X).isFintype = X.isFintype
-- Init.Notation
/-- `p+` is shorthand for `many1(p)`. It uses parser `p` 1 or more times, and produces a
`nullNode` containing the array of parsed results. This parser has arity 1.

If `p` has arity more than 1, it is auto-grouped in the items generated by the parser.
 -/
«stx_+» : Lean.TrailingParserDescr
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.beq : {α : Type u} →
  (self : Std.Packages.LinearPreorderOfOrdArgs α) →
    let this := self.ord;
    BEq α
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Iso.sumBoxProdDistrib_symm_apply : ∀ {V₁ : Type u_5} {V₂ : Type u_6} {W : Type u_7} (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) (H : SimpleGraph W)
  (s : V₁ × W ⊕ V₂ × W),
  (RelIso.symm (SimpleGraph.Iso.sumBoxProdDistrib G₁ G₂ H)) s = Sum.elim (Prod.map Sum.inl id) (Prod.map Sum.inr id) s
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
_private.Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind.0.NumberField.Ideal.primesOverSpanEquivMonicFactorsModAux_symm_apply : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (A : Polynomial ℤ) {Q : Polynomial (ZMod p)}
  (hQ : Q ∈ (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) A)).toFinset),
  ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsModAux✝ A).symm ⟨Q, hQ⟩) =
    Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm) Q
-- Mathlib.Topology.Irreducible
/-- An irreducible space is one that is nonempty
and where there is no non-trivial pair of disjoint opens.  -/
IrreducibleSpace : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.coe_extendLe : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t),
  ⇑(Module.Basis.extendLe hs hst ht) = Subtype.val
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.iSupLift_of_mem : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] {ι : Type u_1}
  [inst_7 : StarRing R] [inst_8 : IsScalarTower R A A] [inst_9 : SMulCommClass R A A] [inst_10 : StarModule R A]
  [inst_11 : Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K}
  {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)}
  {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i),
  (NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩
-- Mathlib.Algebra.Order.Group.MinMax
min_sub_sub_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  min (a - c) (b - c) = min a b - c
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_iff_Union_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, StableUnderSpecialization s ↔ ⋃ x ∈ s, closure {x} = s
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.instInhabited : {ι : Type u_1} → {I : BoxIntegral.Box ι} → Inhabited (BoxIntegral.Prepartition I)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instZero : {σ : Type u_1} → {R : Type u_2} → [Zero R] → Zero (MvPowerSeries σ R)
-- Init.Data.Array.Lemmas
/-- Variant of `foldr_reverse` with a side condition for the `start` argument.  -/
Array.foldr_reverse' : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β → β} {b : β} {start : ℕ},
  start = xs.size → Array.foldr f b xs.reverse start = Array.foldl (fun x y => f y x) b xs
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.copy_eq : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B] (f : A →⋆* B)
  (f' : A → B) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.card_four' : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] [IsAddKleinFour G], Fintype.card G = 4
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *⋆-algebra homomorphism* is an algebra homomorphism between `R`-algebras `A` and `B`
equipped with a `star` operation, and this homomorphism is also `star`-preserving.  -/
StarAlgHom : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [Algebra R A] → [Star A] → [inst_4 : Semiring B] → [Algebra R B] → [Star B] → Type (max u_2 u_3)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.neg_pi_div_two_le_arg_iff : ∀ {z : ℂ}, -(Real.pi / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
-- Mathlib.Analysis.Normed.Group.Basic
normGroupNorm.eq_1 : ∀ (E : Type u_5) [inst : NormedGroup E],
  normGroupNorm E = { toGroupSeminorm := normGroupSeminorm E, eq_one_of_map_eq_zero' := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Nonsingular.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.Nonsingular P =
    (W'.Equation P ∧
      ((MvPolynomial.eval P) W'.polynomialX ≠ 0 ∨
        (MvPolynomial.eval P) W'.polynomialY ≠ 0 ∨ (MvPolynomial.eval P) W'.polynomialZ ≠ 0))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂)[k]? = t₂[k]?.or t₁[k]?
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.toContext : Lean.Elab.Tactic.Grind.Context → Lean.Elab.Tactic.Context
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.ev_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((CategoryTheory.ihom A).map f))
      ((CategoryTheory.ihom.ev A).app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) f
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.lift_map : ∀ (R : Type u_1) [inst : CommRing R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {D : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) {x x_1 : CategoryTheory.Free R C} (f : x ⟶ x_1),
  (CategoryTheory.Free.lift R F).map f = Finsupp.sum f fun f' r => r • F.map f'
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Coalgebra F} (h : CategoryTheory.Limits.IsTerminal A),
  { f := CategoryTheory.CategoryStruct.comp A.str (CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv h), h := ⋯ } =
    CategoryTheory.CategoryStruct.id A
-- Init.Internal.Order.Basic
Lean.Order.le_csup : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {c : α → Prop} (hc : Lean.Order.chain c) {y : α},
  c y → Lean.Order.PartialOrder.rel y (Lean.Order.CCPO.csup hc)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.inf_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β]
  (f g : InfTopHom α β) (a : α), (f ⊓ g) a = f a ⊓ g a
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- Extend two variable map to completions.  -/
AbstractCompletion.extend₂ : {α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) →
      {β : Type uβ} →
        [inst_1 : UniformSpace β] →
          (pkg' : AbstractCompletion.{vβ, uβ} β) →
            {γ : Type uγ} → [UniformSpace γ] → (α → β → γ) → pkg.space → pkg'.space → γ
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_smul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s : Set α) (a : α),
  lowerClosure (a • s) = a • lowerClosure s
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.measure_Ioo_eq_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] {m : MeasurableSpace X}
  (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [DenselyOrdered X] {a b : X}, μ (Set.Ioo a b) = 0 ↔ b ≤ a
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.mk.injEq : ∀ (numNodes numNull numCollisions maxDepth numNodes_1 numNull_1 numCollisions_1 maxDepth_1 : ℕ),
  ({ numNodes := numNodes, numNull := numNull, numCollisions := numCollisions, maxDepth := maxDepth } =
      { numNodes := numNodes_1, numNull := numNull_1, numCollisions := numCollisions_1, maxDepth := maxDepth_1 }) =
    (numNodes = numNodes_1 ∧ numNull = numNull_1 ∧ numCollisions = numCollisions_1 ∧ maxDepth = maxDepth_1)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsBase.coloops_subset : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → M.coloops ⊆ B
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.pow_lt_self : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I : Ideal A), I ≠ ⊥ → I ≠ ⊤ → ∀ (e : ℕ), 2 ≤ e → I ^ e < I
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ ∩ m₂).contains k = true ↔ m₁.contains k = true ∧ m₂.contains k = true
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Directly insert a `Key`, `LazyEntry` pair into a `RefinedDiscrTree`.  -/
Lean.Meta.RefinedDiscrTree.insert : {α : Type} →
  Lean.Meta.RefinedDiscrTree α →
    Lean.Meta.RefinedDiscrTree.Key → Lean.Meta.RefinedDiscrTree.LazyEntry × α → Lean.Meta.RefinedDiscrTree α
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- We track how the comparison was constructed by adding and scaling previous comparisons,
back to the original assumptions.  -/
Mathlib.Tactic.Linarith.PComp.src : Mathlib.Tactic.Linarith.PComp → Mathlib.Tactic.Linarith.CompSource
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- Given a ring homomorphism `f : R →+* S` sending all elements of an ideal to zero,
lift it to the quotient by this ideal.  -/
Ideal.Quotient.lift : {R : Type u} →
  [inst : Ring R] →
    (I : Ideal R) →
      {S : Type v} → [inst_1 : I.IsTwoSided] → [inst_2 : Semiring S] → (f : R →+* S) → (∀ a ∈ I, f a = 0) → R ⧸ I →+* S
-- Mathlib.RingTheory.Valuation.LocalSubring
ValuationSubring.toLocalSubring_injective : ∀ {K : Type u_3} [inst : Field K], Function.Injective ValuationSubring.toLocalSubring
-- Std.Sat.CNF.Basic
Std.Sat.CNF.append : {α : Type u_1} → Std.Sat.CNF α → Std.Sat.CNF α → Std.Sat.CNF α
-- Mathlib.Algebra.Notation.Prod
Prod.fst_star : ∀ {R : Type u_6} {S : Type u_7} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).1 = star x.1
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.addCommMonoidTopologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : SeparatelyContinuousAdd M]
  [inst_3 : T2Space M] (s : AddSubmonoid M) (hs : ∀ (x y : ↥s), x + y = y + x),
  s.addCommMonoidTopologicalClosure hs = { toAddMonoid := s.topologicalClosure.toAddMonoid, add_comm := ⋯ }
-- Mathlib.Topology.Algebra.Module.IsWeak
LinearMap.IsWeak.tendsto_iff_forall_eval_tendsto : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [hB : B.IsWeak] {α : Type u_7} {l : Filter α} {f : α → E}
  {x : E},
  Function.Injective ⇑B →
    (Filter.Tendsto f l (nhds x) ↔ ∀ (y : F), Filter.Tendsto (fun i => (B (f i)) y) l (nhds ((B x) y)))
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.instT1Space : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R] [T1Space R], T1Space (Matrix.SpecialLinearGroup n R)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
/-- The map that turns a triangle index into an explicit triangle.  -/
SimpleGraph.TripartiteFromTriangles.toTriangle : {α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → [DecidableEq α] → [DecidableEq β] → [DecidableEq γ] → α × β × γ ↪ Finset (α ⊕ β ⊕ γ)
-- Mathlib.Data.PNat.Factors
/-- The prime factors of n, regarded as a multiset  -/
PNat.factorMultiset : ℕ+ → PrimeMultiset
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.restrictScalars_apply : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : Algebra S R] [inst_9 : IsScalarTower S R M]
  [inst_10 : IsScalarTower S R N] (Q : QuadraticMap R M N) (x : M), Q.restrictScalars x = Q x
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushout_obj_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPushoutsAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] (A : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.pushout P Q f).obj A).hom = CategoryTheory.Limits.pushout.inr A.hom f
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ici : ∀ {α : Type u_1} [inst : LinearOrder α], IsPiSystem (Set.range Set.Ici)