mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Basic
Localization.algEquiv_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  (Localization.algEquiv M S) (Localization.mk x y) = IsLocalization.mk' S x y
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkSizeOfSpecTheorems : Array Lean.Name → Array Lean.Name → Lean.NameMap Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.hasTotal_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [K.HasTotal c₁₂], L.HasTotal c₁₂
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_eq_right_of_det_ne_zero : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [IsDomain R] [inst_3 : Fintype m]
  [inst_4 : DecidableEq m] (A : Matrix m m R) (B : Matrix m n R), A.det ≠ 0 → (A * B).rank = B.rank
-- Mathlib.Order.DirSupClosed
dirSupInaccOn_iff_of_linearOrder : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : LinearOrder α],
  DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
-- Mathlib.CategoryTheory.Shift.Localization
/-- A morphism property `W` on a category `C` is compatible with the shift by a
monoid `A` when for all `a : A`, a morphism `f` belongs to `W`
if and only if `f⟦a⟧'` does.  -/
CategoryTheory.MorphismProperty.IsCompatibleWithShift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.MorphismProperty C → (A : Type w) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → Prop
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d d' : D} (f : d ⟶ d'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d').hom
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Also see `Module.finrank_bot_le_finrank_of_isScalarTower_of_free`
for a version with different typeclass constraints.  -/
Module.finrank_bot_le_finrank_of_isScalarTower : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] (S : Type u_2) (T : Type u_3) [inst_2 : Semiring S]
  [inst_3 : Semiring T] [inst_4 : Module R T] [inst_5 : Module S T] [inst_6 : Module R S] [IsScalarTower R S T]
  [IsScalarTower S T T] [FaithfulSMul S T] [Module.Finite R T], Module.finrank R S ≤ Module.finrank R T
-- Aesop.Options.Public
/-- The maximum number of rule applications in any branch of the search tree
(i.e., the maximum search depth). When a branch exceeds this limit, it is
considered unprovable, but other branches may still be explored. 0 means no
limit.
 -/
Aesop.Options.maxRuleApplicationDepth : Aesop.Options → ℕ
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instSemigroup : Semigroup ℕ
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.measurable : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} {f : α → β}
  {μa : autoParam (MeasureTheory.Measure α) MeasureTheory.Measure.QuasiMeasurePreserving._auto_1}
  {μb : autoParam (MeasureTheory.Measure β) MeasureTheory.Measure.QuasiMeasurePreserving._auto_3},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → Measurable f
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddAction : {α : Type u_1} →
  {β : Type u_2} → {l : Filter α} → {M : Type u_5} → [inst : AddMonoid M] → [AddAction M β] → AddAction M (l.Germ β)
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.toTopHom.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom α β), f.toTopHom = { toFun := f.toFun, map_top' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
  (p.concat h).reverse = SimpleGraph.Walk.cons ⋯ p.reverse
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_ofNat : ∀ (n : ℕ), { toBitVec := BitVec.ofNat 32 n } = OfNat.ofNat n
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toUSize = USize.ofNatLT (UInt8.size - 1) ⋯
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- The relation we induct along in the proof by DeVos of the Cauchy-Davenport theorem.
`(s₁, t₁) < (s₂, t₂)` iff
* `|s₁ * t₁| < |s₂ * t₂|`
* or `|s₁ * t₁| = |s₂ * t₂|` and `|s₂| + |t₂| < |s₁| + |t₁|`
* or `|s₁ * t₁| = |s₂ * t₂|` and `|s₁| + |t₁| = |s₂| + |t₂|` and `|s₁| < |s₂|`.  -/
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.DevosMulRel : {α : Type u_2} → [Group α] → [DecidableEq α] → Finset α × Finset α → Finset α × Finset α → Prop
-- Mathlib.Topology.EMetricSpace.Defs
edist_triangle4 : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y z t : α), edist x t ≤ edist x y + edist y z + edist z t
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.isPlausibleStep_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it : Std.Iter α} {step : Std.IterStep (Std.Iter α) α},
  it.IsPlausibleStep step ↔ step = Std.Rxi.Iterator.step it
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens}, X.zeroLocus ∅ = Set.univ
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.embeddingLiftIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (X : C),
  (CategoryTheory.Mat_.embeddingLiftIso F).hom.app X =
    CategoryTheory.Limits.biproduct.desc fun x => CategoryTheory.CategoryStruct.id (F.obj X)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionList : Lean.ToJson Lean.Lsp.CompletionList
-- Mathlib.Order.SuccPred.CompleteLinearOrder
csInf_mem_of_not_isPredLimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α},
  s.Nonempty → BddBelow s → ¬Order.IsPredLimit (sInf s) → sInf s ∈ s
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β]
  [inst_4 : Min γ] [inst_5 : Top γ] (f : InfTopHom β γ) (g : InfTopHom α β),
  f.comp g = { toInfHom := f.comp g.toInfHom, map_top' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.Limits.pushoutSymmetry f g).hom =
    CategoryTheory.Limits.pushout.inr g f
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ},
  MvPowerSeries.IsWeightedHomogeneous w f p → ∀ {d : σ →₀ ℕ}, (Finsupp.weight w) d ≠ p → (MvPowerSeries.coeff d) f = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_alter_eq_sub_one : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, k ∈ t → (f t[k]?).isNone = true → (t.alter k f).size = t.size - 1
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_zero_swapped : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 0).HasBasis p U → (uniformity α).HasBasis p fun i => {x | x.1 - x.2 ∈ U i}
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C],
  HomotopicalAlgebra.bifibrantObjects C ≤ HomotopicalAlgebra.cofibrantObjects C
-- Mathlib.Computability.Ackermann
ack_strictMono_left : ∀ (n : ℕ), StrictMono fun m => ack m n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddMonoidHom.map_addCyclic : ∀ {G : Type u_2} [inst : AddGroup G] [h : IsAddCyclic G] (σ : G →+ G), ∃ m, ∀ (g : G), σ g = m • g
-- Mathlib.Algebra.Module.ULift
ULift.distribSMul' : {R : Type u} → {M : Type v} → [inst : AddZeroClass M] → [DistribSMul R M] → DistribSMul R (ULift.{u_1, v} M)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.subtype_apply : ∀ {α : Sort u_1} {p : α → Prop} (x : Subtype p), (Function.Embedding.subtype p) x = ↑x
-- Std.Data.ExtTreeSet.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.ExtTreeSet.all : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → (α → Bool) → Bool
-- Mathlib.Algebra.Group.Action.Basic
/-- Embedding of `α` into functions `M → α` induced by an additive action of `M` on `α`.  -/
AddAction.toFun : (M : Type u_2) → (α : Type u_5) → [inst : AddMonoid M] → [AddAction M α] → α ↪ M → α
-- Init.Data.UInt.Bitwise
UInt8.shiftLeft_add : ∀ {a b c : UInt8}, b < 8 → c < 8 → b + c < 8 → a <<< (b + c) = a <<< b <<< c
-- Init.Control.Lawful.Instances
ExceptT.lift.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (t : m α),
  ExceptT.lift t = ExceptT.mk (Except.ok <$> t)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The morphism `F.obj U ⟶ Π F.obj (U i)` whose components
are given by the restriction maps from `U j` to `U i ⊓ U j`.
 -/
TopCat.Presheaf.SheafConditionEqualizerProducts.res : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              F.obj (Opposite.op (iSup U)) ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.inv_hom_id_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D),
  CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app X₂) ((e.hom.app X₁).app X₂) =
    CategoryTheory.CategoryStruct.id ((G.obj X₁).obj X₂)
-- Mathlib.FieldTheory.Normal.Defs
/-- In a scalar tower `K₃/K₂/K₁/F` with `K₁` and `K₂` normal over `F`, the group homomorphism
which restricts algebra isomorphisms of `K₃` to `K₁` is equal to the composition of
the group homomorphism given by restricting an algebra isomorphism of `K₃` to `K₂` and
the group homomorphism given by restricting an algebra isomorphism of `K₂` to `K₁`.  -/
IsScalarTower.AlgEquiv.restrictNormalHom_comp : ∀ (F : Type u_6) (K₁ : Type u_7) (K₂ : Type u_8) (K₃ : Type u_9) [inst : Field F] [inst_1 : Field K₁]
  [inst_2 : Field K₂] [inst_3 : Field K₃] [inst_4 : Algebra F K₁] [inst_5 : Algebra F K₂] [inst_6 : Algebra F K₃]
  [inst_7 : Algebra K₁ K₂] [inst_8 : Algebra K₁ K₃] [inst_9 : Algebra K₂ K₃] [inst_10 : IsScalarTower F K₁ K₃]
  [inst_11 : IsScalarTower F K₁ K₂] [inst_12 : IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [inst_14 : Normal F K₁]
  [inst_15 : Normal F K₂],
  AlgEquiv.restrictNormalHom K₁ = (AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)
-- Mathlib.RingTheory.Derivation.Lie
Derivation.instLieAlgebra : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → LieAlgebra R (Derivation R A A)
-- Mathlib.Data.DFinsupp.Lex
/-- The less-than relation for the colexicographic ordering is decidable.  -/
DFinsupp.Colex.decidableLT : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [inst_1 : LinearOrder ι] → [inst_2 : (i : ι) → LinearOrder (α i)] → DecidableLT (Colex (Π₀ (i : ι), α i))
-- Mathlib.Order.Filter.NAry
Filter.image2_mem_map₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β} {s : Set α} {t : Set β},
  s ∈ f → t ∈ g → Set.image2 m s t ∈ Filter.map₂ m f g
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.mk.sizeOf_spec : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SizeOf G]
  (toOpenAddSubgroup : OpenAddSubgroup G)
  (isNormal' : autoParam (↑toOpenAddSubgroup).Normal OpenNormalAddSubgroup.isNormal'._autoParam),
  sizeOf { toOpenAddSubgroup := toOpenAddSubgroup, isNormal' := isNormal' } =
    1 + sizeOf toOpenAddSubgroup + sizeOf isNormal'
-- Init.System.FilePath
System.instToStringFilePath : ToString System.FilePath
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instZeroQuotient : {S : Type u_2} →
  (M : Type u_3) → [inst : SMul S M] → [Zero M] → [inst_2 : Add M] → (c : ModuleCon S M) → Zero (ModuleCon.Quotient M c)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (ra rb : Lean.Meta.Grind.Arith.CommRing.RingExpr) (a_1 b_1 : Lean.Expr)
  (ra_1 rb_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core a b ra rb =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core a_1 b_1 ra_1 rb_1) =
    (a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1)
-- Mathlib.Order.Filter.Basic
Filter.frequently_bot : ∀ {α : Type u} {p : α → Prop}, ¬∃ᶠ (x : α) in ⊥, p x
-- Mathlib.Algebra.Regular.Basic
IsLeftRegular.mul_left_eq_self_iff : ∀ {R : Type u_1} [inst : Monoid R] {a b : R}, IsLeftRegular a → (a * b = a ↔ b = 1)
-- Init.Tactics
/-- `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
theorems included (relevant for declarations defined by well-founded recursion).
 -/
Lean.Parser.Tactic.tacticRfl' : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derived'_unit : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] {G' : CategoryTheory.Functor D₁ D₂} {F' : CategoryTheory.Functor D₂ D₁}
  (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [inst_6 : G'.IsLeftDerivedFunctor α W₁]
  [inst_7 : F'.IsRightDerivedFunctor β W₂] (η : CategoryTheory.Functor.id D₁ ⟶ G'.comp F')
  (ε : F'.comp G' ⟶ CategoryTheory.Functor.id D₂)
  (hη :
    autoParam
      (∀ (X₁ : C₁),
        CategoryTheory.CategoryStruct.comp (η.app (L₁.obj X₁)) (F'.map (α.app X₁)) =
          CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁)))
      CategoryTheory.Adjunction.derived'._auto_1)
  (hε :
    autoParam
      (∀ (X₂ : C₂),
        CategoryTheory.CategoryStruct.comp (G'.map (β.app X₂)) (ε.app (L₂.obj X₂)) =
          CategoryTheory.CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)))
      CategoryTheory.Adjunction.derived'._auto_3),
  (adj.derived' W₁ W₂ α β η ε hη hε).unit = η
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.instFinalProdProd' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsSiftedOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] {D' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D']
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D') [F.Final] [G.Final], (F.prod' G).Final
-- Init.Data.UInt.Bitwise
UInt64.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : UInt64}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {a : α} {c : ℕ},
  Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c) a = none
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.toCycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), X.toCycles f g fg h n = X.toCycles f g fg h n
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.NormedSpaceInfo.mk.inj : ∀ {normedSpace baseField normedSpace_1 baseField_1 : Lean.Expr},
  { normedSpace := normedSpace, baseField := baseField } = { normedSpace := normedSpace_1, baseField := baseField_1 } →
    normedSpace = normedSpace_1 ∧ baseField = baseField_1
-- Init.Data.BitVec.Lemmas
BitVec.le_trans : ∀ {n : ℕ} {x y z : BitVec n}, x ≤ y → y ≤ z → x ≤ z
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.subsingleton_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], Subsingleton (TopologicalSpace.NonemptyCompacts α) ↔ Subsingleton α
-- Mathlib.CategoryTheory.PathCategory.Basic
_private.Mathlib.CategoryTheory.PathCategory.Basic.0.CategoryTheory.composePath.match_1.eq_2 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} (motive : (x : C) → Quiver.Path X x → Sort u_3)
  (x b : C) (p : Quiver.Path X b) (e : b ⟶ x) (h_1 : Unit → motive X Quiver.Path.nil)
  (h_2 : (x b : C) → (p : Quiver.Path X b) → (e : b ⟶ x) → motive x (p.cons e)),
  (match x, p.cons e with
    | .(X), Quiver.Path.nil => h_1 ()
    | x, p.cons e => h_2 x b p e) =
    h_2 x b p e
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.coe_coe : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M},
  ⇑(LieModule.Weight.toLinear R L M χ) = ⇑χ
-- Mathlib.Tactic.ITauto
/-- `(p: A ∨ B → C) ⊢ B → C`  -/
Mathlib.Tactic.ITauto.Proof.orImpR : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Constructor for morphisms to the point of a limit fan.  -/
CategoryTheory.Limits.Fan.IsLimit.lift : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : β → C} →
        {c : CategoryTheory.Limits.Fan F} → CategoryTheory.Limits.IsLimit c → {A : C} → ((i : β) → A ⟶ F i) → (A ⟶ c.pt)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.fromQuotient_comp_toQuotient : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M), solution.fromQuotient ∘ₗ relations.toQuotient = solution.π
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Init.Data.UInt.Lemmas
mod_usizeSize_uInt8Size : ∀ (n : ℕ), n % USize.size % UInt8.size = n % UInt8.size
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.State.mk : Std.HashMap Lean.Expr ℕ → Lean.Elab.Tactic.Omega.State
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKey? k = none
-- Mathlib.Topology.Algebra.Group.Basic
continuous_zsmul : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (z : ℤ),
  Continuous fun a => z • a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMapZero.toNNReal_neg_smul : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] (r : NNReal) (f : ContinuousMapZero X ℝ),
  (-(r • f)).toNNReal = r • (-f).toNNReal
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A coproduct of coproducts is a coproduct  -/
CategoryTheory.Limits.Cofan.isColimitTrans : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X : α → C} →
        (c : CategoryTheory.Limits.Cofan X) →
          CategoryTheory.Limits.IsColimit c →
            {β : α → Type u_1} →
              {Y : (a : α) → β a → C} →
                (π : (a : α) → (b : β a) → Y a b ⟶ X a) →
                  ((a : α) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (X a) (π a))) →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.Cofan.mk c.pt fun x =>
                        match x with
                        | ⟨a, b⟩ => CategoryTheory.CategoryStruct.comp (π a b) (c.inj a))
-- Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
/-- This is the uniqueness theorem of integral curves applied to a real-indexed family of integral
curves with the same starting point.  -/
eqOn_of_isMIntegralCurveOn_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ {x : M} (γ : ℝ → ℝ → M),
      (∀ (a : ℝ), γ a 0 = x) →
        (∀ a > 0, IsMIntegralCurveOn (γ a) v (Set.Ioo (-a) a)) →
          ∀ {a a' : ℝ}, 0 < a' → a' ≤ a → Set.EqOn (γ a') (γ a) (Set.Ioo (-a') a')
-- Init.Data.Option.Attach
Option.attachWith_eq_none_iff : ∀ {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), o = some a → p a), o.attachWith p H = none ↔ o = none
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The modular group `SL(2, A)` acts transitively on `OnePoint K`, if `A` is a PID whose fraction
field is `K`. (This includes the case `A = ℤ`, `K = ℚ`.)  -/
OnePoint.exists_mem_SL2 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] (A : Type u_2) [inst_2 : CommRing A] [IsDomain A]
  [inst_4 : Algebra A K] [IsFractionRing A K] [IsPrincipalIdealRing A] (c : OnePoint K),
  ∃ g, (Matrix.SpecialLinearGroup.mapGL K) g • OnePoint.infty = c
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Ici : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α}, IsPreconnected (Set.Ici a)