mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Cont.eval.match_1.eq_2 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (fs : Turing.ToPartrec.Code) (as : List ℕ) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ fs as k))
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ ns k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp f k))
  (h_5 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix f k)),
  (match Turing.ToPartrec.Cont.cons₁ fs as k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ fs as k => h_2 fs as k
    | Turing.ToPartrec.Cont.cons₂ ns k => h_3 ns k
    | Turing.ToPartrec.Cont.comp f k => h_4 f k
    | Turing.ToPartrec.Cont.fix f k => h_5 f k) =
    h_2 fs as k
-- Mathlib.Data.W.Constructions
WType.Listα.cons.injEq : ∀ {γ : Type u} (a a_1 : γ), (WType.Listα.cons a = WType.Listα.cons a_1) = (a = a_1)
-- Mathlib.Data.Fin.VecNotation
/-- `vecTail v` gives a vector consisting of all entries of `v` except the first  -/
Matrix.vecTail : {α : Type u} → {n : ℕ} → (Fin n.succ → α) → Fin n → α
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.decidableLE.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α} [inst_3 : DecidableLE α] (a b : AddLocalization s),
  a.decidableLE b = a.recOnSubsingleton₂ b fun x x_1 x_2 x_3 => decidable_of_iff' (↑x_3 + x ≤ ↑x_2 + x_1) ⋯
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_ofReal_im : ∀ (x : ℝ), (Complex.cos ↑x).im = 0
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The connecting homomorphism of the spectral object. (Use `δ` instead.)  -/
CategoryTheory.Abelian.SpectralObject.δ' : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (self : CategoryTheory.Abelian.SpectralObject C ι) →
            (n₀ n₁ : ℤ) →
              n₀ + 1 = n₁ →
                ((CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_2
                        CategoryTheory.Abelian.SpectralObject._proof_4).comp
                    (self.H n₀) ⟶
                  (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Abelian.SpectralObject._proof_6
                        CategoryTheory.Abelian.SpectralObject._proof_2).comp
                    (self.H n₁))
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_closedBall_closedBall_closedBall : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.Topology.Homotopy.Contractible
ContinuousMap.HomotopyEquiv.contractibleSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [ContractibleSpace Y]
  (e : ContinuousMap.HomotopyEquiv X Y), ContractibleSpace X
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
_private.Mathlib.Geometry.Euclidean.Angle.Oriented.Basic.0.Orientation.termω : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.Basic
/-- **Alias** of `sq_pos_of_ne_zero`.

---

**Alias** of the reverse direction of `sq_pos_iff`. -/
pow_two_pos_of_ne_zero : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {a : R},
  a ≠ 0 → 0 < a ^ 2
-- Mathlib.NumberTheory.Height.Basic
/-- Extension for the `positivity` tactic: `Height.mulHeight₁` is always positive.  -/
Mathlib.Meta.Positivity.evalMulHeight₁ : Mathlib.Meta.Positivity.PositivityExt
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?_some_eq_eq : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x y : α} {v : β} {t : RBTree.RBMap α β cmp},
  t.findEntry? x = some (y, v) → cmp x y = Ordering.eq
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_fromRows_eq_fromBlocks : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R)
  (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R),
  (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
-- Mathlib.Topology.Order.OrderClosed
ClosedIciTopology.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α],
  (∀ (a : α), IsClosed (Set.Ici a)) → ClosedIciTopology α
-- Mathlib.Algebra.Order.Ring.Opposite
AddOpposite.instIsOrderedRing : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R], IsOrderedRing Rᵃᵒᵖ
-- Mathlib.Order.Booleanisation
/-- The supremum on `Booleanisation α` is as follows: For `a b : α`,
* `a ⊔ b` is `a ⊔ b`
* `a ⊔ bᶜ` is `(b \ a)ᶜ`
* `aᶜ ⊔ b` is `(a \ b)ᶜ`
* `aᶜ ⊔ bᶜ` is `(a ⊓ b)ᶜ`  -/
Booleanisation.instSup : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → Max (Booleanisation α)
-- Mathlib.Topology.ExtremallyDisconnected
StoneCech.projective : ∀ {X : Type u} [inst : TopologicalSpace X] [DiscreteTopology X], CompactT2.Projective (StoneCech X)
-- Mathlib.Algebra.Module.FinitePresentation
/-- A module is finitely presented if it is finitely generated by some set `s`
and the kernel of the presentation `Rˢ → M` is also finitely generated.
 -/
Module.FinitePresentation : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.Data.List.Rotate
List.IsRotated.trans : ∀ {α : Type u} {l l' l'' : List α}, l ~r l' → l' ~r l'' → l ~r l''
-- Lean.Meta.Tactic.Grind.ProveEq
/-- State for the `AbstractM` monad used to implement `abstractGroundMismatches?`  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State : Type
-- Mathlib.Dynamics.Flow
Flow.restrictAddSubmonoid_apply : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) (S : AddSubmonoid τ) (t : ↥S) (x : α), (ϕ.restrictAddSubmonoid S).toFun t x = ϕ.toFun (↑t) x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsAddMonHom.addMonoidHom.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f : M ⟶ N)
  [inst_4 : CategoryTheory.IsAddMonHom f] (X : C),
  CategoryTheory.IsAddMonHom.addMonoidHom f X =
    { toFun := fun x => CategoryTheory.CategoryStruct.comp x f, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts a `UInt64` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofUInt64 : Float.Model.Format → UInt64 → Float.Model.UnpackedFloat
-- Lean.Elab.Do.Basic
/-- `DoOps` emitting `Pure.pure` / `Bind.bind`.  -/
Lean.Elab.Do.DoOps.default : Lean.Elab.Do.DoOps
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.mk : {α : Type u_5} →
  {β : Type u_6} →
    [inst : NonAssocSemiring α] →
      [inst_1 : NonAssocSemiring β] →
        (toMonoidHom : α →* β) →
          (↑toMonoidHom).toFun 0 = 0 →
            (∀ (x y : α), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y) → α →+* β
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The image of the filter `atTop` on `Ici a` under the coercion equals `atTop`.  -/
Filter.map_val_Ici_atTop : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] (a : α), Filter.map Subtype.val Filter.atTop = Filter.atTop
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq : Int16.instRxcHasSize = HasModel.instRxcHasSize✝
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictWidthInfty_nonneg : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)), 0 ≤ 𝒢.strictWidthInfty
-- Mathlib.Analysis.Seminorm
/-- The seminorm of a scalar multiplication is the product of the absolute value of the scalar
and the original seminorm.  -/
SeminormClass.map_smul_eq_mul : ∀ {F : Type u_12} {𝕜 : outParam (Type u_13)} {E : outParam (Type u_14)} {inst : SeminormedRing 𝕜} {inst_1 : AddGroup E}
  {inst_2 : SMul 𝕜 E} {inst_3 : FunLike F E ℝ} [self : SeminormClass F 𝕜 E] (f : F) (a : 𝕜) (x : E),
  f (a • x) = ‖a‖ * f x
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.mem_inv_smul_iff_smul_mem : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {g : G} {x : X} {pt : DiscreteTiling.PlacedTile ps}, x ∈ g⁻¹ • pt ↔ g • x ∈ pt
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Result.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {E : Q(«$α») → Type u_1} {e expr : Q(«$α»)} {val : E expr}
  {proof : Q(«$e» = «$expr»)} {expr_1 : Q(«$α»)} {val_1 : E expr_1} {proof_1 : Q(«$e» = «$expr_1»)},
  { expr := expr, val := val, proof := proof } = { expr := expr_1, val := val_1, proof := proof_1 } →
    expr = expr_1 ∧ val ≍ val_1 ∧ proof = proof_1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyπ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.CategoryStruct.comp S₁.homologyπ (CategoryTheory.ShortComplex.homologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) S₂.homologyπ
-- Lean.Parser.Level
Lean.Parser.levelParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
CategoryTheory.Pseudofunctor.isEquivalence_toDescentData : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsStack J] {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Sieve.ofArrows X f ∈ J S → (F.toDescentData f).IsEquivalence
-- Mathlib.Topology.IsClosedRestrict
isClosedMap_restrict_of_compactSpace : ∀ {ι : Type u_1} {α : ι → Type u_2} {S : Set ι} [inst : (i : ι) → TopologicalSpace (α i)]
  [∀ (i : ι), CompactSpace (α i)], IsClosedMap S.domRestrict
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Purity.ofNat_ctorIdx : ∀ (x : Lean.Compiler.LCNF.Purity), Lean.Compiler.LCNF.Purity.ofNat x.ctorIdx = x
-- Std.Data.HashSet.Lemmas
Std.HashSet.ofList_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α},
  (Std.HashSet.ofList l).Equiv (List.foldl (fun acc a => acc.insert a) ∅ l)
-- Mathlib.Data.ENat.Basic
ENat.WithBot.eq_top_iff_forall_ge : ∀ {n : WithBot ℕ∞}, n = ⊤ ↔ ∀ (m : ℕ), ↑m ≤ n
-- Std.Time.DateTime.Timestamp
/-- Creates a `Timestamp` from a `Duration`.
 -/
Std.Time.Timestamp.ofDurationSinceUnixEpoch : Std.Time.Duration → Std.Time.Timestamp
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapArrowHom_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {F' F'' G' G'' : HomologicalComplex C c} (φ' : F' ⟶ G') (φ'' : F'' ⟶ G'')
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] [inst_5 : HomologicalComplex.HasHomotopyCofiber φ'']
  (H : ∀ (j : ι), ∃ i, c.Rel i j) (α : CategoryTheory.Arrow.mk φ ⟶ CategoryTheory.Arrow.mk φ')
  (β : CategoryTheory.Arrow.mk φ' ⟶ CategoryTheory.Arrow.mk φ''),
  HomologicalComplex.homotopyCofiber.mapArrowHom φ φ'' H (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapArrowHom φ φ' H α)
      (HomologicalComplex.homotopyCofiber.mapArrowHom φ' φ'' H β)
-- Mathlib.Algebra.Module.LinearMap.Rat
AddMonoidHom.toRatLinearMap_injective : ∀ {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℚ M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module ℚ M₂], Function.Injective AddMonoidHom.toRatLinearMap
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.instCoeSortType : CoeSort AlgebraicGeometry.LocallyRingedSpace (Type u)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g g_1 : f.left ⟶ f'.left)
  (e_g : g = g_1) (w : CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom),
  CategoryTheory.CostructuredArrow.homMk g w = CategoryTheory.CostructuredArrow.homMk g_1 ⋯
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticTag.default : Lean.Lsp.DiagnosticTag
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.sub : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : SubtractionMonoid β] {f f' : α → β},
  HasCompactSupport f → HasCompactSupport f' → HasCompactSupport (f - f')
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval₂_at_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.eval₂ f 0 p = f (p.coeff 0)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.unitOfList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeMap.unitOfList [] cmp = ∅
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.invStructInv_invHomId : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (I : hom.InvStruct),
  I.invStructInv.invHomId = I.homInvId
-- Mathlib.FieldTheory.Separable
/-- If `R` is of characteristic `p`, `p ∣ n` and `b` is a unit,
then `a * X ^ n + b * X + c` is separable.  -/
Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C' : ∀ {R : Type u} [inst : CommRing R] (p n : ℕ) (a b c : R) [CharP R p],
  p ∣ n → IsUnit b → (Polynomial.C a * Polynomial.X ^ n + Polynomial.C b * Polynomial.X + Polynomial.C c).Separable
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k fallback : α},
  (Std.DTreeMap.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).getD fallback
-- Mathlib.Order.Concept
/-- Copy a concept, adjusting definitional equalities.  -/
Concept.copy : {α : Type u_2} →
  {β : Type u_3} →
    {r : α → β → Prop} → (c : Concept α β r) → (e : Set α) → (i : Set β) → e = c.extent → i = c.intent → Concept α β r
-- Batteries.Recycling.RBTree.Basic
/-- `O(n₁ * log (n₁ + n₂))`. Intersects the maps `t₁` and `t₂`
using `mergeFn a b` to produce the new value.
 -/
RBTree.RBSet.intersectWith : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {cmpα : α → α → Ordering} →
        {cmpβ : β → β → Ordering} →
          {cmpγ : γ → γ → Ordering} →
            (α → β → Ordering) → (α → β → γ) → RBTree.RBSet α cmpα → RBTree.RBSet β cmpβ → RBTree.RBSet γ cmpγ
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_of_one_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], 1 ≤ a → |a|ₘ = a
-- Mathlib.Data.Sym.Sym2
Sym2.diagSet_eq_fromRel_eq : ∀ {α : Type u_1}, Sym2.diagSet = Sym2.fromRel ⋯
-- Mathlib.Topology.Algebra.Ring.Basic
/-- Ring topologies on `R` form a complete lattice, with `⊥` the discrete topology and `⊤` the
indiscrete topology.

The infimum of a collection of ring topologies is the topology generated by all their open sets
(which is a ring topology).

The supremum of two ring topologies `s` and `t` is the infimum of the family of all ring topologies
contained in the intersection of `s` and `t`.  -/
RingTopology.instCompleteSemilatticeInf : {R : Type u_1} → [inst : Ring R] → CompleteSemilatticeInf (RingTopology R)
-- Mathlib.Data.Finset.Insert
/-- Useful in proofs by induction.  -/
Finset.forall_of_forall_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} {a : α} {s : Finset α}, (∀ x ∈ insert a s, p x) → ∀ x ∈ s, p x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback v : β}, (t.insert k v).getD k fallback = v
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.left_distrib : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b c : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul a (Lean.Grind.Ring.OfSemiring.add b c) =
    Lean.Grind.Ring.OfSemiring.add (Lean.Grind.Ring.OfSemiring.mul a b) (Lean.Grind.Ring.OfSemiring.mul a c)
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- The canonical skew-symmetric matrix as an element in the symplectic group.  -/
SymplecticGroup.symJ : (l : Type u_1) →
  (R : Type u_2) → [inst : DecidableEq l] → [inst_1 : Fintype l] → [inst_2 : CommRing R] → ↥(Matrix.symplecticGroup l R)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.mul.eq_2 : ∀ (x : ONote), (x = ONote.zero → False) → x.mul ONote.zero = 0
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.substFunc.eq_2 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (x : {n : ℕ} → L.Functions n → L'.Term (Fin n))
  (l : ℕ) (f : L.Functions l) (ts : Fin l → L.Term α),
  (FirstOrder.Language.func f ts).substFunc x = (x f).subst fun i => (ts i).substFunc fun {n} => x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.LimitCone.mk.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor J C} {cone : CategoryTheory.Limits.Cone F} {isLimit : CategoryTheory.Limits.IsLimit cone}
  {cone_1 : CategoryTheory.Limits.Cone F} {isLimit_1 : CategoryTheory.Limits.IsLimit cone_1},
  { cone := cone, isLimit := isLimit } = { cone := cone_1, isLimit := isLimit_1 } → cone = cone_1 ∧ isLimit ≍ isLimit_1
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.IsWeightedHomogeneous.mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {w : σ → ℕ} {f g : MvPowerSeries σ R} {p q : ℕ},
  MvPowerSeries.IsWeightedHomogeneous w f p →
    MvPowerSeries.IsWeightedHomogeneous w g q → MvPowerSeries.IsWeightedHomogeneous w (f * g) (p + q)
-- Mathlib.Data.Int.Cast.Lemmas
eq_intCast' : ∀ {F : Type u_1} {α : Type u_3} [inst : AddGroupWithOne α] [inst_1 : FunLike F ℤ α] [AddMonoidHomClass F ℤ α] (f : F),
  f 1 = 1 → ∀ (n : ℤ), f n = ↑n
-- Lean.Widget.UserWidget
Lean.Widget.WidgetSource.mk.injEq : ∀ (sourcetext sourcetext_1 : String),
  ({ sourcetext := sourcetext } = { sourcetext := sourcetext_1 }) = (sourcetext = sourcetext_1)
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
/-- Complete graphs are strongly regular. Note that `μ` can take any value
for complete graphs, since there are no distinct pairs of non-adjacent vertices.  -/
SimpleGraph.IsSRGWith.top : ∀ {V : Type u} [inst : Fintype V] {μ : ℕ} [inst_1 : DecidableEq V],
  ⊤.IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuous_of_isBounded : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [inst : AddCommGroup E]
  [inst_1 : NormedField 𝕝] [inst_2 : Module 𝕝 E] [inst_3 : AddCommGroup F] [inst_4 : NormedField 𝕝₂]
  [inst_5 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_6 : RingHomIsometric τ₁₂] {p : SeminormFamily 𝕝 E ι}
  {q : SeminormFamily 𝕝₂ F ι'} {x : TopologicalSpace E},
  WithSeminorms p →
    ∀ {x_1 : TopologicalSpace F}, WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Seminorm.IsBounded p q f → Continuous ⇑f
-- Lean.Server.Rpc.Basic
Lean.Server.instNonemptyRpcEncodable : ∀ {α : Type}, Nonempty (Lean.Server.RpcEncodable α)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.of_smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T : Set α → β} {C : ℝ} {c : ENNReal},
  c ≠ ⊤ → MeasureTheory.DominatedFinMeasAdditive (c • μ) T C → MeasureTheory.DominatedFinMeasAdditive μ T (c.toReal * C)
-- Mathlib.Topology.CantorBendixson
CantorBendixson.isClosed_perfectKernel : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → IsClosed (CantorBendixson.perfectKernel s)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The natural transformation `K.homologyπ i : K.cycles i ⟶ K.homology i`
for all `K : HomologicalComplex C c`.  -/
HomologicalComplex.natTransHomologyπ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          (i : ι) →
            [inst_2 : CategoryTheory.CategoryWithHomology C] →
              HomologicalComplex.cyclesFunctor C c i ⟶ HomologicalComplex.homologyFunctor C c i
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaObjObjEquiv_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ}
  {Y Y' : C} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y),
  CategoryTheory.shrinkCoyonedaObjObjEquiv
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g)) f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f) g
-- Mathlib.GroupTheory.Congruence.Defs
Con.comap_rel : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M → N} (H : ∀ (x y : M), f (x * y) = f x * f y)
  {c : Con N} {x y : M}, (Con.comap f H c) x y ↔ c (f x) (f y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert_le_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k}, (compare (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey! t.minKey!).isLE = true
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
/-- Every Kan complex is a quasicategory.  -/
SSet.instQuasicategoryOfKanComplex : ∀ (S : SSet) [S.KanComplex], S.Quasicategory
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} {f g : X ⟶ Y}
  (h₁ : f.f = g.f), (∀ (i : X.I), CategoryTheory.CategoryStruct.comp (f.φ i) (CategoryTheory.eqToHom ⋯) = g.φ i) → f = g
-- Mathlib.CategoryTheory.Yoneda
/-- If `F ≅ F'`, and `F` is representable, then `F'` is representable.  -/
CategoryTheory.Functor.RepresentableBy.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F F' : CategoryTheory.Functor Cᵒᵖ (Type v)} → {Y : C} → F.RepresentableBy Y → (F ≅ F') → F'.RepresentableBy Y
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_le_iff : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, ⌊a⌋ ≤ z ↔ a < ↑z + 1
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_algEquivOfEq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : f = g), ⇑(AdjoinRoot.algEquivOfEq R f g hfg) = ⇑(AdjoinRoot.algHomOfDvd R f g ⋯)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_comm' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), Associated (gcd a b) (gcd b a)
-- Init.Data.SInt.Lemmas
Int16.eq_iff_ofBitVec_eq : ∀ {a b : BitVec 16}, a = b ↔ Int16.ofBitVec a = Int16.ofBitVec b