mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The localization map of a submodule.  -/
Submodule.toLocalized' : {R : Type u_1} →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Algebra R S] →
                      [inst_7 : Module S N] →
                        [inst_8 : IsScalarTower R S N] →
                          (p : Submonoid R) →
                            [inst_9 : IsLocalization p S] →
                              (f : M →ₗ[R] N) →
                                [inst_10 : IsLocalizedModule p f] →
                                  (M' : Submodule R M) → ↥M' →ₗ[R] ↥(Submodule.localized' S p f M')
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_ric_eq_fallback : ∀ {n i fallback : ℕ}, n < i → (*...=n).toList.getD i fallback = fallback
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
isGLB_ciInf_set : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : β → α} {s : Set β},
  BddBelow (f '' s) → s.Nonempty → IsGLB (f '' s) (⨅ i, f ↑i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.instFiniteObjOppositeSimplexCategoryTensorObj : ∀ (X Y : SSet) (n : SimplexCategoryᵒᵖ) [Finite (X.obj n)] [Finite (Y.obj n)],
  Finite ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj n)
-- Init.Data.Fin.Lemmas
Fin.one_eq_zero_iff : ∀ {n : ℕ} [inst : NeZero n], 1 = 0 ↔ n = 1
-- Mathlib.Data.Finset.Basic
Finset.attach_empty : ∀ {α : Type u_1}, ∅.attach = ∅
-- Mathlib.Order.Monotone.Basic
antitone_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone (⇑OrderDual.toDual ∘ f) ↔ Monotone f
-- Mathlib.Data.Finset.Card
/-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a
set `u` of size `n` which is both a superset of `s` and a subset of `t`.  -/
Finset.exists_subsuperset_card_eq : ∀ {α : Type u_1} {s t : Finset α} {n : ℕ}, s ⊆ t → s.card ≤ n → n ≤ t.card → ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.card = n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotation by π / 2 is the "right-angle-rotation" map `J`.  -/
Orientation.rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)), o.rotation ↑(Real.pi / 2) = o.rightAngleRotation
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite
on compacts and inner regular, they coincide up to a multiplicative constant.  -/
MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  [μ.InnerRegular] [μ'.InnerRegular], μ' = μ'.addHaarScalarFactor μ • μ
-- Init.Data.String.Lemmas.FindPos
String.posGE_eq_posGE_toSlice : ∀ {s : String} {p : String.Pos.Raw} (h : p ≤ s.rawEndPos), s.posGE p h = String.Pos.ofToSlice (s.toSlice.posGE p ⋯)
-- Mathlib.Algebra.Polynomial.Laurent
/-- `trunc : R[T;T⁻¹] →+ R[X]` maps a Laurent polynomial `f` to the polynomial whose terms of
nonnegative degree coincide with the ones of `f`.  The terms of negative degree of `f` "vanish".
`trunc` is a left-inverse to `Polynomial.toLaurent`.  -/
LaurentPolynomial.trunc : {R : Type u_1} → [inst : Semiring R] → LaurentPolynomial R →+ Polynomial R
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonAssocCommRingQuotient : {R : Type u_1} → [inst : NonAssocCommRing R] → (c : RingCon R) → NonAssocCommRing c.Quotient
-- Mathlib.RepresentationTheory.FiniteIndex
/-- Let `S ≤ G` be a finite index subgroup, `g₁, ..., gₙ` a set of right coset representatives of
`S`, and `A` a `k`-linear `S`-representation. This is an isomorphism `Ind_S^G(A) ≅ Coind_S^G(A)`.
The forward map sends `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`, and the inverse sends `f : G → A` to
`∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧` for `1 ≤ i ≤ n`.  -/
Rep.indCoindIso : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {S : Subgroup G} →
          [DecidableRel ⇑(QuotientGroup.rightRel S)] →
            [S.FiniteIndex] →
              (A : Rep.{max w u, u, v} k ↥S) → Rep.ind S.subtype A ≅ Rep.coind.{u, v, v, max u w} S.subtype A
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`.  -/
CategoryTheory.mateEquiv_conjugateEquiv_vcomp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor A C} {H : CategoryTheory.Functor B D}
  {L₁ : CategoryTheory.Functor A B} {R₁ : CategoryTheory.Functor B A} {L₂ : CategoryTheory.Functor C D}
  {R₂ : CategoryTheory.Functor D C} {L₃ : CategoryTheory.Functor C D} {R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁)
  (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (α : CategoryTheory.TwoSquare G L₁ L₂ H) (β : L₃ ⟶ L₂),
  (CategoryTheory.mateEquiv adj₁ adj₃) (α.whiskerRight β) =
    ((CategoryTheory.mateEquiv adj₁ adj₂) α).whiskerBottom ((CategoryTheory.conjugateEquiv adj₂ adj₃) β)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.unitSMul_smul : ∀ (K : Type u_1) [inst : Field K] (u : (NumberField.RingOfIntegers K)ˣ) (x : NumberField.mixedEmbedding.mixedSpace K),
  u • x = (NumberField.mixedEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u) * x
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.Finset.sups_aux : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α},
  a ∈ upperClosure ↑(s ⊻ t) ↔ a ∈ upperClosure ↑s ∧ a ∈ upperClosure ↑t
-- Init.Data.BitVec.Lemmas
/-- Equation theorem for `smod` in terms of `umod`.  -/
BitVec.smod_eq : ∀ {w : ℕ} (x y : BitVec w),
  x.smod y =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      have u := x.umod (-y);
      if u = 0#w then u else u + y
    | true, false =>
      have u := (-x).umod y;
      if u = 0#w then u else y - u
    | true, true => -(-x).umod (-y)
-- Init.Data.List.Lemmas
List.reverseAux_reverseAux_nil : ∀ {α : Type u_1} {as bs : List α}, (as.reverseAux bs).reverseAux [] = bs.reverseAux as
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.subset_subalgebra : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [inst_4 : SubringClass S A] [inst_5 : SMulMemClass S R A] {s : S} (a : ↥s),
  spectrum R ↑a ⊆ spectrum R a
-- Mathlib.RepresentationTheory.Rep.Res
Rep.instAdditiveResFunctor : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G),
  (Rep.resFunctor f).Additive
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- `μ` is integral over `ℤ`.  -/
IsPrimitiveRoot.isIntegral : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K}, IsPrimitiveRoot μ n → 0 < n → IsIntegral ℤ μ
-- Mathlib.Topology.Algebra.Monoid
ContinuousAt.fun_nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M} {x : X}, ContinuousAt f x → ∀ (n : ℕ), ContinuousAt (fun i => n • f i) x
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAsPartialEquiv_target : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι), (Z.localTrivAsPartialEquiv i).target = (Z.localTriv i).target
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.toArray.size = t.size
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.guard.injEq : ∀ (e e_1 : Lean.Expr),
  (Lean.Meta.Grind.EMatchTheoremConstraint.guard e = Lean.Meta.Grind.EMatchTheoremConstraint.guard e_1) = (e = e_1)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHom_whisker_cancel_inv : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C}
  (α : Y ≅ Y₁),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.inv) (Y₁ ⟶[V] Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerRight V α.hom Z))
        (CategoryTheory.eComp V X Y Z)) =
    CategoryTheory.eComp V X Y₁ Z
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.Forall.match_1.eq_1 : ∀ {α : Type u_2} (motive : (x : ℕ) → ((Fin x → α) → Prop) → Sort u_1) (P : (Fin 0 → α) → Prop)
  (h_1 : (P : (Fin 0 → α) → Prop) → motive 0 P) (h_2 : (n : ℕ) → (P : (Fin (n + 1) → α) → Prop) → motive n.succ P),
  (match 0, P with
    | 0, P => h_1 P
    | n.succ, P => h_2 n P) =
    h_1 P
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.zero₁_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.zero₁._auto_1) {Z : C}
  (h_1 : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.range_extend : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : LinearIndepOn K id s), Set.range ⇑(Module.Basis.extend hs) = hs.extend ⋯
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.lift_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [inst_2 : CommRing P] (g : (i : ι) → G i →+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x) (i : ι) (x : G i),
  (Ring.DirectLimit.lift G f P g Hg) ((Ring.DirectLimit.of G f i) x) = (g i) x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Product of non-unital subsemirings is isomorphic to their product as semigroups.  -/
NonUnitalSubsemiring.prodEquiv : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        (s : NonUnitalSubsemiring R) → (t : NonUnitalSubsemiring S) → ↥(s.prod t) ≃+* ↥s × ↥t
-- Lean.Elab.MutualInductive
/-- An intermediate step for mutual inductive elaboration. See `InductiveElabDescr`.  -/
Lean.Elab.Command.InductiveElabStep2 : Type
-- Mathlib.Tactic.CategoryTheory.Elementwise
_private.Mathlib.Tactic.CategoryTheory.Elementwise.0.Mathlib.Tactic.Elementwise.mkUnusedName.loop : List Lean.Name → Lean.Name → optParam ℕ 0 → Lean.Name
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (toAlgHom : A →ₐ[R] B) (map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toAlgHom.toRingHom x ∈ ℬ i) (toAlgHom_1 : A →ₐ[R] B)
  (map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toAlgHom_1.toRingHom x ∈ ℬ i),
  ({ toAlgHom := toAlgHom, map_mem := map_mem } = { toAlgHom := toAlgHom_1, map_mem := map_mem_1 }) =
    (toAlgHom = toAlgHom_1)
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.prelude : Lean.Parser.Parser
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppEquivDFinsupp_symm_apply : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : Zero N] (f : Π₀ (i : ι), η i →₀ N) (s : (i : ι) × η i),
  (sigmaFinsuppEquivDFinsupp.symm f) s = (f s.fst) s.snd
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.specOrderIsoPrimeSpectrum_apply : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  (AlgebraicGeometry.specOrderIsoPrimeSpectrum R) x = OrderDual.toDual x
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_shiftRight_mod : ∀ (a : BitVec 8) (b : ℕ), { toBitVec := a >>> (b % 8) } = { toBitVec := a } >>> UInt8.ofNat b
-- Std.Time.Zoned.Database.Basic
/-- Converts a `TZif.TZif` structure to a `ZoneRules` structure.
 -/
Std.Time.TimeZone.convertTZif : Std.Time.TimeZone.TZif.TZif → String → Except String Std.Time.TimeZone.ZoneRules
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.atIdxSlow?.match_1.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β)
  (motive :
    (n : ℕ) →
      ((a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
              Option β) →
        Sort u_2)
  (k : ℕ)
  (recur :
    (a' : Std.Iter β) →
      (b' : ℕ) →
        InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
            (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
          Option β)
  (h_1 :
    (recur :
        (a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
              Option β) →
      motive 0 recur)
  (h_2 :
    (k : ℕ) →
      (recur :
          (a' : Std.Iter β) →
            (b' : ℕ) →
              InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                  (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                Option β) →
        motive k.succ recur),
  (match k.succ, recur with
    | 0, recur => h_1 recur
    | k.succ, recur => h_2 k recur) =
    h_2 k recur
-- Init.Data.Array.Basic
Array.getElem_toList : ∀ {α : Type u} {xs : Array α} {i : ℕ} (h : i < xs.toList.length), xs.toList[i] = xs[i]
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.EStateM.tryCatch.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (ok : EStateM.Result ε σ α)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)) (h_2 : (ok : EStateM.Result ε σ α) → motive ok),
  (∀ (e : ε) (s : σ), ok = EStateM.Result.error e s → False) →
    (match ok with
      | EStateM.Result.error e s => h_1 e s
      | ok => h_2 ok) =
      h_2 ok
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- `Φ.iteration J` identifies to the colimit of `Φ.iterationFunctor J`.  -/
CategoryTheory.SmallObject.SuccStruct.isColimitIterationCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  CategoryTheory.Limits.IsColimit (Φ.iterationCocone J)
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of an inner regular measure under left addition is again inner regular.  -/
MeasureTheory.innerRegular_map_add_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.InnerRegular] (g : G),
  (MeasureTheory.Measure.map (fun x => g + x) μ).InnerRegular
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.unbotD_zero : ∀ {α : Type u} [inst : Zero α] (d : α), WithBot.unbotD d 0 = 0
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.strictLimitsOfShape_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] {Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.strictLimitsOfShape J ≤ Q.strictLimitsOfShape J
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.map_ι₁_mapHomologicalComplexObjIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (F : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel] {D : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_2, u_3} D] [inst_4 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)]
  [inst_7 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F))]
  [inst_8 :
    ∀ (i : ι),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i)
        (((H.mapHomologicalComplex c).obj F).X i)]
  [inst_9 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F))
        (-CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F)))]
  [inst_10 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.mapHomologicalComplex c).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F)))]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.cylinder.ι₁ F))
      (HomologicalComplex.cylinder.mapHomologicalComplexObjIso F H hc).hom =
    HomologicalComplex.cylinder.ι₁ ((H.mapHomologicalComplex c).obj F)
-- Mathlib.Algebra.Order.Module.Pointwise
BddAbove.smul_of_nonpos : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β] {s : Set β} {a : α},
  a ≤ 0 → BddAbove s → BddBelow (a • s)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side, version subtracting vectors.  -/
Orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle (x - y) x).tan = ‖x‖
-- Init.Data.List.Nat.Modify
List.eraseIdx_modify_of_eq : ∀ {α : Type u_1} (f : α → α) (i : ℕ) (l : List α), (l.modify i f).eraseIdx i = l.eraseIdx i
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.cexp : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ},
  AEMeasurable f μ → AEMeasurable (fun x => Complex.exp (f x)) μ
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instOfIsLocalRingOfIsBezout : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsLocalRing R] [IsBezout R], ValuationRing R
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.SurjectiveOnStalks.baseChange : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  [inst_3 : Algebra R T] [inst_4 : Algebra R S],
  (algebraMap R T).SurjectiveOnStalks → (algebraMap S (TensorProduct R S T)).SurjectiveOnStalks
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_of_le_mul_two : ∀ {x : ℤ} {y : ℕ}, -↑y ≤ x * 2 → x * 2 < ↑y → x.bmod y = x
-- Mathlib.Algebra.Group.Commute.Basic
Commute.conj : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → ∀ (h : G), Commute (h * a * h⁻¹) (h * b * h⁻¹)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.toContinuousMap_coe : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q), f.toContinuousMap = ↑f
-- Init.Data.Int.Order
Int.neg_le_neg : ∀ {a b : ℤ}, a ≤ b → -b ≤ -a
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.precomp_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y), (I.precomp g).Y = Z
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aeval.eq_1 : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  Polynomial.aeval x = (Polynomial.aevalEquiv R A) x
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyFaithful.map_injective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyFaithful F → ∀ {X Y : C} {f g : X ⟶ Y}, (∀ (i : I), (F i).map f = (F i).map g) → f = g
-- Mathlib.Topology.Sheaves.PUnit
TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : TopCat.Presheaf C (TopCat.of PUnit.{u_1 + 1})),
  F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.homologyMap_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (a : R) [inst_4 : S₁.HasHomology] [inst_5 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap (a • φ) = a • CategoryTheory.ShortComplex.homologyMap φ
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_sub_right : ∀ {m n k : ℕ}, n ≤ m * k → m.gcd (m * k - n) = m.gcd n
-- Mathlib.Tactic.Translate.Core
/-- Eta expands `e` exactly `n` times.  -/
Mathlib.Tactic.Translate.etaExpandN : ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_nat_inj : ∀ {α β : Cardinal.{u_1}} (n : ℕ), α + ↑n = β + ↑n ↔ α = β