mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.toHomeomorphSourceTarget_symm_apply_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (a : ↑e.target), ↑(e.toHomeomorphSourceTarget.symm a) = ↑e.symm ↑a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getDoLetArrowVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.star : {C : Type u} → CategoryTheory.WithInitial C
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- `seminormFromBounded'` is a ring seminorm on `R`.  -/
seminormFromBounded : {R : Type u_1} →
  [inst : CommRing R] →
    {f : R → ℝ} →
      {c : ℝ} →
        f 0 = 0 →
          0 ≤ f →
            (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
              (∀ (a b : R), f (a + b) ≤ f a + f b) → (∀ (x : R), f (-x) = f x) → RingSeminorm R
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsNontrivial.mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], (∃ γ, γ ≠ 0 ∧ γ ≠ 1) → ValuativeRel.IsNontrivial R
-- Init.SizeOf
UInt8.ofBitVec.sizeOf_spec : ∀ (toBitVec : BitVec 8), sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.expect_eq_zero_iff_ne_zero : ∀ {G : Type u_1} {R : Type u_3} [inst : AddGroup G] [inst_1 : Fintype G] [inst_2 : Semifield R] [inst_3 : CharZero R]
  {ψ : AddChar G R}, (Finset.univ.expect fun x => ψ x) = 0 ↔ ψ ≠ 0
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((HomologicalComplex.single C c j).map f) j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j B).hom h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_pos : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelAddMonoid M] {f : ι → M}, 0 < f → 0 < ∑ i, f i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.HashMap.Raw.unitOfList l ↔ l.contains k = true
-- Mathlib.Order.Birkhoff
LowerSet.supIrred_Iic : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), SupIrred (LowerSet.Iic a)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.π_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (s : CategoryTheory.Limits.CokernelCofork f), s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = 0
-- Std.Http.Protocol.H1.Reader
/-- Replaces the reader's input iterator with a new one.
 -/
Std.Http.Protocol.H1.Reader.setInput : {dir : Std.Http.Protocol.H1.Direction} →
  ByteArray.Iterator → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Data.List.Nodup
List.Nodup.of_cons : ∀ {α : Type u} {l : List α} {a : α}, (a :: l).Nodup → l.Nodup
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
dvd_of_one_le_padicValNat : ∀ {p n : ℕ}, 1 ≤ padicValNat p n → p ∣ n
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (CategoryTheory.Comon D)) (X_1 : C),
  ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso.inv.app X).app X_1).hom =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_self_le : ∀ {x k : ℤ}, 0 < k → k * x.fdiv k ≤ x
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.bernoulli_apply : ∀ {p : NNReal} (h : p ≤ 1) (b : Bool), (PMF.bernoulli p h) b = ↑(bif b then p else 1 - p)
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.addEntryFn : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → σ → β → σ
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.isClosed_image_of_isClosed : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] {s : Set M},
  IsClosed s → s ⊆ Function.support ↑f → IsClosed (↑(extChartAt I c) '' s)
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Variant of `getD_map` that holds without `LawfulEqOrd`.  -/
Std.DTreeMap.Internal.Impl.Const.getD_map' : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → γ} {k : α} {fallback : γ} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.map f t) k fallback =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.DTreeMap.Internal.Impl.Const.get? t k) ⋯).getD fallback
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.instSmallPullback₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) [E.Small] {T : C} (f : T ⟶ S) [inst_2 : J.IsStableUnderBaseChange]
  [inst_3 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)],
  (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).Small
-- Mathlib.Algebra.BigOperators.WithTop
/-- A product of finite terms is finite.  -/
WithBot.prod_ne_bot : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithBot M₀}, (∀ i ∈ s, f i ≠ ⊥) → ∏ i ∈ s, f i ≠ ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.spine_arrow : ∀ (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op { len := n })) (i : Fin n),
  (X.spine n Δ).arrow i = (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc i).op)) Δ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.maxKeyD fallback = t.keys.getLastD fallback
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.val_unit' : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α} (h : IsUnit a), ↑h.unit' = a
-- Mathlib.Topology.Algebra.Group.Basic
topologicalAddGroup_of_indiscreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddGroup H] [IndiscreteTopology H], IsTopologicalAddGroup H
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- More general version of `isIso_π_of_isLimit`.  -/
CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit' : ∀ {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] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantTo i₀ →
    ∀ [CategoryTheory.IsCofiltered J] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (j : J)
      (π : j ⟶ i₀), CategoryTheory.IsIso (c.π.app j)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instAddCommGroupHom : {k : Type u} →
  {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → AddCommGroup (A ⟶ B)
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_natCast : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : ℕ)
  (v : m → α), Matrix.vecMul v ↑x = MulOpposite.op ↑x • v
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk : ∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
  (∀ {X Y Z : AlgebraicGeometry.Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : AlgebraicGeometry.IsAffine Z],
      P f → P (CategoryTheory.CategoryStruct.comp e.hom f)) →
    (∀ {X Y Z : AlgebraicGeometry.Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y],
        P f → P (CategoryTheory.CategoryStruct.comp f e.hom)) →
      P.toProperty.RespectsIso
-- Init.Data.Option.Attach
Option.attach_bind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β},
  (o.bind f).attach =
    o.attach.bind fun x =>
      match x with
      | ⟨x, h⟩ =>
        Option.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, h'⟩ => ⟨y, ⋯⟩)
          (f x).attach
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmod_congr_of_sub_mem_span : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) (a b : ℕ),
  x - ↑a ∈ Ideal.span {↑p ^ n} → x - ↑b ∈ Ideal.span {↑p ^ n} → ↑a = ↑b
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {g : α → γ},
  Filter.EventuallyConst f l → Filter.EventuallyConst g l → Filter.EventuallyConst (fun x => (f x, g x)) l
-- Init.Control.Lawful.Instances
ExceptT.run_liftM : ∀ {α ε : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] (x : m α), (liftM x).run = Except.ok <$> x
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.isScalarTower : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M), IsScalarTower S R ↥p
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_succ_floor : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (a : R), a < ↑⌊a⌋₊.succ
-- Lean.Data.Lsp.Basic
Lean.Lsp.instHashableMarkupContent.hash : Lean.Lsp.MarkupContent → UInt64
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_log_le_self : ∀ (b : Ordinal.{u_1}) {x : Ordinal.{u_1}}, x ≠ 0 → b ^ Ordinal.log b x ≤ x
-- Mathlib.Probability.Distributions.Gamma
/-- Measure defined by the gamma distribution  -/
ProbabilityTheory.gammaMeasure : ℝ → ℝ → MeasureTheory.Measure ℝ
-- Lean.Class
/-- Return `true` if the given `declName` is a type class with output parameters.  -/
Lean.hasOutParams : Lean.Environment → Lean.Name → Bool
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPos_addNeg : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  assignment.addNegAssignment.hasPosAssignment = assignment.hasPosAssignment
-- Mathlib.Topology.Compactification.StoneCech
preStoneCechUnit.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] (x : α),
  preStoneCechUnit x = Quot.mk (fun F G => ∃ x, ↑F ≤ nhds x ∧ ↑G ≤ nhds x) (pure x)
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.eq_to_beq : ∀ (a b : Bool), (a = b) = ((a == b) = true)
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap_id : ∀ (σ : Type u_1) (R : Type u_4) [inst : CommSemiring R], MvPolynomial.comap (AlgHom.id R (MvPolynomial σ R)) = id
-- Init.Data.ByteArray.Basic
/-- The current position.

This position is not necessarily valid for the array, for instance if one keeps calling
`Iterator.next` when `Iterator.atEnd` is true. If the position is not valid, then the
current byte is `(default : UInt8)`.  -/
ByteArray.Iterator.pos : ByteArray.Iterator → ℕ
-- Init.Data.SInt.Bitwise
Int64.toUInt64_xor : ∀ (a b : Int64), (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (r : 𝕜) (f : E →L[𝕜] F),
  ContinuousLinearMap.rTensor G (r • f) = r • ContinuousLinearMap.rTensor G f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instZeroHom.eq_1 : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M N : CategoryTheory.AddMon D),
  M.instZeroHom N =
    {
      zero :=
        {
          hom :=
            CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit M.X)
              CategoryTheory.AddMonObj.zero,
          isAddMonHom_hom := ⋯ } }
-- Mathlib.Order.Max
/-- Order without minimal elements. Sometimes called coinitial or dense.  -/
NoMinOrder : (α : Type u_3) → [LT α] → Prop
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.add_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ ν : MeasureTheory.Measure α},
  μ₁.AbsolutelyContinuous ν → μ₂.AbsolutelyContinuous ν → (μ₁ + μ₂).AbsolutelyContinuous ν
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.compLeft.eq_1 : ∀ {A : Type u_2} {B : Type u_3} (E : Type u_6) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : CommGroup E]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace E]
  [inst_6 : IsTopologicalGroup E] (f : A →ₜ* B),
  ContinuousMonoidHom.compLeft E f = { toFun := fun g => g.comp f, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }
-- Lean.Data.JsonRpc
/-- A variant of `Message` that has been parsed *partially*, without the payload.
This is useful when we want to process the metadata of a `Message` without parsing and converting
the whole thing.
 -/
Lean.JsonRpc.MessageMetaData : Type
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stVar.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.stVar v l (Turing.TM2to1.StAct.pop f) = f v l.head?
-- Mathlib.Order.Irreducible
not_supIrred : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, ¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
-- Init.Meta.Defs
Lean.Syntax.instCoeArraySepArray : {sep : String} → Coe (Array Lean.Syntax) (Lean.Syntax.SepArray sep)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Rep.Tor_map : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ) {X Y : Rep.{u, u, u} k G} (f : X ⟶ Y),
  (Rep.Tor k G n).map f = CategoryTheory.NatTrans.leftDerived ((Rep.coinvariantsTensor k G).map f) n
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- The Galois connection between fixing submonoids and fixed points of a monoid action  -/
fixingSubmonoid_fixedPoints_gc : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α],
  GaloisConnection (⇑OrderDual.toDual ∘ fixingSubmonoid M) ((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
-- Mathlib.Logic.Basic
Exists.fst : ∀ {b : Prop} {p : b → Prop}, Exists p → b
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.symm_mapDomainRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N),
  (MonoidAlgebra.mapDomainRingEquiv R e).symm = MonoidAlgebra.mapDomainRingEquiv R e.symm
-- Mathlib.Topology.Bases
Topology.IsOpenEmbedding.separableSpace : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] [TopologicalSpace.SeparableSpace β]
  {f : α → β}, Topology.IsOpenEmbedding f → TopologicalSpace.SeparableSpace α
-- Mathlib.Topology.Algebra.InfiniteSum.Order
le_hasSum_of_le_sum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : Preorder α] [inst_1 : AddCommMonoid α]
  [inst_2 : TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIciTopology α] [L.NeBot],
  HasSum f a L → (∀ (s : Finset ι), c ≤ ∑ i ∈ s, f i) → c ≤ a
-- Init.Data.Vector.Extract
Vector.mem_extract_iff_getElem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a : α} {i j : ℕ},
  a ∈ xs.extract i j ↔ ∃ k, ∃ (hm : k < min j n - i), xs[i + k] = a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit.inj : ∀ {c₁ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr} {decVar : Lean.FVarId} {h : Lean.Meta.Grind.Arith.Cutsat.UnsatProof}
  {decVars : Array Lean.FVarId} {c₁_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr} {decVar_1 : Lean.FVarId}
  {h_1 : Lean.Meta.Grind.Arith.Cutsat.UnsatProof} {decVars_1 : Array Lean.FVarId},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit c₁ decVar h decVars =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit c₁_1 decVar_1 h_1 decVars_1 →
    c₁ = c₁_1 ∧ decVar = decVar_1 ∧ h = h_1 ∧ decVars = decVars_1
-- Mathlib.Order.Interval.Basic
NonemptyInterval.map₂_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (a : NonemptyInterval α)
  (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.1 = f a.toProd.1 a_1.toProd.1
-- Mathlib.Topology.UniformSpace.Compact
/-- On a compact uniform space, the topology determines the uniform structure, entourages are
exactly the neighborhoods of the diagonal.  -/
compactSpace_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] [CompactSpace α], uniformity α = ⨆ x, nhds (x, x)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      (toPrecoverage : CategoryTheory.Precoverage C) →
        (∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f],
            CategoryTheory.Presieve.singleton f ∈ toPrecoverage.coverings X) →
          (∀ ⦃X Y : C⦄ (f : Y ⟶ X),
              ∀ S ∈ toPrecoverage.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage.coverings Y) →
            (∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
                S ∈ toPrecoverage.coverings X →
                  (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage.coverings Y) →
                    S.bind Ti ∈ toPrecoverage.coverings X) →
              CategoryTheory.Pretopology C
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_7} {F : Type u_8} [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : FunLike F R S] [inst_5 : MonoidHomClass F R S] {n : ℕ} [inst_6 : NeZero n] {f : F}
  (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty) (a : ↥(rootsOfUnity n R)), ⋯ = ⋯
-- Mathlib.Algebra.Lie.Ideal
LieHom.ker.eq_1 : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), f.ker = LieIdeal.comap f ⊥
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.prod_apply : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R),
  (f.prod g) x = (f x, g x)
-- Lean.Widget.UserWidget
Lean.Widget.instRpcEncodableGetWidgetsResponse : Lean.Server.RpcEncodable Lean.Widget.GetWidgetsResponse
-- Mathlib.Algebra.Group.Units.Opposite
AddUnits.opEquiv.eq_1 : ∀ {M : Type u_2} [inst : AddMonoid M],
  AddUnits.opEquiv =
    {
      toFun := fun u =>
        AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ },
      invFun := fun X =>
        AddOpposite.rec'
          (fun u => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X,
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- The radical of a quadratic form is preserved by isometry equivalences.  -/
QuadraticMap.IsometryEquiv.map_radical : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup M']
  [inst_2 : AddCommGroup P] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R M'] [inst_6 : Module R P]
  {Q : QuadraticMap R M P} {Q' : QuadraticMap R M' P} (e : Q.IsometryEquiv Q'),
  Submodule.map (↑e.toLinearEquiv) Q.radical = Q'.radical
-- Mathlib.Algebra.Ring.Pi
Pi.nonUnitalCommRing : {I : Type u} → {f : I → Type v} → [(i : I) → NonUnitalCommRing (f i)] → NonUnitalCommRing ((i : I) → f i)
-- Mathlib.Data.FunLike.Basic
/-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search.  -/
DFunLike.subsingleton_cod : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] [∀ (a : α), Subsingleton (β a)], Subsingleton F
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.nilpotencyClass_le_of_upperCentralSeries_eq : ∀ {G : Type u_1} [inst : AddGroup G] {a b : ℕ},
  a < b → AddSubgroup.upperCentralSeries G a = AddSubgroup.upperCentralSeries G b → AddGroup.nilpotencyClass G ≤ a
-- Mathlib.Topology.Algebra.UniformConvergence
instMonoidUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Monoid β] → Monoid (UniformOnFun α β 𝔖)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_add_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ),
  ⌊a + ↑n⌋ = ⌊a⌋ + ↑n
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurryObjFlip_inv_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 : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D × C),
  F.uncurryObjFlip.inv.app X = CategoryTheory.CategoryStruct.id ((F.obj X.2).obj X.1)
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- A function whose domain's cardinality is infinite and strictly greater than its codomain's
has an infinite fiber.  -/
Cardinal.exists_infinite_fiber : ∀ {β α : Type u} (f : β → α), Cardinal.mk α < Cardinal.mk β → ∀ [Infinite β], ∃ a, Infinite ↑(f ⁻¹' {a})
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.IsStrongTriangulatedGenerator.isClassicalTriangulatedGenerator : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.IsStrongTriangulatedGenerator → P.IsClassicalTriangulatedGenerator
-- Mathlib.Data.Finset.Sups
Finset.infs_assoc : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t u : Finset α), s ⊼ t ⊼ u = s ⊼ (t ⊼ u)
-- Mathlib.Analysis.Normed.Operator.Mul
NonUnitalAlgHom.coe_Lmul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_3} [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R],
  ⇑(NonUnitalAlgHom.Lmul 𝕜 R) = ⇑(ContinuousLinearMap.mul 𝕜 R)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The equivalence `Karoubi (CochainComplex C α) ≌ CochainComplex (Karoubi C) α`.  -/
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (α : Type u_3) →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            CategoryTheory.Idempotents.Karoubi (CochainComplex C α) ≌
              CochainComplex (CategoryTheory.Idempotents.Karoubi C) α