mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SuccPred.Tree
RootedTree.mk.sizeOf_spec : ∀ (α : Type u_2) [semilatticeInf : SemilatticeInf α] [orderBot : OrderBot α] [predOrder : PredOrder α]
  [isPredArchimedean : IsPredArchimedean α],
  sizeOf
      { α := α, semilatticeInf := semilatticeInf, orderBot := orderBot, predOrder := predOrder,
        isPredArchimedean := isPredArchimedean } =
    1 + sizeOf α + sizeOf semilatticeInf + sizeOf orderBot + sizeOf predOrder + sizeOf isPredArchimedean
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.isArithOfCastLike.go : Lean.Expr → Lean.Meta.Grind.Result✝
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.sup_mul_inf : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I J : Ideal A), (I ⊔ J) * (I ⊓ J) = I * J
-- Aesop.Util.Basic
Aesop.isAppOfUpToDefeq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ_nil : ∀ (m : ℕ), SimplexCategoryGenRel.standardσ [] ⋯ = CategoryTheory.CategoryStruct.id (SimplexCategoryGenRel.mk m)
-- Mathlib.Order.Concept
Concept.extent_top : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, ⊤.extent = Set.univ
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.coe_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N), ↑⊤ = ⊤
-- Mathlib.Algebra.Ring.NonZeroDivisors
isRegular_iff_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] {r : R}, IsRegular r ↔ r ∈ nonZeroDivisors R
-- Mathlib.Data.ULift
PLift.map_injective : ∀ {α : Sort u} {β : Sort v} {f : α → β}, Function.Injective (PLift.map f) ↔ Function.Injective f
-- Batteries.Data.Stream
Std.Stream.take_eq_takeTR : @Std.Stream.take = @Std.Stream.takeTR
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.BlockMem.coe_bot : ∀ (G : Type u_1) [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (a : X), ↑⊥ = {a}
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₂_hom_comp_i_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupHomology.cycles A 2)),
  (ModuleCat.Hom.hom (groupHomology.shortComplexH2 A).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₂ A).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.iCycles A 2)) x)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.inv_int_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (b : ℤ),
  (b != 0) = true → Lean.Grind.CommRing.denoteInt b * (Lean.Grind.CommRing.denoteInt b)⁻¹ = 1
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Icc_castLE : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Icc (Fin.castLE h i) (Fin.castLE h j) = Set.Icc i j
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mul_mem_cancel_left : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d e : C} {f : c ⟶ d}
  {g : d ⟶ e}, f ∈ S.arrows c d → (CategoryTheory.CategoryStruct.comp f g ∈ S.arrows c e ↔ g ∈ S.arrows d e)
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.le_of_add_le_add_left : ∀ {α : Type u_2} {inst : AddCommMonoid α} {inst_1 : Preorder α} [self : IsOrderedCancelAddMonoid α] (a b c : α),
  a + b ≤ a + c → b ≤ c
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeries.eq_2 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E),
  f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.CompleteEquipartiteSubgraph.mk.inj : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} {parts : Finset (Finset V)} {card_parts : parts.card = r ∨ t = 0}
  {card_mem_parts : ∀ {p : Finset V}, p ∈ parts → p.card = t}
  {isCompleteBetween : (↑parts).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2} {parts_1 : Finset (Finset V)}
  {card_parts_1 : parts_1.card = r ∨ t = 0} {card_mem_parts_1 : ∀ {p : Finset V}, p ∈ parts_1 → p.card = t}
  {isCompleteBetween_1 : (↑parts_1).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2},
  { parts := parts, card_parts := card_parts, card_mem_parts := card_mem_parts,
        isCompleteBetween := isCompleteBetween } =
      { parts := parts_1, card_parts := card_parts_1, card_mem_parts := card_mem_parts_1,
        isCompleteBetween := isCompleteBetween_1 } →
    parts = parts_1
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Submonoids of a monoid form a complete lattice.  -/
Submonoid.instCompleteLattice : {M : Type u_1} → [inst : MulOneClass M] → CompleteLattice (Submonoid M)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_comap : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (f : G ≃ₜ G),
  (∀ ⦃K : TopologicalSpace.Compacts G⦄, μ (TopologicalSpace.Compacts.map ⇑f ⋯ K) = μ K) →
    ∀ (U : TopologicalSpace.Opens G), μ.innerContent ((TopologicalSpace.Opens.comap ↑f) U) = μ.innerContent U
-- Mathlib.Data.Sum.Order
Sum.Lex.inr_le_inr_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : β}, toLex (Sum.inr a) ≤ toLex (Sum.inr b) ↔ a ≤ b
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- If `n % 4 = 3`, then `(-1)^(n/2) = -1`.  -/
ZMod.neg_one_pow_div_two_of_three_mod_four : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- If the source of a faithful functor has a subobject classifier, the functor reflects
isomorphisms. This holds for any balanced category.
 -/
CategoryTheory.HasSubobjectClassifier.reflectsIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.HasSubobjectClassifier C] (D : Type u₀)
  [inst_2 : CategoryTheory.Category.{v₀, u₀} D] (F : CategoryTheory.Functor C D) [F.Faithful], F.ReflectsIsomorphisms
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.smul.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α α_1 : R₀ ⟶ R.obj) (e_α : α = α_1)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ φ_1 : M₀.presheaf ⟶ A.obj) (e_φ : φ = φ_1)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (r r_1 : ↑(R.obj.obj X)),
  r = r_1 →
    ∀ (m m_1 : ↑(A.obj.obj X)),
      m = m_1 → PresheafOfModules.Sheafify.smul α φ r m = PresheafOfModules.Sheafify.smul α_1 φ_1 r_1 m_1
-- Mathlib.Probability.Distributions.Binomial
_private.Mathlib.Probability.Distributions.Binomial.0.ProbabilityTheory.variance_of_hasLaw_binomial : {Ω : Type u_2} →
  {m : MeasurableSpace Ω} →
    {P : MeasureTheory.Measure Ω} →
      {n : ℕ} →
        {p : ↑unitInterval} →
          {X : Ω → ℝ} →
            ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) P →
              ProofWanted (ProbabilityTheory.variance X P = ↑p * (1 - ↑p) * ↑n)
-- Mathlib.Order.Restriction
Preorder.restrictLe₂_comp_restrictLe : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} {a b : α} (hab : a ≤ b),
  Preorder.restrictLe₂ hab ∘ Preorder.restrictLe b = Preorder.restrictLe a
-- Mathlib.Topology.FiberBundle.Trivialization
/-- In the domain of a bundle trivialization, the projection is continuous  -/
Bundle.Trivialization.continuousAt_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z}, x ∈ e.source → ContinuousAt proj x
-- Init.Data.Option.Attach
Option.all_attach : ∀ {α : Type u_1} {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool},
  (∀ (x : α) (h : o = some x), q ⟨x, h⟩ = p x) → Option.all q o.attach = Option.all p o
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff! m₂).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.comm : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} {inst_2 : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6}
  {inst_3 : AddCommMonoid M} {inst_4 : CategoryTheory.HasShift C₁ M} {inst_5 : CategoryTheory.HasShift C₂ M}
  {inst_6 : CategoryTheory.HasShift D M} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  (h : CategoryTheory.CommShift₂Setup D M) [self : G.CommShift₂ h] (X₁ : C₁) (X₂ : C₂) (m n : M),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso (G.obj ((CategoryTheory.shiftFunctor C₁ m).obj X₁)) n).hom.app X₂)
      ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso (G.flip.obj X₂) m).hom.app X₁)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso (G.flip.obj ((CategoryTheory.shiftFunctor C₂ n).obj X₂)) m).hom.app X₁)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D m).map ((CategoryTheory.Functor.commShiftIso (G.obj X₁) n).hom.app X₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm ((G.obj X₁).obj X₂) m n).inv
          ((↑(h.ε m n)).app
            ((CategoryTheory.shiftFunctor D n).obj ((CategoryTheory.shiftFunctor D m).obj ((G.obj X₁).obj X₂))))))
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.stalkToFiber_germ : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.LocalPredicate T) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U)
  (f : (fun X => X) ((TopCat.subsheafToTypes P).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (TopCat.stalkToFiber P x))
      ((CategoryTheory.ConcreteCategory.hom ((TopCat.subsheafToTypes P).presheaf.germ U x hx)) f) =
    ↑f ⟨x, hx⟩
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabAnonymousCtor : Lean.Elab.Term.TermElab
-- Mathlib.Analysis.Convex.Strict
strictConvex_Ioc : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β), StrictConvex 𝕜 (Set.Ioc r s)
-- Mathlib.NumberTheory.LSeries.Deriv
/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then the L-series
of `f` is differentiable with derivative the negative of the L-series of the point-wise
product of `log` with `f`.  -/
LSeries_hasDerivAt : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeries.abscissaOfAbsConv f < ↑s.re → HasDerivAt (LSeries f) (-LSeries (LSeries.logMul f) s) s
-- Init.Data.UInt.Lemmas
UInt16.toNat_toBitVec : ∀ (x : UInt16), x.toBitVec.toNat = x.toNat
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.send : {α : Type} → Std.Bounded✝ α → α → BaseIO (Task (Except Std.Broadcast.Error ℕ))
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.instInhabitedAlt.default : Lean.Elab.Tactic.ElimApp.Alt
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.inductiveVal : Lean.Meta.Cases.Context → Lean.InductiveVal
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.algebraMap_ringEquiv_symm_apply : ∀ (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hA : IsGaloisGroup G A B]
  [inst_5 : FaithfulSMul A B] [inst_6 : CommSemiring A'] [inst_7 : Algebra A' B] [inst_8 : FaithfulSMul A' B]
  [hA' : IsGaloisGroup G A' B] (x : A'),
  (algebraMap A B) ((IsGaloisGroup.ringEquiv G A A' B).symm x) = (algebraMap A' B) x
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.Top.adjDecidable : (V : Type u_2) → DecidableRel ⊤.Adj
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.finrank : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) [StrongRankCondition R], Module.finrank R S = f.natDegree
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- We say that an equivalence of categories `E` is triangulated if both `E.functor` and
`E.inverse` are triangulated functors.
 -/
CategoryTheory.Equivalence.IsTriangulated : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.Limits.HasZeroObject D] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : CategoryTheory.Preadditive D] →
                [inst_6 : CategoryTheory.HasShift C ℤ] →
                  [inst_7 : CategoryTheory.HasShift D ℤ] →
                    [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                      [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                        [CategoryTheory.Pretriangulated C] →
                          [CategoryTheory.Pretriangulated D] →
                            (E : C ≌ D) → [E.functor.CommShift ℤ] → [E.inverse.CommShift ℤ] → Prop
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.sigmaMap : ∀ {ι : Type u_6} {κ : Type u_7} {X : ι → Type u_8} {Y : κ → Type u_9} [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : (i : κ) → TopologicalSpace (Y i)] {f : ι → κ},
  Function.Bijective f → ∀ {g : (i : ι) → X i → Y (f i)}, (∀ (i : ι), IsHomeomorph (g i)) → IsHomeomorph (Sigma.map f g)
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricMeasure_real_singleton : ∀ {p : ↑unitInterval}, p ≠ 0 → ∀ (n : ℕ), (ProbabilityTheory.geometricMeasure p).real {n} = (1 - ↑p) ^ n * ↑p
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_update : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R) (x : M →₀ R),
  MonoidAlgebra.ofCoeff (x.update m r) = MonoidAlgebra.update m r (MonoidAlgebra.ofCoeff x)
-- Mathlib.Data.List.Sublists
List.sublists_reverse : ∀ {α : Type u} (l : List α), l.reverse.sublists = List.map List.reverse l.sublists'
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.symm_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.symm.P = P.P
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instCoeMonCat.eq_1 : GrpCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ GrpCat MonCat).obj }
-- Mathlib.RingTheory.QuasiFinite.Polynomial
/-- `R[X]` is not quasi-finite over `R` at any prime.  -/
Polynomial.not_quasiFiniteAt : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) [inst_1 : P.IsPrime], ¬Algebra.QuasiFiniteAt R P
-- Mathlib.SetTheory.ZFC.Basic
/-- An abbrev of `ZFSet.Definable` for unary functions.  -/
ZFSet.Definable₁ : (ZFSet.{u} → ZFSet.{u}) → Type (u + 1)
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.isDefEq : Lean.Elab.Structural.IndGroupInst → Lean.Elab.Structural.IndGroupInst → Lean.MetaM Bool
-- Lean.Parser.Term
Lean.Parser.Term.local.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Bases
Topology.IsInducing.secondCountableTopology : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : TopologicalSpace β]
  [SecondCountableTopology β], Topology.IsInducing f → SecondCountableTopology α
-- Mathlib.Topology.ContinuousMap.Compact
/-- When `α` is compact and `𝕜` is a normed field,
the `𝕜`-algebra of bounded continuous maps `α →ᵇ β` is
`𝕜`-linearly isometric to `C(α, β)`.
 -/
ContinuousMap.linearIsometryBoundedOfCompact : (α : Type u_1) →
  (E : Type u_3) →
    [inst : TopologicalSpace α] →
      [inst_1 : CompactSpace α] →
        [inst_2 : SeminormedAddCommGroup E] →
          (𝕜 : Type u_4) →
            [inst_3 : NormedRing 𝕜] →
              [inst_4 : Module 𝕜 E] → [inst_5 : IsBoundedSMul 𝕜 E] → C(α, E) ≃ₗᵢ[𝕜] BoundedContinuousFunction α E
-- Mathlib.Algebra.Opposites
AddOpposite.instUnique.eq_1 : ∀ {α : Type u_1} [inst : Unique α], AddOpposite.instUnique = Unique.mk' αᵃᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : LinearOrder J} {inst_2 : OrderBot J}
  {X Y : C} {f : X ⟶ Y} {inst_3 : SuccOrder J} {inst_4 : WellFoundedLT J} {F : CategoryTheory.Functor J C}
  {isoBot : F.obj ⊥ ≅ X}
  {isWellOrderContinuous :
    autoParam F.IsWellOrderContinuous CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous._autoParam}
  {incl : F ⟶ (CategoryTheory.Functor.const J).obj Y}
  {isColimit : CategoryTheory.Limits.IsColimit { pt := Y, ι := incl }}
  {fac :
    autoParam (CategoryTheory.CategoryStruct.comp isoBot.inv (incl.app ⊥) = f)
      CategoryTheory.TransfiniteCompositionOfShape.fac._autoParam}
  {F_1 : CategoryTheory.Functor J C} {isoBot_1 : F_1.obj ⊥ ≅ X}
  {isWellOrderContinuous_1 :
    autoParam F_1.IsWellOrderContinuous CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous._autoParam}
  {incl_1 : F_1 ⟶ (CategoryTheory.Functor.const J).obj Y}
  {isColimit_1 : CategoryTheory.Limits.IsColimit { pt := Y, ι := incl_1 }}
  {fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp isoBot_1.inv (incl_1.app ⊥) = f)
      CategoryTheory.TransfiniteCompositionOfShape.fac._autoParam},
  { F := F, isoBot := isoBot, isWellOrderContinuous := isWellOrderContinuous, incl := incl, isColimit := isColimit,
        fac := fac } =
      { F := F_1, isoBot := isoBot_1, isWellOrderContinuous := isWellOrderContinuous_1, incl := incl_1,
        isColimit := isColimit_1, fac := fac_1 } →
    F = F_1 ∧ isoBot ≍ isoBot_1 ∧ incl ≍ incl_1 ∧ isColimit ≍ isColimit_1
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- Tilde of `R` as an `R`-module is isomorphic to the structure sheaf `𝒪_{Spec R}`.  -/
AlgebraicGeometry.tildeSelf : {R : CommRingCat} →
  AlgebraicGeometry.tilde (ModuleCat.of ↑R ↑R) ≅ SheafOfModules.unit (AlgebraicGeometry.Spec R).ringCatSheaf
-- Mathlib.Algebra.Order.Monoid.PNat
PNat.equivNonZeroDivisorsNat_symm_apply_coe : ∀ (x : ↥(nonZeroDivisors ℕ)), ↑(PNat.equivNonZeroDivisorsNat.symm x) = ↑x
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_dvd_true : ∀ {a b a' b' : ℕ}, Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.mod a' = 0 → a ∣ b
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toCols₂_fromCols : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R),
  (A₁.fromCols A₂).toCols₂ = A₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldl_eq_foldl_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} [inst : Std.TransCmp cmp]
  {f : δ → α → β → δ} {init : δ}, Std.ExtTreeMap.foldl f init t = List.foldl (fun a b => f a b.1 b.2) init t.toList
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.liftKaehlerDifferential_comp_D : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D' : Derivation R S M) (x : S), D'.liftKaehlerDifferential ((KaehlerDifferential.D R S) x) = D' x
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polarSubmodule_eq_polar : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] (m : SubMulAction 𝕜 E),
  ↑(StrongDual.polarSubmodule 𝕜 m) = StrongDual.polar 𝕜 ↑m
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.mul_assoc_rev : ∀ {R : Type u_1} [sR : CommSemiring R] (a b c : R), a * (b * c) = a * b * c
-- Mathlib.RingTheory.Ideal.Basic
Ideal.mem_pi : ∀ {ι : Type u_1} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] (I : (i : ι) → Ideal (R i)) (r : (i : ι) → R i),
  r ∈ Ideal.pi I ↔ ∀ (i : ι), r i ∈ I i
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.instInhabitedAlt : {a : Type} → [Inhabited a] → Inhabited (Lean.Elab.Term.Do.Alt a)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.mopRingEquivOp_symm_apply : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R) (a : ↥S.op),
  S.mopRingEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)
-- ProofWidgets.Cancellable
ProofWidgets.CancellableTask.cancel : ProofWidgets.CancellableTask → IO Unit
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
addition/subtraction of `x : P`.  -/
IsometryEquiv.vaddConst : {V : Type u_2} →
  {P : Type u_3} →
    [inst : SeminormedAddCommGroup V] → [inst_1 : PseudoMetricSpace P] → [NormedAddTorsor V P] → P → V ≃ᵢ P
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isFiltered_of_isCardinalFiltered : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ], CategoryTheory.IsFiltered J
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.sup_not_iff_top : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n), T.Iff (φ ⊔ φ.not) ⊤