mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The type coding the basic relations that will give rise to the divided power algebra.
The class of `MvPolynomial.X (n, a)` will be equal to `dpow n a`, for `a ∈ M`.  -/
DividedPowerAlgebra.Rel : (R : Type u_2) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [Module R M] → MvPolynomial (ℕ × M) R → MvPolynomial (ℕ × M) R → Prop
-- Mathlib.Data.Finsupp.Defs
Finsupp.ext : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f g : α →₀ M}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_add_mul_left_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (x + y * z) y → IsCoprime x y
-- Mathlib.Analysis.InnerProductSpace.Defs
PUnit.instInnerProductSpace : {𝕜 : Type u_1} → [inst : RCLike 𝕜] → InnerProductSpace 𝕜 PUnit.{u_4 + 1}
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.charFun_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (t : E),
  MeasureTheory.charFun (ProbabilityTheory.stdGaussian E) t = Complex.exp (-↑‖t‖ ^ 2 / 2)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instInhabited : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Inhabited β] → Inhabited (MeasureTheory.SimpleFunc α β)
-- Std.Time.Date.Unit.Week
/-- Convert `Day.Offset` into `Week.Offset`.
 -/
Std.Time.Week.Offset.ofDays : Std.Time.Day.Offset → Std.Time.Week.Offset
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insert.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → t.insert a b = t_1.insert a b_1
-- Mathlib.Order.LiminfLimsup
Filter.mem_liminf_iff_eventually_mem : ∀ {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α}, a ∈ Filter.liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLeast? : Std.PRange.Least? UInt16
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.id_obj : ∀ (V : Type u_1) [inst : Quiver V] (X : V), (𝟭q V).obj X = X
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- The axiom of choice says that every type is a projective object in `Type`.  -/
CategoryTheory.Projective.inst : ∀ (X : Type u), CategoryTheory.Projective X
-- Aesop.BaseM
Aesop.BaseM.State.mk.injEq : ∀ (rulePatternCache : Aesop.RulePatternCache) (stats : Aesop.Stats) (rulePatternCache_1 : Aesop.RulePatternCache)
  (stats_1 : Aesop.Stats),
  ({ rulePatternCache := rulePatternCache, stats := stats } =
      { rulePatternCache := rulePatternCache_1, stats := stats_1 }) =
    (rulePatternCache = rulePatternCache_1 ∧ stats = stats_1)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_one : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (PowerSeries.coeff n) 1 = if n = 0 then 1 else 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D}
  (h : E.IsPointwiseRightKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)]
  (g : CategoryTheory.StructuredArrow Y L),
  CategoryTheory.CategoryStruct.comp h.isoLimit.inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom)
        ((CategoryTheory.CostructuredArrow.hom E).app g.right)) =
    CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g
-- Mathlib.Algebra.Order.Archimedean.Real.Hom
Real.nonemptyOrderRingHom : ∀ (α : Type u_1) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α], Nonempty (α →+*o ℝ)
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.continuousOn_norm_circleTransformBoundingFunction : ∀ {R r : ℝ},
  r < R →
    ∀ (z : ℂ),
      ContinuousOn ((fun x => ‖x‖) ∘ Complex.circleTransformBoundingFunction R z) (Metric.closedBall z r ×ˢ Set.univ)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.exists_insert_toList_zoom_node : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {c' : RBTree.RBColor} {l : RBTree.RBNode α}
  {v' : α} {r : RBTree.RBNode α} {p : RBTree.RBNode.Path α} {v : α} {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.zoom (cmp v) t = (RBTree.RBNode.node c' l v' r, p) →
      ∃ L R, t.toList = L ++ v' :: R ∧ (RBTree.RBNode.insert cmp t v).toList = L ++ v :: R
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Auxiliary definition for `monoidal_coherence`.  -/
Mathlib.Tactic.Coherence.mkProjectMapExpr : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.toIsHausdorff : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} {M : Type u_4} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : IsAdicComplete I M], IsHausdorff I M
-- Mathlib.Topology.MetricSpace.ProperSpace
ProperSpace.mk : ∀ {α : Type u} [inst : PseudoMetricSpace α], (∀ (x : α) (r : ℝ), IsCompact (Metric.closedBall x r)) → ProperSpace α
-- Mathlib.Topology.Separation.Hausdorff
/-- A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.  -/
t2_iff_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ ∀ {x y : X}, (nhds x ⊓ nhds y).NeBot → x = y
-- Init.Data.BitVec.Lemmas
BitVec.and_eq_allOnes_iff : ∀ {w : ℕ} {x y : BitVec w}, x &&& y = BitVec.allOnes w ↔ x = BitVec.allOnes w ∧ y = BitVec.allOnes w
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.insert : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {a : α} {b : β},
  m.WF → (m.insert a b).WF
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.Functor.FullyFaithful.hasShift.map_zero_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_2} D] [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift D A]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C)
  (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (X : C),
  F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).hom.app X) =
    CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) ((CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X))
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.apply_clm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, (↑T).IsSymmetric → ∀ (x y : E), inner 𝕜 (T x) y = inner 𝕜 x (T y)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.ext : ∀ {α : Type u} [inst : AddMonoid α] {u v : AddUnits α}, ↑u = ↑v → u = v
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.isStableUnderTransfiniteCompositionOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.IsStableUnderTransfiniteComposition] (J : Type w) [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J], W.IsStableUnderTransfiniteCompositionOfShape J
-- Init.Data.BitVec.Lemmas
BitVec.eq_zero_or_eq_one : ∀ (a : BitVec 1), a = 0#1 ∨ a = 1#1
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.instToJsonStructured : Lean.ToJson Lean.Json.Structured
-- Mathlib.Topology.Maps.Strict.Basic
/-- A map is a strict map if and only if the canonical bijection
`Quotient (Setoid.ker f) ≃ Set.range f` is a homeomorphism.  -/
Topology.isStrictMap_iff_isHomeomorph_quotientKerEquivRange : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsStrictMap f ↔ IsHomeomorph ⇑(Setoid.quotientKerEquivRange f)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The domain of an isomorphism.  -/
Mathlib.Tactic.Bicategory.srcExprOfIso : Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is of the form `Int`  -/
Lean.Meta.Grind.Arith.isIntType : Lean.Expr → Bool
-- Init.Meta.Defs
Lean.instQuoteListMkStr1 : {α : Type} → [Lean.Quote α] → Lean.Quote (List α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α} {k k' : α},
  compare k k' = Ordering.eq →
    ∀
      {h' :
        Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯) = true},
      k ∉ t →
        List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
          k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey k' h' = k
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix.eq_1 : ∀ {R : Type u_3} {N : Type u_5} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : Invertible 2] [inst_4 : AddCommGroup N] [inst_5 : Module R N] (b : Module.Basis n R N)
  (Q : QuadraticForm R N), QuadraticForm.toMatrix b Q = (LinearMap.toMatrix₂ b b) (QuadraticMap.associated Q)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_zsmul_add_ne_bot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) {n : ℤ},
  -↑(LieModule.chainBotCoeff α β) ≤ n → n ≤ ↑(LieModule.chainTopCoeff α β) → LieModule.genWeightSpace M (n • α + ⇑β) ≠ ⊥
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.instInhabitedSparseCasesOnInfo.default : Lean.Meta.SparseCasesOnInfo
-- Batteries.Data.BinomialHeap.Basic
/-- A cons node contains a tree of root `val`, children `node` and rank `rank`,
and then `next` which is the rest of the forest.  -/
Batteries.BinomialHeap.Imp.Heap.cons : {α : Type u} →
  ℕ → α → Batteries.BinomialHeap.Imp.HeapNode α → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α
-- Mathlib.Algebra.Algebra.Shrink
/-- Shrinking `α` to a smaller universe preserves algebra structure.  -/
Shrink.algEquiv : (R : Type u_1) →
  (α : Type u_2) →
    [inst : Small.{v, u_2} α] →
      [inst_1 : CommSemiring R] → [inst_2 : Semiring α] → [inst_3 : Algebra R α] → Shrink.{v, u_2} α ≃ₐ[R] α
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.State.toAssert : Aesop.RuleTac.ForwardM.State → Array (Lean.Expr × Lean.Expr × ℕ)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.mk.injEq : ∀ (carrier : Type u) [str : Add carrier] (carrier_1 : Type u) (str_1 : Add carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i →
    1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT✝ s i) + 1) <
      s (MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s i)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.exact_homologyShortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ) [CategoryTheory.Mono f],
  (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex✝ f n).Exact
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.congrN!.go : Congr!.Config → ℕ → ℕ → Lean.MVarId → CongrMetaM Unit
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.createImportInitResults.go : {α : Type} →
  Lean.Core.Context →
    Lean.Environment →
      (Lean.Name →
          Lean.ConstantInfo →
            Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
        ℕ →
          ℕ →
            Lean.Meta.RefinedDiscrTree.PreDiscrTree α →
              Lean.Meta.RefinedDiscrTree.ImportErrorData✝ →
                IO.Ref Lean.Meta.State → IO.Ref Lean.Core.State → BaseIO (Lean.Meta.RefinedDiscrTree.InitResults✝ α)
-- Batteries.Data.Float.Lemmas
Float.isNaN_eq_decide_eq_nan : ∀ {f : Float}, f.isNaN = decide (f = Float.nan)
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- If `x` generates `S` over `R` and is integral over `R`, then it defines a power basis.
See `PowerBasis.ofAdjoinEqTop` for a version over a field.
 -/
PowerBasis.ofAdjoinEqTop' : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [IsDomain R] →
          [inst_3 : Algebra R S] →
            [IsIntegrallyClosed R] →
              [IsDomain S] → [Module.IsTorsionFree R S] → {x : S} → IsIntegral R x → R[x] = ⊤ → PowerBasis R S
-- Mathlib.RingTheory.Algebraic.Integral
instIsPushoutFractionRingMvPolynomial : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [inst_3 : IsDomain S] [inst_4 : FaithfulSMul R S] {σ : Type u_4},
  Algebra.IsPushout R (FractionRing (MvPolynomial σ R)) S (FractionRing (MvPolynomial σ S))
-- Mathlib.GroupTheory.PGroup
IsPGroup.disjoint_of_coprime : ∀ {G : Type u_1} [inst : Group G] {p₁ p₂ : ℕ} {H₁ H₂ : Subgroup G},
  IsPGroup p₁ ↥H₁ → IsPGroup p₂ ↥H₂ → p₁.Coprime p₂ → Disjoint H₁ H₂
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_zero : ∀ {α : Type u_1} [inst : Zero α], SymAlg.unsym 0 = 0
-- Lean.Meta.Sym.LooseBVarsS
/-- Lifts loose bound variables `>= s` in `e` by `d`.
It assumes the input is maximally shared, and ensures the output is too.
 -/
Lean.Meta.Sym.liftLooseBVarsS : Lean.Expr → ℕ → ℕ → Lean.Meta.Sym.SymM Lean.Expr
-- Init.Data.List.Lemmas
List.dropLast_concat_getLast : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.dropLast ++ [l.getLast h] = l
-- Mathlib.NumberTheory.Height.Northcott
/-- A field that satisfies the Northcott property for `mulHeight₁` also does for `logHeight₁`.  -/
Height.instNorthcottRealLogHeight₁OfMulHeight₁ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] [Northcott Height.mulHeight₁],
  Northcott Height.logHeight₁
-- Init.Data.Array.Lemmas
Array.mem_filter : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {a : α}, a ∈ Array.filter p xs ↔ a ∈ xs ∧ p a = true
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabUnlockLimits : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.GroupWithZero.Defs
mul_inv_cancel_left₀ : ∀ {G₀ : Type u} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (b : G₀), a * (a⁻¹ * b) = b
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- A completion of `α` is the data of a complete separated uniform space
and a map from `α` with dense range and inducing the original uniform structure on `α`.  -/
AbstractCompletion : (α : Type u) → [UniformSpace α] → Type (max u (v + 1))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_none : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f], (CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app none = g
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.mk_toFun : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {f : ℝ → ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s f).toFun = f
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.inv : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : DivisionMonoid β] {f : α → β},
  HasCompactMulSupport f → HasCompactMulSupport f⁻¹
-- Std.Async.Basic
/-- Construct an `AsyncTask` that is already resolved with value `x`.
 -/
Std.Async.AsyncTask.pure : {α : Type} → α → Std.Async.AsyncTask α
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.inclusion_injective : ∀ {R : Type u} [inst : NonAssocRing R] {S T : Subring R} (h : S ≤ T), Function.Injective ⇑(Subring.inclusion h)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {A B : CommAlgCat R} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Mathlib.AlgebraicGeometry.Fiber
/-- `f.fiber y` is the scheme-theoretic fiber of `f` at `y`.  -/
AlgebraicGeometry.Scheme.Hom.fiber : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → ↥Y → AlgebraicGeometry.Scheme
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.realSize.eq_2 : ∀ {α : Type u_1} (a : α) (c s : Batteries.BinomialHeap.Imp.HeapNode α),
  (Batteries.BinomialHeap.Imp.HeapNode.node a c s).realSize = c.realSize + 1 + s.realSize
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_rco : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : LT α] [inst_4 : DecidableLT α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Rco α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.LinearAlgebra.Projection
LinearMap.isCompl_of_proj : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {f : E →ₗ[R] ↥p}, (∀ (x : ↥p), f ↑x = x) → IsCompl p f.ker
-- Init.Data.Array.FinRange
/-- Returns an array of all elements of `Fin n` in order, starting at `0`.

Examples:
* `Array.finRange 0 = (#[] : Array (Fin 0))`
* `Array.finRange 2 = (#[0, 1] : Array (Fin 2))`
 -/
Array.finRange : (n : ℕ) → Array (Fin n)
-- Mathlib.Data.Multiset.Fold
Multiset.fold_eq_foldr : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (s : Multiset α),
  Multiset.fold op b s = Multiset.foldr op b s
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the arithmetic function `ζ` does not vanish on the right half-plane
`re s > 1`.  -/
ArithmeticFunction.LSeries_zeta_ne_zero_of_one_lt_re : ∀ {s : ℂ}, 1 < s.re → LSeries (fun n => ↑(ArithmeticFunction.zeta n)) s ≠ 0
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_eq_right_inv : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible a], a * b = 1 → ⅟a = b
-- Mathlib.Data.List.Basic
List.IsPrefix.idxOf_eq_of_mem : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α],
  l₁ <+: l₂ → ∀ {a : α}, a ∈ l₁ → List.idxOf a l₁ = List.idxOf a l₂
-- Lean.Language.Basic
/-- Untransformed snapshot; should be accessed with care so as not to present untransformed data. Use
a corresponding `applyTransform` function to access transformed data instead.
 -/
Lean.Language.TransformedSnap.raw : {α : Type} → Lean.Language.TransformedSnap α → α
-- Init.Data.UInt.Lemmas
UInt64.neg_neg : ∀ {a : UInt64}, - -a = a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k}, (cmp (t.insertIfNew k v).minKey! k).isLE = true
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_eq_equivFun : ∀ {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 ι] (m : M) (i : ι),
  (b.toDual m) (b i) = b.equivFun m i
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_ones : ∀ {n : ℕ}, (Composition.ones n).reverse = Composition.ones n
-- Mathlib.Data.List.Nodup
List.Nodup.inter : ∀ {α : Type u} {l₁ : List α} [inst : BEq α] (l₂ : List α), l₁.Nodup → (l₁ ∩ l₂).Nodup
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.coe_div : ∀ {M : Type u_8} {N : Type u_9} [inst : One M] [inst_1 : DivisionMonoid N] (f g : OneHom M N), ⇑(f / g) = ⇑f / ⇑g
-- Mathlib.Data.Fintype.Card
Fintype.card_bool : Fintype.card Bool = 2
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
multiplication on `𝕜`, then it continuously acts on `WeakDual 𝕜 E`.  -/
WeakDual.instContinuousSMul : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (M : Type u_6) [inst_7 : Monoid M] [inst_8 : DistribMulAction M 𝕜] [inst_9 : SMulCommClass 𝕜 M 𝕜]
  [inst_10 : TopologicalSpace M] [inst_11 : ContinuousSMul M 𝕜], ContinuousSMul M (WeakDual 𝕜 E)
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.Projective S.X₂ →
        (CategoryTheory.HasProjectiveDimensionLT S.X₃ (n + 2) ↔ CategoryTheory.HasProjectiveDimensionLT S.X₁ (n + 1))
-- Mathlib.Algebra.Star.Basic
/-- When multiplication is commutative, `star` preserves division.  -/
star_div₀ : ∀ {R : Type u} [inst : CommGroupWithZero R] [inst_1 : StarMul R] (x y : R), star (x / y) = star x / star y
-- Mathlib.Combinatorics.Configuration
Configuration.ofField.mem_iff : ∀ {K : Type u_3} [inst : Field K] (v w : Projectivization K (Fin 3 → K)), v ∈ w ↔ v.orthogonal w
-- Mathlib.Data.Fin.FlagRange
Flag.mem_rangeFin : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {n : ℕ} {f : Fin (n + 1) → α} {x : α} {h0 : f 0 = ⊥}
  {hlast : f (Fin.last n) = ⊤} {hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ},
  x ∈ Flag.rangeFin f h0 hlast hcovBy ↔ ∃ k, f k = x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Coercion from `G' : Subgraph G` to a `SimpleGraph G'.verts`.  -/
SimpleGraph.Subgraph.coe : {V : Type u} → {G : SimpleGraph V} → (G' : G.Subgraph) → SimpleGraph ↑G'.verts