mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyMap_comp_eq_zero_of_distTriang : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)),
  DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ (n : ℤ),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₁ n)
          (HomologicalComplex.homologyMap T.mor₂ n) =
        0
-- Lean.Meta.Sym.Pattern
/-- Mark pattern variable `i` for type checking. That is, at the end of phase 1
we must check whether the type of this pattern variable is compatible with the type of
the value assigned to it.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.pushCheckTypePending : ℕ → Lean.Meta.Sym.UnifyM✝ Unit
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableEqSpan : DecidableEq Std.Time.Nanosecond.Span
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Number of variables for which `PowIdentity` equations have been pushed.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.powIdentityVarCount : Lean.Meta.Grind.Arith.CommRing.CommRing → ℕ
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_cast : ∀ {w v i : ℕ} (h : w = v) (x : BitVec w), (BitVec.cast h x).getLsbD i = x.getLsbD i
-- Std.Internal.UV.UDP
/-- Represents a UDP socket.
 -/
Std.Internal.UV.UDP.Socket : Type
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_mul_base : ∀ {a b : ℝ}, a ≠ 0 → b ≠ 0 → ∀ (c : ℝ), Real.logb (a * b) c = ((Real.logb a c)⁻¹ + (Real.logb b c)⁻¹)⁻¹
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.sup_nonemptyCompacts : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  {f g : α → TopologicalSpace.NonemptyCompacts β},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x ⊔ g x
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If a group satisfies the universal property of a free group with respect to a given type, then
it admits a free group basis based on this type. Here, the universal property is expressed as
in `IsFreeGroup.lift` and its properties.  -/
FreeGroupBasis.ofLift : {G : Type u} →
  [inst : Group G] →
    (X : Type u) →
      (of : X → G) →
        (lift : {H : Type u} → [inst_1 : Group H] → (X → H) ≃ (G →* H)) →
          (∀ {H : Type u} [inst_1 : Group H] (f : X → H) (a : X), (lift f) (of a) = f a) → FreeGroupBasis X G
-- Lean.Meta.ArgsPacker
Lean.Meta.ArgsPacker.uncurryWithType : Lean.Meta.ArgsPacker → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk'_toSquare : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C)
  [inst_2 : CategoryTheory.Mono sq.f₁₃] (H : ∀ (F : CategoryTheory.Sheaf J (Type v)), (sq.op.map F.obj).IsPullback),
  (CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' sq H).toSquare = sq
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_lt_tsum : ∀ {α : Type u_1} {f g : α → ENNReal} {i : α},
  tsum f ≠ ⊤ → (∀ (a : α), f a ≤ g a) → f i < g i → ∑' (x : α), f x < ∑' (x : α), g x
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- Constructor for objects of the homotopy category of a `2`-truncated simplicial set.  -/
SSet.Truncated.HomotopyCategory.mk : {V : SSet.Truncated 2} →
  V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }) → V.HomotopyCategory
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- To give a refinement of the disjoint union, it suffices to give refinements of both
components.  -/
CategoryTheory.PreZeroHypercover.sumLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} →
          {G : CategoryTheory.PreZeroHypercover S} → E.Hom G → F.Hom G → (E.sum F).Hom G
-- Mathlib.Topology.Connected.PathConnected
Submonoid.pathComponentOne.eq_1 : ∀ (M : Type u_4) [inst : Monoid M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousMul M],
  Submonoid.pathComponentOne M = { carrier := pathComponent 1, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_lt_iff_tsub_lt : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → c ≤ a → (a - b < c ↔ a - c < b)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_inter_lt_top_of_right_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, μ t ≠ ⊤ → μ (s ∩ t) < ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α} {v : β}, (cmp t.maxKey! (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.eq_4 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f fs : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.zero' → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.succ → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.tail → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (c f fs : Turing.ToPartrec.Code) → c = f.cons fs → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (c f g : Turing.ToPartrec.Code) → c = f.comp g → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (c f g : Turing.ToPartrec.Code) → c = f.case g → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (c f : Turing.ToPartrec.Code) → c = f.fix → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.cons fs, k with
    | c@h:Turing.ToPartrec.Code.zero', k => h_1 c h k
    | c@h:Turing.ToPartrec.Code.succ, k => h_2 c h k
    | c@h:Turing.ToPartrec.Code.tail, k => h_3 c h k
    | c@h:(f.cons fs), k => h_4 c f fs h k
    | c@h:(f.comp g), k => h_5 c f g h k
    | c@h:(f.case g), k => h_6 c f g h k
    | c@h:f.fix, k => h_7 c f h k) =
    h_4 (f.cons fs) f fs ⋯ k
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd T.hom g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd T.hom g) h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_of_isEmpty : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t.isEmpty = true → Std.DTreeMap.Internal.Impl.Const.get! t a = default
-- Mathlib.Algebra.Ring.Parity
even_add_two : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Even (a + 2) ↔ Even a
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- Group-like elements over a domain are linearly independent.  -/
linearIndepOn_isGroupLikeElem : ∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup A] [inst_3 : Module R A]
  [inst_4 : Coalgebra R A] [Module.IsTorsionFree R A], LinearIndepOn R id {a | IsGroupLikeElem R a}
-- Lean.Parser.Attr
/-- Adds one or more tags to a tactic.

Tags should be applied to the canonical names for tactics.
 -/
Lean.Parser.Attr.tactic_tag : Lean.Parser.Parser
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?_of_some : ∀ {α : Type u_1} {cut : α → Ordering} {y : α} {t : RBTree.RBNode α},
  ∃ x, RBTree.RBNode.upperBound? cut t (some y) = some x
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_union_le_size_add_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.eq_def : ∀ (e : Lean.Expr) (offset : ℕ) (f : Lean.Expr → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM (Option Lean.Expr)),
  Lean.Meta.Sym.visitChild✝ e offset f =
    have key := ({ expr := e }, offset);
    do
    let __do_lift ← get
    match __do_lift[key]? with
      | some r => pure r
      | x => do
        let __do_lift ← liftM (f e offset)
        match __do_lift with
          | some r => Lean.Meta.Sym.save✝ key r
          | x =>
            match e with
            | Lean.Expr.lit a => Lean.Meta.Sym.save✝ key e
            | Lean.Expr.mvar mvarId => Lean.Meta.Sym.save✝ key e
            | Lean.Expr.bvar deBruijnIndex => Lean.Meta.Sym.save✝ key e
            | Lean.Expr.fvar fvarId => Lean.Meta.Sym.save✝ key e
            | Lean.Expr.const declName us => Lean.Meta.Sym.save✝ key e
            | Lean.Expr.sort u => Lean.Meta.Sym.save✝ key e
            | e => do
              let __do_lift ← Lean.Meta.Sym.visit✝ e offset f
              Lean.Meta.Sym.save✝ key __do_lift
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_of_assemble₃_eq_some_left : ∀ {w x y : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₃ w x y = some c → ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = false
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ)
  (acc xc : aig.RefVec w) (idx : ℕ)
  (h1 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig xc curr acc).aig.decls.size)
  (h2 : idx < aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig xc curr acc).aig.decls[idx] = aig.decls[idx]
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.post_forget_eq_forget_comp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (X : T),
  (CategoryTheory.Over.post F).comp (CategoryTheory.Over.forget (F.obj X)) = (CategoryTheory.Over.forget X).comp F
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.mk.injEq : ∀ (item : Lean.Lsp.CallHierarchyItem) (fromRanges : Array Lean.Lsp.Range) (children : Array Lean.Lsp.Ipc.CallHierarchy)
  (item_1 : Lean.Lsp.CallHierarchyItem) (fromRanges_1 : Array Lean.Lsp.Range)
  (children_1 : Array Lean.Lsp.Ipc.CallHierarchy),
  ({ item := item, fromRanges := fromRanges, children := children } =
      { item := item_1, fromRanges := fromRanges_1, children := children_1 }) =
    (item = item_1 ∧ fromRanges = fromRanges_1 ∧ children = children_1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressParams : Type
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.measureSpace : {α : Type u_4} →
  {β : Type u_5} → [MeasureTheory.MeasureSpace α] → [MeasureTheory.MeasureSpace β] → MeasureTheory.MeasureSpace (α × β)
-- Mathlib.Data.Multiset.AddSub
/-- **Alias** of the forward direction of `Multiset.add_le_add_iff_right`. -/
Multiset.le_of_add_le_add_right : ∀ {α : Type u_1} {s t u : Multiset α}, s + u ≤ t + u → s ≤ t
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {c d : E → 𝔸'},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      DifferentiableWithinAt 𝕜 d s x →
        fderivWithin 𝕜 (fun y => c y * d y) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData) {Z : C} (h_1 : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.rightHomologyIso.hom (CategoryTheory.CategoryStruct.comp h.homologyIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp S.rightHomologyIso.hom h_1
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_Lp_of_measure_ne_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [inst : NormedAddCommGroup E]
  {p : ENNReal} {s : Set α} (f : ↥(MeasureTheory.Lp E p μ)), 1 ≤ p → μ s ≠ ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.algHom_ext : ∀ {R : Type u_1} {S : Type u_2} (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra.EssFiniteType R S] (f g : S →ₐ[R] T),
  (∀ s ∈ Algebra.EssFiniteType.finset R S, f s = g s) → f = g
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The isomorphisms `Functor.CommShift.isoZero F` and `Functor.CommShift.isoZero G` are
compatible with the unit of an adjunction `F ⊣ G`.
 -/
CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoZero : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A],
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj (CategoryTheory.Functor.CommShift.isoZero F A)
    (CategoryTheory.Functor.CommShift.isoZero G A)
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_bot : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  [inst_3 : FaithfulSMul M X], ↑⊥ = 0
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
_private.Lean.Meta.Tactic.Grind.MarkNestedSubsingletons.0.Lean.Meta.Grind.M : Type → Type
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindPattern.elabProp : Array Lean.Expr → Lean.Syntax → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- The counit iso in the equivalence of sheaf categories.  -/
CategoryTheory.Equivalence.sheafCongr.counitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    (CategoryTheory.Equivalence.sheafCongr.inverse J K e A).comp
                        (CategoryTheory.Equivalence.sheafCongr.functor J K e A) ≅
                      CategoryTheory.Functor.id (CategoryTheory.Sheaf K A)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
the push-forward of finite measures `f* : FiniteMeasure X → FiniteMeasure Y` is continuous
(in the topologies of weak convergence of measures).  -/
MeasureTheory.FiniteMeasure.continuous_map : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] [inst_2 : TopologicalSpace Ω]
  [inst_3 : OpensMeasurableSpace Ω] [inst_4 : TopologicalSpace Ω'] [inst_5 : BorelSpace Ω'] {f : Ω → Ω'},
  Continuous f → Continuous fun ν => ν.map f
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_tProd_mk : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (i : δ) → MeasurableSpace (X i)] (l : List δ), Measurable (List.TProd.mk l)
-- Mathlib.Data.Set.Prod
Set.Nonempty.prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty
-- Std.Sat.AIG.Basic
Std.Sat.AIG.BinaryInput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {lhs rhs lhs_1 rhs_1 : aig.Ref},
  { lhs := lhs, rhs := rhs } = { lhs := lhs_1, rhs := rhs_1 } → lhs = lhs_1 ∧ rhs = rhs_1
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.bind.eq_1 : ∀ {m : Type w → Type w'} [inst : Monad m] {α β : Type w} (x : Std.Iterators.PostconditionT m α)
  (f : α → Std.Iterators.PostconditionT m β),
  x.bind f =
    { Property := fun b => ∃ a, x.Property a ∧ (f a).Property b,
      operation := do
        let a ← x.operation
        (fun b => ⟨↑b, ⋯⟩) <$> (f ↑a).operation }
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_add_of_right_mem : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [inst_4 : AddRightCancelMonoid ι] [inst_5 : GradedRing 𝒜]
  {a b : A}, b ∈ 𝒜 j → ↑(((DirectSum.decompose 𝒜) (a * b)) (i + j)) = ↑(((DirectSum.decompose 𝒜) a) i) * b
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.nonempty_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [ZeroLEOneClass k] {n : ℕ} (s : Affine.Simplex k P n),
  s.closedInterior.Nonempty
-- Init.Core
dif_neg : ∀ {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α}, dite c t e = e hnc
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.mk.injEq : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (inv : SSet.Edge x₁ x₀)
  (homInvId : hom.CompStruct inv (SSet.Edge.id x₀)) (invHomId : inv.CompStruct hom (SSet.Edge.id x₁))
  (inv_1 : SSet.Edge x₁ x₀) (homInvId_1 : hom.CompStruct inv_1 (SSet.Edge.id x₀))
  (invHomId_1 : inv_1.CompStruct hom (SSet.Edge.id x₁)),
  ({ inv := inv, homInvId := homInvId, invHomId := invHomId } =
      { inv := inv_1, homInvId := homInvId_1, invHomId := invHomId_1 }) =
    (inv = inv_1 ∧ homInvId ≍ homInvId_1 ∧ invHomId ≍ invHomId_1)
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.lt_or_eq` -/
LE.le.ssubset_or_eq : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a ⊂ b ∨ a = b
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.inhabited : {Γ : Type u_1} → [inst : Inhabited Γ] → Inhabited (Turing.ListBlank Γ)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMulAction : {M : Type u_1} →
  {X : Type u_2} →
    [inst : Monoid M] →
      [inst_1 : MulAction M X] →
        [inst_2 : TopologicalSpace X] → [ContinuousConstSMul M X] → MulAction M (SeparationQuotient X)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.open_target : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (self : PartialDiffeomorph I J M N n),
  IsOpen self.target
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_negAddY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).negAddY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)
-- Mathlib.LinearAlgebra.LinearPMap
Submodule.toLinearPMap_apply_aux : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0)
  (x : ↥(Submodule.map (LinearMap.fst R E F) g)), ↑g.toLinearPMap x = Submodule.valFromGraph hg ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.get! (Std.DTreeMap.filterMap f t) k = ((Std.DTreeMap.Const.get? t k).bind (f k')).get!
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- The value of the Infimum of a set of outer measures on a nonempty set is not simply
the minimum value of a measure on that set: it is the infimum sum of measures of countable set of
sets that covers that set, where a different measure can be used for each set in the cover.  -/
MeasureTheory.OuterMeasure.sInf_apply' : ∀ {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α},
  s.Nonempty → (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)
-- Mathlib.CategoryTheory.Limits.Types.End
/-- The end of a bifunctor valued in `Type`, defined as the subtype of compatible families.  -/
CategoryTheory.Limits.Types.end_ : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u))) → Type (max w u)
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.modEq_iff_toIocMod_eq_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₂_ext : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.coboundaries₂ A)}, (∀ (g h : G), f₁ (g, h) = f₂ (g, h)) → f₁ = f₂
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instCoeOutIdeal : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → CoeOut hI.SubDPIdeal (Ideal A)
-- Init.Data.Option.Lemmas
Option.ne_none_iff_exists' : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ x, o = some x
-- Std.Time.DateTime
_private.Std.Time.DateTime.0.Std.Time.DateTime.mk.inj : ∀ {date : Thunk Std.Time.PlainDateTime} {timestamp : Std.Time.Timestamp} {rules : Std.Time.TimeZone.ZoneRules}
  {timezone : Std.Time.TimeZone} {date_1 : Thunk Std.Time.PlainDateTime} {timestamp_1 : Std.Time.Timestamp}
  {rules_1 : Std.Time.TimeZone.ZoneRules} {timezone_1 : Std.Time.TimeZone},
  { date := date, timestamp := timestamp, rules := rules, timezone := timezone } =
      { date := date_1, timestamp := timestamp_1, rules := rules_1, timezone := timezone_1 } →
    date = date_1 ∧ timestamp = timestamp_1 ∧ rules = rules_1 ∧ timezone = timezone_1
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.ofNat_mul_aleph0 : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n * Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.smul_mem_pointwise_smul_iff : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] {g : G}
  {S : ValuationSubring K} {x : K}, g • x ∈ g • S ↔ x ∈ S