mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.LawfulXor.Basic
xor_right_eq : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a : α}, (fun x => x ^^^ a) = fun x => a ^^^ x
-- Lean.Exception
Lean.interruptExceptionId : Lean.InternalExceptionId
-- Mathlib.Data.ENat.Basic
ENat.top_pos : 0 < ⊤
-- Mathlib.Data.Multiset.Dedup
Multiset.coe_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), (↑l).dedup = ↑l.dedup
-- Aesop.Stats.Report
_private.Aesop.Stats.Report.0.Aesop.StatsReport.default.fmtRuleStats : Array (Aesop.DisplayRuleName × Aesop.RuleStatsTotals) → Std.Format
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.coe_sInf' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : InfSet α] {s : Set α},
  s.Nonempty → BddBelow s → ↑(sInf s) = sInf ((fun a => ↑a) '' s)
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_lt : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ}, ↑m < ↑n ↔ m < n
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.one : {α : Type u_1} → [One α] → One (WithZero α)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_sub_of_degree_lt : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q.degree < p.degree → (p - q).leadingCoeff = p.leadingCoeff
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_image2_eq_csSup_csInf : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) →
    (∀ (a : α), GaloisConnection (l₂ a) (u a)) →
      s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sSup s) (sInf t)
-- Mathlib.Analysis.Complex.Norm
Complex.dist_of_re_eq : ∀ {z w : ℂ}, z.re = w.re → dist z w = dist z.im w.im
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Analogue of `Finsupp.sum_ite_eq'` for `SkewMonoidAlgebra`.  -/
SkewMonoidAlgebra.sum_ite_eq' : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddCommMonoid N]
  [inst_2 : DecidableEq G] (f : SkewMonoidAlgebra k G) (a : G) (b : G → k → N),
  (f.sum fun x v => if x = a then b x v else 0) = if a ∈ f.support then b a (f.coeff a) else 0
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.map_comp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y₁ : Type u_5} {Y₂ : Type u_6} {Y₃ : Type u_7} (g : Y₂ → Y₃)
  (f : Y₁ → Y₂), LocallyConstant.map g ∘ LocallyConstant.map f = LocallyConstant.map (g ∘ f)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCommGroup.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α], OrderDual.instCommGroup = { toGroup := OrderDual.instGroup, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves finite colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite
limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteLimits F.op
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.zero_limZero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], CauSeq.LimZero 0
-- Mathlib.Data.Finset.Basic
Multiset.toFinset_add : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), (s + t).toFinset = s.toFinset ∪ t.toFinset
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.Const.toList.eq_1 : ∀ {α : Type u} {β : Type v} (m : Std.DHashMap.Raw α fun x => β),
  Std.DHashMap.Raw.Const.toList m = Std.DHashMap.Raw.Internal.foldRev (fun acc k v => (k, v) :: acc) [] m
-- Init.Data.Array.Bootstrap
Array.foldlM.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → α → m β) (init : β) (as : Array α)
  (start stop : ℕ),
  Array.foldlM f init as start stop =
    if h : stop ≤ as.size then (fun stop h => Array.foldlM.loop f as stop h (stop - start) start init) stop h
    else (fun stop h => Array.foldlM.loop f as stop h (stop - start) start init) as.size ⋯
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.congr_fun : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {F G : f₀.Homotopy f₁}, F = G → ∀ (x : ↑unitInterval × X), F x = G x
-- Mathlib.Data.Num.Bitwise
/-- `SNum.testBit n a` is `true` iff the `n`-th bit (starting from the LSB) of `a` is active.
If the size of `a` is less than `n`, this evaluates to `false`.  -/
SNum.testBit : ℕ → SNum → Bool
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.conj_cpow : ∀ (x n : ℂ), x.arg ≠ Real.pi → (starRingEnd ℂ) x ^ n = (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)
-- Init.Data.Rat.Lemmas
Rat.floor.eq_1 : ∀ (a : ℚ), a.floor = if a.den = 1 then a.num else a.num / ↑a.den
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis'.eRk_eq_eRk_union : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → ∀ (Y : Set α), M.eRk (I ∪ Y) = M.eRk (X ∪ Y)
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.head_add : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] (a b : Fin n.succ → α),
  Matrix.vecHead (a + b) = Matrix.vecHead a + Matrix.vecHead b
-- Mathlib.Order.Filter.NAry
Filter.map₂.neBot : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot],
  (Filter.map₂ m f g).NeBot
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- If `f(p(t) = g(q(t))` for two paths `p` and `q`, then the induced path homotopy classes
`f(p)` and `g(p)` are the same as well, despite having a priori different types  -/
ContinuousMap.Homotopy.heq_path_of_eq_image : ∀ {X₁ X₂ Y : TopCat} {f : C(↑X₁, ↑Y)} {g : C(↑X₂, ↑Y)} {x₀ x₁ : ↑X₁} {x₂ x₃ : ↑X₂} {p : Path x₀ x₁} {q : Path x₂ x₃},
  (∀ (t : ↑unitInterval), f (p t) = g (q t)) →
    (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom f)).map ⟦p⟧ ≍
      (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom g)).map ⟦q⟧
-- Mathlib.Algebra.Free
FreeAddSemigroup.of.eq_1 : ∀ {α : Type u} (x : α), FreeAddSemigroup.of x = { head := x, tail := [] }
-- Init.Data.Int.Gcd
Int.ediv_gcd_ne_zero_if_ne_zero_right : ∀ {b : ℤ} (a : ℤ), b ≠ 0 → b / ↑(a.gcd b) ≠ 0
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.liftExpand_of : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_3}
  [inst_2 : MulAction R X] {C : Sort u_2} {P : X → ↥S → C}
  {hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩} (r : X) (s : ↥S),
  OreLocalization.liftExpand P hP (r /ₒ s) = P r s
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.neBot_cobounded_of_noBotOrder : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α] [NoBotOrder α],
  (Bornology.cobounded α).NeBot
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.congrHom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂)
  (h₂ : g₁ = g₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ g₁] [inst_2 : CategoryTheory.Limits.HasPullback f₂ g₂],
  (CategoryTheory.Limits.pullback.congrHom h₁ h₂).hom =
    CategoryTheory.Limits.pullback.map f₁ g₁ f₂ g₂ (CategoryTheory.CategoryStruct.id X)
      (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
-- Mathlib.RingTheory.Localization.Defs
Localization.add_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (a : R) (b : ↥M) (c : R) (d : ↥M),
  Localization.mk a b + Localization.mk c d = Localization.mk (↑b * c + ↑d * a) (b * d)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_5.eq_1 : ∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] {x y : (CategoryTheory.WithInitial C)ᵒᵖ}
  (motive : (x ⟶ y) → Sort u_3) (f : Opposite.unop y ⟶ Opposite.unop x)
  (h_1 : (f : Opposite.unop y ⟶ Opposite.unop x) → motive (Opposite.op f)),
  (match Opposite.op f with
    | Opposite.op f => h_1 f) =
    h_1 f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The pointwise negation of finset `-s` is defined as `{-x | x ∈ s}` in scope `Pointwise`.  -/
Finset.neg : {α : Type u_2} → [DecidableEq α] → [Neg α] → Neg (Finset α)
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsAffineMap.map_smul_add_smul : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N] {f : M → N} [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {a b : R},
  Convexity.IsAffineMap R f → 0 ≤ a → 0 ≤ b → a + b = 1 → ∀ (x y : M), f (a • x + b • y) = a • f x + b • f y
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.skip.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.insertMany m l) k fallback =
      Std.ExtDHashMap.Const.getD m k fallback
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.orderTop_nsmul_le_orderTop_pow : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] {x : HahnSeries Γ R} {n : ℕ}, n • x.orderTop ≤ (x ^ n).orderTop
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If `f : X → Y` is coinducing and has connected fibers, it induces a homeomorphism on `π₀`.  -/
Topology.IsCoinducing.connectedComponentsHomeomorph : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f : X → Y} →
          Topology.IsCoinducing f →
            (∀ (y : Y), IsConnected (f ⁻¹' {y})) → ConnectedComponents X ≃ₜ ConnectedComponents Y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_eq_get!_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.get! a = (t.get? a).get!
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_map_ite : ∀ {α : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] (p : α → Prop) [inst_1 : DecidablePred p] (f g : α → M)
  (l : List α),
  (List.map (fun a => if p a then f a else g a) l).sum =
    (List.map f (List.filter (fun b => decide (p b)) l)).sum + (List.map g (List.filter (fun a => decide ¬p a) l)).sum
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.incl_mk_nat_card : ∀ (n : ℕ), Fintype.card (FintypeCat.Skeleton.incl.obj (FintypeCat.Skeleton.mk n)).obj = n
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.bijective_costar_iff_bijective_star : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V)
  [inst_2 : Quiver.HasInvolutiveReverse U] [inst_3 : Quiver.HasInvolutiveReverse V] [φ.MapReverse] (u : U),
  Function.Bijective (φ.costar u) ↔ Function.Bijective (φ.star u)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- `rpow` as a `MonoidHom`  -/
NNReal.rpowMonoidHom : ℝ → NNReal →* NNReal
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- The homomorphism `N(H) → Aut(H)` with kernel `C(H)`.  -/
Subgroup.normalizerMonoidHom : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → ↥(Subgroup.normalizer ↑H) →* MulAut ↥H
-- Mathlib.Algebra.Group.Nat.Even
Nat.add_one_lt_of_even : ∀ {m n : ℕ}, Even n → Even m → n < m → n + 1 < m
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {k a : α} {v : β}, (m.insert k v).get! a = if (k == a) = true then v else m.get! a
-- Mathlib.GroupTheory.Congruence.Defs
/-- The integer scaling induced on the quotient by a congruence relation on a type
with a subtraction.  -/
AddCon.instZSMul : {M : Type u_1} → [inst : AddGroup M] → (c : AddCon M) → SMul ℤ c.Quotient
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_isFlat_of_subsingleton : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : Subsingleton A] (s : Set A), (AlgebraicIndependent.matroid R A).IsFlat s
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.nonneg_of_isNNRat : ∀ {A : Type u_1} {e : A} {n d : ℕ} [inst : Semiring A] [inst_1 : LinearOrder A],
  Mathlib.Meta.NormNum.IsNNRat e n d → decide (n = 0) = true → 0 ≤ e
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instCofibrationLeftOfOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y)
  [HomotopicalAlgebra.Cofibration f], HomotopicalAlgebra.Cofibration (CategoryTheory.Over.Hom.left f)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.to_comma_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y : F.Elements}
  (f : X ⟶ Y),
  CategoryTheory.StructuredArrow.Hom.right ((CategoryTheory.CategoryOfElements.toStructuredArrow F).map f) = ↑f
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_singleton : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α] (b a : α),
  {b}.truncatedInf a = if b ≤ a then b else ⊥
-- Mathlib.Algebra.Group.ULift
ULift.addCommSemigroup : {α : Type u} → [AddCommSemigroup α] → AddCommSemigroup (ULift.{u_1, u} α)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_inv`. -/
AntivaryOn.of_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn f⁻¹ g⁻¹ s → AntivaryOn f g s
-- Mathlib.Data.PNat.Xgcd
/-- `ap` is a variable which changes through the algorithm.  -/
PNat.XgcdType.ap : PNat.XgcdType → ℕ
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_natCast_le_lift : ∀ {o : Ordinal.{u}} {n : ℕ}, Ordinal.omega ↑n ≤ Ordinal.lift.{v, u} o ↔ Ordinal.omega ↑n ≤ o
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Composing `f : Lp E p μ` with `L : E →L[𝕜] F`, seen as a `𝕜`-linear map on `Lp E p μ`.  -/
ContinuousLinearMap.compLpₗ : {α : Type u_1} →
  {E : Type u_4} →
    {F : Type u_5} →
      {m : MeasurableSpace α} →
        (p : ENNReal) →
          (μ : MeasureTheory.Measure α) →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedAddCommGroup F] →
                {𝕜 : Type u_6} →
                  {𝕜' : Type u_7} →
                    [inst_2 : NontriviallyNormedField 𝕜] →
                      [inst_3 : NontriviallyNormedField 𝕜'] →
                        [inst_4 : NormedSpace 𝕜 E] →
                          [inst_5 : NormedSpace 𝕜' F] →
                            {σ : 𝕜 →+* 𝕜'} →
                              [RingHomIsometric σ] →
                                (E →SL[σ] F) → ↥(MeasureTheory.Lp E p μ) →ₛₗ[σ] ↥(MeasureTheory.Lp F p μ)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub : ∀ (f : ℕ → ℤ) (p : ℕ) [Fact (Nat.Prime p)],
  (∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i) → IsCauSeq (padicNorm p) fun x => ↑(f x)
-- Batteries.Classes.Order
lexOrd_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β],
  compare = compareLex (compareOn fun x => x.1) (compareOn fun x => x.2)
-- Lean.Parser.Term
/-- A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses.
For example, `(· + ·)` is equivalent to `fun x y => x + y`. Tuple notation and type ascription notation also serve as scopes.
Note that `(· : ty)` expands to `((fun x => x) : ty)`, so `ty` should be a function type.
 -/
Lean.Parser.Term.cdot : Lean.Parser.Parser
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.instIsEquivalenceInverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  (CategoryTheory.ShrinkHoms.inverse C).IsEquivalence
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.relabelNat.eq_1 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (aig : Std.Sat.AIG α), aig.relabelNat = aig.relabelNat'.1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.HasPushout.comp_left_right_iff_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z Z' : C} {f : Z ⟶ X} {g : Z' ⟶ Y} (i : Z' ⟶ Z)
  [inst_1 : CategoryTheory.IsIso i],
  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) g ↔
    CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv i) g)
-- Lean.Elab.Tactic.RCases
/-- Interpret an rcases pattern as an alternation, where non-alternations are treated as one
alternative.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.asAlts : Lean.Elab.Tactic.RCases.RCasesPatt → List Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.RingTheory.QuasiFinite.Basic
PrimeSpectrum.equivSubtype.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R],
  PrimeSpectrum.equivSubtype R =
    { toFun := fun I => ⟨I.asIdeal, ⋯⟩, invFun := fun I => { asIdeal := ↑I, isPrime := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.doubleCoset_union_leftCoset : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) (a : G), ⋃ h, (↑h * a) • ↑K = DoubleCoset.doubleCoset a ↑H ↑K
-- Mathlib.Algebra.Order.Group.PosPart
posPart_nonpos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, a⁺ ≤ 0 ↔ a ≤ 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.startsWith_slice_of_isEmpty : ∀ {pat : String.Slice} {s : String}, pat.isEmpty = true → s.startsWith pat = true
-- Mathlib.Data.Int.GCD
Nat.gcdA.eq_1 : ∀ (x y : ℕ), x.gcdA y = (x.xgcd y).1
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.instSub.eq_1 : ∀ {M : Type u_2} {G : Type u_5} [inst : AddZeroClass M] [inst_1 : AddCommGroup G],
  AddMonoidHom.instSub = { sub := fun f g => AddMonoidHom.mk' (fun x => f x - g x) ⋯ }
-- Lean.Parser.Term
Lean.Parser.Term.forall.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedOverlaps : Inhabited Lean.Meta.Match.Overlaps
-- Init.Data.Vector.FinRange
/-- `finRange n` is the vector of all elements of `Fin n` in order.  -/
Vector.finRange : (n : ℕ) → Vector (Fin n) n
-- Mathlib.Topology.UniformSpace.Closeds
hausdorffEntourage_id : ∀ {α : Type u_1}, hausdorffEntourage SetRel.id = SetRel.id
-- Mathlib.Topology.Sober
QuasiSober.mk : ∀ {α : Type u_3} [inst : TopologicalSpace α],
  (∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S) → QuasiSober α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_coe_center_sq : ∀ (z w : UpperHalfPlane) (r : ℝ),
  dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_eq_top_iff_isCoprime : ∀ {R : Type u_2} [inst : CommSemiring R] (x y : R), Ideal.span {x} ⊔ Ideal.span {y} = ⊤ ↔ IsCoprime x y
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_mem_matrix_iff : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {S : Set α} {M : Matrix m n α} {r : l → m}
  {c : o → n}, Function.Surjective r → Function.Surjective c → (M.submatrix r c ∈ S.matrix ↔ M ∈ S.matrix)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.kernelSequence_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.kernelSequence f).g = f
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.homEquiv_symm_apply : ∀ {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} {X Y : C} {X' Y' : D}
  (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (g : L.obj X ⟶ L.obj Y),
  (CategoryTheory.Localization.Preadditive.homEquiv eX eY).symm g =
    CategoryTheory.CategoryStruct.comp eX.inv (CategoryTheory.CategoryStruct.comp g eY.hom)
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_det : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Fintype n] [inst_3 : DecidableEq n] [inst_4 : CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R},
  Continuous A → Continuous fun x => (A x).det
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V] (g : ↥(Subgroup.center (SpecialLinearGroup R V))) (x : V),
  SpecialLinearGroup.centerEquivRootsOfUnity g • x = (fun x => ↑↑g x) x
-- Init.System.ST
/-- Checks whether two reference cells are in fact aliases for the same cell.

Even if they contain the same value, two references allocated by different executions of `IO.mkRef`
or `ST.mkRef` are distinct. Modifying one has no effect on the other. Likewise, a single reference
cell may be aliased, and modifications to one alias also modify the other.
 -/
ST.Ref.ptrEq : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → ST.Ref σ α → m Bool
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_diff_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.Data.FinEnum
FinEnum.card_ulift : ∀ {α : Type u} [inst : FinEnum (ULift.{u_1, u} α)] [inst_1 : FinEnum α],
  FinEnum.card (ULift.{u_1, u} α) = FinEnum.card α
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquivClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B] [inst_7 : EquivLike F A B]
  [toCoalgEquivClass : CoalgEquivClass F R A B] [toMulEquivClass : MulEquivClass F A B], BialgEquivClass F R A B
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_empty : ∀ {α : Type u} {β : Type v}, ∅.size = 0
-- Mathlib.FieldTheory.AxGrothendieck
FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero : ∀ {ι : Type u_1} {α : Type u_2} [inst : Finite α] [inst_1 : Finite ι] {p : ℕ},
  Nat.Prime p ∨ p = 0 →
    ∀ (φ : FirstOrder.Language.ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)),
      FirstOrder.Language.Theory.ACF p ⊨ᵇ FirstOrder.genericPolyMapSurjOnOfInjOn φ mons
-- Batteries.Data.List.Basic
List.instDecidableIsChainOfDecidableRel.go : {α : Type u_1} →
  {R : α → α → Prop} → [h : DecidableRel R] → (a : α) → (l : List α) → Decidable (List.IsChain R (a :: l))
-- Mathlib.Order.CompleteLattice.Basic
/-- The symmetric case of `iInf_and`,
useful for rewriting into an infimum over a conjunction.  -/
iInf_and' : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p → q → α},
  ⨅ (h₁ : p), ⨅ (h₂ : q), s h₁ h₂ = ⨅ (h : p ∧ q), s ⋯ ⋯