mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- Given a morphism of presheaves of commutative rings `φ'`, this is the
in derivation `M.Derivation' φ'` that is given by a compatible family of derivations
with values in the modules `M.obj X` for all `X`.  -/
PresheafOfModules.Derivation'.mk : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
      {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
        {φ' : S' ⟶ R} →
          (d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)) →
            (∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(R.obj X)),
                (d Y).d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) =
                  (CategoryTheory.ConcreteCategory.hom (M.map f)) ((d X).d x)) →
              M.Derivation' φ'
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of an empty set is the trivial subgroup.  -/
Subgroup.normalClosure_empty : ∀ {G : Type u_1} [inst : Group G], Subgroup.normalClosure ∅ = ⊥
-- Aesop.Forward.Match.Types
Aesop.instInhabitedMatch : Inhabited Aesop.Match
-- Lean.Meta.WHNF
Lean.Meta.reduceNative? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Geometry.Manifold.Instances.Real
Icc_chartedSpaceChartAt : ∀ {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)},
  chartAt (EuclideanHalfSpace 1) z = if ↑z < y then IccLeftChart x y else IccRightChart x y
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredProd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered C] [CategoryTheory.IsFiltered D], CategoryTheory.IsFiltered (C × D)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_eq_some_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_prod : ∀ (J₁ : Type u) (J₂ : Type u') [inst : CategoryTheory.Category.{v, u} J₁] [inst_1 : CategoryTheory.Category.{v', u'} J₂]
  (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [CategoryTheory.IsCardinalFiltered J₁ κ]
  [CategoryTheory.IsCardinalFiltered J₂ κ], CategoryTheory.IsCardinalFiltered (J₁ × J₂) κ
-- Aesop.Saturate
Aesop.saturateMain : Aesop.LocalRuleSet → Lean.MVarId → Aesop.SaturateM Lean.MVarId
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_div : ∀ {a b : USize} (h : System.Platform.numBits = 32), (a / b).toBitVec32 h = a.toBitVec32 h / b.toBitVec32 h
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.commRing : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {R : Type u_10} →
                                      [inst_9 : CommRing R] →
                                        [inst_10 : TopologicalSpace R] →
                                          [inst_11 : ChartedSpace H' R] →
                                            [ContMDiffRing I' n R] → CommRing (ContMDiffMap I I' N R n)
-- Std.Http.Data.Chunk
Std.Http.instInhabitedChunk.default : Std.Http.Chunk
-- Aesop.Index.Basic
Aesop.instInhabitedIndexingMode : Inhabited Aesop.IndexingMode
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.distinctConstantsTheory_mono : ∀ {L : FirstOrder.Language} {α : Type u'} {s t : Set α},
  s ⊆ t → L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t
-- Mathlib.Data.List.Basic
List.mem_dropLast_iff_idxOf_lt : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α},
  a ∈ l → (a ∈ l.dropLast ↔ List.idxOf a l < l.length - 1)
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.hasTemperateGrowth_inner_left : ∀ {H : Type u_8} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H] (c : H),
  Function.HasTemperateGrowth fun x => inner ℝ x c
-- Mathlib.Data.Finset.Insert
/-- To prove a proposition about `S : Finset α`,
it suffices to prove it for the empty `Finset`,
and to show that if it holds for some `Finset α ⊆ S`,
then it holds for the `Finset` obtained by inserting a new element of `S`.
 -/
Finset.induction_on' : ∀ {α : Type u_3} {motive : Finset α → Prop} [inst : DecidableEq α] (S : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α), a ∈ S → s ⊆ S → a ∉ s → motive s → motive (insert a s)) → motive S
-- Init.Prelude
/-- Strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
 -/
UInt8.lt : UInt8 → UInt8 → Prop
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The type of morphisms in `ProfiniteAddGrp`.  -/
ProfiniteAddGrp.Hom : ProfiniteAddGrp.{u} → ProfiniteAddGrp.{u} → Type u
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Submonoid closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
Submonoid.closure_mono : ∀ {M : Type u_1} [inst : MulOneClass M] ⦃s t : Set M⦄, s ⊆ t → Submonoid.closure s ≤ Submonoid.closure t
-- Mathlib.Order.Category.Semilat
SemilatSupCat.instCoeSortType : CoeSort SemilatSupCat (Type u_1)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_add_aleph0 : Cardinal.aleph0 + Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.functor_comp : ∀ {J K L : Type u} [inst : LinearOrder J] [inst_1 : LinearOrder K] [inst_2 : LinearOrder L] (f : J →o K) (g : K →o L),
  CategoryTheory.SimplicialThickening.functor (g.comp f) =
    CategoryTheory.EnrichedFunctor.comp SSet (CategoryTheory.SimplicialThickening.functor f)
      (CategoryTheory.SimplicialThickening.functor g)
-- Mathlib.Data.DFinsupp.Submonoid
AddSubmonoid.mem_iSup_iff_exists_dfinsupp : ∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] [inst_1 : AddCommMonoid γ] (S : ι → AddSubmonoid γ) (x : γ),
  x ∈ iSup S ↔ ∃ f, (DFinsupp.sumAddHom fun i => (S i).subtype) f = x
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.mk : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma →
    Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma →
      Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma →
        Mathlib.Tactic.ClickSuggestions.PreDiscrTrees
-- Mathlib.Data.Nat.Log
Nat.lt_pow_succ_log_self : ∀ {b : ℕ}, 1 < b → ∀ (x : ℕ), x < b ^ (Nat.log b x).succ
-- Mathlib.Topology.UniformSpace.Pi
cauchy_pi_iff : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] [Nonempty ι] {l : Filter ((i : ι) → α i)},
  Cauchy l ↔ ∀ (i : ι), Cauchy (Filter.map (Function.eval i) l)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsBrownianReal.shift : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ},
  ProbabilityTheory.IsBrownianReal B P →
    ∀ (t₀ : NNReal), ProbabilityTheory.IsBrownianReal (fun t ω => B (t₀ + t) ω - B t₀ ω) P
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.toLinearMap_apply_apply_Polarization : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (x y : M), (P.toLinearMap y) (P.Polarization x) = (P.RootForm x) y
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower such that `E / F` is purely inseparable,
if `{ u_i }` is a family of separable elements of `K` which is `F`-linearly independent,
then it is also `E`-linearly independent.  -/
LinearIndependent.map_of_isPurelyInseparable_of_isSeparable : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E] {ι : Type u_1}
  {v : ι → K}, (∀ (i : ι), IsSeparable F (v i)) → LinearIndependent F v → LinearIndependent E v
-- Mathlib.Analysis.MellinTransform
/-- If `f` is a locally integrable real-valued function on `Ioi 0` which is `O(x ^ (-a))` at `∞`
and `O(x ^ (-b))` at `0`, then its Mellin transform integral converges for `b < s < a`.  -/
mellin_convergent_of_isBigO_scalar : ∀ {a b : ℝ} {f : ℝ → ℝ} {s : ℝ},
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    (f =O[Filter.atTop] fun x => x ^ (-a)) →
      s < a →
        (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) →
          b < s → MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.I : Type u → Type v → Bool → Type (max u v)
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.decomposeFin.symm_sign : ∀ {n : ℕ} (p : Fin (n + 1)) (e : Equiv.Perm (Fin n)),
  Equiv.Perm.sign (Equiv.Perm.decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * Equiv.Perm.sign e
-- Lean.Data.Lsp.Internal
/-- Converts `id` to its compact serialization representation.  -/
Lean.Lsp.RefIdent.toJsonRepr : Lean.Lsp.RefIdent → Lean.Lsp.RefIdent.RefIdentJsonRepr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Evaluation on an object `X` gives a functor
`PresheafOfModules R ⥤ ModuleCat (R.obj X)`.  -/
PresheafOfModules.evaluation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) →
      (X : Cᵒᵖ) → CategoryTheory.Functor (PresheafOfModules R) (ModuleCat ↑(R.obj X))
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The internal ring tactic representation of `c.norm`  -/
Mathlib.Tactic.Determinant.Cert.val : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → (c : Mathlib.Tactic.Determinant.Cert rα) → Mathlib.Tactic.Determinant.CertVal rα c.norm
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.biUnion_Iic_aecover : ∀ {α : Type u_1} {ι : Type u_2} [Countable ι] [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : Preorder ι] {φ : ι → Set α},
  MeasureTheory.AECover μ Filter.atTop φ → MeasureTheory.AECover μ Filter.atTop fun n => ⋃ k ∈ Set.Iic n, φ k
-- Mathlib.Order.BoundedOrder.Monotone
monotone_lt : ∀ {α : Type u} [inst : Preorder α] {x : α}, Monotone fun x_1 => x < x_1
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.memCarrier : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {s : hI.SubDPIdeal} {x : A},
  x ∈ s.carrier ↔ x ∈ s
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.instInhabited : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Inhabited (Matrix.SpecialLinearGroup n R)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X * c`
has Gaussian law with mean `c * μ` and variance `c ^ 2 * v`.  -/
ProbabilityTheory.gaussianReal_mul_const : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (c : ℝ),
      ProbabilityTheory.HasLaw (fun ω => X ω * c) (ProbabilityTheory.gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)) P
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
continuous_of_linear_of_bound : ∀ {𝕜 : Type u_1} {E : Type u_3} {G : Type u_5} [inst : Ring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup G] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 G] {f : E → G},
  (∀ (x y : E), f (x + y) = f x + f y) →
    (∀ (c : 𝕜) (x : E), f (c • x) = c • f x) → ∀ {C : ℝ}, (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → Continuous f
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.exprsEqualUpToIdsCore : Lean.Expr → Lean.Expr → ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIdsM Bool
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.finsetInf_mem : ∀ {α : Type u_2} {s : Set α} {ι : Type u_4} {f : ι → α} {t : Finset ι} [inst : SemilatticeInf α] [inst_1 : OrderTop α],
  CountableInfClosed s → t.Nonempty → (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s
-- Mathlib.GroupTheory.IndexNSmul
/-- If `A` is a subgroup of finite index of an additive group `M` that is finitely generated
and torsion-free as a `ℤ`-module, then `A` and `M` have the same rank.  -/
AddSubgroup.finrank_eq_of_finiteIndex : ∀ {M : Type u_1} [inst : AddCommGroup M] [Module.Finite ℤ M] [Module.IsTorsionFree ℤ M] (A : AddSubgroup M)
  [A.FiniteIndex], Module.finrank ℤ ↥A = Module.finrank ℤ M
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toSubMulAction_strictMono : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  StrictMono Submodule.toSubMulAction
-- Lean.Meta.Injective
Lean.Meta.mkInjectiveTheoremNameFor : Lean.Name → Lean.Name
-- Aesop.Script.Step
Aesop.Script.Step.sTactic? : Aesop.Script.Step → Option Aesop.Script.STactic
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.degree_nodal : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R],
  (Lagrange.nodal s v).degree = ↑s.card
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.resolveId? : Lean.Syntax → optParam String "term" → optParam Bool false → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_eq_iff : ∀ {R : Type u} [inst : LinearOrder R] {x y z : Tropical R}, x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack : Type
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimitSMulWithZero : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → SMulWithZero R ↑(ModuleCat.FilteredColimits.M F)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instAddAction : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddAction α (LowerSet α)
-- Mathlib.Order.Filter.Pointwise
Filter.subtractionCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : SubtractionCommMonoid α],
  Filter.subtractionCommMonoid = { toSubtractionMonoid := Filter.subtractionMonoid, add_comm := ⋯ }
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Any edge in the 2-truncated simplicial set `A` defines a morphism in the homotopy category
by taking its equivalence class.
 -/
SSet.Truncated.HomotopyCategory₂.homMk : {A : SSet.Truncated 2} →
  [inst : A.Quasicategory₂] →
    {x y : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })} →
      SSet.Truncated.Edge x y → ({ pt := x } ⟶ { pt := y })
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParamPerms.mk : ℕ → Array Lean.Elab.FixedParamPerm → Array (Array (Array ℕ)) → Lean.Elab.FixedParamPerms
-- Init.Data.List.Sublist
List.infix_append : ∀ {α : Type u_1} (l₁ l₂ l₃ : List α), l₂ <:+: l₁ ++ l₂ ++ l₃
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toList_eq_nil_iff : ∀ {α : Type u} {r : Std.Roo α} [LE α] [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], r.toList = [] ↔ ∀ (a : α), Std.PRange.succ? r.lower = some a → ¬a < r.upper
-- Mathlib.Data.ENNReal.Basic
/-- A version of `WithTop.recTopCoe` that uses `ENNReal.ofNNReal`.  -/
ENNReal.recTopCoe : {C : ENNReal → Sort u_2} → C ⊤ → ((x : NNReal) → C ↑x) → (x : ENNReal) → C x
-- Mathlib.Data.Nat.Squarefree
Squarefree.nodup_primeFactorsList : ∀ {n : ℕ}, Squarefree n → n.primeFactorsList.Nodup
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.card_addOrderOf_eq_totient : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ},
  Nat.card { u // addOrderOf u = n } = n.totient
-- Mathlib.Geometry.Euclidean.Projection
/-- Reflecting a point in two subspaces produces the same result if
and only if the point has the same orthogonal projection in each of
those subspaces.  -/
EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s₁ s₂ : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s₁] [inst_6 : Nonempty ↥s₂] [inst_7 : s₁.direction.HasOrthogonalProjection]
  [inst_8 : s₂.direction.HasOrthogonalProjection] (p : P),
  (EuclideanGeometry.reflection s₁) p = (EuclideanGeometry.reflection s₂) p ↔
    ↑((EuclideanGeometry.orthogonalProjection s₁) p) = ↑((EuclideanGeometry.orthogonalProjection s₂) p)
-- Mathlib.Tactic.Linter.TextBased
/-- Removes quotation marks '"' at front and back of string.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.removeQuotations : String → String
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma_mem : ∀ {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
  γ ∈ CongruenceSubgroup.Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instIsStableUnderTransfiniteCompositionInnerAnodyneExtensions : SSet.innerAnodyneExtensions.IsStableUnderTransfiniteComposition
-- Lean.Parser.Basic
Lean.Parser.trailingNodeFn : Lean.SyntaxNodeKind → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Topology.Connected.LocallyPathConnected
connectedComponentsEquivZerothHomotopy_symm_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyPathConnectedSpace X] (x : X),
  connectedComponentsEquivZerothHomotopy.symm (ZerothHomotopy.mk x) = ⟦x⟧
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given an injective function, there is an embedding from the comapped graph into the original
graph.  -/
SimpleGraph.Embedding.comap : {V : Type u_1} → {W : Type u_2} → (f : V ↪ W) → (G : SimpleGraph W) → SimpleGraph.comap (⇑f) G ↪g G
-- Mathlib.Data.ENat.Basic
ENat.add_one_pos : ∀ {n : ℕ∞}, 0 < n + 1
-- Init.Tactics
/-- Like `refine`, but operating on stateful `Std.Do.SPred` goals.
```lean
example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
  mintro ⟨HP, HQ, HR⟩
  mrefine ⟨HP, HR⟩

example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mrefine ⟨⌜42⌝, H⟩
```
 -/
Lean.Parser.Tactic.mrefineMacro : Lean.ParserDescr
-- Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
/-- The adjoint of the nilpotent part of a JC decomposition lies in the subalgebra generated by
the adjoint of the sum.  -/
LieAlgebra.ad_mem_adjoin_of_isNilpotent : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [PerfectField K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] {n s : Module.End K V},
  Commute n s →
    IsNilpotent n →
      s.IsSemisimple → (LieAlgebra.ad K (Module.End K V)) n ∈ K[(LieAlgebra.ad K (Module.End K V)) (n + s)]
-- Init.Data.List.Basic
/-- Erases duplicated elements in the list, using a given comparison function,
keeping the first occurrence of duplicated elements.

`O(|l|^2)`.

Examples:
 * `[1, 3, 4, 2, 1, 5].eraseDupsBy (· % 3 == · % 3) = [1, 3, 2]`
 -/
List.eraseDupsBy : {α : Type u_1} → (α → α → Bool) → List α → List α
-- Mathlib.Algebra.BigOperators.Group.List.Basic
MonoidHom.map_list_prod : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (l : List M),
  f l.prod = (List.map (⇑f) l).prod
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyonedaType.eq_1 : CommMonCat.coyonedaType =
  {
    obj := fun X =>
      { obj := fun M => CommMonCat.of (Opposite.unop X → ↑M),
        map := fun {X_1 Y} f =>
          CommMonCat.ofHom (MonoidHom.pi fun i => (CommMonCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X_1) i)),
        map_id := ⋯, map_comp := ⋯ },
    map := fun {X Y} f =>
      {
        app := fun N =>
          CommMonCat.ofHom
            (MonoidHom.pi fun i => Pi.evalMonoidHom (fun a => ↑N) ((CategoryTheory.ConcreteCategory.hom f.unop) i)),
        naturality := ⋯ },
    map_id := CommMonCat.coyonedaType._proof_4, map_comp := @CommMonCat.coyonedaType._proof_5 }
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.toOne : {E : Type u_3} → [inst : AddGroup E] → [DecidableEq E] → One (AddGroupSeminorm E)
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is a numeral and has type `Nat`.  -/
Lean.Meta.Grind.Arith.isNatNum : Lean.Expr → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_getValue?_ext : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {l l' : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys l' →
      (∀ (a : α), Std.Internal.List.getKey? a l = Std.Internal.List.getKey? a l') →
        (∀ (a : α), Std.Internal.List.getValue? a l = Std.Internal.List.getValue? a l') → l.Perm l'
-- Mathlib.RingTheory.FiniteType
AlgHom.FiniteType.comp_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {f : A →ₐ[R] B} {g : B →ₐ[R] C}, f.FiniteType → Function.Surjective ⇑g → (g.comp f).FiniteType
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso.congr_simp : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n a a' : M) (ha' : n + a = a'),
  F.shiftIso n a a' ha' = F.shiftIso n a a' ha'
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The family of the morphisms `f x.i : A x.i ⟶ B x.i`
parametrized by `x : FunctorObjIndex f πX`.  -/
CategoryTheory.SmallObject.functorObjLeftFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) →
                CategoryTheory.SmallObject.functorObjSrcFamily f πX x ⟶
                  CategoryTheory.SmallObject.functorObjTgtFamily f πX x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplax_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : CategoryTheory.Oplax.StrongTrans F.toOplax G.toOplax) {a b : B}
  (f : a ⟶ b), (CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplax η).naturality f = η.naturality f
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.comm_comp_rTensor_comp_comm_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] (g : N →ₗ[R] P),
  ↑(TensorProduct.comm R P Q) ∘ₗ LinearMap.rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = LinearMap.lTensor Q g