mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- An isomorphism is in particular a strong epimorphism.  -/
CategoryTheory.strongEpi_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.IsIso f],
  CategoryTheory.StrongEpi f
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.freeAddMonoidCongr.eq_1 : ∀ {α : Type u_6} {β : Type u_7} (e : α ≃ β),
  FreeAddMonoid.freeAddMonoidCongr e =
    { toFun := ⇑(FreeAddMonoid.map ⇑e), invFun := ⇑(FreeAddMonoid.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (π : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))
  (hπ :
    ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π c i)
          ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
            (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))))
  (isLimitWedge : (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π c) ⋯))
  (map_comp_π :
    ∀ {c c' : C} (f : c ⟶ c') (j : C),
      CategoryTheory.CategoryStruct.comp (H.map f) (π c' j) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f))))
  (π_1 : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))
  (hπ_1 :
    ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π_1 c i)
          ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
        CategoryTheory.CategoryStruct.comp (π_1 c j)
          ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
            (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))))
  (isLimitWedge_1 : (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π_1 c) ⋯))
  (map_comp_π_1 :
    ∀ {c c' : C} (f : c ⟶ c') (j : C),
      CategoryTheory.CategoryStruct.comp (H.map f) (π_1 c' j) =
        CategoryTheory.CategoryStruct.comp (π_1 c j)
          ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f)))),
  ({ π := π, hπ := hπ, isLimitWedge := isLimitWedge, map_comp_π := map_comp_π } =
      { π := π_1, hπ := hπ_1, isLimitWedge := isLimitWedge_1, map_comp_π := map_comp_π_1 }) =
    (π = π_1 ∧ isLimitWedge ≍ isLimitWedge_1)
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- **Alias** of `Metric.measure_eball_pos`. -/
EMetric.measure_ball_pos : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
  [μ.IsOpenPosMeasure] (x : X) {r : ENNReal}, r ≠ 0 → 0 < μ (Metric.eball x r)
-- Mathlib.Order.CompleteLattice.Basic
iInf_false : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : False → α}, iInf s = ⊤
-- Mathlib.Computability.NFA
NFA.mem_acceptsFrom : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {S : Set σ} {x : List α},
  x ∈ M.acceptsFrom S ↔ ∃ s ∈ M.accept, s ∈ M.evalFrom S x
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.mkTuple : Array Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.map_objs_eq : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {D : Type u_1}
  [inst_1 : CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj),
  (CategoryTheory.Subgroupoid.map φ hφ S).objs = φ.obj '' S.objs
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.inv_zero : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : DecidableEq α], 0⁻¹ = 0
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.π_homologyIsoSc'_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyπ j)
      (CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom h) =
    CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom
      (CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ h)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.order_pow : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] [NoZeroDivisors R] (x : HahnSeries Γ R) (n : ℕ), (x ^ n).order = n • x.order
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- In a pseudometric space, an open ball of infinite radius is the whole space  -/
Metric.eball_top_eq_univ : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Metric.eball x ⊤ = Set.univ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.mk.sizeOf_spec : ∀ (name : String) (kind : Lean.Lsp.SymbolKind) (tags : Array Lean.Lsp.SymbolTag) (location : Lean.Lsp.Location)
  (containerName? : Option String),
  sizeOf { name := name, kind := kind, tags := tags, location := location, containerName? := containerName? } =
    1 + sizeOf name + sizeOf kind + sizeOf tags + sizeOf location + sizeOf containerName?
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.instIsScalarTower : ∀ {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : ContinuousAdd 𝕜] [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E]
  [inst_6 : TopologicalSpace E] [inst_7 : CommSemiring 𝕝] [inst_8 : Module 𝕝 𝕜] [inst_9 : Module 𝕝 E]
  [IsScalarTower 𝕝 𝕜 E], IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.sum_dual_apply_smul_coord : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [inst_3 : Fintype ι] (f : Module.Dual R M), ∑ x, f (b x) • b.coord x = f
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Given two sets `s, t` in a Hausdorff normal σ-compact finite-dimensional manifold `M`
with `s` open and `s ⊆ interior t`, there is a smooth function `f : M → [0,1]` which is equal to `s`
in a neighbourhood of `s` and has support contained in `t`.  -/
exists_contMDiffMap_one_nhds_of_subset_interior : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] {n : ℕ∞} [T2Space M] [NormalSpace M] [SigmaCompactSpace M]
  {s t : Set M},
  IsClosed s →
    s ⊆ interior t → ∃ f, (∀ᶠ (x : M) in nhdsSet s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.insert : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s : Set ι} {x : ι},
  LinearIndepOn K v s → v x ∉ Submodule.span K (v '' s) → LinearIndepOn K v (insert x s)
-- Init.GetElem
/-- This instance overrides the default implementation of `a[i]?` via `decidableGetElem?`,
giving better definitional equalities.  -/
List.instGetElem?NatLtLength : {α : Type u_1} → GetElem? (List α) ℕ α fun as i => i < as.length
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.le_toIdeal_homogeneousHull : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (I : Ideal A),
  I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_alterKey_of_key_ne : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
  {l : List ((a : α) × β a)} (p : (a : α) × β a), p.fst ≠ a → (p ∈ Std.Internal.List.alterKey a f l ↔ p ∈ l)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} [inst_2 : SizeOf α]
  (lhs : aig.RefVec len) (bit : aig.Ref), sizeOf { lhs := lhs, bit := bit } = 1 + sizeOf lhs + sizeOf bit
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.sub_submartingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.Submartingale g ℱ μ → MeasureTheory.Supermartingale (f - g) ℱ μ
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_mul : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (x y : ↥s), ↑(x * y) = ↑x * ↑y
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_equivProd_symm_apply : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R), ((QuaternionAlgebra.equivProd c₁ c₂ c₃).symm a).imI = a.2.1
-- Mathlib.Topology.GDelta.Basic
/-- An open set is a Gδ set.  -/
IsOpen.isGδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → IsGδ s
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Ordered.zoom' : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t' : RBTree.RBNode α} {path' : RBTree.RBNode.Path α}
  {t : RBTree.RBNode α} {path : RBTree.RBNode.Path α},
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.Path.Ordered cmp path →
      RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path) t →
        RBTree.RBNode.Path.Zoomed cut path →
          RBTree.RBNode.zoom cut t path = (t', path') →
            RBTree.RBNode.Ordered cmp t' ∧
              RBTree.RBNode.Path.Ordered cmp path' ∧
                RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path') t' ∧ RBTree.RBNode.Path.Zoomed cut path'
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_map_abs : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] [inst_9 : DecidableEq ι],
  b.cartanMatrix.map abs = 4 - b.cartanMatrix
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instDivCoeOfSubgroupClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → DivInvMonoid (R i)] →
              [∀ (i : ι), SubgroupClass (S i) (R i)] → Div (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addConGen_monotone : ∀ {M : Type u_1} [inst : Add M], Monotone addConGen
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_some : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F}
  (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂},
  WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =
    WeierstrassCurve.Affine.Point.some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The compatibility isomorphisms of the total complex with the shifts
in both variables "commute" only up to a sign `(x * y).negOnePow`.  -/
HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ)
  [inst_2 : K.HasTotal (ComplexShape.up ℤ)],
  ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x ≪≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) x).mapIso (K.totalShift₂Iso y) =
    (x * y).negOnePow •
      HomologicalComplex₂.total.mapIso ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).app K) (ComplexShape.up ℤ) ≪≫
        ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y ≪≫
          (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).mapIso (K.totalShift₁Iso x) ≪≫
            (CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).app (K.total (ComplexShape.up ℤ))
-- Init.Data.SInt.Basic
/-- Bitwise and for 8-bit signed integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set,
according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.land : Int8 → Int8 → Int8
-- Init.Data.String.Subslice
String.Slice.Subslice.extendLeft_self : ∀ {s : String.Slice} {sl : s.Subslice}, sl.extendLeft sl.startInclusive ⋯ = sl
-- Init.Data.Array.Lemmas
/-- Variant of `foldr_push` with the `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
 -/
Array.foldr_push' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {init : β} {xs : Array α} {a : α} {start : ℕ},
  start = xs.size + 1 → Array.foldr f init (xs.push a) start = Array.foldr f (f a init) xs
-- Mathlib.Topology.Algebra.ConstMulAction
set_smul_mem_nhds_zero_iff : ∀ {α : Type u_2} {G₀ : Type u_6} [inst : GroupWithZero G₀] [inst_1 : AddMonoid α] [inst_2 : DistribMulAction G₀ α]
  [inst_3 : TopologicalSpace α] [ContinuousConstSMul G₀ α] {s : Set α} {c : G₀}, c ≠ 0 → (c • s ∈ nhds 0 ↔ s ∈ nhds 0)
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedInfoTree.default : Lean.Elab.InfoTree
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.Context.mk : ℕ → Lean.Meta.Grind.Arith.Linear.LinearM.Context
-- Mathlib.Order.Monotone.Basic
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright.  -/
not_monotone_not_antitone_iff_exists_le_le : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
-- Init.Control.Except
Except.map.eq_1 : ∀ {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) (err : ε), Except.map f (Except.error err) = Except.error err
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_zero_strictMono : StrictMono fun x => Ordinal.veblen x 0
-- Batteries.Data.Fin.Coding
/-- Decode `(i : Fin n) × Fin (f i)` from `Fin (Fin.sum f)`.  -/
Fin.decodeSigma : {n : ℕ} → (f : Fin n → ℕ) → Fin (Fin.sum f) → (i : Fin n) × Fin (f i)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
      CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv
          (F.rightDerivedToHomotopyCategory.map f) =
        CategoryTheory.CategoryStruct.comp
          (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ)
          (J.isoRightDerivedToHomotopyCategoryObj F).inv
-- Mathlib.Data.Matrix.Basic
Matrix.entryLinearMap_eq_comp : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α] {i : m} {j : n},
  Matrix.entryLinearMap R α i j = LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ ↑(Matrix.ofLinearEquiv R).symm
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- This isn't marked as simp to avoid looping with unfolding `coeff`.  -/
AddMonoidAlgebra.ofCoeff_mapRange : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S) (x : M →₀ R),
  AddMonoidAlgebra.ofCoeff (Finsupp.mapRange ⇑f ⋯ x) = AddMonoidAlgebra.map f (AddMonoidAlgebra.ofCoeff x)
-- Init.Data.Slice.Array.Iterator
Subarray.copy_eq_toArray : ∀ {α : Type u} {s : Subarray α}, ↑s = Std.Slice.toArray s
-- Init.Prelude
/-- `a / b` computes the result of dividing `a` by `b`. See `HDiv`.  -/
Div.div : {α : Type u} → [self : Div α] → α → α → α
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_diagonal : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (v : n → α),
  (Matrix.diagonal v)⁻¹ = Matrix.diagonal (Ring.inverse v)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_eq_bot_iff : ∀ {x : ENNReal}, x.log = ⊥ ↔ x = 0
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_add_add : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k + f l) μ
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_div_natCast : ∀ {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_3} [inst : NormedField 𝕜] [NormedSpace ℝ 𝕜] [CharZero 𝕜] {n : ℕ},
  n ≠ 0 →
    ∀ (f : α → 𝕜) (p : ENNReal) (μ : MeasureTheory.Measure α),
      MeasureTheory.lpNorm (f / ↑n) p μ = MeasureTheory.lpNorm f p μ / ↑n
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.isScalarTower_right : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B] [inst_9 : Monoid S] [inst_10 : DistribMulAction S A] [IsScalarTower S A A]
  [inst_12 : SMulCommClass R S A], IsScalarTower S (TensorProduct R A B) (TensorProduct R A B)
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finsum_mem_union` that requires `s ∩ support f` and
`t ∩ support f` rather than `s` and `t` to be finite.  -/
finsum_mem_union' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
  Disjoint s t →
    (s ∩ Function.support f).Finite →
      (t ∩ Function.support f).Finite →
        ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.Localization.exists_leftFraction₂ : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C}
  (f f' : L.obj X ⟶ L.obj Y), ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPolynomial.toMvPowerSeries_isDenseInducing : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R],
  IsDenseInducing MvPolynomial.toMvPowerSeries
-- Mathlib.NumberTheory.ModularForms.NormTrace
instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf : {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} → MulAction (↥ℋ) (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSum_weierstrassP : ∀ (L : PeriodPair) (z : ℂ), HasSum (fun l => 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) (L.weierstrassP z)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonpos : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  MeasurableSet s → (∀ x ∈ s, f x ≤ 0) → ∫ (x : X) in s, f x ∂μ ≤ 0
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.leftUnitor_inv_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.f =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.fst).inv
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.firstMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Limits.HasProducts A] [inst_3 : CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Presheaf.firstMap R P =
    CategoryTheory.Limits.Pi.lift fun x =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) x.1)
        (P.map (CategoryTheory.Limits.pullback.fst ↑x.1.snd ↑x.2.snd).op)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.one_lt_prod_of_one_lt : ∀ {M : Type u_3} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] (l : List M),
  (∀ x ∈ l, 1 < x) → l ≠ [] → 1 < l.prod
-- Mathlib.Data.Multiset.MapFold
Multiset.map_eq_zero : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β}, Multiset.map f s = 0 ↔ s = 0
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- The converse is true when `S` is a Dedekind domain.
See `Ideal.ramificationIdx'_eq_one_iff_of_isDedekindDomain`.  -/
Ideal.ramificationIdx'_eq_one_of_map_localization : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [inst_3 : P.IsPrime] [IsNoetherianRing S],
  Ideal.map (algebraMap R S) p ≤ P →
    P ≠ ⊥ →
      P.primeCompl ≤ nonZeroDivisors S →
        Ideal.map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P) →
          p.ramificationIdx' P = 1
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Adjunction.instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms : ∀ {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} {F' : CategoryTheory.Functor D C}
  (adj : F ⊣ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) [hf : CategoryTheory.Mono f] [F.ReflectsMonomorphisms],
  CategoryTheory.Mono ((adj.homEquiv X Y) f)
-- Mathlib.Data.Part
Part.bind_some_eq_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : Part α), (x.bind fun y => Part.some (f y)) = Part.map f x