mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.linearIndependent_baseSupp : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] [IsDomain R]
  [CharZero R], LinearIndependent R b.baseSupp
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  (X : (CategoryTheory.isCardinalPresentable C κ).FullSubcategory),
  CategoryTheory.IsCardinalPresentable ((CategoryTheory.isCardinalPresentable C κ).ι.obj X) κ
-- Mathlib.Topology.GDelta.Basic
residual.eq_1 : ∀ (X : Type u_5) [inst : TopologicalSpace X], residual X = Filter.countableGenerate {t | IsOpen t ∧ Dense t}
-- Init.Data.List.Lemmas
List.concat_beq_concat : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l₁ l₂ : List α}, (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.f_int_negSucc : ∀ (k : ℕ) {a : ℝ},
  a ≤ 1 → ∀ (t : ℝ) (n : ℕ), HurwitzKernelBounds.f_int k a t (Int.negSucc n) = HurwitzKernelBounds.f_nat k (1 - a) t n
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_inj : ∀ {M : Type u_2} [inst : MulOneClass M] {S T : Submonoid M}, S.op = T.op ↔ S = T
-- Mathlib.CategoryTheory.Skeletal
/-- Given a bifunctor, we descend to a function on objects of `ThinSkeleton`  -/
CategoryTheory.ThinSkeleton.map₂ObjMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) →
              CategoryTheory.ThinSkeleton C → CategoryTheory.ThinSkeleton D → CategoryTheory.ThinSkeleton E
-- Mathlib.Data.ENNReal.Lemmas
ENNReal.coe_indicator : ∀ {α : Type u_2} (s : Set α) (f : α → NNReal) (a : α), ↑(s.indicator f a) = s.indicator (fun x => ↑(f x)) a
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The canonical extension of a functor `C ⥤ Karoubi D` to a functor
`Karoubi C ⥤ Karoubi D`  -/
CategoryTheory.Idempotents.FunctorExtension₁.obj : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D) →
          CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)
-- Mathlib.Analysis.Fourier.AddCircle
fourier_zero : ∀ {T : ℝ} {x : AddCircle T}, (fourier 0) x = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_zero_eq_const : SimplexCategory.δ 0 = { len := 0 }.const { len := 0 + 1 } 1
-- Mathlib.RingTheory.HopfAlgebra.Quotient
HopfAlgebra.Quotient.antipode_mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : HopfAlgebraStruct R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : Ideal.IsHopfIdeal R I] (a : A),
  (HopfAlgebraStruct.antipode R) ((Ideal.Quotient.mk I) a) = (Ideal.Quotient.mk I) ((HopfAlgebraStruct.antipode R) a)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_closure_left`.

---

Replacing a set by its closure does not change the Hausdorff edistance.  -/
EMetric.hausdorffEdist_closure₁ : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist (closure s) t = Metric.hausdorffEDist s t
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instIteratorLoop.loop.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] {inst_2 : DecidableLT α} [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [inst_5 : Monad n] (γ : Type u)
  (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α)
  (acc acc_1 : γ),
  acc = acc_1 →
    ∀ (next next_1 : α) (e_next : next = next_1) (h : LargeEnough next)
      (f f_1 : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (Pl out c))),
      f = f_1 →
        Std.Rxo.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc next h f =
          Std.Rxo.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc_1 next_1 ⋯ f_1
-- Init.Data.Int.OfNat
Nat.ToInt.sub_congr : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a - b) = if b' + -1 * a' ≤ 0 then a' - b' else 0
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_leftOp_iff_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  {F : CategoryTheory.Functor J Cᵒᵖ}, CategoryTheory.Limits.HasLimit F.leftOp ↔ CategoryTheory.Limits.HasColimit F
-- Mathlib.Analysis.Seminorm
Seminorm.smul_ball_preimage : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜), a ≠ 0 → (fun x => a • x) ⁻¹' p.ball y r = p.ball (a⁻¹ • y) (r / ‖a‖)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i)
  (w :
    ∀ (i : ℕ) (hi : i < n),
      CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom =
        CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)),
  (CategoryTheory.ComposableArrows.isoMk app w).inv = CategoryTheory.ComposableArrows.homMk (fun i => (app i).inv) ⋯
-- Mathlib.Data.Real.Basic
Real.ofCauchy : CauSeq.Completion.Cauchy abs → ℝ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_erase_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.minKey! = Ordering.eq → (t.erase k).minKey! = t.minKey!
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.pop : Lean.Parser.SyntaxStack → Lean.Parser.SyntaxStack
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.smul : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a b : α → 𝕜} {u v : α → E} {l : Filter α},
  Asymptotics.IsEquivalent l a b →
    Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l (fun x => a x • u x) fun x => b x • v x
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_withDensity_eq_setIntegral_toReal_smul₀ : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → ENNReal} {s : Set X},
  AEMeasurable f (μ.restrict s) →
    (∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) →
      ∀ (g : X → E),
        MeasurableSet s → (∫ (x : X) in s, g x ∂μ.withDensity fun x => f x) = ∫ (x : X) in s, (f x).toReal • g x ∂μ
-- Mathlib.Algebra.MonoidAlgebra.Grading
/-- `AddMonoidAlgebra.grade` describe an internally graded algebra.  -/
AddMonoidAlgebra.grade.isInternal : ∀ {ι : Type u_2} {R : Type u_3} [inst : DecidableEq ι] [AddMonoid ι] [inst_2 : CommSemiring R],
  DirectSum.IsInternal (AddMonoidAlgebra.grade R)
-- Batteries.Data.AssocList
/-- Implementation of `==` on `AssocList`.  -/
Batteries.AssocList.beq : {α : Type u_1} → {β : Type u_2} → [BEq α] → [BEq β] → Batteries.AssocList α β → Batteries.AssocList α β → Bool
-- Init.Data.SInt.Lemmas
Int16.toBitVec_sub : ∀ {a b : Int16}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.RestrictionCoextensionAdj.unit'_app : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (Y : ModuleCat S),
  (ModuleCat.RestrictionCoextensionAdj.unit' f).app Y = ModuleCat.ofHom (ModuleCat.RestrictionCoextensionAdj.app' f Y)
-- Std.Data.DTreeMap.Internal.Operations
/-- A balanced tree of one of the given sizes.  -/
Std.DTreeMap.Internal.Impl.SizedBalancedTree : (α : Type u) → (α → Type v) → ℕ → ℕ → Type (max u v)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Complex.measurableEquivPi_symm_apply : ∀ (p : Fin 2 → ℝ), Complex.measurableEquivPi.symm p = ↑(p 0) + ↑(p 1) * Complex.I
-- Std.Sync.Channel
/-- Return `true` if the channel is closed.
 -/
Std.CloseableChannel.isClosed : {α : Type} → Std.CloseableChannel α → BaseIO Bool
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
CategoryTheory.ShortComplex.isoMk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e₁ e₁_1 : S₁.X₁ ≅ S₂.X₁) (e_e₁ : e₁ = e₁_1) (e₂ e₂_1 : S₁.X₂ ≅ S₂.X₂)
  (e_e₂ : e₂ = e₂_1) (e₃ e₃_1 : S₁.X₃ ≅ S₂.X₃) (e_e₃ : e₃ = e₃_1)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom)
  (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom),
  CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃ = CategoryTheory.ShortComplex.isoMk e₁_1 e₂_1 e₃_1 ⋯ ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- A morphism property satisfies `IsStableUnderComposition` if the composition of
two such morphisms still falls in the class.  -/
CategoryTheory.MorphismProperty.IsStableUnderComposition : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.mem_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K : Subgroup G} {y : N},
  y ∈ Subgroup.map f K ↔ ∃ x ∈ K, f x = y
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.norm_of_mem_sphere : ∀ {n d k : ℕ} {x : Fin n → ℕ}, x ∈ Behrend.sphere n d k → ‖WithLp.toLp 2 (Nat.cast ∘ x)‖ = √↑k
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_Seq_seq : ∀ {ps : Std.Do.PostShape} {α β : Type u} (f : Std.Do.PredTrans ps (α → β)) (x : Std.Do.PredTrans ps α)
  (Q : Std.Do.PostCond β ps), (f <*> x).apply Q = f.apply (fun g => x.apply (fun a => Q.1 (g a), Q.2), Q.2)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ : Std.DTreeMap α (fun x => Unit) cmp} {l : List α},
  (Std.DTreeMap.Const.insertManyIfNewUnit t₁ l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) t₁ l)
-- Mathlib.Order.Minimal
Minimal.eq_of_le : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : PartialOrder α], Minimal P x → P y → y ≤ x → y = x
-- Mathlib.Order.Bounds.Basic
isGreatest_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], IsGreatest Set.univ ⊤
-- Mathlib.Topology.Path
Path.continuous_uncurry_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {Y : Type u_4} [inst_1 : TopologicalSpace Y] {g : Y → Path x y},
  Continuous ↿g ↔ Continuous g
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_apply_zero : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R},
  cfc f 0 = (algebraMap R A) (f 0)
-- Mathlib.Data.Setoid.Basic
/-- Equivalence closure of binary relations is monotone.  -/
Setoid.eqvGen_mono : ∀ {α : Type u_1} {r s : α → α → Prop},
  (∀ (x y : α), r x y → s x y) → Relation.EqvGen.setoid r ≤ Relation.EqvGen.setoid s
-- Lean.SubExpr
Lean.SubExpr.instFromJsonGoalsLocation : Lean.FromJson Lean.SubExpr.GoalsLocation
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.exactFVar : Lean.MVarId → Lean.FVarId → Lean.Meta.TransparencyMode → Aesop.Script.TacticBuilder
-- Init.Notation
/-- Boolean “and”, also known as conjunction. `and x y` can be written `x && y`.

The corresponding propositional connective is `And : Prop → Prop → Prop`, written with the `∧`
operator.

The Boolean `and` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `false` then `y` is not evaluated at runtime.


Conventions for notations in identifiers:

 * The recommended spelling of `&&` in identifiers is `and`. -/
«term_&&_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α), Std.DTreeMap.Internal.Impl.leaf.getEntry? k = none
-- Qq.Macro
Qq.Impl.whnf : (e : Lean.Expr) → optParam Lean.Expr e → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.GroupAction.Period
/-- For any non-zero `n` less than the period of `m` on `a`, `a` is moved by `m ^ n`.  -/
MulAction.pow_smul_ne_of_lt_period : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α} {n : ℕ},
  0 < n → n < MulAction.period m a → m ^ n • a ≠ a
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_scomp_eq_sum_orderedFinpartition : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {s t : Set 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ},
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContDiffWithinAt 𝕜 n f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              ↑i ≤ n →
                iteratedDerivWithin i (g ∘ f) s x =
                  ∑ c, (∏ j, iteratedDerivWithin (c.partSize j) f s x) • iteratedDerivWithin c.length g t (f x)
-- Init.Data.Dyadic.Basic
Dyadic.le_antisymm : ∀ {x y : Dyadic}, x ≤ y → y ≤ x → x = y
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iff_comap_eq : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H
-- Std.Internal.UV.System
/-- Gets information about the operating system.
 -/
Std.Internal.UV.System.osUname : IO Std.Internal.UV.System.UnameInfo
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.mapsTo_sphere : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ℝ), Set.MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eq_get_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {he : l.isEmpty = false},
  Std.Internal.List.minKey l he = (Std.Internal.List.minKey? l).get ⋯
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.grade.decompose_single : ∀ {ι : Type u_2} {R : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R] (i : ι) (r : R),
  (DirectSum.decompose (AddMonoidAlgebra.grade R)) (AddMonoidAlgebra.single i r) =
    (DirectSum.of (fun i => ↥(AddMonoidAlgebra.grade R i)) i) ⟨AddMonoidAlgebra.single i r, ⋯⟩
-- Mathlib.Algebra.Ring.Ext
Ring.toNonUnitalRing_injective : ∀ {R : Type u}, Function.Injective (@Ring.toNonUnitalRing R)
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `FunLike.natCast_eq_nsmul_one`. -/
FunLike.coe_natCast : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : NatCast F'] [inst_2 : One F'] [inst_3 : SMul ℕ α]
  [inst_4 : SMul ℕ F'] [IsSMulApply ℕ F' α α] [IsNatCastApply F' α] [IsOneApplyEqSelf F' α] (n : ℕ), ↑n = n • 1
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- The reverse of a path is another path.  See also `SimpleGraph.Walk.reverse`.  -/
SimpleGraph.Path.reverse : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Path u v → G.Path v u
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.ncard_oddComponents_mono : ∀ {V : Type u} (G : SimpleGraph V) [Finite V] {G' : SimpleGraph V},
  G ≤ G' → G'.oddComponents.ncard ≤ G.oddComponents.ncard
-- Lean.Parser.Basic
Lean.Parser.chFn : Char → optParam Bool false → Lean.Parser.ParserFn
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.toConnectedComponents_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), (ZerothHomotopy.mk x).toConnectedComponents = ⟦x⟧
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.is_skeletal : CategoryTheory.Skeletal FintypeCat.Skeleton
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedAddMonoid` under a strictly monotone map.  -/
StrictMono.isOrderedAddMonoid : ∀ {α : Type u} {β : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] (f : β → α),
  StrictMono f → (∀ (x y : β), f (x + y) = f x + f y) → IsOrderedAddMonoid β
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.target_inter_inv_preimage_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (s : Set Y), e.target ∩ ↑e.symm ⁻¹' ↑e ⁻¹' s = e.target ∩ s
-- Lean.Parser.Do
Lean.Parser.Term.doLetExpr : Lean.Parser.Parser
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- `reassoc_of% t`, where `t` is
an equation `f = g` between morphisms `X ⟶ Y` in a category (possibly after a `∀` binder),
produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`,
but with compositions fully right associated and identities removed.
This also works for equations between isomorphisms, provided that
`Tactic.CategoryTheory.IsoReassoc` has been imported.
 -/
Mathlib.Tactic.Reassoc.«termReassoc_of%_» : Lean.ParserDescr
-- Mathlib.NumberTheory.FLT.Four
/-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has
`a` odd and `c` positive.  -/
Fermat42.exists_pos_odd_minimal : ∀ {a b c : ℤ}, Fermat42 a b c → ∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsProper.isUniquelyCodimOneFace : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [self : P.IsProper] (x : ↑P.II),
  (↑x).IsUniquelyCodimOneFace (↑(P.p x)).toS
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.map_prod_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η]
  {f : β → δ}, Measurable f → (κ.map f).prod η = (κ.prod η).map (Prod.map f id)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular epimorphism is an isomorphism if it is a monomorphism.  -/
CategoryTheory.isIso_of_regularEpi_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (h : CategoryTheory.RegularEpi f)
  [CategoryTheory.Mono f], CategoryTheory.IsIso f
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure : Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits.injective : ∀ (b : ℕ), Function.Injective b.digits
-- Mathlib.Topology.NhdsWithin
/-- Writing a punctured neighborhood filter as a sup of left and right filters.  -/
punctured_nhds_eq_nhdsWithin_sup_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {x : α},
  nhdsWithin x {x}ᶜ = nhdsWithin x (Set.Iio x) ⊔ nhdsWithin x (Set.Ioi x)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x x_1 : C) (x_2 : D),
  (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D) x
          x_1).app
      x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x_2 x x_1).inv
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IciExtend.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β),
  Set.IciExtend f = f ∘ Set.projIci a
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_injective : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ),
  Function.Injective f → Function.Injective ⇑(MvPolynomial.rename f)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalOpOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.opOp C).Monoidal
-- Mathlib.CategoryTheory.Action.Basic
Action.trivial_V : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G] (X : V),
  (Action.trivial G X).V = X
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_sup_div_sup_le_mabs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b c : α), |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ
-- Mathlib.Data.List.Sublists
List.sublistsAux.eq_1 : ∀ {α : Type u} (a : α) (r : List (List α)), List.sublistsAux a r = List.foldl (fun r l => r ++ [l, a :: l]) [] r
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type Bₙ (rank n, corresponding to so(2n+1)).  -/
CartanMatrix.B : (n : ℕ) → Matrix (Fin n) (Fin n) ℤ
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.circleTransformDeriv_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E),
  Complex.circleTransformDeriv R z w f = fun θ => (circleMap z R θ - w)⁻¹ • Complex.circleTransform R z w f θ
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Note that `hφ = Quotient.out_eq'` is a useful choice here.  -/
AddAction.orbitRel.Quotient.orbit_eq_orbit_out : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (x : AddAction.orbitRel.Quotient G α)
  {φ : AddAction.orbitRel.Quotient G α → α}, Function.RightInverse φ Quotient.mk' → x.orbit = AddAction.orbit G (φ x)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.codeBlockSuggestions : Lean.Elab.TermElabM (Array (Lean.StrLit → Lean.Doc.DocM (Array Lean.Doc.CodeBlockSuggestion)))
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp.eq_1 : AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp =
  { preimage := fun {X Y} f => AddCommGrpCat.ofHom (AddGrpCat.Hom.hom f),
    map_preimage := @AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp._proof_1,
    preimage_map := @AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp._proof_2 }
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_T : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] (n : ℤ), (LaurentPolynomial.T n).degree = ↑n