mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option (β a) → Option (β a)},
      (Std.DHashMap.Internal.toListModel (↑(m.alter a f)).buckets).Perm
        (Std.Internal.List.alterKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.lt_succ_iff_not_isMax`. -/
Order.lt_succ_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → a < Order.succ a
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Ico : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} [ClosedIciTopology α], MeasurableSet (Set.Ico a b)
-- Lean.Compiler.IR.Basic
/-- Variable identifier  -/
Lean.IR.VarId : Type
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.ext : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  {φ₁ φ₂ : (PiTensorProduct R fun i => s i) →ₗ[R] E},
  φ₁.compMultilinearMap (PiTensorProduct.tprod R) = φ₂.compMultilinearMap (PiTensorProduct.tprod R) → φ₁ = φ₂
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability in the left endpoint.

If `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `a`, then `u ↦ ∫ x in u..b, f x` has
derivative `-f a` at `a` in the sense of strict differentiability.  -/
intervalIntegral.integral_hasStrictDerivAt_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      ContinuousAt f a → HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_zero : ∀ {𝕜 : 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] {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 0 s x
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
cmp_mul_pos_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a : R} [MulPosStrictMono R],
  0 < a → ∀ (b c : R), cmp (b * a) (c * a) = cmp b c
-- Mathlib.Analysis.CStarAlgebra.Basic
NormedStarGroup.mk : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E],
  (∀ (x : E), ‖star x‖ ≤ ‖x‖) → NormedStarGroup E
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_add_left : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : Add α] [inst_1 : Add γ] (f : α → β → γ),
  (∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b) →
    ∀ (A₁ A₂ : Matrix l m α) (B : Matrix n p β),
      Matrix.kroneckerMap f (A₁ + A₂) B = Matrix.kroneckerMap f A₁ B + Matrix.kroneckerMap f A₂ B
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- If `f` is eventually differentiable along a nontrivial filter `l : Filter ℝ` that is generated
by convex sets, the norm of `f` tends to infinity along `l`, and `f' = O(g)` along `l`, where `f'`
is the derivative of `f`, then `g` is not integrable on any set `k` belonging to `l`.
Auxiliary version assuming that `E` is complete.  -/
not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [CompleteSpace E] {f : ℝ → E} {g : ℝ → F} {k : Set ℝ} (l : Filter ℝ) [l.NeBot] [Filter.TendstoIxxClass Set.Icc l l],
  k ∈ l →
    (∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) →
      Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop →
        deriv f =O[l] g → ¬MeasureTheory.IntegrableOn g k MeasureTheory.volume
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Quiver.Hom.id_toLoc : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (a : C),
  (CategoryTheory.CategoryStruct.id a).toLoc = CategoryTheory.CategoryStruct.id { as := a }
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationLineMapWeights.eq_1 : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] (i j : ι) (c : k),
  Finset.affineCombinationLineMapWeights i j c = c • Finset.weightedVSubVSubWeights k j i + Pi.single i 1
-- Mathlib.Data.Part
Part.some_get : ∀ {α : Type u_1} {a : Part α} (ha : a.Dom), Part.some (a.get ha) = a
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.add_right_cancel_of_ne_top : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R]
  {x y z : ArchimedeanClass R}, x ≠ ⊤ → y + x = z + x → y = z
-- Init.Data.Vector.Lemmas
Vector.getElem_of_mem : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, a ∈ xs → ∃ i, ∃ (h : i < n), xs[i] = a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast_lt_size_of_lt_aig_size : ∀ {w x : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig),
  x < aig.decls.size → x < (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig.decls.size
-- Mathlib.Topology.Algebra.Support
mulTSupport_comp_subset : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : One α] [inst_1 : TopologicalSpace X] [inst_2 : One β]
  {g : α → β}, g 1 = 1 → ∀ (f : X → α), mulTSupport (g ∘ f) ⊆ mulTSupport f
-- Mathlib.Control.Monad.Cont
ContT.instLawfulMonad : ∀ {r : Type u} {m : Type u → Type v}, LawfulMonad (ContT r m)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtOrthonormalBasis_det : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E)
  [inst_8 : DecidableEq ι],
  (InnerProductSpace.gramSchmidtOrthonormalBasis h f).toBasis.det f =
    ∏ i, inner 𝕜 ((InnerProductSpace.gramSchmidtOrthonormalBasis h f) i) (f i)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set of differentiability points of a function, with derivative in a given complete set,
is Borel-measurable.  -/
measurableSet_of_differentiableAt_of_isComplete : ∀ (𝕜 : 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)
  [inst_5 : MeasurableSpace E] [OpensMeasurableSpace E] {K : Set (E →L[𝕜] F)},
  IsComplete K → MeasurableSet {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
-- Init.Prelude
/-- The notation typeclass for heterogeneous exponentiation.
This enables the notation `a ^ b : γ` where `a : α`, `b : β`.
 -/
HPow : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.GroupTheory.Congruence.Defs
/-- Two additive congruence relations are equal iff their underlying binary relations
are equal.  -/
AddCon.coe_inj : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, ⇑c = ⇑d ↔ c = d
-- Mathlib.Combinatorics.Colex
Finset.Colex.ofColex_top : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Fintype α], ofColex ⊤ = Finset.univ
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.antidiagonal_mono_left`. -/
Finset.addAntidiagonal_mono_left : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO},
  u ⊆ s → Finset.antidiagonal hu ht a ⊆ Finset.antidiagonal hs ht a
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonShowMessageResponse : Lean.FromJson Lean.Lsp.ShowMessageResponse
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- The range of a ring homomorphism from a local ring as a `LocalSubring`.  -/
LocalSubring.range : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] → [inst_1 : CommRing S] → [IsLocalRing R] → [Nontrivial S] → (R →+* S) → LocalSubring S
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) {i j : K} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F i).inv
      ((CategoryTheory.Limits.colimit F).map f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f)))
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F j).inv
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
AddMonoidHom.compLeftContinuousBounded.eq_1 : ∀ {β : Type v} {γ : Type w} (α : Type u_3) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : AddMonoid β] [inst_3 : BoundedAdd β] [inst_4 : ContinuousAdd β] [inst_5 : PseudoMetricSpace γ]
  [inst_6 : AddMonoid γ] [inst_7 : BoundedAdd γ] [inst_8 : ContinuousAdd γ] (g : β →+ γ) {C : NNReal}
  (hg : LipschitzWith C ⇑g),
  AddMonoidHom.compLeftContinuousBounded α g hg =
    { toFun := fun f => BoundedContinuousFunction.comp (⇑g) hg f, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceToList : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.EReal.Inv
EReal.inv_strictAntiOn : StrictAntiOn (fun x => x⁻¹) (Set.Ioi 0)
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → derivWithin f (Set.Iio x) x ≤ 0 → 0 ≤ derivWithin f (Set.Ioi x) x → IsMinOn f S x
-- Mathlib.CategoryTheory.Endomorphism
/-- In a groupoid, endomorphisms form a group  -/
CategoryTheory.End.group : {C : Type u} → [inst : CategoryTheory.Groupoid C] → (X : C) → Group (CategoryTheory.End X)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_inj : ∀ {w : ℕ} {x y : BitVec w}, x.toFin = y.toFin ↔ x = y
-- Mathlib.Algebra.Group.Equiv.Basic
/-- An additive analogue of `Equiv.arrowCongr`,
where the equivalence between the targets is additive.  -/
AddEquiv.arrowCongr : {M : Type u_16} →
  {N : Type u_17} →
    {P : Type u_18} → {Q : Type u_19} → [inst : Add P] → [inst_1 : Add Q] → M ≃ N → P ≃+ Q → (M → P) ≃+ (N → Q)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation S hkf hcc fac).right =
    CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp_map_right : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)}
  (φ : X ⟶ Y), ((CategoryTheory.Functor.LeftExtension.precomp L F G).map φ).right = φ.right
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.unreach : {pu : Lean.Compiler.LCNF.Purity} → Lean.Expr → Lean.Compiler.LCNF.Code pu
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instMulActionOfSMulCommClass.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X]
  [inst_1 : SMul N Y] [inst_2 : Monoid R] [inst_3 : MulAction R Y] [inst_4 : SMulCommClass N R Y],
  MulActionHom.instMulActionOfSMulCommClass =
    { toSMul := MulActionHom.instSMulOfSMulCommClass, mul_smul := ⋯, one_smul := ⋯ }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.forIn'_eq_match : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [DecidableLE α] [inst_2 : LT α] [DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxi.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_9 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    have hle := ⋯;
    do
    let __do_lift ← f r.lower hle init
    match __do_lift with
      | ForInStep.yield c => forIn' r.lower<...* c fun a ha acc => f a ⋯ acc
      | ForInStep.done c => pure c
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t : CategoryTheory.Limits.Cone K}
  (P : CategoryTheory.Limits.IsLimit (CategoryTheory.WithTerminal.coneEquiv.functor.obj t))
  (s : CategoryTheory.Limits.Cone K),
  ((CategoryTheory.WithTerminal.isLimitEquiv P).lift s).left =
    ((CategoryTheory.Limits.IsLimit.ofRightAdjoint CategoryTheory.WithTerminal.coneEquiv.toAdjunction P).lift s).left
-- Mathlib.CategoryTheory.Monoidal.Opposite
Quiver.Hom.unmop_mop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}, f.mop.unmop = f
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.ext : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)},
  (∀ (a : X), f a = g a) → f = g
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instLieRing : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieRing (LieDerivation R L L)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
/-- The canonical map from the (global) sections of a sheaf of modules
to the (global) sections of its pushforward.  -/
SheafOfModules.pushforwardSections : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      {M : SheafOfModules R} → M.sections → ((SheafOfModules.pushforward φ).obj M).sections
-- Mathlib.Data.Part
/-- `Part α` is (classically) equivalent to `Option α`.  -/
Part.equivOption : {α : Type u_1} → Part α ≃ Option α
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.isMaximal_of_primeHeight_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [inst_1 : I.IsPrime] [FiniteRingKrullDim R],
  ↑(Ideal.primeHeight✝ I) = ringKrullDim R → I.IsMaximal
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.comp_left_iff_of_isEquivalence : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor C' C) [G.IsEquivalence], (G.comp F).IsDense ↔ F.IsDense
-- Lean.Elab.Match
/-- The inverse of `packMatchTypePatterns`.  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.unpackMatchTypePatterns : Lean.Expr → Lean.Expr × Array Lean.Expr
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
edist_le_ofReal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {r : ℝ}, 0 ≤ r → (edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r)
-- Mathlib.Order.PropInstances
Prop.codisjoint_iff : ∀ {P Q : Prop}, Codisjoint P Q ↔ P ∨ Q
-- Mathlib.Data.Nat.Choose.Sum
Nat.sum_range_choose_halfway : ∀ (m : ℕ), ∑ i ∈ Finset.range (m + 1), (2 * m + 1).choose i = 4 ^ m
-- Init.Data.List.Nat.TakeDrop
List.lt_length_left_of_zip : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {l : List α} {l' : List β}, i < (l.zip l').length → i < l.length
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Additivity of a continuous multilinear map along all coordinates at the same time,
writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`.  -/
ContinuousMultilinearMap.map_add_univ : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] [inst_8 : Fintype ι] (m m' : (i : ι) → M₁ i),
  f (m + m') = ∑ s, f (s.piecewise m m')
-- Init.Data.Range.Polymorphic.Iterators
Std.Rcc.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LE α] →
        [inst_2 : DecidableLE α] →
          [Std.PRange.LawfulUpwardEnumerable α] →
            [Std.PRange.LawfulUpwardEnumerableLE α] →
              [Monad m] → [Std.Iterators.Finite (Std.Rxc.Iterator α) Id] → ForIn' m (Std.Rcc α) α inferInstance
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).Q = CategoryTheory.Limits.cokernel S.f
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.decode_encode : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (s : Sym (Option α) n.succ),
  SymOptionSuccEquiv.decode (SymOptionSuccEquiv.encode s) = s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.of_discrete : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{v_2, u_3} C] {ι : Type u_6}
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} (α : F ⟶ G), CategoryTheory.NatTrans.Equifibered α
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_congr_fun_ae : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f g : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  f =ᵐ[μ.restrict s] g → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn g s μ)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.ext_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j)
      CategoryTheory.Limits.Cocone.ext._auto_1),
  (CategoryTheory.Limits.Cocone.ext φ w).inv.hom = φ.inv
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMapCompIso_inv_app : ∀ {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [inst : Quiver V₁] [inst_1 : Quiver V₂] [inst_2 : Quiver V₃]
  (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) (X : CategoryTheory.Paths V₁),
  (CategoryTheory.Cat.freeMapCompIso F G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj (F.obj X))
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIocMod_symm_apply : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α) (x : ↑(Set.Ioc a (a + p))), (QuotientAddGroup.equivIocMod hp a).symm x = ↑↑x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DHashMap.Raw.Const.get! (m₁.diff m₂) k = if k ∈ m₂ then default else Std.DHashMap.Raw.Const.get! m₁ k
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Composition of multilinear maps. If `g` is multilinear, and if for every `i : ι`, we have a
multilinear map `f i` with index type `β i`, then `m ↦ g (f₁ m_11 m_12 ...) (f₂ m_21 m_22 ...) ...`
is multilinear with index type `(Σ i, β i)`.  -/
MultilinearMap.compMultilinearMap : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  {β : ι → Type u_1} →
                    {N : (i : ι) → β i → Type u_2} →
                      [inst_5 : (i : ι) → (b : β i) → AddCommMonoid (N i b)] →
                        [inst_6 : (i : ι) → (b : β i) → Module R (N i b)] →
                          MultilinearMap R M₁ M₂ →
                            ((i : ι) → MultilinearMap R (N i) (M₁ i)) → MultilinearMap R (fun j => N j.fst j.snd) M₂
-- Mathlib.Data.Set.MemPartition
memPartitionSet_succ : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ) (a : α) [inst : Decidable (a ∈ f n)],
  memPartitionSet f (n + 1) a = if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
-- Init.Data.Ord.Basic
Ordering.ne_lt_iff_isGE : ∀ {o : Ordering}, ¬o = Ordering.lt ↔ o.isGE = true
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.ofNatTrans.inj : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D} {toNatTrans toNatTrans_1 : F.toFunctor ⟶ G.toFunctor},
  { toNatTrans := toNatTrans } = { toNatTrans := toNatTrans_1 } → toNatTrans = toNatTrans_1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.lit.inj : ∀ {v v_1 : Lean.Literal}, Lean.Meta.RefinedDiscrTree.Key.lit v = Lean.Meta.RefinedDiscrTree.Key.lit v_1 → v = v_1
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.extendedHom_eq_one_iff`. -/
FractionalIdeal.extendedHomₐ_eq_one_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A]
  [IsDedekindDomain B], I ≠ 0 → ((FractionalIdeal.extendedHom L B) I = 1 ↔ I = 1)