mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.ForallProp
/-- Returns `true` if `thm?` is none or its patterns are different from the ones in `thm'`  -/
_private.Lean.Meta.Tactic.Grind.ForallProp.0.Lean.Meta.Grind.isNewPat : Array (List Lean.Expr) → Lean.Meta.Grind.EMatchTheorem → Bool
-- Mathlib.Analysis.Normed.Module.Complemented
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : CompleteSpace E] [inst_8 : CompleteSpace (F × G)]
  {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : (↑f).range = ⊤) (hg : (↑g).range = ⊤) (hfg : IsCompl (↑f).ker (↑g).ker) (x : E),
  (f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_div_lt_mk_left_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk (a / b) < MulArchimedeanClass.mk a ↔ MulArchimedeanClass.mk b < MulArchimedeanClass.mk a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF → ∀ {k k' : α} {f : β → β}, (Std.DHashMap.Internal.Raw₀.Const.modify m k f).contains k' = m.contains k'
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivAtFilter_const_add_iff`. -/
HasFDerivAtFilter.const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)} (c : F), HasFDerivAtFilter f f' L → HasFDerivAtFilter (fun x => c + f x) f' L
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuous.const_mul' : ∀ {R : Type u_1} {β : Type u_2} [inst : Ring R] [inst_1 : UniformSpace R] [inst_2 : UniformSpace β]
  [UniformContinuousConstSMul R R] {f : β → R}, UniformContinuous f → ∀ (a : R), UniformContinuous fun x => a * f x
-- Init.Data.List.Lemmas
List.ext_getElem? : ∀ {α : Type u_1} {l₁ l₂ : List α}, (∀ (i : ℕ), l₁[i]? = l₂[i]?) → l₁ = l₂
-- Mathlib.Data.Nat.Factorial.Basic
_private.Mathlib.Data.Nat.Factorial.Basic.0.Nat.factorial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.toCycles_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.toCycles (CategoryTheory.CategoryStruct.comp S.iCycles h) =
    CategoryTheory.CategoryStruct.comp S.f h
-- Mathlib.Order.PFilter
/-- Create an element of type `Order.PFilter` from a set satisfying the predicate
`Order.IsPFilter`.  -/
Order.IsPFilter.toPFilter : {P : Type u_1} → [inst : Preorder P] → {F : Set P} → Order.IsPFilter F → Order.PFilter P
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of a formal power series is exactly `n` if and only if some coefficient of weight `n`
is nonzero, and the `d`th coefficient is `0` for all `d` such that `weight w d < n`.  -/
MvPowerSeries.weightedOrder_eq_nat : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {n : ℕ},
  MvPowerSeries.weightedOrder w f = ↑n ↔
    (∃ d, (MvPowerSeries.coeff d) f ≠ 0 ∧ (Finsupp.weight w) d = n) ∧
      ∀ (d : σ →₀ ℕ), (Finsupp.weight w) d < n → (MvPowerSeries.coeff d) f = 0
-- Mathlib.Order.Interval.Set.Basic
/-- If `a < b`, then `(-∞, a) ⊂ (-∞, b)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Iio_ssubset_Iio_iff`.  -/
Set.Iio_ssubset_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → Set.Iio a ⊂ Set.Iio b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k k' : α}
  {v : β},
  t.WF →
    (Array.find? (fun a => compare a.1 k == Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toArray t) = some (k', v) ↔
      t.getKey? k = some k' ∧ Std.DTreeMap.Internal.Impl.Const.get? t k = some v)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_ne_zero_trans : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, H.relIndex K ≠ 0 → K.relIndex L ≠ 0 → H.relIndex L ≠ 0
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.shape.injEq : ∀ (k : List Lean.SyntaxNodeKind) (arity : Option ℕ) (k_1 : List Lean.SyntaxNodeKind) (arity_1 : Option ℕ),
  (Lean.Elab.Term.Quotation.HeadCheck.shape k arity = Lean.Elab.Term.Quotation.HeadCheck.shape k_1 arity_1) =
    (k = k_1 ∧ arity = arity_1)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The image by a functor which inverts `W` of an equivalence class of left fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {E : Type u_3} →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
          {X Y : C} →
            CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y →
              (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → (F.obj X ⟶ F.obj Y)
-- Mathlib.Topology.AlexandrovDiscrete
Topology.IsInducing.alexandrovDiscrete : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [AlexandrovDiscrete α]
  {f : β → α}, Topology.IsInducing f → AlexandrovDiscrete β
-- Mathlib.Data.Num.Basic
/-- Division of `ZNum`, where `x / 0 = 0`.  -/
ZNum.div : ZNum → ZNum → ZNum
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.get?_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α},
  Std.DHashMap.Raw.Const.get? m a = Std.DHashMap.Internal.Raw₀.Const.get? ⟨m, ⋯⟩ a
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.comm_trans_lid : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M = TensorProduct.rid R M
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
returning `none` if no such element exists.
 -/
Std.ExtTreeSet.getLT? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Option α
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaIsoYoneda_inv_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{max w v₁, u₁} C] (X : C) (X_1 : Cᵒᵖ),
  (CategoryTheory.uliftYonedaIsoYoneda.inv.app X).app X_1 = Equiv.ulift.toIso.inv
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- The maps between restricted products over a fixed index type,
given maps on the factors.  -/
RestrictedProduct.map : {ι : Type u_1} →
  {𝓕 : Filter ι} →
    {G : ι → Type u_9} →
      {H : ι → Type u_10} →
        {C : (i : ι) → Set (G i)} →
          {D : (i : ι) → Set (H i)} →
            (φ : (i : ι) → G i → H i) →
              (∀ᶠ (i : ι) in 𝓕, Set.MapsTo (φ i) (C i) (D i)) →
                RestrictedProduct (fun i => G i) (fun i => C i) 𝓕 → RestrictedProduct (fun i => H i) (fun i => D i) 𝓕
-- Mathlib.Order.Category.BddOrd
BddOrd.ext : ∀ {X Y : BddOrd} {f g : X ⟶ Y},
  (∀ (x : ↑X.toPartOrd), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Lean.Declaration
Lean.ConstantInfo.thmInfo : Lean.TheoremVal → Lean.ConstantInfo
-- Mathlib.Order.Interval.Multiset
Multiset.Ioo_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Multiset.Ioo a b = 0
-- Std.Do.SPred.DerivedLaws
/-- A decomposition of a stateful predicate into the conjunction of two other stateful predicates.

Decomposing assertions in postconditions into conjunctions of simpler predicates increases the
chance that automation will be able to prove the entailment of the postcondition and the next precondition.
 -/
Std.Do.SPred.Tactic.IsAnd : {σs : List (Type u)} → Std.Do.SPred σs → outParam (Std.Do.SPred σs) → outParam (Std.Do.SPred σs) → Prop
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp'.eq_1 : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R],
  finsuppTensorFinsupp' R ι κ = finsuppTensorFinsuppLid R R ι κ
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Function.Surjective ⇑h
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient
to check only injectivity instead of bijectivity of the bilinear pairing.  -/
LinearMap.IsPerfPair.of_injective' : ∀ {K : Type u_2} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Field K]
  [inst_3 : Module K M] [inst_4 : Module K N] {p : M →ₗ[K] N →ₗ[K] K} [FiniteDimensional K N],
  Function.Injective ⇑p → Function.Injective ⇑p.flip → p.IsPerfPair
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyoneda_map_app : ∀ {X Y : AddCommGrpCatᵒᵖ} (f : X ⟶ Y) (N : AddCommGrpCat),
  (AddCommGrpCat.coyoneda.map f).app N = AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f.unop).compHom'
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isColocal_iff_isIso_map : ∀ {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 : G ⊣ F) [G.Full] [G.Faithful] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.ObjectProperty.isColocal (fun x => x ∈ Set.range G.obj) f ↔ CategoryTheory.IsIso (F.map f)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabCompletion : Lean.Elab.Term.TermElab
-- Init.Meta.Defs
/-- `eraseSuffix? n s` return `n'` if `n` is of the form `n == n' ++ s`.
 -/
Lean.Name.eraseSuffix? : Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
fderiv_continuousAlternatingMap_apply_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} {x : E}
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  DifferentiableAt 𝕜 f x →
    (∀ (i : ι), DifferentiableAt 𝕜 (g i) x) →
      ∀ (dx : E),
        (fderiv 𝕜 (fun x => (f x) fun x_1 => g x_1 x) x) dx =
          (((fderiv 𝕜 f x) dx) fun x_1 => g x_1 x) +
            ∑ i, (f x) (Function.update (fun x_1 => g x_1 x) i ((fderiv 𝕜 (g i) x) dx))
-- Init.Data.Nat.ToString
Nat.ofDigitChars_append : ∀ {b : ℕ} {l m : List Char} (init : ℕ), b.ofDigitChars (l ++ m) init = b.ofDigitChars m (b.ofDigitChars l init)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Counters.mk.inj : ∀ {thm : Lean.PHashMap Lean.Meta.Grind.Origin ℕ} {fvarUserNames : Lean.PHashMap Lean.FVarId Lean.Name}
  {case apps : Lean.PHashMap Lean.Name ℕ} {thm_1 : Lean.PHashMap Lean.Meta.Grind.Origin ℕ}
  {fvarUserNames_1 : Lean.PHashMap Lean.FVarId Lean.Name} {case_1 apps_1 : Lean.PHashMap Lean.Name ℕ},
  { thm := thm, fvarUserNames := fvarUserNames, case := case, apps := apps } =
      { thm := thm_1, fvarUserNames := fvarUserNames_1, case := case_1, apps := apps_1 } →
    thm = thm_1 ∧ fvarUserNames = fvarUserNames_1 ∧ case = case_1 ∧ apps = apps_1
-- Mathlib.Topology.MetricSpace.Algebra
/-- Class `LipschitzAdd M` says that the addition `(+) : X × X → X` is Lipschitz jointly in
the two arguments.  -/
LipschitzAdd : (β : Type u_2) → [PseudoMetricSpace β] → [AddMonoid β] → Prop
-- Mathlib.FieldTheory.SeparableClosure
/-- The same-universe version of `Field.lift_insepDegree_eq_of_equiv`.  -/
Field.insepDegree_eq_of_equiv : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K), Field.insepDegree F E = Field.insepDegree F K
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.size : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.DeclValue pu → ℕ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → ¬cmp k t.minKey! = Ordering.eq → (t.erase k).minKey! = t.minKey!
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} (h : IsBoundedLinearMap 𝕜 f),
  HasFDerivWithinAt f (IsBoundedLinearMap.toContinuousLinearMap f h) s x
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplex_d_neg : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G) (n : ℕ),
  (tateComplex M).d (-(↑n + 2)) (-(↑n + 1)) = (groupHomology.inhomogeneousChains M).d (n + 1) n
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.hasLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {J : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Over X)],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Subobject X)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] [inst_4 : MulZeroOneClass α] [inst_5 : MulZeroOneClass β]
  [inst_6 : MulZeroOneClass γ] [inst_7 : MulZeroOneClass δ] (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- If two functions differ only on a discrete set, then their logarithmic counting
functions agree.
 -/
ValueDistribution.logCounting_congr_codiscrete : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
  f =ᶠ[Filter.codiscrete ℂ] g → ValueDistribution.logCounting f = ValueDistribution.logCounting g
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.insert_eq_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {p : α}, insert p t = t.insert p
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.isZero_X : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) {i : Option ι}, i = none → CategoryTheory.Limits.IsZero (HomologicalComplex.extend.X K i)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mk.congr_simp : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes boxes_1 : Finset (BoxIntegral.Box ι)) (e_boxes : boxes = boxes_1)
  (le_of_mem' : ∀ J ∈ boxes, J ≤ I)
  (pairwiseDisjoint : (↑boxes).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)),
  { boxes := boxes, le_of_mem' := le_of_mem', pairwiseDisjoint := pairwiseDisjoint } =
    { boxes := boxes_1, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The middle left map in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPostPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPostPost F)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_if_append : ∀ {m n : ℤ}, (m...n).toList = if m < n then (m...n - 1).toList ++ [n - 1] else []
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- A helper to construct a strongly locally contractible space from a neighborhood basis where
each basis element is contractible as a subspace.  -/
StronglyLocallyContractibleSpace.of_bases : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {p : X → ι → Prop} {s : X → ι → Set X},
  (∀ (x : X), (nhds x).HasBasis (p x) (s x)) →
    (∀ (x : X) (i : ι), p x i → ContractibleSpace ↑(s x i)) → StronglyLocallyContractibleSpace X
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.coe_primesOverFinset : ∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A},
  p ≠ ⊥ →
    ∀ [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B] [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B]
      [IsDomain A] [Module.IsTorsionFree A B], ↑(IsDedekindDomain.primesOverFinset p B) = p.primesOver B
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
borel_eq_generateFrom_of_subbasis : ∀ {α : Type u_1} {s : Set (Set α)} [t : TopologicalSpace α] [SecondCountableTopology α],
  t = TopologicalSpace.generateFrom s → borel α = MeasurableSpace.generateFrom s
-- Lean.Environment
Lean.AsyncBranch.asyncEnv.sizeOf_spec : sizeOf Lean.AsyncBranch.asyncEnv = 1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f =
      CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g ↔
    f = g
-- Mathlib.Data.PEquiv
/-- The identity map as a partial equivalence.  -/
PEquiv.refl : (α : Type u_1) → α ≃. α
-- Init.Data.UInt.Lemmas
UInt64.ofFin_uint32ToFin : ∀ (n : UInt32), UInt64.ofFin (Fin.castLE UInt32.toFin_toUInt64._proof_1 n.toFin) = n.toUInt64
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side.  -/
EuclideanGeometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the second projection `Y j ⟶ X i₂`  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.p₂ : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {S : C} →
            (self : F.PreOneHypercoverDenseData S) → ⦃i₁ i₂ : self.I₀⦄ → (j : self.I₁ i₁ i₂) → self.Y j ⟶ self.X i₂
-- Mathlib.RepresentationTheory.FiniteIndex
/-- Given a finite index subgroup `S ≤ G`, `Coind_S^G` is left adjoint to the restriction functor
`Res k G ⥤ Res k S`, since it is naturally isomorphic to `Ind_S^G`.  -/
Rep.coindResAdjunction : (k : Type u) →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) →
          [DecidableRel ⇑(QuotientGroup.rightRel S)] →
            [S.FiniteIndex] → Rep.coindFunctor k S.subtype ⊣ Rep.resFunctor S.subtype
-- Mathlib.Topology.Order.Basic
/-- **Alias** of `PredOrder.hasBasis_nhds_Ico_of_exists_gt`. -/
PredOrder.hasBasis_nhds_Ioc_of_exists_gt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [PredOrder α] {a : α},
  (∃ l, a < l) → (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_desc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
  {Z : CochainComplex C ℤ} (h : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.desc φ α β eq) h) =
    CategoryTheory.CategoryStruct.comp β h
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.Lifting₂.flip : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                              (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F'] →
                                  CategoryTheory.Localization.Lifting₂ L₂ L₁ W₂ W₁ F.flip F'.flip
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.map_le : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B]
  {S : NonUnitalStarSubalgebra R A} {f : F} {U : NonUnitalStarSubalgebra R B},
  NonUnitalStarSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalStarSubalgebra.comap f U
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.pullback_addMonoidHom_def : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : R1Space α] [inst_2 : AddGroup α]
  [inst_3 : TopologicalSpace β] [inst_4 : R1Space β] [inst_5 : AddGroup β] [inst_6 : ContinuousAdd β]
  [inst_7 : NormedAddCommGroup γ] {φ : α →+ β} (hφ : Topology.IsClosedEmbedding ⇑φ)
  (f : CompactlySupportedContinuousMap β γ) (b : β) (a : α),
  (CompactlySupportedContinuousMap.pullback_addMonoidHom hφ f b) a = f (b + φ a)