mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R},
  CliffordAlgebraQuaternion.toQuaternion.comp CliffordAlgebraQuaternion.ofQuaternion =
    AlgHom.id R (QuaternionAlgebra R c₁ 0 c₂)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The map `desc` makes the diagram with the natural transformations commute  -/
CategoryTheory.Limits.IsColimit.fac_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone F) (j : J) {Z : C} (h : s.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.ι.app j) (CategoryTheory.CategoryStruct.comp (self.desc s) h) =
    CategoryTheory.CategoryStruct.comp (s.ι.app j) h
-- Mathlib.Topology.Category.LightProfinite.Basic
FintypeCat.toLightProfinite_map_hom_hom_apply : ∀ {X Y : FintypeCat} (f : X ⟶ Y) (a : X.obj),
  (TopCat.Hom.hom (FintypeCat.toLightProfinite.map f).hom) a = (CategoryTheory.ConcreteCategory.hom f) a
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.mk : Lean.Meta.SimpTheoremTree →
  Lean.Meta.SimpTheoremTree →
    Lean.PHashSet Lean.Meta.Origin →
      Lean.PHashSet Lean.Name →
        Lean.PHashSet Lean.Meta.Origin → Lean.PHashMap Lean.Name (Array Lean.Name) → Lean.Meta.SimpTheorems
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.sin x = Real.cos a - Real.cos b
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.cosh_log : ∀ {x : ℝ}, 0 < x → Real.cosh (Real.log x) = (x + x⁻¹) / 2
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) h)
-- Mathlib.Topology.Closure
interior_closure_idem : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior (closure (interior (closure s))) = interior (closure s)
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofBitVec : ∀ (n : BitVec 8), { toBitVec := n }.toBitVec = n
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_toContinuousMap : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β), ⇑f.toContinuousMap = ⇑f
-- Init.Data.Nat.Lemmas
Nat.one_add_le_iff : ∀ {m n : ℕ}, 1 + m ≤ n ↔ m < n
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isIso_fromTildeΓ_of_presentation : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec R).Modules) (P : SheafOfModules.Presentation M),
  CategoryTheory.IsIso M.fromTildeΓ
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.embeddingPiTangent_ker_mfderiv : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι] {s : Set M}
  (f : SmoothBumpCovering ι I M s), ∀ x ∈ s, (↑(mfderiv% ⇑(SmoothBumpCovering.embeddingPiTangent✝ f) x)).ker = ⊥
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.SheafOfTypes.balanced : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [CategoryTheory.HasSheafify J (Type w)], CategoryTheory.Balanced (CategoryTheory.Sheaf J (Type w))
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.mkContinuousLinear_norm_le' : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
  (H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖),
  ‖MultilinearMap.mkContinuousLinear f C H‖ ≤ max C 0
-- Mathlib.Order.Lattice
OrderDual.instSemilatticeSup : (α : Type u_1) → [h : SemilatticeInf α] → SemilatticeSup αᵒᵈ
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.isPlot_id : ∀ {n : ℕ}, Diffeology.IsPlot id
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.mul_right_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ {q : Polynomial R}, q ≠ 0 → p * q ≠ 0
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.List.splitWrtCompositionAux.match_3.eq_1 : ∀ {α : Type u_1} (motive : List α → List ℕ → Sort u_2) (x : List α) (h_1 : (x : List α) → motive x [])
  (h_2 : (l : List α) → (n : ℕ) → (ns : List ℕ) → motive l (n :: ns)),
  (match x, [] with
    | x, [] => h_1 x
    | l, n :: ns => h_2 l n ns) =
    h_1 x
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.instOrdResult : {α : Type} → [Ord α] → Ord (Mathlib.Tactic.ClickSuggestions.Result α)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.coord_toDualEquiv_symm_apply : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (i : ι) (f : Module.Dual R M),
  (b.coord i) (b.toDualEquiv.symm f) = (b.dualBasis.coord i) f
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The empty set is a block.  -/
MulAction.IsBlock.empty : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X], MulAction.IsBlock G ∅
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- A `TensorAlgebra` over a nontrivial semiring is nontrivial.  -/
TensorAlgebra.instNontrivial : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  Nontrivial (TensorAlgebra R M)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The results of applying `domDomCongr` to two maps are equal if
and only if those maps are.  -/
MultilinearMap.domDomCongr_eq_iff : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2}
  (σ : ι₁ ≃ ι₂) (f g : MultilinearMap R (fun x => M₂) M₃),
  MultilinearMap.domDomCongr σ f = MultilinearMap.domDomCongr σ g ↔ f = g
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₁ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₁
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.mono : ∀ {V : Type u} {G : SimpleGraph V} {n m : ℕ}, n ≤ m → G.Colorable n → G.Colorable m
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map.mk : ∀ {α : Type u} {L : List (α × Bool)} {β : Type v} {f : α → β},
  (FreeAddGroup.map f) (FreeAddGroup.mk L) = FreeAddGroup.mk (List.map (fun x => (f x.1, x.2)) L)
-- Mathlib.Topology.Algebra.Monoid
Topology.IsInducing.separatelyContinuousAdd : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [AddHomClass F M N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N] [SeparatelyContinuousAdd N] (f : F),
  Topology.IsInducing ⇑f → SeparatelyContinuousAdd M
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCocircuit.isCircuit : ∀ {α : Type u_1} {M : Matroid α} {K : Set α}, M.IsCocircuit K → M✶.IsCircuit K
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedConsumerNode : Inhabited Lean.Meta.SynthInstance.ConsumerNode
-- Mathlib.Tactic.NormNum.Result
NNRat.rawCast.eq_1 : ∀ {α : Type u} [inst : DivisionSemiring α] (n d : ℕ), NNRat.rawCast n d = ↑n / ↑d
-- Batteries.Data.Random.MersenneTwister
/-- Mersenne Twister initialization given an optional seed.  -/
Batteries.Random.MersenneTwister.Config.init : (cfg : Batteries.Random.MersenneTwister.Config) →
  optParam (BitVec cfg.wordSize) cfg.initSeed → Batteries.Random.MersenneTwister.State cfg
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_eq' : ∀ {m n : ℕ}, m.shiftRight n = m >>> n
-- Std.Time.Time.HourMarker
/-- Ante meridiem.
 -/
Std.Time.HourMarker.am : Std.Time.HourMarker
-- Mathlib.Algebra.Group.Conj
AddConjClasses.map.eq_1 : ∀ {α : Type u} {β : Type v} [inst : AddMonoid α] [inst_1 : AddMonoid β] (f : α →+ β),
  AddConjClasses.map f = Quotient.lift (AddConjClasses.mk ∘ ⇑f) ⋯
-- Mathlib.Order.Hom.Bounded
BotHom.dual_symm_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : OrderBot α] [inst_2 : LE β] [inst_3 : OrderBot β]
  (f : TopHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ), (BotHom.dual.symm f) a = f a
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_copy_iff : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String}, p.copy.Splits t₁ t₂ ↔ p.Splits t₁ t₂
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_self : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (a : ↥S), AddLocalization.mk (↑a) a = 0
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.δ₀Functor_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1))
  {X Y : Fin (n + 1)} (f : X ⟶ Y),
  (CategoryTheory.ComposableArrows.δ₀Functor.obj F).map f = F.map (CategoryTheory.homOfLE ⋯)
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swap_map : ∀ {X Y : TwoP} (f : X ⟶ Y),
  TwoP.swap.map f =
    CategoryTheory.InducedCategory.homMk
      { toFun := ⇑(CategoryTheory.ConcreteCategory.hom f.hom), map_fst := ⋯, map_snd := ⋯ }
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termι'' : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_nonempty_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  (s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Order.Monotone.Defs
AntitoneOn.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, AntitoneOn g t → AntitoneOn f s → Set.MapsTo f s t → MonotoneOn (g ∘ f) s
-- Lean.Data.DeclarationRange
Lean.instToExprDeclarationRange : Lean.ToExpr Lean.DeclarationRange
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instIsScalarTower : ∀ {α : Type u_1} {R : Type u_6} {R' : Type u_7} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  [inst_2 : SMul R' ENNReal] [inst_3 : IsScalarTower R' ENNReal ENNReal] [inst_4 : SMul R R']
  [IsScalarTower R R' ENNReal] {x : MeasurableSpace α}, IsScalarTower R R' (MeasureTheory.Measure α)
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.clear.injEq : ∀ (ref ref_1 : Lean.Syntax),
  (Lean.Elab.Tactic.RCases.RCasesPatt.clear ref = Lean.Elab.Tactic.RCases.RCasesPatt.clear ref_1) = (ref = ref_1)
-- Mathlib.Algebra.Opposites
AddOpposite.op_surjective : ∀ {α : Type u_1}, Function.Surjective AddOpposite.op
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.card_interedges_add_card_interedges_compl : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s t : Finset α} [inst_1 : DecidableEq α],
  Disjoint s t → (G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.exponent_def : ∀ (K : Type u_2) {L : Type u_3} [inst : CommRing K] [inst_1 : Ring L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (a : L),
  a ^ ringExpChar K ^ IsPurelyInseparable.exponent K L ∈ (algebraMap K L).range
-- Mathlib.Topology.MetricSpace.Holder
/-- For fixed `f : X → Y` and `C : ℝ≥0`, the set of all parameters `r : ℝ≥0` such that
`f` is `(C, r)`-Hölder is convex.  -/
convex_setOfPred_holderWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (f : X → Y) (C : NNReal),
  Convex NNReal {r | HolderWith C r f}
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.inf : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMaxOn f s a → IsLocalMaxOn g s a → IsLocalMaxOn (fun x => f x ⊓ g x) s a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  Std.DHashMap.Raw.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.DHashMap.Raw.Const.get m a ⋯
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.continuousLinearMapClassOfFiniteDimensional : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [inst_5 : AddCommGroup F']
  [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [IsTopologicalAddGroup F'] [ContinuousSMul 𝕜 F']
  [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E], ContinuousLinearMapClass (E →ₗ[𝕜] F') 𝕜 E F'
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.addLeft.eq_1 : ∀ {α : Type u_2} [inst : Add α] [inst_1 : LinearOrder α] [inst_2 : AddLeftStrictMono α] (m : α),
  OrderEmbedding.addLeft m = OrderEmbedding.ofStrictMono (fun n => m + n) ⋯
-- Mathlib.Data.Set.Function
Set.LeftInvOn.left_prodMk : ∀ {α : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s : Set α} {f₁ : α → β₁} {f₂ : α → β₂} {g₁ : β₁ → α},
  Set.LeftInvOn g₁ f₁ s → Set.LeftInvOn (fun x => g₁ x.1) (fun x => (f₁ x, f₂ x)) s
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.leftUnitor_inv_toNatTrans : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C),
  (CategoryTheory.Bicategory.leftUnitor F).inv.toNatTrans = F.toFunctor.leftUnitor.inv
-- Lean.Elab.Tactic.Split
_private.Lean.Elab.Tactic.Split.0.Lean.Elab.Tactic.evalSplit.throwTermUnsupported : Lean.Term → Option Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.appr_spec : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]), x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.string.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.string = 1
-- Mathlib.Data.PNat.Basic
PNat.one_lt_of_lt : ∀ {a b : ℕ+}, a < b → 1 < b
-- Mathlib.Order.Lattice.Congruence
LatticeCon.sup : ∀ {α : Type u_2} [inst : Lattice α] (self : LatticeCon α) {w x y z : α},
  self.toSetoid w x → self.toSetoid y z → self.toSetoid (w ⊔ y) (x ⊔ z)
-- Mathlib.Analysis.Analytic.IsolatedZeros
AnalyticOnNhd.eqOn_zero_or_eventually_ne_zero_of_preconnected : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  AnalyticOnNhd 𝕜 f U → IsPreconnected U → Set.EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ 0
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.instBEqComparisonResult.beq : Mathlib.Linter.TextBased.ComparisonResult✝ → Mathlib.Linter.TextBased.ComparisonResult✝ → Bool
-- Mathlib.Order.UpperLower.Closure
/-- **Alias** of the forward direction of `bddBelow_upperClosure`. -/
BddBelow.of_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow ↑(upperClosure s) → BddBelow s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.dropUntil_first : ∀ {V : Type u} {G : SimpleGraph V} {v u : V} [inst : DecidableEq V] (p : G.Walk u v) (h : u ∈ p.support),
  p.dropUntil u h = p
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k fallback : α},
      (List.map Prod.fst l).contains k = false → (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_omega_iff_analyticOnNhd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 ⊤ f ↔ AnalyticOnNhd 𝕜 f Set.univ
-- Mathlib.Algebra.Order.Hom.Basic
RingNormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : NonUnitalNonAssocRing α]
  [inst_1 : Semiring β] [inst_2 : PartialOrder β] [inst_3 : FunLike F α β]
  [toRingSeminormClass : RingSeminormClass F α β], (∀ (f : F) {a : α}, f a = 0 → a = 0) → RingNormClass F α β
-- Mathlib.Topology.Order.Compact
cocompact_eq_atTop : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [NoMaxOrder α] [OrderBot α] [ClosedIciTopology α]
  [CompactIccSpace α], Filter.cocompact α = Filter.atTop
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.match_1.splitter : {α : Type u_1} →
  (n : ℕ) →
    (motive : { l // l.length = (n + 2 + 1) / 2 } × { l // l.length = (n + 2) / 2 } → Sort u_2) →
      (x : { l // l.length = (n + 2 + 1) / 2 } × { l // l.length = (n + 2) / 2 }) →
        ((l : { l // l.length = (n + 2 + 1) / 2 }) → (r : { l // l.length = (n + 2) / 2 }) → motive (l, r)) → motive x
-- Mathlib.Data.Rat.Defs
Rat.den_zero : Rat.den 0 = 1
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_6 : ∀ {a0 a1 a2 a3 a4 a5 a6 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 6).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) =
    a6
-- Init.Data.Nat.Basic
Nat.add_sub_of_le : ∀ {a b : ℕ}, a ≤ b → a + (b - a) = b
-- Mathlib.RingTheory.Ideal.Maps
/-- The kernel of a homomorphism to a domain is a prime ideal.  -/
RingHom.ker_isPrime : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [IsDomain S]
  [inst_3 : FunLike F R S] [inst_4 : RingHomClass F R S] (f : F), (RingHom.ker f).IsPrime
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop} [inst_1 : SizeOf α]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] [inst_4 : (a : β) → SizeOf (P a)] (inner : Std.IterM m β)
  (invariant : ∀ (out : β), inner.IsPlausibleIndirectOutput out → P out),
  sizeOf { inner := inner, invariant := invariant } = 1 + sizeOf inner
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.orbitRel_le_fst : ∀ (G : Type u_1) (α : Type u_2) (β : Type u_3) [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : AddAction G β],
  AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (AddAction.orbitRel G α)
-- Lean.Meta.Basic
/-- Pending instances that were not synthesized because `maxSynthPendingDepth` has been reached.  -/
Lean.Meta.Diagnostics.synthPendingFailures : Lean.Meta.Diagnostics → Lean.PHashMap Lean.Expr Lean.MessageData
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.powerRevlex_k.eq_1 : ∀ (k₁ k₂ : ℕ),
  Lean.Grind.CommRing.powerRevlex_k k₁ k₂ =
    Bool.rec (Bool.rec Ordering.eq Ordering.lt (k₂.blt k₁)) Ordering.gt (k₁.blt k₂)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (I J : CategoryTheory.InjectiveResolution X), CategoryTheory.CategoryStruct.comp J.ι (I.homotopyEquiv J).inv = I.ι
-- Mathlib.CategoryTheory.Localization.Triangulated
/-- The pretriangulated structure on the localized category.  -/
CategoryTheory.Triangulated.Localization.pretriangulated : {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) →
          [inst_2 : CategoryTheory.HasShift C ℤ] →
            [inst_3 : CategoryTheory.Preadditive C] →
              [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
                [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                  [inst_6 : CategoryTheory.Pretriangulated C] →
                    [inst_7 : CategoryTheory.HasShift D ℤ] →
                      [L.CommShift ℤ] →
                        (W : CategoryTheory.MorphismProperty C) →
                          [L.IsLocalization W] →
                            [W.HasLeftCalculusOfFractions] →
                              [W.IsCompatibleWithTriangulation] →
                                [inst_12 : CategoryTheory.Limits.HasZeroObject D] →
                                  [inst_13 : CategoryTheory.Preadditive D] →
                                    [inst_14 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                                      [L.Additive] → CategoryTheory.Pretriangulated D
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_iff : ∀ {m n k : ℕ}, m.lcm n ∣ k ↔ m ∣ k ∧ n ∣ k
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_updateCol : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : DecidableEq n] (i : n) {A : X → Matrix m n R} {B : X → m → R},
  Continuous A → Continuous B → Continuous fun x => (A x).updateCol i (B x)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.instNonempty : ∀ {α : Type u_1} [Nonempty α], Nonempty (Topology.WithUpperSet α)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Proj.eq_1 : ∀ {I : Type u} (J : I → Prop) [inst : (i : I) → Decidable (J i)] (c : I → Bool) (i : I),
  Profinite.NobelingProof.Proj J c i = if J i then c i else false
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommSemiring.mk.injEq : ∀ (toSemiring : Lean.Meta.Sym.Arith.Semiring) (ringId : ℕ) (commSemiringInst : Lean.Expr)
  (addRightCancelInst? : Option (Option Lean.Expr)) (toQFn? : Option Lean.Expr)
  (toSemiring_1 : Lean.Meta.Sym.Arith.Semiring) (ringId_1 : ℕ) (commSemiringInst_1 : Lean.Expr)
  (addRightCancelInst?_1 : Option (Option Lean.Expr)) (toQFn?_1 : Option Lean.Expr),
  ({ toSemiring := toSemiring, ringId := ringId, commSemiringInst := commSemiringInst,
        addRightCancelInst? := addRightCancelInst?, toQFn? := toQFn? } =
      { toSemiring := toSemiring_1, ringId := ringId_1, commSemiringInst := commSemiringInst_1,
        addRightCancelInst? := addRightCancelInst?_1, toQFn? := toQFn?_1 }) =
    (toSemiring = toSemiring_1 ∧
      ringId = ringId_1 ∧
        commSemiringInst = commSemiringInst_1 ∧ addRightCancelInst? = addRightCancelInst?_1 ∧ toQFn? = toQFn?_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.congr_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β},
  m₁.Equiv m₂ → (m₃.Equiv m₁ ↔ m₃.Equiv m₂)
-- Mathlib.GroupTheory.Nilpotent
AddGroup.nilpotencyClass.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G], AddGroup.nilpotencyClass G = if hG : AddGroup.IsNilpotent G then Nat.find ⋯ else 0