mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BoundedOrder.Basic
/-- A bounded order describes an order `(≤)` with a top and bottom element,
denoted `⊤` and `⊥` respectively.  -/
BoundedOrder : (α : Type u) → [LE α] → Type u
-- Mathlib.Data.Set.Finite.Lattice
/-- **Alias** of `iInf_iSup_of_monotone`. -/
Set.iInf_iSup_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι']
  [inst_3 : Order.Coframe α] {f : ι → ι' → α}, (∀ (i : ι), Monotone (f i)) → ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j
-- Mathlib.InformationTheory.Hamming
/-- Type synonym for a Pi type which inherits the usual algebraic instances, but is equipped with
the Hamming metric and norm, instead of `Pi.normedAddCommGroup` which uses the sup norm.  -/
Hamming : {ι : Type u_1} → (ι → Type u_2) → Type (max u_1 u_2)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, (m.getKey? a).isSome = true ↔ a ∈ m
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.mk.injEq : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (toFun : UpperHalfPlane → ℂ)
  (slash_action_eq' : ∀ γ ∈ Γ, SlashAction.map k γ toFun = toFun) (toFun_1 : UpperHalfPlane → ℂ)
  (slash_action_eq'_1 : ∀ γ ∈ Γ, SlashAction.map k γ toFun_1 = toFun_1),
  ({ toFun := toFun, slash_action_eq' := slash_action_eq' } =
      { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 }) =
    (toFun = toFun_1)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceOfNatLT : Lean.Meta.Simp.DSimproc
-- Mathlib.GroupTheory.Coxeter.Length
_private.Mathlib.GroupTheory.Coxeter.Length.0.CoxeterSystem.termπ_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Types.Images
_private.Mathlib.CategoryTheory.Limits.Types.Images.0.CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage : {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} →
  (∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) →
    F.obj (Opposite.op 0) → (n : ℕ) → F.obj (Opposite.op n)
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_add_right_add : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G), ⁅a, b + c⁆ + ⁅b, c + a⁆ + ⁅c, a + b⁆ = 0
-- Lean.Util.MonadCache
/-- Adapter for implementing `MonadCache` interface using `HashMap`s.
We just have to specify how to extract/modify the `HashMap`.  -/
Lean.MonadHashMapCacheAdapter : (α : Type) → Type → (Type → Type) → [BEq α] → [Hashable α] → Type
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instSubsingleton : ∀ {α : Type u_1} [IsEmpty α] {m : MeasurableSpace α}, Subsingleton (MeasureTheory.Measure α)
-- Lean.Meta.MethodSpecs
/-- `opImpl = Cls.op instClsT`  -/
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem.type : Lean.MethodSpecTheorem✝ → Lean.Expr
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finsum_mem_union'` that requires `s ∩ support f` and
`t ∩ support f` rather than `s` and `t` to be disjoint  -/
finsum_mem_union'' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
  Disjoint (s ∩ Function.support f) (t ∩ Function.support f) →
    (s ∩ Function.support f).Finite →
      (t ∩ Function.support f).Finite →
        ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Data.Sym.Basic
Sym.erase_cons_head : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (s : Sym α n) (a : α) (h : optParam (a ∈ a ::ₛ s) ⋯),
  (a ::ₛ s).erase a h = s
-- Init.Data.String.Lemmas.Pattern.Find.String
String.contains_slice_eq_false_iff : ∀ {t : String.Slice} {s : String}, s.contains t = false ↔ ¬t.copy.toList <:+: s.toList
-- Mathlib.Tactic.NormNum.Prime
_private.Mathlib.Tactic.NormNum.Prime.0.Mathlib.Meta.NormNum.evalMinFac.core : (n : Q(ℕ)) →
  (sℕ : Q(AddMonoidWithOne ℕ)) →
    (nn : Q(ℕ)) → Q(Mathlib.Meta.NormNum.IsNat «$n» «$nn») → ℕ → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$n».minFac))
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modify_eq : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  (f : σ → σ),
  modify f = do
    let __do_lift ← get
    set (f __do_lift)
-- Init.Data.SInt.Lemmas
UInt32.toInt32_ofBitVec : ∀ (b : BitVec 32), { toBitVec := b }.toInt32 = Int32.ofBitVec b
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_nat_eq : ∀ {M : Type u_4} [inst : AddCommMonoid M] (s : AddSubmonoid M), (Submodule.span ℕ ↑s).toAddSubmonoid = s
-- Mathlib.Analysis.Complex.Periodic
_private.Mathlib.Analysis.Complex.Periodic.0.Function.Periodic.term𝕢 : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.instIsStrictOrderedRingFiniteElement : ∀ (K : Type u_1) [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  IsStrictOrderedRing (ArchimedeanClass.FiniteElement K)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Ioo_castAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m ⁻¹' Set.Ioo (Fin.castAdd m i) (Fin.castAdd m j) = Set.Ioo i j
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toCycle_eq_toList : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle) (x : α),
  f x ≠ x → f.toCycle hf = ↑(f.toList x)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instIsCancelMulZeroOfIsCancelAdd : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] [IsCancelAdd R] [IsCancelMulZero R], IsCancelMulZero (HahnSeries Γ R)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (h : k ∈ m), (m.get k h == k) = true
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance satisfies the triangle inequality.  -/
Metric.hausdorffDist_triangle' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t u : Set α},
  Metric.hausdorffEDist t u ≠ ⊤ → Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u
-- Init.Data.UInt.Lemmas
UInt32.toNat_mod_uInt64Size : ∀ (n : UInt32), n.toNat % UInt64.size = n.toNat
-- Init.Data.SInt.Lemmas
UInt32.toInt32_ofNatLT : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatLT n hn).toInt32 = Int32.ofNat n
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_neg_right`. -/
Monovary.of_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Monovary f (-g) → Antivary f g
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.zsmul_zero' : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] (a : α), 0 • a = 0
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.toCycles_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.toCycles (CategoryTheory.ShortComplex.cyclesMap φ) =
    CategoryTheory.CategoryStruct.comp φ.τ₁ S₂.toCycles
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.baseChange_toPresentation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ),
  (Algebra.PreSubmersivePresentation.baseChange R P).toPresentation = Algebra.Presentation.baseChange R P.toPresentation
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.ModEq.add_iff_left`. -/
AddCommGroup.ModEq.add_left_cancel : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b c d p : M},
  a ≡ b [PMOD p] → a + c ≡ b + d [PMOD p] → c ≡ d [PMOD p]
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.orthogonal_comm : ∀ {F : Type u_1} [inst : Field F] {m : Type u_2} [inst_1 : Fintype m] {v w : Projectivization F (m → F)},
  v.orthogonal w ↔ w.orthogonal v
-- Mathlib.Probability.Martingale.OptionalStopping
/-- **Doob's maximal inequality**: Given a non-negative submartingale `f`, for all `ε : ℝ≥0`,
we have `ε • μ {ε ≤ f* n} ≤ ∫ ω in {ε ≤ f* n}, f n` where `f* n ω = max_{k ≤ n}, f k ω`.

In some literature, the Doob's maximal inequality refers to what we call Doob's Lp inequality
(which is a corollary of this lemma and will be proved in an upcoming PR).  -/
MeasureTheory.maximal_ineq : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f 𝒢 μ →
    0 ≤ f →
      ∀ {ε : NNReal} (n : ℕ),
        ↑ε * μ {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω} ≤
          ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω}, f n ω ∂μ)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).getKeyD k' fallback =
    if (k == k') = true then if (f (Std.DHashMap.Const.get? m k)).isSome = true then k else fallback
    else m.getKeyD k' fallback
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instBEqEMatchTheoremConstraint.beq : Lean.Meta.Grind.EMatchTheoremConstraint → Lean.Meta.Grind.EMatchTheoremConstraint → Bool
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
injOn_pi_polarCoord_symm : ∀ {ι : Type u_1}, Set.InjOn (fun p i => ↑polarCoord.symm (p i)) (Set.univ.pi fun x => polarCoord.target)
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_div_iff_forall_mul_mem : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {x : A}
  {I J : Submodule R A}, x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getKey? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getKey? k toInsert
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simprocArrayCore : Bool → Lean.Meta.Simp.SimprocsArray → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.pow_card_le_prod : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] [MulLeftMono N] (s : Finset ι) (f : ι → N)
  (n : N), (∀ x ∈ s, n ≤ f x) → n ^ s.card ≤ s.prod f
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- For a point on the sphere, the product of distances to two other intersection
points on a line through the point is zero.  -/
EuclideanGeometry.Sphere.mul_dist_eq_zero_of_mem_sphere : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p a b : P},
  p ∈ line[ℝ, a, b] → a ∈ s → b ∈ s → p ∈ s → dist p a * dist p b = 0
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.copy_eq : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {s : Set M} (hs : s = ↑S), S.copy s hs = S
-- Lean.Level
Lean.Level.instOfNat : (n : ℕ) → OfNat Lean.Level n
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_apply_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2))
  (s : (E.toPreOneHypercover.multicospanIndex F).sections) (i : E.toPreOneHypercover.multicospanShape.L),
  ↑((E.sectionsEquivOfHasPullbacks F) s) i = s.val i
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- If `j` is not the maximum element, `F.obj (Order.succ j)` is obtained
from `F.obj j` by attaching cells in the family of morphisms `basicCell j`.  -/
HomotopicalAlgebra.RelativeCellComplex.attachCells : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        (self : HomotopicalAlgebra.RelativeCellComplex basicCell f) →
                          (j : J) →
                            ¬IsMax j →
                              HomotopicalAlgebra.AttachCells (basicCell j) (self.F.map (CategoryTheory.homOfLE ⋯))
-- Init.Data.Rat.Lemmas
Rat.divInt.eq_1 : ∀ (x : ℤ) (d : ℕ), Rat.divInt x (Int.ofNat d) = inline (mkRat x d)
-- Lean.Meta.SizeOf
/-- Generate proof for `C._sizeOf_<idx> t = sizeOf t` where `C._sizeOf_<idx>` is a auxiliary function
generated for a nested inductive type in `C`.
For example, given
```lean
inductive Expr where
  | app (f : String) (args : List Expr)
```
We generate the auxiliary function `Expr._sizeOf_1 : List Expr → Nat`.
To generate the `sizeOf` spec lemma
```
sizeOf (Expr.app f args) = 1 + sizeOf f + sizeOf args
```
we need an auxiliary lemma for showing `Expr._sizeOf_1 args = sizeOf args`.
Recall that `sizeOf (Expr.app f args)` is definitionally equal to `1 + sizeOf f + Expr._sizeOf_1 args`, but
`Expr._sizeOf_1 args` is **not** definitionally equal to `sizeOf args`. We need a proof by induction.
 -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.mkSizeOfAuxLemma : Lean.Expr → Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Init.Core
instDecidableEqPSigma : {α : Sort u} → {β : α → Sort v} → [h₁ : DecidableEq α] → [h₂ : (a : α) → DecidableEq (β a)] → DecidableEq (PSigma β)
-- ProofWidgets.Component.FilterDetails
/-- Props for the `FilterDetails` component.  -/
ProofWidgets.FilterDetailsProps : Type
-- Lean.Data.Lsp.Client
Lean.Lsp.instFromJsonRegistrationParams : Lean.FromJson Lean.Lsp.RegistrationParams
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- The composition of structomorphisms is a structomorphism.  -/
Structomorph.trans : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      {M'' : Type u_4} →
        [inst : TopologicalSpace H] →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : ChartedSpace H M] →
              [inst_3 : TopologicalSpace M'] →
                [inst_4 : TopologicalSpace M''] →
                  {G : StructureGroupoid H} →
                    [inst_5 : ChartedSpace H M'] →
                      [inst_6 : ChartedSpace H M''] → Structomorph G M M' → Structomorph G M' M'' → Structomorph G M M''
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Extract the matrix components from a morphism of biproducts.  -/
CategoryTheory.Limits.biproduct.components : {J : Type} →
  [inst : Finite J] →
    {K : Type} →
      [inst_1 : Finite K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] →
                {f : J → C} → {g : K → C} → (⨁ f ⟶ ⨁ g) → (j : J) → (k : K) → f j ⟶ g k
-- Mathlib.Data.Nat.Factorial.Basic
/-- factorial notation `(n)!` for `Nat.factorial n`.
In Lean, names can end with exclamation marks (e.g. `List.get!`), so you cannot write
`n!` in Lean, but must write `(n)!` or `n !` instead. The former is preferred, since
Lean can confuse the `!` in `n !` as the (prefix) Boolean negation operation in some
cases.
For numerals the parentheses are not required, so e.g. `0!` or `1!` work fine.  -/
Nat.term_! : Lean.TrailingParserDescr
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.succ_eq_of_lt_aleph0 : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph0 → Order.succ c = c + 1
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.linearIndependent_single_one : ∀ (R : Type u_1) (ι : Type u_3) [inst : Semiring R], LinearIndependent R fun i => fun₀ | i => 1
-- Mathlib.Geometry.Euclidean.Triangle
/-- The greatest angle of a possibly degenerate triangle is more than `π / 3`, unless all angles
are equal.  -/
EuclideanGeometry.pi_div_three_lt_angle_of_le_of_le_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₂ p₃ p₁ ≤ EuclideanGeometry.angle p₁ p₂ p₃ →
    EuclideanGeometry.angle p₃ p₁ p₂ ≤ EuclideanGeometry.angle p₁ p₂ p₃ →
      EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₂ p₃ p₁ ∨
          EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₃ p₁ p₂ ∨
            EuclideanGeometry.angle p₂ p₃ p₁ ≠ EuclideanGeometry.angle p₃ p₁ p₂ →
        Real.pi / 3 < EuclideanGeometry.angle p₁ p₂ p₃
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.faithful : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [Φ.IsLocalizedFullyFaithful] [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G],
  G.Faithful
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C (Type w)}
  {x y : CategoryTheory.Subfunctor F}, x = y ↔ x.obj = y.obj
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.app_one : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  (s : CategoryTheory.Limits.Cotrident f) (j : J),
  CategoryTheory.CategoryStruct.comp (f j) (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) =
    s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelSemigroup α],
  Colex.instLeftCancelSemigroup = { toSemigroup := Colex.instSemigroup, toIsLeftCancelMul := ⋯ }
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.FinValue.val : (self : Lean.Meta.Sym.FinValue) → Fin self.n
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.coe_of : ∀ (R : Type u) [inst : AddCommMonoid R], ↑(AddCommMonCat.of R) = R
-- Mathlib.Data.PEquiv
PEquiv.single_trans_single_of_ne : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : DecidableEq γ]
  {b₁ b₂ : β}, b₁ ≠ b₂ → ∀ (a : α) (c : γ), (PEquiv.single a b₁).trans (PEquiv.single b₂ c) = ⊥
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_le' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a b : α}, |a| ≤ b ↔ a ≤ b ∧ -a ≤ b
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddCommGroupContinuousMap : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddCommGroup β] → [IsTopologicalAddGroup β] → AddCommGroup C(α, β)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.and'.injEq : ∀ (a : Mathlib.Tactic.ITauto.AndKind) (a_1 a_2 : Mathlib.Tactic.ITauto.IProp) (a_3 : Mathlib.Tactic.ITauto.AndKind)
  (a_4 a_5 : Mathlib.Tactic.ITauto.IProp),
  (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2 = Mathlib.Tactic.ITauto.IProp.and' a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_one' : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {𝕜 : Type u_3} [inst : NormedField 𝕜],
  p ≠ 0 → p ≠ ⊤ → ∀ (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm 1 p μ = μ.real Set.univ ^ p.toReal⁻¹
-- Mathlib.Data.PNat.Defs
/-- If `h : k | m`, then `k * (div_exact m k) = m`. Note that this is not equal to `m / k`.  -/
PNat.divExact : ℕ+ → ℕ+ → ℕ+
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjMulCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet.eq_1 : ∀ {M : Type u_1} (s : Set M) [inst : Mul M] [inst_1 : Fintype M] [inst_2 : DecidableEq M]
  [inst_3 : DecidablePred fun x => x ∈ s] (u v : M),
  SimpleGraph.instDecidableRelAdjMulCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet s u v =
    decidable_of_iff (u ≠ v ∧ ∃ g ∈ s, u * g = v ∨ u = v * g) ⋯
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- There is an induced injective homomorphism of a subgraph of `G` into `G`.  -/
SimpleGraph.Subgraph.hom : {V : Type u} → {G : SimpleGraph V} → (x : G.Subgraph) → x.coe →g G
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_eq_getD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)], t.get! a = t.getD a default
-- Mathlib.Analysis.LConvolution
/-- Convolution of the zero function with a function returns the zero function.  -/
MeasureTheory.zero_mlconvolution : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Mul G] [inst_1 : Inv G] (f : G → ENNReal)
  (μ : MeasureTheory.Measure G), MeasureTheory.mlconvolution 0 f μ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.lift_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] {F : CategoryTheory.Limits.MonoFactorisation f}
  (hF : CategoryTheory.Limits.IsImage F),
  CategoryTheory.CategoryStruct.comp (hF.lift (CategoryTheory.Limits.Image.monoFactorisation f))
      (CategoryTheory.Limits.image.ι f) =
    F.m
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_map_snd : ∀ {α : Type u_1} (s : Multiset α), Multiset.map Prod.snd s.antidiagonal = s.powerset
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.isHomogeneous_homogenize : ∀ {R : Type u_1} [inst : CommSemiring R] {n : ℕ} (p : Polynomial R), (p.homogenize n).IsHomogeneous n
-- Mathlib.Topology.MetricSpace.Isometry
/-- Any map on a subsingleton is an isometry  -/
isometry_subsingleton : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} [Subsingleton α],
  Isometry f
-- Mathlib.Order.BooleanAlgebra.Basic
compl_himp : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], (x ⇨ y)ᶜ = x \ y
-- Init.Control.Lawful.MonadLift.Instances
OptionT.lift_bind : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α β : Type u} (ma : m α) (f : α → m β),
  OptionT.lift (ma >>= f) = do
    let a ← OptionT.lift ma
    OptionT.lift (f a)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.instCategoryStruct : {ι : Type v} → CategoryTheory.CategoryStruct.{v, v} (CategoryTheory.Pairwise ι)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet_iff_iCondIndep : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.iCondIndepSet m' hm' s μ ↔
    ProbabilityTheory.iCondIndep m' hm' (fun i => MeasurableSpace.generateFrom {s i}) μ
-- Std.Async.System
Std.Async.System.instDecidableEqCPUInfo : DecidableEq Std.Async.System.CPUInfo
-- Init.Data.Array.MapIdx
Array.mapIdx_spec : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α} {p : (i : ℕ) → β → i < xs.size → Prop},
  (∀ (i : ℕ) (h : i < xs.size), p i (f i xs[i]) h) →
    ∃ (eq : (Array.mapIdx f xs).size = xs.size), ∀ (i : ℕ) (h : i < xs.size), p i (Array.mapIdx f xs)[i] h