mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Algebra
/-- If `A` is the localization of `R` at a submonoid `S`, then `A[X]` is the localization of
`R[X]` at `S.map Polynomial.C`.

See also `MvPolynomial.isLocalization` for the multivariate case.  -/
Polynomial.isLocalization : ∀ {R : Type u_5} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_6) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A], IsLocalization (Submonoid.map Polynomial.C S) (Polynomial A)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse, version subtracting vectors.  -/
InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / Real.sin (InnerProductGeometry.angle x (x - y)) = ‖x - y‖
-- Mathlib.Combinatorics.Derangements.Finite
numDerangements_add_two : ∀ (n : ℕ), numDerangements (n + 2) = (n + 1) * (numDerangements n + numDerangements (n + 1))
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.contMDiff_sum : ∀ {ι : Type uι} {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] {s : Set M} (f : SmoothPartitionOfUnity ι I M s),
  ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun x => ∑ᶠ (i : ι), (f i) x
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsNormal.conj : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  S.IsNormal →
    ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c},
      γ ∈ S.arrows c c →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p) ∈
          S.arrows d d
-- Init.Data.Vector.Basic
Vector.unexpandMk : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.instIsTriangularizableSubtypeMemLieSubmodule : ∀ (K : Type u_1) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : Field K] [inst_4 : LieAlgebra K L] [inst_5 : Module K M] [inst_6 : LieModule K L M] [FiniteDimensional K M]
  (N : LieSubmodule K L M) [LieModule.IsTriangularizable K L M], LieModule.IsTriangularizable K L ↥N
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_symm_mk' : ∀ {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M →ₗ[R] M₂} {inv_fun : M₂ → M}
  {left_inv : Function.LeftInverse inv_fun f.toFun} {right_inv : Function.RightInverse inv_fun f.toFun},
  ⇑{ toLinearMap := f, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }.symm = inv_fun
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Post-composition with the preimage of an inducing function whose range is closed preserves
upper hemicontinuity.  -/
UpperHemicontinuous.isInducing_comp : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {γ : Type u_5}
  [inst_2 : TopologicalSpace γ] {i : γ → β},
  UpperHemicontinuous f → Topology.IsInducing i → IsClosed (Set.range i) → UpperHemicontinuous fun x => i ⁻¹' f x
-- Init.Data.List.Basic
/-- Splits a list into the longest segments in which each pair of adjacent elements are related by `R`.

`O(|l|)`.

Examples:
* `[1, 1, 2, 2, 2, 3, 2].splitBy (· == ·) = [[1, 1], [2, 2, 2], [3], [2]]`
* `[1, 2, 5, 4, 5, 1, 4].splitBy (· < ·) = [[1, 2, 5], [4, 5], [1, 4]]`
* `[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => true) = [[1, 2, 5, 4, 5, 1, 4]]`
* `[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => false) = [[1], [2], [5], [4], [5], [1], [4]]`
 -/
List.splitBy : {α : Type u} → (α → α → Bool) → List α → List (List α)
-- Init.Data.UInt.Lemmas
USize.toBitVec_mod : ∀ {a b : USize}, (a % b).toBitVec = a.toBitVec % b.toBitVec
-- Init.Data.Nat.Lemmas
Nat.pow_succ' : ∀ {m n : ℕ}, m ^ n.succ = m * m ^ n
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.snd_comp_quotientMulEquivQuotientProd : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J),
  (RingHom.snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableWithinAt.const_cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} {c : ℂ},
  DifferentiableWithinAt ℂ f s x → c ≠ 0 ∨ f x ≠ 0 → DifferentiableWithinAt ℂ (fun x => c ^ f x) s x
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.transHomeomorph_apply : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z), ↑(e.transHomeomorph f') = ⇑f' ∘ ↑e
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS_nc_NonnegCoeffs : ∀ {e : Lean.Grind.CommRing.Expr}, e.toPolyS_nc.NonnegCoeffs
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `𝔖 : Set (Set α)` is nonempty and directed and `𝓑` is a filter basis on `β × β`, then the
family `UniformOnFun.gen 𝔖 S V` for `S ∈ 𝔖` and `V ∈ 𝓑` is a filter basis on
`(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)`.
We will show in `has_basis_uniformity_of_basis` that, if `𝓑` is a basis for `𝓤 β`, then the
corresponding filter is the uniformity of `α →ᵤ[𝔖] β`.  -/
UniformOnFun.isBasis_gen : ∀ {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ (𝓑 : FilterBasis (β × β)), Filter.IsBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2
-- Init.Data.Fin.Basic
/-- Modulus of bounded numbers, usually invoked via the `%` operator.

The resulting value is that computed by the `%` operator on `Nat`.
 -/
Fin.mod : {n : ℕ} → Fin n → Fin n → Fin n
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_neg : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f : F.obj X ⟶ Y),
  (adj.homEquiv X Y) (-f) = -(adj.homEquiv X Y) f
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_surjective : ∀ {n : ℕ}, Function.Surjective SimplexCategory.toMk₁
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_symm_apply : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  (Γ : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ),
  CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax.symm Γ = Γ.toOplax
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.prod.instIsMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G]
  [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {H : Type u_3} [inst_5 : Mul H] {mH : MeasurableSpace H}
  {ν : MeasureTheory.Measure H} [MeasurableMul H] [ν.IsMulLeftInvariant] [MeasureTheory.SFinite ν],
  (μ.prod ν).IsMulLeftInvariant
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.DTreeMap.getKeyGED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → α → α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} [inst_3 : SizeOf C]
  (I : Type w) (X : I → C) (coversTop : J.CoversTop X) (presentation : (i : I) → (M.over (X i)).Presentation),
  sizeOf { I := I, X := X, coversTop := coversTop, presentation := presentation } = 1 + sizeOf I
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightComp_inv_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ L₃ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (r' : L₃ ⟶ R₂) (X : CategoryTheory.Comma L L₃),
  ((CategoryTheory.Comma.mapRightComp L r r').inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic) (based condition)  -/
AddAction.IsPreprimitive.of_isTrivialBlock_of_notMem_fixedPoints : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] {a : X},
  a ∉ AddAction.fixedPoints G X →
    (∀ ⦃B : Set X⦄, a ∈ B → AddAction.IsBlock G B → AddAction.IsTrivialBlock B) → AddAction.IsPreprimitive G X
-- Init.Data.Bool
Bool.not_ite_eq_false_eq_true : ∀ {p : Prop} [h : Decidable p] {b c : Bool}, (¬if p then b = false else c = true) ↔ if p then b = true else c = false
-- Mathlib.NumberTheory.SumTwoSquares
/-- If `n` is a squarefree natural number, then `-1` is a square modulo `n` if and only if
`n` has no divisor `q` that is `≡ 3 mod 4`.  -/
ZMod.isSquare_neg_one_iff' : ∀ {n : ℕ}, Squarefree n → (IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3)
-- Lean.Meta.PProdN
_private.Lean.Meta.PProdN.0.Lean.Meta.mkTypeSnd : Lean.Expr → Lean.Expr
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.instAddMonoid.eq_1 : ∀ {α : Type u_1} {rels : FreeAddMonoid α → FreeAddMonoid α → Prop},
  PresentedAddMonoid.instAddMonoid =
    { add := PresentedAddMonoid.instAddMonoid._aux_1, add_assoc := ⋯, zero := PresentedAddMonoid.instAddMonoid._aux_4,
      zero_add := ⋯, add_zero := ⋯, nsmul := PresentedAddMonoid.instAddMonoid._aux_8, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isLittleO_deriv_one_add_smoothingFn : (deriv fun x => 1 + AkraBazziRecurrence.smoothingFn x) =o[Filter.atTop] fun x => x⁻¹
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.equiv.congr_simp : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (R' : Type u_6)
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [h : Algebra.IsPushout R S R' S'], Algebra.IsPushout.equiv R S R' S' = Algebra.IsPushout.equiv R S R' S'
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.instDecidableRelReachable : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → [Fintype V] → [DecidableRel G.Adj] → DecidableRel G.Reachable
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_zero`. -/
SkewMonoidAlgebra.toFinsupp_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], SkewMonoidAlgebra.coeff 0 = 0
-- Mathlib.Analysis.ODE.Transform
isIntegralCurveOn_comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ}
  {a : ℝ}, a ≠ 0 → (IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v ∘ fun x => x * a) (a⁻¹ • s) ↔ IsIntegralCurveOn γ v s)
-- Std.Time.Date.Basic
/-- Convert `Nanosecond.Offset` into `Week.Offset`.
 -/
Std.Time.Nanosecond.Offset.toWeeks : Std.Time.Nanosecond.Offset → Std.Time.Week.Offset
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_mul_left_add_left : ∀ (m n k : ℕ), (n * k + m).Coprime n ↔ m.Coprime n
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.brecOn_2.go : {motive_1 : Lean.IR.Alt → Sort u} →
  {motive_2 : Lean.IR.FnBody → Sort u} →
    {motive_3 : Array Lean.IR.Alt → Sort u} →
      {motive_4 : List Lean.IR.Alt → Sort u} →
        (t : List Lean.IR.Alt) →
          ((t : Lean.IR.Alt) → t.below → motive_1 t) →
            ((t : Lean.IR.FnBody) → t.below → motive_2 t) →
              ((t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t) →
                ((t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t) → motive_4 t ×' Lean.IR.Alt.below_2 t
-- Mathlib.Order.Filter.SmallSets
Filter.Eventually.exists_mem_basis_of_smallSets : ∀ {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop},
  (∀ᶠ (t : Set α) in l.smallSets, P t) → l.HasBasis p s → ∃ i, p i ∧ P (s i)
-- Mathlib.Data.Seq.Defs
/-- Split a sequence at `n`, producing a finite initial segment
and an infinite tail.  -/
Stream'.Seq.splitAt : {α : Type u} → ℕ → Stream'.Seq α → List α × Stream'.Seq α
-- Init.Data.Ord.Basic
Ordering.swap_eq_eq : ∀ {o : Ordering}, o.swap = Ordering.eq ↔ o = Ordering.eq
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.find?.match_1.eq_2 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (startPos endPos : s.Pos)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos)),
  (match String.Slice.Pattern.SearchStep.rejected startPos endPos with
    | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
    | String.Slice.Pattern.SearchStep.rejected startPos endPos => h_2 startPos endPos) =
    h_2 startPos endPos
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatDivExactHAddDivOfNat : ∀ {n k : ℕ+}, Mathlib.Tactic.Ring.CSLiftVal (n.divExact k) (n.div k + 1)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.range_comp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (f : L.Hom M N) (g : L.Hom N P),
  (g.comp f).range = FirstOrder.Language.Substructure.map g f.range
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.eq_symm_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂}
  {y : M}, y = e.symm x ↔ e y = x
-- Mathlib.Algebra.Category.AlgCat.FilteredColimits
/-- (Implementation): The algebra instance on the cocone point of the underlying diagram of rings
is induced from the `j`-th inclusion map. Any choice of `j` gives a propositionally equal algebra
instance.  -/
_private.Mathlib.Algebra.Category.AlgCat.FilteredColimits.0.AlgCat.algebraOfIsFiltered : {R : Type u} →
  [inst : CommRing R] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        {F : CategoryTheory.Functor J (AlgCat R)} →
          [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget RingCat)] →
            {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget₂ (AlgCat R) RingCat))} →
              [CategoryTheory.IsFilteredOrEmpty J] → CategoryTheory.Limits.IsColimit c → J → Algebra R ↑c.pt
-- Init.Data.List.MinMaxOn
List.maxOn_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []),
  List.maxOn f (xs ++ ys) ⋯ = maxOn f (List.maxOn f xs hxs) (List.maxOn f ys hys)
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.bot_lt_mul_inv : ∀ {K : Type u_3} [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I ≠ ⊥ → ⊥ < I * I⁻¹
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkGenPattern : List Lean.Level → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The addition of two Jacobian point representatives on a Weierstrass curve.  -/
WeierstrassCurve.Jacobian.add : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → (Fin 3 → R) → Fin 3 → R
-- Mathlib.Order.RelSeries
/-- The longest `<`-series when a type is finite dimensional  -/
LTSeries.longestOf : (α : Type u_1) → [inst : Preorder α] → [FiniteDimensionalOrder α] → LTSeries α
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inr_desc_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : K ⟶ M) (β : L ⟶ M) (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i)
      ((CategoryTheory.Limits.biprod.desc α β).f i) =
    β.f i
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_le : ∀ {a b : ISize}, a ≤ b → a.toNatClampNeg ≤ b.toNatClampNeg
-- Init.Data.BitVec.Bitblast
BitVec.msb_sub : ∀ {w : ℕ} {x y : BitVec w}, (x - y).msb = (x.msb ^^ ((~~~y + 1#w).msb ^^ BitVec.carry (w - 1 - 0) x (~~~y + 1#w) false))
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.ker_le_ker_completion : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H), (NormedAddCommGroup.toCompl.comp (NormedAddGroupHom.incl f.ker)).range ≤ f.completion.ker
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.Nil.hcongr_5 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (v : V) (v' : V'),
          v ≍ v' → ∀ (w : V) (w' : V'), w ≍ w' → ∀ (a : G.Walk v w) (a' : G'.Walk v' w'), a ≍ a' → a.Nil ≍ a'.Nil
-- Aesop.Search.Queue
Aesop.FIFOQueue.mk.injEq : ∀ (goals : Array Aesop.GoalRef) (pos : ℕ) (goals_1 : Array Aesop.GoalRef) (pos_1 : ℕ),
  ({ goals := goals, pos := pos } = { goals := goals_1, pos := pos_1 }) = (goals = goals_1 ∧ pos = pos_1)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
WeakDual.CharacterSpace.equivAlgHom_coe : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : CompleteSpace A]
  [inst_3 : NormedAlgebra 𝕜 A] (f : ↑(WeakDual.characterSpace 𝕜 A)), ⇑(WeakDual.CharacterSpace.equivAlgHom f) = ⇑f
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂_apply : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂) (M : Matrix n m N₂) (x : M₁) (y : M₂),
  (((Matrix.toLinearMapₛₗ₂ σ₁ b₁ b₂) M) x) y = ∑ i, ∑ j, σ₁ ((b₁.repr x) i) • (b₂.repr y) j • M i j
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.coe_const : ∀ (α : Type u_1) {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (b : β),
  ⇑(ContinuousMap.const α b) = Function.const α b
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.forget₂_grp_map_ofHom : ∀ {X Y : Type u} [inst : CommGroup X] [inst_1 : CommGroup Y] (f : X →* Y),
  (CategoryTheory.forget₂ CommGrpCat GrpCat).map (CommGrpCat.ofHom f) = GrpCat.ofHom f
-- Mathlib.Analysis.Analytic.Constructions
analyticAt_inverse_one_sub : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A], AnalyticAt 𝕜 (fun x => Ring.inverse (1 - x)) 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_swap_mul_of_covariant_mul : ∀ (N : Type u_2) (r : N → N → Prop) [inst : CommSemigroup N] [CovariantClass N N (fun x1 x2 => x1 * x2) r],
  CovariantClass N N (Function.swap fun x1 x2 => x1 * x2) r
-- Mathlib.Analysis.Calculus.Deriv.Linear
ContinuousLinearMap.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →L[𝕜] F), HasDerivAt (⇑e) (e 1) x
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (A : Matrix m n α) (x y : n → α), A.mulVec (x + y) = A.mulVec x + A.mulVec y
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- The area form on an oriented real inner product space of dimension 2 can be evaluated in terms
of a complex-number representation of the space.  -/
Orientation.areaForm_map_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ),
  (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
    ∀ (x y : E), (o.areaForm x) y = ((starRingEnd ℂ) (f x) * f y).im
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.mk : {aig : Std.Sat.AIG ℕ} →
  (cnf : Std.Sat.CNF ℕ) →
    Std.Sat.AIG.toCNF.Cache✝ aig cnf → Std.Sat.AIG.toCNF.State.Inv✝ aig cnf → Std.Sat.AIG.toCNF.State✝ aig
-- Lean.Elab.Tactic.Conv.Simp
Lean.Elab.Tactic.Conv.applySimpResult : Lean.Meta.Simp.Result → Lean.Elab.Tactic.TacticM Unit
-- Lean.Elab.Match
Lean.Elab.Term.Discr.mk : Lean.Expr → Option Lean.Syntax → Lean.Elab.Term.Discr
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- Ioc version of `coe_eq_coe_iff_of_mem_Ico`.  -/
AddCircle.coe_eq_coe_iff_of_mem_Ioc : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  {a : 𝕜} [Archimedean 𝕜] {x y : 𝕜}, x ∈ Set.Ioc a (a + p) → y ∈ Set.Ioc a (a + p) → (↑x = ↑y ↔ x = y)
-- Mathlib.RingTheory.RingHom.Bijective
RingHom.Bijective.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
-- Lean.Meta.Tactic.ElimInfo
_private.Lean.Meta.Tactic.ElimInfo.0.Lean.Meta.addImplicitTargets.collect : Lean.Meta.ElimInfo →
  Array Lean.Expr →
    Lean.Expr → ℕ → ℕ → Array Lean.MVarId → Array Lean.Expr → Lean.MetaM (Array Lean.MVarId × Array Lean.Expr)
-- Mathlib.Data.Finset.Basic
/-- **Alias** of the reverse direction of `List.toFinset_nonempty_iff`. -/
List.Aesop.toFinset_nonempty_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l ≠ [] → l.toFinset.Nonempty
-- Batteries.Data.Fin.Coding
Fin.encodeQuotient_decodeQuotient : ∀ {n : ℕ} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s] (x : Fin (Fin.countP fun i => decide (Fin.getRepr s i = i))),
  Fin.encodeQuotient s (Fin.decodeQuotient s x) = x
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : TopologicalSpace.Opens X) (hs : Nonempty ↥s),
  ↑(s.openPartialHomeomorphSubtypeCoe hs) = Subtype.val
-- Init.Data.ByteArray.Basic
/-- True if the position is not zero.  -/
ByteArray.Iterator.hasPrev : ByteArray.Iterator → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] {P : C} (p : (b : β) → f b ⟶ P) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.desc p) = p b
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.mem_of_inv_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : DivisionRing S] [inst_2 : Algebra R S] {x : S}
  {A : Subalgebra R S}, IsIntegral R x → x⁻¹ ∈ A → x ∈ A