mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Congr
/-- In the case `y = x`, see also `fderivWithin_congr_set_nhdsNE`,
which does not require the domain to be a T₁ space.  -/
fderivWithin_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E} [T1Space E] (y : E),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
-- Mathlib.Order.RelIso.Basic
RelEmbedding.map_rel_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α}, s (f a) (f b) ↔ r a b
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.of_le_add : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ}, (∀ (x y : α), f x ≤ f y + dist x y) → LipschitzWith 1 f
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (c : F), fderiv 𝕜 (fun y => c + f y) x = fderiv 𝕜 f x
-- Mathlib.RingTheory.Teichmuller
_private.Mathlib.RingTheory.Teichmuller.0.Perfection.teichmullerAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sInfHom α β), (sInfHom.id β).comp f = f
-- Mathlib.Topology.Algebra.Group.Basic
nhdsAddHom.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  nhdsAddHom = { toFun := nhds, map_add' := ⋯ }
-- Mathlib.Analysis.Complex.CoveringMap
/-- `(· ^ n) : 𝕜 \ {0} → 𝕜 \ {0}` is a covering map (if `n ≠ 0` in `𝕜`).  -/
isCoveringMap_npow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℕ), ↑n ≠ 0 → IsCoveringMap fun x => ⟨↑x ^ n, ⋯⟩
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.length : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red L₁ L₂ → ∃ n, L₁.length = L₂.length + 2 * n
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_const_left' : ∀ {w a : ℕ} {b : BitVec w} {c : ℕ}, BitVec.ofNat w a + b + BitVec.ofNat w c = BitVec.ofNat w a + BitVec.ofNat w c + b
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.mul : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'}, f₁ =Θ[l] g₁ → f₂ =Θ[l] g₂ → (fun x => f₁ x * f₂ x) =Θ[l] fun x => g₁ x * g₂ x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_hom : ∀ {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 : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  (g : CategoryTheory.CostructuredArrow F f.left),
  ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).left.hom =
    CategoryTheory.CategoryStruct.comp (G.map g.hom) f.hom
-- Init.Data.List.TakeDrop
List.all_takeWhile : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.takeWhile p l).all p = true
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a},
  p.IsHamiltonianCycle → p.tail.IsHamiltonian
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pattern.Model.find?_eq_some_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [inst_4 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_6 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice} {pos : s.Pos},
  s.find? pat = some pos ↔
    String.Slice.Pattern.Model.MatchesAt pat pos ∧ ∀ pos' < pos, ¬String.Slice.Pattern.Model.MatchesAt pat pos'
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.productiveRel_of_left : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α m] [inst_4 : Std.Iterators.Productive α₂ m]
  {it it' : Std.IterM m β},
  it'.internalState.it₁.finitelyManySteps.Rel it.internalState.it₁.finitelyManySteps →
    Std.Iterators.Types.Flatten.ProductiveRel✝ α β m it' it
-- Mathlib.Algebra.Group.Action.Prod
Prod.faithfulSMulLeft : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul M β] [FaithfulSMul M α] [Nonempty β],
  FaithfulSMul M (α × β)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_to_mulHom : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B), ⇑↑f = ⇑f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The result of evaluating an expression into normal form.  -/
Mathlib.Tactic.BicategoryLike.Eval.Result : Type
-- Mathlib.Logic.ExistsUnique
ExistsUnique.unique : ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂
-- Init.Prelude
/-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
equality type. See also `rfl`, which is usually used instead.  -/
Eq.refl : ∀ {α : Sort u_1} (a : α), a = a
-- Mathlib.Analysis.Quaternion
/-- The norm of the components as a Euclidean vector equals the norm of the quaternion.  -/
Quaternion.norm_toLp_equivTuple : ∀ (x : Quaternion ℝ), ‖WithLp.toLp 2 ((Quaternion.equivTuple ℝ) x)‖ = ‖x‖
-- Init.Data.Nat.Div.Basic
Nat.mod_eq_sub_mul_div : ∀ {x k : ℕ}, x % k = x - k * (x / k)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.ofComplex_toComplex : ∀ (c : CliffordAlgebra CliffordAlgebraComplex.Q),
  CliffordAlgebraComplex.ofComplex (CliffordAlgebraComplex.toComplex c) = c
-- Lean.Meta.Basic
Lean.Meta.ExprParamInfo.mk.injEq : ∀ (name : Lean.Name) (type : Lean.Expr) (binderInfo : Lean.BinderInfo) (name_1 : Lean.Name) (type_1 : Lean.Expr)
  (binderInfo_1 : Lean.BinderInfo),
  ({ name := name, type := type, binderInfo := binderInfo } =
      { name := name_1, type := type_1, binderInfo := binderInfo_1 }) =
    (name = name_1 ∧ type = type_1 ∧ binderInfo = binderInfo_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.DTreeMap.Const.unitOfList l cmp).getKey! k' = k
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.of_apply : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : K),
  (PerfectClosure.of K p) x = PerfectClosure.mk K p (0, x)
-- Mathlib.Topology.Algebra.Ring.Basic
/-- In a topological semiring, the left-multiplication `AddMonoidHom` is continuous.  -/
mulLeft_continuous : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R] [IsSemitopologicalRing R] (x : R),
  Continuous ⇑(AddMonoidHom.mulLeft x)
-- Mathlib.Analysis.Normed.Group.Basic
nontrivialTopology_iff_exists_nnnorm_ne_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], NontrivialTopology E ↔ ∃ x, ‖x‖₊ ≠ 0
-- Mathlib.Computability.Encoding
/-- An encoding of a type in a certain alphabet, together with a decoding.  -/
Computability.Encoding : Type u → Type v → Type (max u v)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roo.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  {r : Std.Roo α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Roo.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.eventually_or : ∀ {α : Type u} {f : Ultrafilter α} {p q : α → Prop},
  (∀ᶠ (x : α) in ↑f, p x ∨ q x) ↔ (∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, q x
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Iio ↑a = Set.Iio a
-- Mathlib.GroupTheory.Sylow
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group of size at least `p ^ n`
then there is a subgroup of cardinality `p ^ n`.  -/
Sylow.exists_subgroup_card_pow_prime_of_le_card : ∀ {G : Type u} [inst : Group G] {n p : ℕ}, Nat.Prime p → IsPGroup p G → p ^ n ≤ Nat.card G → ∃ H, Nat.card ↥H = p ^ n
-- Aesop.Rule.Name
Aesop.DisplayRuleName.normUnfold : Aesop.DisplayRuleName
-- Mathlib.GroupTheory.IsSubnormal
_private.Mathlib.GroupTheory.IsSubnormal.0.Subgroup.IsSubnormal.isSubnormal_iff.match_1_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.bot_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X), ⊥ f ↔ False
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_succ_self : ∀ {n : ℕ} (p : Fin n), p.predAbove p.succ = p
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.ofMatroid.injEq : ∀ {α : Type u_2} (toMatroid toMatroid_1 : Matroid α),
  ({ toMatroid := toMatroid } = { toMatroid := toMatroid_1 }) = (toMatroid = toMatroid_1)
-- Mathlib.RingTheory.Ideal.Height
Ideal.finiteHeight_of_finiteRingKrullDim : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [FiniteRingKrullDim R], I.FiniteHeight
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.isCasesAttrCandidate? : Lean.Name → Bool → Lean.CoreM (Option Lean.Name)
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.PatternMatchState.occs.sizeOf_spec : ∀ (subgoals : Array (ℕ × Lean.MVarId)) (idx : ℕ) (remaining : List (ℕ × ℕ)),
  sizeOf (Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx remaining) =
    1 + sizeOf subgoals + sizeOf idx + sizeOf remaining
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.collectParams : List Lean.Meta.Grind.TGrind → Lean.CoreM (Array Lean.Meta.Grind.TParam)
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} {c : ComplexShape ι} {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁)
  (h : i₀ ≠ i₁) (X : C) {K : HomologicalComplex C c}
  (g : HomologicalComplex.double (CategoryTheory.CategoryStruct.id X) hi₀₁ ⟶ K),
  (HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId hi₀₁ h X).homEquiv g =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.doubleXIso₀ (CategoryTheory.CategoryStruct.id X) hi₀₁).inv
      (g.f i₀)
-- Batteries.Data.List.Basic
List.takeWhile₂_eq_takeWhile₂TR : @List.takeWhile₂ = @List.takeWhile₂TR
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- Eta-expanded form of `ContinuousOn.mul` -/
ContinuousOn.fun_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun i => f i * g i) s
-- Mathlib.Topology.Compactness.Compact
IsCompact.ne_univ : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [NoncompactSpace X], IsCompact s → s ≠ Set.univ
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.isElementary' : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (self : L.ElementarySubstructure M),
  (↑self).IsElementary
-- Mathlib.Topology.UniformSpace.Real
NNReal.coeNNRealReal_zero : ContinuousMap.coeNNRealReal 0 = 0
-- Lean.Data.Json.Basic
Lean.Json.Structured.arr.inj : ∀ {elems elems_1 : Array Lean.Json}, Lean.Json.Structured.arr elems = Lean.Json.Structured.arr elems_1 → elems = elems_1
-- Mathlib.Analysis.Calculus.Deriv.Basic
fderiv_apply_one_eq_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, (fderiv 𝕜 f x) 1 = deriv f x
-- Batteries.Data.Fin.Lemmas
/-- **Alias** of `Fin.exists_eq_some_of_findSome?_eq_some`. -/
Fin.exists_of_findSome?_eq_some : ∀ {n : ℕ} {α : Type u_1} {x : α} {f : Fin n → Option α}, Fin.findSome? f = some x → ∃ i, f i = some x
-- Mathlib.Topology.UnitInterval
unitInterval.coe_pos : ∀ {x : ↑unitInterval}, 0 < ↑x ↔ 0 < x
-- Init.Data.List.Basic
/-- Each element of a list is related to all later elements of the list by `R`.

`Pairwise R l` means that all the elements of `l` with earlier indexes are `R`-related to all the
elements with later indexes.

For example, `Pairwise (· ≠ ·) l` asserts that `l` has no duplicates, and `Pairwise (· < ·) l`
asserts that `l` is (strictly) sorted.

Examples:
 * `Pairwise (· < ·) [1, 2, 3] ↔ (1 < 2 ∧ 1 < 3) ∧ 2 < 3`
 * `Pairwise (· = ·) [1, 2, 3] = False`
 * `Pairwise (· ≠ ·) [1, 2, 3] = True`
 -/
List.Pairwise : {α : Type u} → (α → α → Prop) → List α → Prop
-- Mathlib.Data.List.TakeDrop
List.length_dropSlice : ∀ {α : Type u} (i j : ℕ) (xs : List α), (List.dropSlice i j xs).length = xs.length - min j (xs.length - i)
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.zero_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  [inst_4 : (CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] (P Q : CategoryTheory.DifferentialObject S C),
  CategoryTheory.DifferentialObject.Hom.f 0 = 0
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.types_id_apply : ∀ (X : Type u) (x : X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Data.Set.Sups
Set.sups_right_comm : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t u : Set α), s ⊻ t ⊻ u = s ⊻ u ⊻ t
-- Mathlib.RingTheory.SimpleModule.Isotypic
instIsSimpleModuleSubtypeMemSubmoduleValSetOfPredNonemptyLinearEquivId : ∀ (R : Type u_2) (M : Type u) (S : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S] (m : ↑{m | Nonempty (↥m ≃ₗ[R] S)}),
  IsSimpleModule R ↥↑m
-- Mathlib.Algebra.Group.Action.Basic
IsUnit.smul_left_cancel : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : MulAction α β] {a : α},
  IsUnit a → ∀ {x y : β}, a • x = a • y ↔ x = y
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsPosSemidef.isNonneg : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I₁ : R →+* R}
  [inst_3 : LE R] {B : M →ₛₗ[I₁] M →ₗ[R] R}, B.IsPosSemidef → B.IsNonneg
-- Lean.Expr
Lean.Expr.Data.hasLevelParam : Lean.Expr.Data → Bool
-- Mathlib.Algebra.Category.Grp.Basic
AddEquiv.toAddGrpIso.eq_1 : ∀ {X Y : AddGrpCat} (e : ↑X ≃+ ↑Y),
  e.toAddGrpIso =
    { hom := AddGrpCat.ofHom e.toAddMonoidHom, inv := AddGrpCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  P.isoModSerre f
-- Mathlib.Data.Num.Prime
PosNum.Prime.eq_1 : ∀ (n : PosNum), n.Prime = Nat.Prime ↑n
-- Mathlib.LinearAlgebra.Pi
LinearMap.iSup_range_single_le_iInf_ker_proj : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (I J : Set ι),
  Disjoint I J → ⨆ i ∈ I, (LinearMap.single R φ i).range ≤ ⨅ i ∈ J, (LinearMap.proj i).ker
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Mathlib.Data.Seq.Computation
/-- equivalence relation for computations  -/
Computation.«term_~__1» : Lean.TrailingParserDescr
-- Mathlib.Tactic.IrreducibleDef
/-- `val_proj x` elabs to the *primitive projection* `@x.val`.  -/
_private.Mathlib.Tactic.IrreducibleDef.0.Lean.Elab.Command.termVal_proj_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpIdIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Functor.mapAddGrpIdIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.AddGrp.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapAddGrp.obj X).X) ⋯ ⋯)
      ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncGTIsoTruncGE.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b),
  t.truncGTIsoTruncGE a b h = t.truncGTIsoTruncGE a b h
-- Aesop.Rule.Name
Aesop.PhaseName.instToString : ToString Aesop.PhaseName
-- Mathlib.RingTheory.Ideal.Height
/-- In a trivial commutative ring, the height of any ideal is `∞`.  -/
Ideal.height_of_subsingleton : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [Subsingleton R], I.height = ⊤
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.ssubset_of_not_superset`.

---

Set notation form of `LE.le.lt_of_not_ge` -/
HasSubset.Subset.ssubset_of_not_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊆ a → a ⊂ b
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.toOplaxMonoidal_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D),
  Function.Injective (@CategoryTheory.Functor.Monoidal.toOplaxMonoidal C inst inst_1 D inst_2 inst_3 F)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.strictMap_le_map : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D), P.strictMap F ≤ P.map F
-- Init.Data.UInt.Lemmas
UInt8.pow_zero : ∀ (x : UInt8), x ^ 0 = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∈ t ↔ (t.getKey? a).isSome = true
-- Mathlib.Data.Vector.Defs
List.Vector.instDecidableEq : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → DecidableEq (List.Vector α n)
-- Init.Data.Option.Lemmas
Option.bind_map_comm : ∀ {α : Type u_1} {β : Type u_2} {x : Option (Option α)} {f : α → β},
  x.bind (Option.map f) = (Option.map (Option.map f) x).bind id
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.Cover.pullbackHom.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : W ⟶ X)
  (i : 𝒰.toPreZeroHypercover.1) [inst_2 : ∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)],
  𝒰.pullbackHom f i = CategoryTheory.Limits.pullback.snd f (𝒰.f i)
-- Mathlib.Data.Int.Log
Int.clog_of_right_le_zero : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) {r : R}, r ≤ 0 → Int.clog b r = 0
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_mul_of_nonneg_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosMono α],
  b ≤ c → 0 ≤ a → b * a ≤ c * a
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_mk_shrink : ∀ (α : Type u) [inst : Small.{v, u} α],
  Cardinal.lift.{max u w, v} (Cardinal.mk (Shrink.{v, u} α)) = Cardinal.lift.{max v w, u} (Cardinal.mk α)
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instNormForall : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {ι : Type u_2} →
        {E : ι → Type u_3} →
          [Fintype ι] →
            [inst_3 : (i : ι) → NormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → Module ℂ (E i)] →
                [inst_5 : (i : ι) → SMul A (E i)] →
                  [(i : ι) → CStarModule A (E i)] → Norm (WithCStarModule A ((i : ι) → E i))
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves finite coproducts, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite
products.  -/
CategoryTheory.Limits.preservesFiniteProducts_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.PreservesFiniteCoproducts F],
  CategoryTheory.Limits.PreservesFiniteProducts F.op
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α}, MeasureTheory.IsFundamentalDomain G s μ → ⋃ g, g • s =ᵐ[μ] Set.univ
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableAt_fun_neg_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, DifferentiableAt 𝕜 (fun y => -f y) x ↔ DifferentiableAt 𝕜 f x
-- Init.Data.Vector.Attach
/-- This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Vector.foldr_subtype : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → β → β}
  {g : α → β → β} {x : β},
  (∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) → Vector.foldr f x xs = Vector.foldr g x xs.unattach
-- Std.Time.Format.Modifier
Std.Time.OffsetZ.hourMinuteSecondColon.sizeOf_spec : sizeOf Std.Time.OffsetZ.hourMinuteSecondColon = 1
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_eq_top_iff_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : Associates α},
  a.factors = ⊤ ↔ a = 0