mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
/-- Turn an element of a type `F` satisfying `MulHomClass F M N` into an actual
`MulHom`. This is declared as the default coercion from `F` to `M →ₙ* N`.  -/
MulHomClass.toMulHom : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : FunLike F M N] → [MulHomClass F M N] → F → M →ₙ* N
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.QuotStep.transportAlongEquiv.eq_1 : ∀ {α₁ : Type u_1} {m : Type u_1 → Type u_2} {β α₂ : Type u_1} [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [inst_2 : Monad m] [inst_3 : LawfulMonad m] {ita : Std.IterM m β} {itb : Std.IterM m β}
  (h : ita.Equiv itb),
  Std.IterM.QuotStep.transportAlongEquiv h =
    Quot.lift
      (fun s₁ =>
        have this := ⋯;
        Quot.mk (fun s₁ s₂ => (↑s₁).bundledQuotient = (↑s₂).bundledQuotient) this.choose)
      ⋯
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.commaFromOver_obj_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Over X)) (a : J),
  (CategoryTheory.WithTerminal.commaFromOver.obj K).hom.app a = (K.obj a).hom
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k : α},
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k =
        (m.contains k || (List.map Prod.fst l).contains k)
-- Batteries.Data.List.Lemmas
List.countPBefore_succ : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ},
  List.countPBefore p xs (i + 1) =
    if h : xs = [] then 0
    else if p (xs.head h) = true then List.countPBefore p xs.tail i + 1 else List.countPBefore p xs.tail i
-- Mathlib.Algebra.Opposites
MulOpposite.op_mul : ∀ {α : Type u_1} [inst : Mul α] (x y : α), MulOpposite.op (x * y) = MulOpposite.op y * MulOpposite.op x
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁)
      (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) =
    CategoryTheory.CategoryStruct.comp
      (x.negOnePow •
        CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁'))
      h
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.id_comp : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : IrreducibleSpace ↥X] (f : X.RationalMap Y),
  (AlgebraicGeometry.Scheme.RationalMap.id X).comp f = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLE_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, (cmp a k).isLE = true} (h : t₁.Equiv t₂), t₁.getKeyLE k h' = t₂.getKeyLE k ⋯
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_inclusion : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M),
  ⇑(BooleanSubalgebra.inclusion h) = Set.inclusion h
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.toList_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {l : List ((_ : α) × β)},
  List.map (fun p => (p.fst, f p.fst p.snd)) l =
    List.map (fun p => (p.fst, p.snd)) (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.injective_iff_projective_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : C},
  CategoryTheory.Injective J ↔ CategoryTheory.Projective (Opposite.op J)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.mk.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C} {m : M}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (f : CategoryTheory.ShiftedHom X Y m),
  CategoryTheory.Localization.SmallShiftedHom.mk W f = CategoryTheory.Localization.SmallHom.mk W f
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D)
  (G : CategoryTheory.Functor D C) {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [G.IsCoverDense J]
  [G.Full] [inst_5 : G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj]
  {P Q : CategoryTheory.Functor Cᵒᵖ A} (f : P ⟶ Q), K.W (G.op.whiskerLeft f) ↔ J.W f
-- Mathlib.Data.Finset.Grade
Multiset.isAtom_singleton : ∀ {α : Type u_1} (a : α), IsAtom {a}
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  (r : R) (f : ι →₀ M), (r • f).toDFinsupp = r • f.toDFinsupp
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_or_reachable_compl : ∀ {V : Type u} (G : SimpleGraph V) (u v w : V), G.Reachable u v ∨ Gᶜ.Reachable u w
-- Mathlib.Logic.Small.Defs
small_succ : ∀ (α : Type v), Small.{v + 1, v} α
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
max_mul_mul_le_max_mul_max : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : LinearOrder R] {a d : R} [PosMulMono R] [MulPosMono R] (b c : R),
  0 ≤ a → 0 ≤ d → max (a * b) (d * c) ≤ max a c * max d b
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.eq_3 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.zero' → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.succ → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.tail → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (c f fs : Turing.ToPartrec.Code) → c = f.cons fs → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (c f g : Turing.ToPartrec.Code) → c = f.comp g → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (c f g : Turing.ToPartrec.Code) → c = f.case g → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (c f : Turing.ToPartrec.Code) → c = f.fix → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match Turing.ToPartrec.Code.tail, k with
    | c@h:Turing.ToPartrec.Code.zero', k => h_1 c h k
    | c@h:Turing.ToPartrec.Code.succ, k => h_2 c h k
    | c@h:Turing.ToPartrec.Code.tail, k => h_3 c h k
    | c@h:(f.cons fs), k => h_4 c f fs h k
    | c@h:(f.comp g), k => h_5 c f g h k
    | c@h:(f.case g), k => h_6 c f g h k
    | c@h:f.fix, k => h_7 c f h k) =
    h_3 Turing.ToPartrec.Code.tail ⋯ k
-- Mathlib.Order.Filter.Pointwise
/-- `pure` as a `OneHom`.  -/
Filter.pureOneHom : {α : Type u_2} → [inst : One α] → OneHom α (Filter α)
-- Lean.DeprecatedModule
Lean.formatDeprecatedModuleWarning : Lean.Environment → Lean.ModuleIdx → Lean.Name → Lean.DeprecatedModuleEntry → String
-- Mathlib.CategoryTheory.ConnectedComponents
/-- Every function from connected components of a category gives a functor to discrete category  -/
CategoryTheory.ConnectedComponents.functorToDiscrete : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (X : Type u_1) → (CategoryTheory.ConnectedComponents J → X) → CategoryTheory.Functor J (CategoryTheory.Discrete X)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- A product of distinguished triangles is distinguished  -/
CategoryTheory.Pretriangulated.productTriangle_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C),
  (∀ (j : J), T j ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) →
    ∀ [inst_5 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
      [inst_6 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
      [inst_7 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
      [inst_8 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
      CategoryTheory.Pretriangulated.productTriangle T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.bernoulli.congr_simp : ∀ (p p_1 : NNReal) (e_p : p = p_1) (h : p ≤ 1), PMF.bernoulli p h = PMF.bernoulli p_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_inv_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.right =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.right)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instLineDerivAddTopENat : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F], LineDerivAdd E (TestFunction Ω F ⊤) (TestFunction Ω F ⊤)
-- Init.Data.SInt.Bitwise
UInt16.toInt16_xor : ∀ (a b : UInt16), (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMk_f : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : Type v} [inst_1 : AddCommGroup X₁] [inst_2 : AddCommGroup X₂]
  [inst_3 : AddCommGroup X₃] [inst_4 : Module R X₁] [inst_5 : Module R X₂] [inst_6 : Module R X₃] (f : X₁ →ₗ[R] X₂)
  (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0), (CategoryTheory.ShortComplex.moduleCatMk f g hfg).f = ModuleCat.ofHom f
-- Init.Data.Array.Lemmas
Array.id_run_foldlM : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → Id β} {b : β} {xs : Array α} {start stop : ℕ},
  (Array.foldlM f b xs start stop).run = Array.foldl (fun x1 x2 => (f x1 x2).run) b xs start stop
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v =
    Valuation.comap (IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv K v).toRingHom Valued.v
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.is_separable_splitting_field : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [IsGalois F E], ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.mk.sizeOf_spec : ∀ {k : Lean.SyntaxNodeKinds} (ref : Lean.Syntax) (patterns : Array Lean.Syntax) (lhs : Lean.Syntax)
  (rhs : Lean.TSyntax k),
  sizeOf { ref := ref, patterns := patterns, lhs := lhs, rhs := rhs } =
    1 + sizeOf ref + sizeOf patterns + sizeOf lhs + sizeOf rhs
-- Mathlib.Data.NNReal.Defs
NNReal.instCommMonoidWithZero : CommMonoidWithZero NNReal
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instOneHom.eq_1 : ∀ (G H : CommGrpCat), G.instOneHom H = { one := CommGrpCat.ofHom 1 }
-- Lean.Parser.Term
Lean.Parser.Term.basicFun.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.maxKeyD fallback = t_1.maxKeyD fallback_1
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.le_right : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} (self : CategoryTheory.SimplicialThickening.Path i j),
  ∀ k ∈ self.I, k ≤ j
-- Lean.Expr
/-- Return `fun (_ : Unit), e`  -/
Lean.mkSimpleThunk : Lean.Expr → Lean.Expr
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.mk.inj : ∀ {theoremName funName : Lean.Name} {hypothesesPos : Array ℕ} {priority : ℕ} {theoremName_1 funName_1 : Lean.Name}
  {hypothesesPos_1 : Array ℕ} {priority_1 : ℕ},
  { theoremName := theoremName, funName := funName, hypothesesPos := hypothesesPos, priority := priority } =
      { theoremName := theoremName_1, funName := funName_1, hypothesesPos := hypothesesPos_1, priority := priority_1 } →
    theoremName = theoremName_1 ∧ funName = funName_1 ∧ hypothesesPos = hypothesesPos_1 ∧ priority = priority_1
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_mk_ofList : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N') (l : List (M ⊕ N)),
  (AddMonoid.Coprod.map f g) (AddMonoid.Coprod.mk (FreeAddMonoid.ofList l)) =
    AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map ⇑f ⇑g) l))
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValue? k (List.filter (fun p => f p.fst p.snd) l) =
          Option.filter (fun x => f k' x) (Std.Internal.List.getValue? k l)
-- Lean.Elab.InfoTree.Types
/-- Contains the syntax of an identifier which is part of a field redeclaration, like:
```
structure Foo := x : Nat
structure Bar extends Foo :=
  x := 0
--^ here
```
 -/
Lean.Elab.FieldRedeclInfo : Type
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G),
  (MeasureTheory.Measure.addHaarMeasure K₀).IsAddLeftInvariant
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f g) g')
        (CategoryTheory.Limits.pullback.snd f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (CategoryTheory.CategoryStruct.comp g' g))
      g'
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f : X → Y` is Hölder continuous in a neighborhood of every point `x : X` with the same
positive exponent `r` but possibly different coefficients, then the Hausdorff dimension of the range
of `f` is at most the Hausdorff dimension of `X` divided by `r`.  -/
dimH_range_le_of_locally_holder_on : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [SecondCountableTopology X]
  {r : NNReal} {f : X → Y},
  0 < r → (∀ (x : X), ∃ C, ∃ s ∈ nhds x, HolderOnWith C r f s) → dimH (Set.range f) ≤ dimH Set.univ / ↑r
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_subtype : ∀ {𝕜 : 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 : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] (s' : AffineSubspace 𝕜 ↥s) [inst_6 : Nonempty ↥s']
  [inst_7 : s'.direction.HasOrthogonalProjection]
  [inst_8 : (AffineSubspace.map s.subtype s').direction.HasOrthogonalProjection] (p : ↥s),
  ↑↑((EuclideanGeometry.orthogonalProjection s') p) =
    ↑((EuclideanGeometry.orthogonalProjection (AffineSubspace.map s.subtype s')) ↑p)
-- Mathlib.Data.Finset.Lattice.Lemmas
List.toFinset_append : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α}, (l ++ l').toFinset = l.toFinset ∪ l'.toFinset
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- The right Kan extension functor `L.ran` is right adjoint to the
precomposition by `L`.  -/
CategoryTheory.Functor.ranAdjunction : {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] →
        (L : CategoryTheory.Functor C D) →
          (H : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] →
                (CategoryTheory.Functor.whiskeringLeft C D H).obj L ⊣ L.ran
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.callerMeasures : Lean.Elab.WF.GuessLex.RecCallCache → Array Lean.Elab.WF.GuessLex.BasicMeasure
-- Init.Data.Int.Order
Int.nonpos_of_mul_nonneg_left : ∀ {a b : ℤ}, 0 ≤ a * b → b < 0 → a ≤ 0
-- Mathlib.Data.Matrix.Block
Matrix.toBlock_one_disjoint : ∀ {m : Type u_2} {α : Type u_12} [inst : DecidableEq m] [inst_1 : Zero α] [inst_2 : One α] {p q : m → Prop},
  Disjoint p q → Matrix.toBlock 1 p q = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : k ∈ t), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremType.apply.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremType.apply = 1
-- Mathlib.Data.Nat.Multiplicity
/-- The multiplicity of `p` in `(p * (n + 1))!` is one more than the sum
of the multiplicities of `p` in `(p * n)!` and `n + 1`.  -/
Nat.Prime.emultiplicity_factorial_mul_succ : ∀ {n p : ℕ},
  Nat.Prime p →
    emultiplicity p (p * (n + 1)).factorial = emultiplicity p (p * n).factorial + emultiplicity p (n + 1) + 1
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
BialgEquiv.toHopfAlgIso_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : HopfAlgebra R X]
  [inst_4 : HopfAlgebra R Y] (e : X ≃ₐc[R] Y), e.symm.toHopfAlgIso = e.toHopfAlgIso.symm
-- Lean.HeadIndex
Lean.HeadIndex.proj.injEq : ∀ (structName : Lean.Name) (idx : ℕ) (structName_1 : Lean.Name) (idx_1 : ℕ),
  (Lean.HeadIndex.proj structName idx = Lean.HeadIndex.proj structName_1 idx_1) =
    (structName = structName_1 ∧ idx = idx_1)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.addConvolution_indicator_zero_right : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [inst : AddMonoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid F] [inst_4 : Module S E] [inst_5 : Module S F]
  [inst_6 : TopologicalSpace F] (L : F →ₗ[S] E →ₗ[S] F) (f : M → F) (e : E),
  (∀ (y : F), (L y) e = y) → DiscreteConvolution.addConvolution L f ({0}.indicator fun x => e) = f
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_subset : ∀ {α : Type u_1} (a b c : Set α), a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c
-- Mathlib.Algebra.Group.Conj
mem_conjugatesOf_self : ∀ {α : Type u} [inst : Monoid α] {a : α}, a ∈ conjugatesOf a
-- Init.Data.SInt.Lemmas
ISize.ofNat_le_iff_le : ∀ {a b : ℕ},
  a < 2 ^ (System.Platform.numBits - 1) →
    b < 2 ^ (System.Platform.numBits - 1) → (ISize.ofNat a ≤ ISize.ofNat b ↔ a ≤ b)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (Topology.WithLower α)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_injOn : ∀ {n d : ℕ}, Set.InjOn ⇑(Behrend.map d) {x | ∀ (i : Fin n), x i < d}
-- Mathlib.Data.WSeq.Defs
_private.Mathlib.Data.WSeq.Defs.0.Stream'.WSeq.length.match_1.eq_3 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) (val : α) (s' : Stream'.Seq (Option α))
  (h_1 : Unit → motive none) (h_2 : (s' : Stream'.Seq (Option α)) → motive (some (none, s')))
  (h_3 : (val : α) → (s' : Stream'.Seq (Option α)) → motive (some (some val, s'))),
  (match some (some val, s') with
    | none => h_1 ()
    | some (none, s') => h_2 s'
    | some (some val, s') => h_3 val s') =
    h_3 val s'
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.computeSize_eq : ∀ {α : Type u} {β : α → Type v} {buckets : Array (Std.DHashMap.Internal.AssocList α β)},
  Std.DHashMap.Internal.computeSize buckets = (Std.DHashMap.Internal.toListModel buckets).length
-- Std.Do.WP.SimpLemmas
Std.Do.WP.orElse_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {x : OptionT m α} {h : Unit → OptionT m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  (Std.Do.wp (OrElse.orElse x h)).apply Q = (Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)
-- Lean.ExtraModUses
/-- Returns additional recorded import dependencies of the given module.  -/
Lean.getExtraModUses : Lean.Environment → Lean.ModuleIdx → Array Lean.ExtraModUse
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two antitone functions is antitone.  -/
Antitone.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [AddLeftMono α]
  [AddRightMono α], Antitone f → Antitone g → Antitone fun x => f x + g x
-- Mathlib.Data.List.Nodup
List.Nodup.suffix_of_getLast_mem_of_infix : ∀ {α : Type u} {l₁ l₂ : List α}, l₁ <:+: l₂ → ∀ {hne : l₂ ≠ []}, l₂.getLast hne ∈ l₁ → l₂.Nodup → l₁ <:+ l₂
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.two_power_aleph0 : 2 ^ Cardinal.aleph0 = Cardinal.continuum
-- Mathlib.GroupTheory.Congruence.Defs
Con.instCoeTCQuotient.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), c.instCoeTCQuotient = { coe := Con.toQuotient }
-- Mathlib.Analysis.Normed.Group.BallSphere
/-- We equip the ball, in a seminormed group, with a formal operation of negation, namely the
antipodal map.  -/
instInvolutiveNegElemBallOfNat : {E : Type u_1} → [i : SeminormedAddCommGroup E] → {r : ℝ} → InvolutiveNeg ↑(Metric.ball 0 r)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  {X Y : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A} (f : X ⟶ Y),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.map f).hom = f.hom