mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1)
  (h_1 : Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_1 ⋯
-- Mathlib.RingTheory.Flat.Tensor
/-- Define the character module of `M` to be `M →+ ℚ ⧸ ℤ`.
The character module of `M` is an injective module if and only if
`f ⊗ 𝟙 M` is injective for any linear map `f` in the same universe as `M`.
 -/
Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Injective R (CharacterModule M) ↔
    ∀ ⦃N N' : Type v⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N] [inst_6 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.mk.injEq : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} (val val_1 : Fin n → Polynomial R),
  ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.Data.Multiset.Find
/-- `s.find? p ⋯` finds the subsingleton element of `s` satisfying the condition `p`, if one exists.

This is the multiset version of `List.find?`,
and is like `Multiset.choose`, but `Option`-valued.  -/
Multiset.find? : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → (s : Multiset α) → {x | x ∈ s ∧ p x}.Subsingleton → Option α
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.isUnit_toStalkₗ' : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (f : R),
  x ∈ PrimeSpectrum.basicOpen f →
    IsUnit ((algebraMap R (Module.End R ↑((AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x))) f)
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.Offset.ofSeconds.inj : ∀ {second second_1 : Std.Time.Second.Offset}, { second := second } = { second := second_1 } → second = second_1
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.instHaveLebesgueDecompositionZeroRight : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.HaveLebesgueDecomposition 0
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.GradedNatTrans.mk.sizeOf_spec : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} [inst_4 : SizeOf V] [inst_5 : SizeOf C]
  [inst_6 : SizeOf D] (app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X)
  (naturality :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y))
            (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y))
          (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_add_iff_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b c : α},
  a + b ≤ a + c ↔ b ≤ c
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_countablyGeneratedAtom : ∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace.CountablyGenerated α] (p : ℕ → Prop),
  MeasurableSet (MeasurableSpace.countablyGeneratedAtom α p)
-- Mathlib.ModelTheory.PartialEquiv
/-- The substructure which is the codomain of the equivalence.  -/
FirstOrder.Language.PartialEquiv.cod : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.PartialEquiv M N → L.Substructure N
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_ne_zero : ∀ {a : Ordinal.{u_1}} (b : Ordinal.{u_1}), a ≠ 0 → a ^ b ≠ 0
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_right_Icc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => x + c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.exists_ne_zero_of_sSup_eq : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {N : Submodule R M} {f : ↥N →ₛₗ[σ₁₂] M₂},
  f ≠ 0 → ∀ (s : Set (Submodule R M)) (hs : sSup s = N), ∃ m, ∃ (h : m ∈ s), f ∘ₛₗ Submodule.inclusion ⋯ ≠ 0
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instIterator.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_ne_of_natDegree_ne : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≠ n → p.degree ≠ ↑n
-- Lean.Parser.Extra
Lean.Parser.group.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Prelude
/-- A variation on `Classical.choice` that uses typeclass inference to
infer the proof of `Nonempty α`.
 -/
Classical.ofNonempty : {α : Sort u} → [Nonempty α] → α
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- This is a generic version which allows us to prove both
`NonUnitalSubalgebra.unitization_injective` and `NonUnitalStarSubalgebra.unitization_injective`.  -/
AlgHomClass.unitization_injective : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [inst : Field R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S),
  1 ∉ s →
    ∀ [inst_4 : FunLike F (Unitization R ↥s) A] [AlgHomClass F R (Unitization R ↥s) A] (f : F),
      (∀ (x : ↥s), f ↑x = ↑x) → Function.Injective ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst ∧
      CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.hasCoeToSort : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} D] →
      (F : C → D) →
        (P : CategoryTheory.MorphismProperty D) →
          [inst_1 : P.IsMultiplicative] →
            {α : Sort u_1} → [CoeSort D α] → CoeSort (CategoryTheory.InducedWideCategory D F P) α
-- Lean.Meta.Tactic.Grind.Types
/-- Case-split diagnostic information  -/
Lean.Meta.Grind.SplitDiagInfo : Type
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric
/-- `forget₂ (QuadraticModuleCat R) (ModuleCat R)` is a braided functor.  -/
QuadraticModuleCat.instBraidedModuleCatForget₂IsometryCarrierFormLinearMapId : {R : Type u} →
  [inst : CommRing R] → [inst_1 : Invertible 2] → (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).Braided
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst' : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {b : PowerSeries S},
  PowerSeries.HasSubst b →
    ∀ (f : PowerSeries R) (e : ℕ),
      (PowerSeries.coeff e) (PowerSeries.subst b f) =
        ∑ᶠ (d : ℕ), (PowerSeries.coeff d) f • (PowerSeries.coeff e) (b ^ d)
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (entries : Array (α × β)) (indexes : Std.HashMap α (Array ℕ))
  (validity :
    ∀ (k : α) (p : k ∈ indexes),
      let idx := indexes.get k p;
      idx.size > 0 ∧ ∀ i ∈ idx, i < entries.size),
  sizeOf { entries := entries, indexes := indexes, validity := validity } = 1 + sizeOf entries + sizeOf indexes
-- Mathlib.ModelTheory.Syntax
/-- A theory is a set of sentences.  -/
FirstOrder.Language.Theory : FirstOrder.Language → Type (max u v)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
csInf_Icc : ∀ {α : Type u_5} [inst : ConditionallyCompletePartialOrderInf α] {a b : α}, a ≤ b → sInf (Set.Icc a b) = a
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.instBEqCheckResult : BEq Lean.Meta.Grind.CheckResult
-- Mathlib.Order.Hom.Lattice
InfHom.dual_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : InfHom α β) (a : α), (InfHom.dual f) a = f a
-- Mathlib.LinearAlgebra.Dimension.Localization
exists_set_linearIndependent_of_isDomain : ∀ (R : Type uR) (M : Type uM) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R],
  ∃ s, Cardinal.mk ↑s = Module.rank R M ∧ LinearIndepOn R id s
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- If `‖x + y‖ = ‖x‖ + ‖y‖` implies that `x y : E` are in the same ray, then `E` is a strictly
convex space. See also a more  -/
StrictConvexSpace.of_norm_add : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y) → StrictConvexSpace ℝ E
-- Std.Http.Data.Status
Std.Http.Status.internalServerError.sizeOf_spec : sizeOf Std.Http.Status.internalServerError = 1
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_add : ∀ {ι : Sort u_1} {a : ENNReal} [Nonempty ι] (f : ι → ENNReal), (⨆ i, f i) + a = ⨆ i, f i + a
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainTermGoal : Lean.ToJson Lean.Lsp.PlainTermGoal
-- Mathlib.Order.Hom.Lattice
InfHom.instTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : Top β],
  InfHom.instTop = { top := InfHom.const α ⊤ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_filter : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f : ι → M), ∑ a ∈ s with p a, f a = ∑ a ∈ s, if p a then f a else 0
-- Init.Data.Array.Lemmas
Array.append_push : ∀ {α : Type u_1} {xs ys : Array α} {a : α}, xs ++ ys.push a = (xs ++ ys).push a
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Given a morphism in `CofibrantObject C`, this is a choice of morphism
(well defined only up to homotopy) between the chosen bifibrant resolutions.  -/
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X₁ X₂ : HomotopicalAlgebra.CofibrantObject C} →
        (X₁ ⟶ X₂) → (X₁.bifibrantResolutionObj ⟶ X₂.bifibrantResolutionObj)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.ε e.inverse))
      (CategoryTheory.CategoryStruct.comp (e.counitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η e.functor) h
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_4.eq : ∀ {motive_1 : Lean.Language.SnapshotTree → Sort u}
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u}
  {motive_5 : Task Lean.Language.SnapshotTree → Sort u} (t : Task Lean.Language.SnapshotTree)
  (F_1 : (t : Lean.Language.SnapshotTree) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_3 t → motive_4 t)
  (F_5 : (t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t),
  Lean.Language.SnapshotTree.brecOn_4 t F_1 F_2 F_3 F_4 F_5 =
    F_5 t (Lean.Language.SnapshotTree.brecOn_4.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toPosMulStrictMono : ∀ {α : Type u_3} [self : LinearOrderedCommMonoidWithZero α], PosMulStrictMono α
-- Mathlib.Tactic.DepRewrite
/-- Analogue of `kabstract` with support for inserting casts.  -/
Mathlib.Tactic.DepRewrite.dabstract : Lean.Expr → Lean.Expr → Mathlib.Tactic.DepRewrite.Config → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.neg_left : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T} (α : u ⟶ v), CategoryTheory.Arrow.Hom.left (-α) = -CategoryTheory.Arrow.Hom.left α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by inclusion of the second factor.  -/
ContinuousMonoidHom.inr : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → B →ₜ* A × B
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Injective.addActionHom_embedding_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Function.Injective ⇑f)
  {x : ι ↪ α} {i : ι}, ((Function.Injective.addActionHom_embedding ι hf) x) i = f (x i)
-- Mathlib.Util.Superscript
/-- Formatter for the subscript parser.  -/
Mathlib.Tactic.subscript.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.mk.inj : ∀ {ref modifiers : Lean.Syntax} {fieldId : Lean.Name} {type : Lean.Term}
  {matchAlts : Lean.TSyntax `Lean.Parser.Term.matchAlts} {ref_1 modifiers_1 : Lean.Syntax} {fieldId_1 : Lean.Name}
  {type_1 : Lean.Term} {matchAlts_1 : Lean.TSyntax `Lean.Parser.Term.matchAlts},
  { ref := ref, modifiers := modifiers, fieldId := fieldId, type := type, matchAlts := matchAlts } =
      { ref := ref_1, modifiers := modifiers_1, fieldId := fieldId_1, type := type_1, matchAlts := matchAlts_1 } →
    ref = ref_1 ∧ modifiers = modifiers_1 ∧ fieldId = fieldId_1 ∧ type = type_1 ∧ matchAlts = matchAlts_1
-- Mathlib.LinearAlgebra.Trace
LinearMap.IsProj.trace : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  {f : M →ₗ[R] M},
  LinearMap.IsProj p f →
    ∀ [Module.Free R ↥p] [Module.Finite R ↥p] [Module.Free R ↥f.ker] [Module.Finite R ↥f.ker],
      (LinearMap.trace R M) f = ↑(Module.finrank R ↥p)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagations.propagate.go : Lean.Meta.Grind.PendingSolverPropagationsData✝ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Dynamics.Flow
Flow.orbit_eq_range : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) (x : α), ϕ.orbit x = Set.range fun t => ϕ.toFun t x
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_iff_ofReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ᵐ[μ] f → (MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤)
-- Lean.Data.Trie
Lean.Data.Trie.brecOn_1.eq : ∀ {α : Type} {motive_1 : Lean.Data.Trie α → Sort u} {motive_2 : Array (Lean.Data.Trie α) → Sort u}
  {motive_3 : List (Lean.Data.Trie α) → Sort u} (t : Array (Lean.Data.Trie α))
  (F_1 : (t : Lean.Data.Trie α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Data.Trie α)) → Lean.Data.Trie.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Data.Trie α)) → Lean.Data.Trie.below_2 t → motive_3 t),
  Lean.Data.Trie.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Data.Trie.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instUniqueLMulticospanShapeSigmaOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        {c : CategoryTheory.Limits.Cofan E.X} →
          (hc : CategoryTheory.Limits.IsColimit c) →
            {d : CategoryTheory.Limits.Cofan E.Y'} →
              (hd : CategoryTheory.Limits.IsColimit d) → Unique (E.sigmaOfIsColimit hc hd).multicospanShape.L
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd : {R : Type u_1} → {A : Type u_2} → Unitization R A → R × A
-- Mathlib.Topology.Path
/-- `γ.truncate t₀ t₁` is the path which follows the path `γ` on the time interval `[t₀, t₁]`
and stays still otherwise.  -/
Path.truncate : {X : Type u_4} →
  [inst : TopologicalSpace X] → {a b : X} → (γ : Path a b) → (t₀ t₁ : ℝ) → Path (γ.extend (min t₀ t₁)) (γ.extend t₁)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_id_right_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.id (F.obj b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b)) h) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv h)
-- Init.Data.UInt.Lemmas
UInt64.neg_ne_zero : ∀ {a : UInt64}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_neg : ∀ (x : ℝ), Real.sinh (-x) = -Real.sinh x
-- Init.MethodSpecsSimp
Add.add_eq_hAdd : ∀ {α : Type u} [inst : Add α], Add.add = HAdd.hAdd
-- Mathlib.CategoryTheory.Subobject.FactorThru
/-- `P.factorThru f h` provides a factorisation of `f : X ⟶ Y` through some `P : MonoOver Y`,
given the evidence `h : P.Factors f` that such a factorisation exists.  -/
CategoryTheory.MonoOver.factorThru : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (P : CategoryTheory.MonoOver Y) → (f : X ⟶ Y) → P.Factors f → (X ⟶ P.obj.left)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The composition of monoid isomorphisms associated to equivalences of group extensions gives
another equivalence.  -/
GroupExtension.Equiv.trans : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : Group E'] →
                  {S' : GroupExtension N E' G} →
                    S.Equiv S' →
                      {E'' : Type u_5} →
                        [inst_4 : Group E''] → {S'' : GroupExtension N E'' G} → S'.Equiv S'' → S.Equiv S''
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumIndepSet.mk : ∀ {α : Type u_3} [inst : Finite α] {G : SimpleGraph α} {s : Finset α},
  G.IsIndepSet ↑s → (∀ (t : Finset α), G.IsIndepSet ↑t → t.card ≤ s.card) → G.IsMaximumIndepSet s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionList : Lean.FromJson Lean.Lsp.CompletionList
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_def : ∀ (p : Polynomial ℂ), p.logMahlerMeasure = Real.circleAverage (fun x => Real.log ‖Polynomial.eval x p‖) 0 1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.peek.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Option (Γ k) → σ)
  (a_1 : Turing.TM2.Stmt Γ Λ σ) (k_1 : K) (a_2 : σ → Option (Γ k_1) → σ) (a_3 : Turing.TM2.Stmt Γ Λ σ),
  (Turing.TM2.Stmt.peek k a a_1 = Turing.TM2.Stmt.peek k_1 a_2 a_3) = (k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3)
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toArray.isEmpty = m.isEmpty
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instFiniteExtension : ∀ (k : Type u_1) [inst : Field k] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP k p] (n : ℕ),
  Finite (FiniteField.Extension k p n)
-- Mathlib.RingTheory.Artinian.Algebra
/-- Integral element of an algebra over Artinian ring `R` is either a zero divisor or a unit.  -/
IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral' : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [IsArtinianRing R] [inst_2 : Ring A] [inst_3 : Algebra R A]
  [Algebra.IsIntegral R A] {a : A}, IsUnit a ↔ a ∈ nonZeroDivisors A
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.inverseFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : C ≌ D),
  (CategoryTheory.Equivalence.inverseFunctor C D).obj X = Opposite.op X.inverse
-- Mathlib.Data.FinEnum
FinEnum.card_pempty : FinEnum.card PEmpty.{u_1 + 1} = 0
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GSemiring.toGOne : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddMonoid ι} →
      {inst_1 : (i : ι) → AddCommMonoid (A i)} → [self : DirectSum.GSemiring A] → GradedMonoid.GOne A