mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    match h : compare k ky with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryGED k l (ky, y)
    | Ordering.eq => (ky, y)
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryGE k r ⋯ ⋯
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.ext_iff : ∀ {R : Type u_1} [inst : Semiring R] {p q : SkewPolynomial R}, p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Make a triplet from `x : X` and `y : Y` such that `f x = g y`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.mk' : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} → {g : Y ⟶ S} → (x : ↥X) → (y : ↥Y) → f x = g y → AlgebraicGeometry.Scheme.Pullback.Triplet f g
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderiv_fst : ∀ {𝕜 : 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] {p : E × F},
  fderiv 𝕜 Prod.fst p = ContinuousLinearMap.fst 𝕜 E F
-- Init.Data.Array.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.
 -/
Array.foldr_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → β → β} {g : α → β → β}
  {x : β}, (∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) → Array.foldr f x xs = Array.foldr g x xs.unattach
-- Mathlib.Data.Set.Finite.Monad
/-- If `s : Set α` is a set with `Fintype` instance and `f : α → Set β` is a function such that
each `f a`, `a ∈ s`, has a `Fintype` structure, then `s >>= f` has a `Fintype` structure.  -/
Set.fintypeBind : {α β : Type u_1} →
  [DecidableEq β] →
    (s : Set α) → [Fintype ↑s] → (f : α → Set β) → ((a : α) → a ∈ s → Fintype ↑(f a)) → Fintype ↑(s >>= f)
-- Batteries.Data.ByteArray
ByteArray.ofFn_succ : ∀ {n : ℕ} (f : Fin (n + 1) → UInt8), ByteArray.ofFn f = (ByteArray.ofFn fun i => f i.castSucc).push (f (Fin.last n))
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.instIsDiscrete : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] [CategoryTheory.IsDiscrete T],
  CategoryTheory.IsDiscrete (CategoryTheory.ShrinkHoms.{u} T)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertMany_eq_insertListₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (l : List ((a : α) × β a)), ↑(m.insertMany l) = m.insertListₘ l
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_le_one_of_ediam_le : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.ediam A ≤ ↑ε → Metric.coveringNumber ε A ≤ 1
-- Mathlib.Data.List.Sections
List.rel_sections : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop},
  Relator.LiftFun (List.Forall₂ (List.Forall₂ r)) (List.Forall₂ (List.Forall₂ r)) List.sections List.sections
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_add : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M}
  {h₁ h₂ : α → M → N}, (f.sum fun a b => h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalAlgebra.of_f : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] [inst_6 : (i : ι) → DistribMulAction R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {i j : ι}
  (hij : i ≤ j) (x : G i),
  (DirectLimit.NonUnitalAlgebra.of G f j) ((f i j hij) x) = (DirectLimit.NonUnitalAlgebra.of G f i) x
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `AddSubmonoid.FG` in terms of `Set.Finite` instead of
`Finset`.  -/
AddSubmonoid.fg_iff : ∀ {M : Type u_1} [inst : AddMonoid M] (P : AddSubmonoid M), P.FG ↔ ∃ S, AddSubmonoid.closure S = P ∧ S.Finite
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderiv_cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → fderiv ℝ (fun x => Real.cosh (f x)) x = Real.sinh (f x) • fderiv ℝ f x
-- Mathlib.GroupTheory.Index
/-- Typeclass for a subgroup `H` to have finite index in a subgroup `K`.  -/
AddSubgroup.IsFiniteRelIndex : {G : Type u_3} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup G → Prop
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_range_add : ∀ {M : Type u_4} [inst : CommMonoid M] (f : ℕ → M) (n m : ℕ),
  ∏ x ∈ Finset.range (n + m), f x = (∏ x ∈ Finset.range n, f x) * ∏ x ∈ Finset.range m, f (n + x)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The stalk of `Spec R` at `x` is isomorphic to `Rₚ`,
where `p` is the prime corresponding to `x`.  -/
AlgebraicGeometry.StructureSheaf.stalkIso : (R : Type u) →
  [inst : CommRing R] →
    (x : PrimeSpectrum R) →
      Localization.AtPrime x.asIdeal ≃ₐ[R] ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_normalize : ∀ {R : Type u} [inst : Field R] {p : Polynomial R} [inst_1 : DecidableEq R], (normalize p).degree = p.degree
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.dist_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X} {x y : X}, HolderOnWith C r f s → x ∈ s → y ∈ s → dist (f x) (f y) ≤ ↑C * dist x y ^ ↑r
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.ret_supports : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {k : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.contSupp k ⊆ S → Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k))
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.WellFormed : {α : Type u_1} → (cmp : α → α → Ordering) → {β : Type u_2} → Lean.PrefixTreeNode α β cmp → Prop
-- Lean.Structure
Lean.StructureResolutionOrderResult.mk.sizeOf_spec : ∀ (resolutionOrder : Array Lean.Name) (conflicts : Array Lean.StructureResolutionOrderConflict),
  sizeOf { resolutionOrder := resolutionOrder, conflicts := conflicts } = 1 + sizeOf resolutionOrder + sizeOf conflicts
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.inftyNormedAlgebra : {𝕜 : Type u_1} →
  {I : Type u_5} →
    {B : I → Type u_6} →
      [inst : NormedField 𝕜] →
        [inst_1 : (i : I) → NormedRing (B i)] →
          [(i : I) → NormedAlgebra 𝕜 (B i)] → [inst_3 : ∀ (i : I), NormOneClass (B i)] → NormedAlgebra 𝕜 ↥(lp B ⊤)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) [inst_6 : CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) {Z : C}
  (h : (t.truncLT b).obj ((t.truncGE a).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))
      (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) h) =
    CategoryTheory.CategoryStruct.comp ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))) h
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
an index set which is a countable set in any type.  -/
dense_biInter_of_Gδ : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [BaireSpace X] {S : Set α} {f : (x : α) → x ∈ S → Set X},
  (∀ (s : α) (H : s ∈ S), IsGδ (f s H)) →
    S.Countable → (∀ (s : α) (H : s ∈ S), Dense (f s H)) → Dense (⋂ s, ⋂ (h : s ∈ S), f s h)
-- Init.Data.Queue
Std.Queue.toArray : {α : Type u} → Std.Queue α → Array α
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.instPreadditive : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.Preadditive (CategoryTheory.ShortComplex C)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.mem_sum : ∀ {ι : Type u_1} {M : Type u_4} {a : M} {s : Finset ι} {m : ι → Multiset M}, a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i
-- Mathlib.Algebra.Order.Positive.Ring
Positive.instMulSubtypeLtOfNat_mathlib : {R : Type u_2} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Mul { x // 0 < x }
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by projection onto the first factor.  -/
ContinuousAddMonoidHom.fst : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A × B →ₜ+ A
-- Mathlib.Topology.DerivedSet
perfect_iff_eq_derivedSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X}, Perfect U ↔ U = derivedSet U
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Either `C.X j`, if there is some `j` with `c.rel i j`, or `C.X i`.  -/
HomologicalComplex.xNext : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → {c : ComplexShape ι} → HomologicalComplex V c → ι → V
-- Lean.Elab.ParseImportsFast
Lean.instToJsonPrintImportResult : Lean.ToJson Lean.PrintImportResult
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- If we drop the leading coefficient, the sign changes drop by 0 or 1 depending on whether
the first two nonzero coefficients match.  -/
Polynomial.signVariations_eq_eraseLead_add_ite : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {P : Polynomial R},
  P ≠ 0 →
    P.signVariations =
      P.eraseLead.signVariations +
        if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.instIsConstantObjSheafSheafCompose : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (F : CategoryTheory.Sheaf J D) [h : CategoryTheory.Sheaf.IsConstant J F],
  CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)
-- Mathlib.Analysis.Convex.PathConnected
/-- Given two complementary subspaces `p` and `q` in `E`, if the complement of `{0}`
is path connected in `p` then the complement of `q` is path connected in `E`.  -/
isPathConnected_compl_of_isPathConnected_compl_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {p q : Submodule ℝ E}, IsCompl p q → IsPathConnected {0}ᶜ → IsPathConnected (↑q)ᶜ
-- Mathlib.Data.Nat.Cast.Order.Ring
/-- A version of `Nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work
for `ℕ∞` and `ℝ≥0∞`, so we use type-specific lemmas for these types.  -/
Nat.cast_tsub : ∀ {α : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α]
  [inst_4 : Sub α] [OrderedSub α] [AddLeftReflectLE α] (m n : ℕ), ↑(m - n) = ↑m - ↑n
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.self_le_succ_pred : ∀ (o : Ordinal.{u_4}), o ≤ Order.succ o.pred
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_ofInt : ∀ (n : ℤ), Int32.ofBitVec (BitVec.ofInt 32 n) = Int32.ofInt n
-- Init.Data.Repr
instReprId_1 : {α : Type u_1} → [Repr α] → Repr (Id α)
-- Init.Data.Vector.Perm
Vector.Perm.of_toArray_perm : ∀ {α : Type u_1} {n : ℕ} {as bs : Vector α n}, as.toArray.Perm bs.toArray → as.Perm bs
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.addX P Q = P 1 ^ 2 * Q 2 * Q 0
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `initial_iff_initial_comp` below.  -/
CategoryTheory.Functor.initial_iff_equivalence_comp : ∀ {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) [F.IsEquivalence], G.Initial ↔ (F.comp G).Initial
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_const' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ℝ),
  ProbabilityTheory.mgf (fun x => c) μ t = μ.real Set.univ * Real.exp (t * c)
-- Std.Time.Format.Modifier
Std.Time.instReprFraction : Repr Std.Time.Fraction
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometrically : ∀ (P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme),
  (AlgebraicGeometry.geometrically P).IsStableUnderBaseChange
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_ne_one : ∀ {α : Type u_3} [inst : AddGroupWithOne α] [CharZero α] {n : ℤ}, ↑n ≠ 1 ↔ n ≠ 1
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- Smooth of relative dimension `0` is multiplicative.  -/
AlgebraicGeometry.instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat : CategoryTheory.MorphismProperty.IsMultiplicative (@AlgebraicGeometry.SmoothOfRelativeDimension 0)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.isAddModHom : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : CategoryTheory.AddMod D A} (self : M.Hom N),
  CategoryTheory.IsAddModHom A self.hom
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U →
    Continuous f →
      (Topology.IsClosedEmbedding f ↔ ∀ (i : ι), Topology.IsClosedEmbedding ((U i).carrier.restrictPreimage f))
-- Mathlib.Order.Filter.Curry
Filter.mem_curry_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set (α × β)},
  s ∈ l.curry m ↔ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s
-- Init.Data.Vector.Count
Vector.countP_push_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α} {xs : Vector α n},
  p a = true → Vector.countP p (xs.push a) = Vector.countP p xs + 1
-- Mathlib.GroupTheory.Congruence.Defs
Con.commSemigroup.eq_1 : ∀ {M : Type u_4} [inst : CommSemigroup M] (c : Con M),
  c.commSemigroup = Function.Surjective.commSemigroup Quotient.mk'' ⋯ ⋯
-- Mathlib.Algebra.Notation.Prod
Prod.smul_def : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SMul E α] [inst_1 : SMul E β] (c : E) (p : α × β),
  c • p = (c • p.1, c • p.2)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_sup : ∀ {M : Type u_2} [inst : MulOneClass M] (S₁ S₂ : Submonoid Mᵐᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Init.Core
EStateM.Result.error.inj : ∀ {ε σ α : Type u} {a : ε} {a_1 : σ} {a_2 : ε} {a_3 : σ},
  EStateM.Result.error a a_1 = EStateM.Result.error a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Std.Internal.Do.ExceptPost
/-- The unique `EPost.Nil` value is below any `EPost.Nil` value.  -/
Std.Internal.Do.EPost.Nil.le : ∀ (epost : EPost⟨⟩), Lean.Order.PartialOrder.rel epost⟨⟩ epost
-- Mathlib.Topology.UniformSpace.Separation
t0Space_iff_uniformity : ∀ {α : Type u} [inst : UniformSpace α], T0Space α ↔ ∀ (x y : α), (∀ r ∈ uniformity α, (x, y) ∈ r) → x = y
-- Init.Data.Ord.Basic
Ordering.isNe_eq_isLT_or_isGT : ∀ {o : Ordering}, o.isNe = (o.isLT || o.isGT)
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
/-- Lift a copy between graphs to a copy between their line graphs  -/
SimpleGraph.Copy.lineGraph : {V : Type u_1} →
  {V' : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph V'} → G.Copy G' → G.lineGraph.Copy G'.lineGraph
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.pullbackMk_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X₁ X₂ S : C}
  (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [inst_3 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
  (x₁ : CategoryTheory.ToType X₁) (x₂ : CategoryTheory.ToType X₂)
  (h : (CategoryTheory.ConcreteCategory.hom f₁) x₁ = (CategoryTheory.ConcreteCategory.hom f₂) x₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f₁ f₂))
      (CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h) =
    x₂
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_ground : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), (M.delete D).E = M.E \ D
-- Mathlib.Data.Num.Lemmas
Num.succ'.eq_2 : ∀ (p : PosNum), (Num.pos p).succ' = p.succ
-- Lean.Meta.Basic
/-- `MetaM` monad state.
 -/
Lean.Meta.State : Type
-- Mathlib.Algebra.Group.Units.Defs
Units.val_pow_eq_pow_val : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_var_cert : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Var → Int.Internal.Linear.Var → Bool
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulMono.toMulPosMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α] [PosMulMono α],
  MulPosMono α
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.irrefl : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, ¬G.Adj v v
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.of_d_ne : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X (n + 1) ⟶ X n) {i j : α}, i ≠ j + 1 → ChainComplex.of.d X d i j = 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_mk₀_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n),
  α.comp (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.id Y)) ⋯ = α
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, where the point on the left is constant,
expressed as a subtraction involving a `weightedVSubOfPoint` expression.  -/
Finset.sum_smul_const_vsub_eq_sub_weightedVSubOfPoint : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ b : P),
  ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - (s.weightedVSubOfPoint p₂ b) w
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_add : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {a : A} {x y : ℝ}, IsUnit a → a ^ (x + y) = a ^ x * a ^ y
-- Init.Data.String.OrderInstances
String.Pos.instLECoOfNatIntHAddCastUtf8ByteSize : ∀ {s : String}, Lean.Grind.ToInt.LE s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.rightHom_eq_right : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q],
  ⇑RegularWreathProduct.rightHom = RegularWreathProduct.right
-- Lean.Parser.Basic
/-- The parsing tables, which consist of a dynamic set of parser
functions based on the syntaxes that have been declared so far.  -/
Lean.Parser.ParserCategory.tables : Lean.Parser.ParserCategory → Lean.Parser.PrattParsingTables
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_diff!_add_size_inter!_eq_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → (m₁.diff! m₂).size + (m₁.inter! m₂).size = m₁.size
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.union : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsUpperSet s → IsUpperSet t → IsUpperSet (s ∪ t)
-- Mathlib.Order.InitialSeg
PrincipalSeg.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s]
  {f g : PrincipalSeg r s}, f = g ↔ ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
exists_maximal_linearIndepOn : ∀ {ι : Type u'} (R : Type u_2) {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (v : ι → M), ∃ s, LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ a, a ≠ 0 ∧ a • v i ∈ Submodule.span R (v '' s)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppRid_single_tmul_single : ∀ (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (a : ι) (b : κ) (m : M) (r : R),
  (finsuppTensorFinsuppRid R M ι κ) ((fun₀ | a => m) ⊗ₜ[R] fun₀ | b => r) = fun₀ | (a, b) => r • m
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.Rel₁ : (m : Type w → Type w') →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          [Std.Iterators.Finite α₁ m] →
            [Std.Iterators.Productive α₂ m] → Std.IterM m (β₁ × β₂) → Std.IterM m (β₁ × β₂) → Prop
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_multiply : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {q : Type u_6} {α : Type u_12}
  [inst : Fintype l] [inst_1 : Fintype m] [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix l p α) (B' : Matrix l q α) (C' : Matrix m p α) (D' : Matrix m q α),
  Matrix.fromBlocks A B C D * Matrix.fromBlocks A' B' C' D' =
    Matrix.fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1π_comp_map : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.H1π A) (groupHomology.map f φ 1) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ f φ) (groupHomology.H1π B)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α),
  Inv.inv '' Set.Ioi a = Set.Iio a⁻¹