mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_mono : ∀ {G : Type u_1} [inst : AddGroup G] {s t : Set G}, s ⊆ t → AddSubgroup.normalClosure s ≤ AddSubgroup.normalClosure t
-- Mathlib.Order.Filter.Map
Filter.comap_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Function.Injective (Filter.comap f)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.id : IsEllipticNet id
-- Mathlib.Order.KrullDimension
Order.krullDim_ne_top_of_finiteDimensionalOrder : ∀ {α : Type u_1} [inst : Preorder α] [FiniteDimensionalOrder α], Order.krullDim α ≠ ⊤
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.minView!.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l' r' with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') =
    h_2 size k' v' l' r'
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a : α}, (↑m).isEmpty = true → m.getKey? a = none
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.Mon C) → (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).LaxMonoidal
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_le_iff_of_lt_aleph0 : ∀ {c c' : Cardinal.{u}}, c' < Cardinal.aleph0 → (Cardinal.toENat c ≤ Cardinal.toENat c' ↔ c ≤ c')
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.mem_ofStabilizer_iff : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (a : α) {x : α},
  x ∈ SubAddAction.ofStabilizer G a ↔ x ≠ a
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofAlgEquiv_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T),
  (P.ofAlgEquiv e).val = ⇑e ∘ P.val
-- Init.Data.SInt.Lemmas
Int64.toInt16_toISize : ∀ (n : Int64), n.toISize.toInt16 = n.toInt16
-- Mathlib.Data.DFinsupp.BigOperators
/-- The `DFinsupp` version of `Finsupp.liftAddHom`  -/
DFinsupp.liftAddHom : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → AddZeroClass (β i)] →
          [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) ≃+ ((Π₀ (i : ι), β i) →+ γ)
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.mulAntidiagonal_min_mul_min : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty),
  Finset.mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The canonical map `F.left ⟶ F.right` for `F : ComposableArrows C n`.  -/
CategoryTheory.ComposableArrows.hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {n : ℕ} → (F : CategoryTheory.ComposableArrows C n) → F.left ⟶ F.right
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.polynomialX_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R},
  W'.polynomialX =
    MvPolynomial.C W'.a₁ * MvPolynomial.X 1 * MvPolynomial.X 2 -
      (MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 +
        MvPolynomial.C W'.a₄ * MvPolynomial.X 2 ^ 4)
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Construct a `Cert rα` from a ring tactic result  -/
Mathlib.Tactic.Determinant.toCert : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      {e : Q(«$α»)} →
        Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Determinant.CertVal rα) e → Mathlib.Tactic.Determinant.Cert rα
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.fix : Turing.ToPartrec.Code → Turing.ToPartrec.Code
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {M N : CategoryTheory.Comonad C}
  {toNatTrans : CategoryTheory.NatTrans M.toFunctor N.toFunctor}
  {app_ε :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.ε.app X) = M.ε.app X)
      CategoryTheory.ComonadHom.app_ε._autoParam}
  {app_δ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.δ.app X) =
          CategoryTheory.CategoryStruct.comp (M.δ.app X)
            (CategoryTheory.CategoryStruct.comp (toNatTrans.app (M.obj X)) (N.map (toNatTrans.app X))))
      CategoryTheory.ComonadHom.app_δ._autoParam}
  {toNatTrans_1 : CategoryTheory.NatTrans M.toFunctor N.toFunctor}
  {app_ε_1 :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans_1.app X) (N.ε.app X) = M.ε.app X)
      CategoryTheory.ComonadHom.app_ε._autoParam}
  {app_δ_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toNatTrans_1.app X) (N.δ.app X) =
          CategoryTheory.CategoryStruct.comp (M.δ.app X)
            (CategoryTheory.CategoryStruct.comp (toNatTrans_1.app (M.obj X)) (N.map (toNatTrans_1.app X))))
      CategoryTheory.ComonadHom.app_δ._autoParam},
  { toNatTrans := toNatTrans, app_ε := app_ε, app_δ := app_δ } =
      { toNatTrans := toNatTrans_1, app_ε := app_ε_1, app_δ := app_δ_1 } →
    toNatTrans = toNatTrans_1
-- Init.Data.Float.Float
instBEqFloat : BEq Float
-- Mathlib.Probability.UniformOn
/-- See `uniformOn_eq_zero` for a version assuming `MeasurableSingletonClass Ω` instead of
`MeasurableSet s`.  -/
ProbabilityTheory.uniformOn_eq_zero' : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {s : Set Ω},
  MeasurableSet s → (ProbabilityTheory.uniformOn s = 0 ↔ s.Infinite ∨ s = ∅)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_right : ∀ {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin n), Fin.append u v (Fin.natAdd m i) = v i
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedCommMonoid.toUniqueUnits.eq_1 : ∀ {α : Type u} [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedMul α],
  CanonicallyOrderedCommMonoid.toUniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.instLargeCategory : CategoryTheory.LargeCategory SemiNormedGrp
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of seminormed groups, using the sup norm.  -/
Prod.seminormedCommGroup : {E : Type u_2} → {F : Type u_3} → [SeminormedCommGroup E] → [SeminormedCommGroup F] → SeminormedCommGroup (E × F)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.apply_coe_mem_map : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {L : BooleanSubalgebra α}
  (f : BoundedLatticeHom α β) (a : ↥L), f ↑a ∈ BooleanSubalgebra.map f L
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Integral of a simple function whose codomain is `ℝ≥0∞`.  -/
MeasureTheory.SimpleFunc.lintegral : {α : Type u_1} → {_m : MeasurableSpace α} → MeasureTheory.SimpleFunc α ENNReal → MeasureTheory.Measure α → ENNReal
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.map_restrict : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  {F G : TopCat.Presheaf C X} (e : F ⟶ G) {U V : TopologicalSpace.Opens ↑X} (h : U ≤ V)
  (x : CategoryTheory.ToType (F.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (e.app (Opposite.op U))) (TopCat.Presheaf.restrictOpen x U h) =
    TopCat.Presheaf.restrictOpen ((CategoryTheory.ConcreteCategory.hom (e.app (Opposite.op V))) x) U h
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_eq : ∀ (a b : UInt64), a.toUInt32 = b.toUInt32 ↔ a % 4294967296 = b % 4294967296
-- Mathlib.Analysis.PSeries
/-- for series of nonnegative real numbers.  -/
summable_schlomilch_iff_of_nonneg : ∀ {C : ℕ} {u : ℕ → ℕ} {f : ℕ → ℝ},
  (∀ (n : ℕ), 0 ≤ f n) →
    (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) →
      (∀ (n : ℕ), 0 < u n) →
        StrictMono u →
          C ≠ 0 → SuccDiffBounded C u → ((Summable fun k => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f)
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termK : Lean.ParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_xor : ∀ {w : ℕ} {x y : BitVec w} {start len : ℕ},
  BitVec.extractLsb' start len (x ^^^ y) = BitVec.extractLsb' start len x ^^^ BitVec.extractLsb' start len y
-- Mathlib.Order.KrullDimension
Order.krullDim_ne_bot_iff : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α ≠ ⊥ ↔ Nonempty α
-- Init.Data.UInt.Bitwise
UInt64.xor_eq_zero_iff : ∀ {a b : UInt64}, a ^^^ b = 0 ↔ a = b
-- Init.Data.SInt.Lemmas
Int64.toInt16_ofIntClamp : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toInt16 = Int16.ofInt n
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.cons.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (m m_1 : M i) (e_m : m = m_1)
  (w w_1 : Monoid.CoprodI.Word M) (e_w : w = w_1) (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1),
  Monoid.CoprodI.Word.cons m w hmw h1 = Monoid.CoprodI.Word.cons m_1 w_1 ⋯ ⋯
-- Lean.Attributes
Lean.ParametricAttributeImpl.mk.inj : ∀ {α : Type} {toAttributeImplCore : Lean.AttributeImplCore} {getParam : Lean.Name → Lean.Syntax → Lean.AttrM α}
  {afterSet : Lean.Name → α → Lean.AttrM Unit} {preserveOrder : Bool}
  {filterExport : Lean.Environment → Lean.Name → α → Bool} {toAttributeImplCore_1 : Lean.AttributeImplCore}
  {getParam_1 : Lean.Name → Lean.Syntax → Lean.AttrM α} {afterSet_1 : Lean.Name → α → Lean.AttrM Unit}
  {preserveOrder_1 : Bool} {filterExport_1 : Lean.Environment → Lean.Name → α → Bool},
  { toAttributeImplCore := toAttributeImplCore, getParam := getParam, afterSet := afterSet,
        preserveOrder := preserveOrder, filterExport := filterExport } =
      { toAttributeImplCore := toAttributeImplCore_1, getParam := getParam_1, afterSet := afterSet_1,
        preserveOrder := preserveOrder_1, filterExport := filterExport_1 } →
    toAttributeImplCore = toAttributeImplCore_1 ∧
      getParam = getParam_1 ∧ afterSet = afterSet_1 ∧ preserveOrder = preserveOrder_1 ∧ filterExport = filterExport_1
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_mk : ∀ {α : Type u_1} {L₁ : List (α × Bool)} [inst : DecidableEq α], (FreeGroup.mk L₁).toWord = FreeGroup.reduce L₁
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.nodup_toList : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] {a b : α}, (a<...=b).toList.Nodup
-- Init.Data.Nat.Lemmas
Nat.div_div_div_eq_div : ∀ {a b c : ℕ}, b ∣ a → a ∣ c → c / (a / b) / b = c / a
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (property : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out property
-- Mathlib.Order.WithBot
WithBot.map₂_coe_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β), WithBot.map₂ f ↑a ↑b = ↑(f a b)
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- An equality of prefunctors gives an equality on objects.  -/
Prefunctor.congr_obj : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] {F G : U ⥤q V},
  F = G → ∀ (X : U), F.obj X = G.obj X
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mkRingHom_C : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  (DividedPowerAlgebra.ringCon R M).mk' (MvPolynomial.C a) = (algebraMap R (DividedPowerAlgebra R M)) a
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_natAddEmb_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.natAddEmb m) (Finset.Icc i j) = Finset.Icc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The actual `Submonoid` obtained from an element of a `SubmonoidClass`  -/
Submonoid.ofClass : {S : Type u_3} → {M : Type u_4} → [inst : Monoid M] → [inst_1 : SetLike S M] → [SubmonoidClass S M] → S → Submonoid M
-- Lean.Parser.Basic
Lean.Parser.node : Lean.SyntaxNodeKind → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Analysis.Complex.Harmonic.Analytic
InnerProductSpace.HarmonicOnNhd.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f f_1 : E → F),
  f = f_1 → ∀ (s s_1 : Set E), s = s_1 → InnerProductSpace.HarmonicOnNhd f s = InnerProductSpace.HarmonicOnNhd f_1 s_1
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsSFiniteKernel.sFinite : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] (a : α), MeasureTheory.SFinite (κ a)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom : {J : Type u_1} → {a a_1 : CategoryTheory.Limits.WidePushoutShape J} → [DecidableEq J] → DecidableEq (a.Hom a_1)
-- Mathlib.CategoryTheory.Sites.Canonical
/-- If every functor `yoneda.obj X` is a `J`-sheaf, then `J` is subcanonical.  -/
CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  (∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) → J.Subcanonical
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_c_ne_zero' : ∀ {R : Type u_1} {c d : R} [inst : Semiring R], c ≠ 0 → { a := 0, b := 0, c := c, d := d }.toPoly.degree = 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.Hom.hom_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X], CategoryTheory.InducedCategory.Hom.hom 0 = 0
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.mapBaseChange.congr_simp : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B],
  KaehlerDifferential.mapBaseChange R A B = KaehlerDifferential.mapBaseChange R A B
-- Init.Data.Nat.Bitwise.Lemmas
/-- Depending on use cases either `testBit_add_one` or `testBit_div_two`
may be more useful as a `simp` lemma, so neither is a global `simp` lemma.
 -/
Nat.testBit_add_one : ∀ (x i : ℕ), x.testBit (i + 1) = (x / 2).testBit i
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- Symmetric projections are equal iff their range are.  -/
LinearMap.IsSymmetricProjection.ext_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {S T : E →ₗ[𝕜] E}, S.IsSymmetricProjection → T.IsSymmetricProjection → (S = T ↔ S.range = T.range)
-- Lean.InternalExceptionId
/-- Internal exceptions registered in the system.  -/
Lean.internalExceptionsRef : IO.Ref (Array Lean.Name)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The adjunction between the 2-truncated homotopy category functor
and the 2-truncated nerve functor.  -/
SSet.Truncated.nerve₂Adj : SSet.Truncated.hoFunctor₂ ⊣ CategoryTheory.Nerve.nerveFunctor₂
-- Mathlib.Data.Finset.Image
Finset.map_eq_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α ↪ β) (s : Finset α), Finset.map f s = Finset.image (⇑f) s
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisorsRight_eq_left : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀], nonZeroDivisorsRight M₀ = nonZeroDivisorsLeft M₀
-- Mathlib.Order.Part
Monotone.partMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] {f : β → γ} {g : α → Part β},
  Monotone g → Monotone fun x => Part.map f (g x)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instAdd.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupSeminorm.instAdd =
    { add := fun p q => { toFun := fun x => p x + q x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S]
  [inst_4 : Mul S'] [inst_5 : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is
the obvious functor `w.CostructuredArrowDownwards g ⥤ w.StructuredArrowRightwards g`.  -/
CategoryTheory.TwoSquare.EquivalenceJ.inverse : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₂ : C₂} →
                            {X₃ : C₃} →
                              (g : R.obj X₂ ⟶ B.obj X₃) →
                                CategoryTheory.Functor (w.CostructuredArrowDownwards g) (w.StructuredArrowRightwards g)
-- Mathlib.Data.Finset.NAry
Finset.sup'_image₂_le : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeSup δ] {g : γ → δ} {a : δ} (h : (Finset.image₂ f s t).Nonempty),
  (Finset.image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Methods.mk.sizeOf_spec : ∀ (initLB initUB : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr))
  (proveLE proveLT : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr)
  (roundUp roundDown : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr)
  (eval : Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)) (mkNumeral : ℤ → Lean.MetaM Lean.Expr),
  sizeOf
      { initLB := initLB, initUB := initUB, proveLE := proveLE, proveLT := proveLT, roundUp := roundUp,
        roundDown := roundDown, eval := eval, mkNumeral := mkNumeral } =
    1
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.val_mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x : ↥P.ker), (Algebra.Extension.Cotangent.mk x).val = P.ker.toCotangent x
-- Mathlib.Topology.Algebra.MulAction
Subgroup.continuousSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : Group M]
  [inst_3 : MulAction M X] [ContinuousSMul M X] {S : Subgroup M}, ContinuousSMul (↥S) X
-- Mathlib.Topology.Irreducible
/-- An infinite type with cofinite topology is an irreducible topological space.  -/
instIrreducibleSpaceCofiniteTopologyOfInfinite : ∀ {X : Type u_3} [Infinite X], IrreducibleSpace (CofiniteTopology X)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.comp.inj : ∀ {a a_1 a_2 a_3 : Nat.Partrec.Code}, a.comp a_1 = a_2.comp a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Meta.Closure
Lean.Meta.Closure.Context.mk.inj : ∀ {zetaDelta zetaDelta_1 : Bool}, { zetaDelta := zetaDelta } = { zetaDelta := zetaDelta_1 } → zetaDelta = zetaDelta_1
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.IsBadSeq.eq_1 : ∀ {α : Type u_2} (r : α → α → Prop) (s : Set α) (f : ℕ → α),
  Set.PartiallyWellOrderedOn.IsBadSeq r s f = ((∀ (n : ℕ), f n ∈ s) ∧ ∀ (m n : ℕ), m < n → ¬r (f m) (f n))
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_top : ∀ {X : AlgebraicGeometry.Scheme}, ⊤.toSpecΓ = CategoryTheory.CategoryStruct.comp ⊤.ι X.toSpecΓ
-- Mathlib.Algebra.Group.Prod
MonoidHom.coe_prodMap : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N'), ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_inf : ∀ {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Finsubgraph), ↑(G₁ ⊓ G₂) = ↑G₁ ⊓ ↑G₂
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_obj : ∀ (X : CategoryTheory.Cat) (X_1 : ↑X),
  (CategoryTheory.Cat.opFunctorInvolutive.inv.app X).toFunctor.obj X_1 = Opposite.op (Opposite.op X_1)
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The `SMulCon` underlying an `ModuleCon`.  -/
ModuleCon.toSMulCon : {S : Type u_2} → {M : Type u_3} → [inst : Add M] → [inst_1 : SMul S M] → ModuleCon S M → SMulCon S M
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {S₁ : CategoryTheory.ShortComplex C} {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_2 : S.HasLeftHomology] (φ : S ⟶ S₁)
  [inst_3 : S₁.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) (CategoryTheory.ShortComplex.cyclesMap φ) =
    S₁.liftCycles (CategoryTheory.CategoryStruct.comp k φ.τ₂) ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α), Std.Internal.List.getEntry? a [] = none
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Taking injective resolutions is functorial,
if considered with target the homotopy category
(`ℕ`-indexed cochain complexes and cochain maps up to homotopy).
 -/
CategoryTheory.injectiveResolutions : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.HasInjectiveResolutions C] → CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.up ℕ))
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The matrix `T = [[1, 1], [0, 1]]` as an element of `SL(2, ℤ)`.  -/
ModularGroup.T : Matrix.SpecialLinearGroup (Fin 2) ℤ
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_toENNReal_add : ∀ (r : ENNReal) (n : ℕ∞), ⌈↑n + r⌉ₑ = n + ⌈r⌉ₑ