mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If the (product-like) biproduct comparison for `F` and `f` is a monomorphism, then `F`
preserves the biproduct of `f`. For the converse, see `mapBiproduct`.  -/
CategoryTheory.Limits.preservesBiproduct_of_mono_biproductComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C}
  [inst_6 : CategoryTheory.Limits.HasBiproduct f] [inst_7 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)]
  [CategoryTheory.Mono (F.biproductComparison f)], CategoryTheory.Limits.PreservesBiproduct f F
-- Mathlib.LinearAlgebra.Matrix.Module
Matrix.Module.single_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (i j : ι) (r : R) (v : ι → M),
  Matrix.single i j r • v = Pi.single i (r • v j)
-- Mathlib.Data.EReal.Basic
/-- The order embedding of `ℝ` into `EReal`.  -/
EReal.orderEmbedding : ℝ ↪o EReal
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRight_obj_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRight L r hr).obj X).hom =
    CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)
-- Lean.Util.Diff
/-- Given two `Subarray`s, find their common suffix and return their differing prefixes  -/
Lean.Diff.matchSuffix : {α : Type u_1} → [BEq α] → Subarray α → Subarray α → Subarray α × Subarray α × Array α
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.toMethodsRef : Lean.Meta.Sym.DSimp.Methods → Lean.Meta.Sym.DSimp.MethodsRef
-- Init.Data.Int.Order
Int.le_add_of_nonneg_left : ∀ {a b : ℤ}, 0 ≤ b → a ≤ b + a
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.snd_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C × D), (CategoryTheory.Prod.snd C D).obj X = X.2
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.substAssignedUVars.go : Array (Option Lean.Level) → Lean.Level → Lean.Level
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {v : β k},
      Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) = true →
        compare k a ≠ Ordering.eq → Std.DTreeMap.Internal.Impl.contains a t = true
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.val_assemble₂_le : ∀ {w x : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₂ w x = some c → c.val ≤ 2047
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.instInv.eq_1 : ∀ {M : Type u_1},
  Mathlib.Tactic.FieldSimp.NF.instInv =
    {
      inv := fun l =>
        List.map
          (fun x =>
            match x with
            | (a, x) => (-a, x))
          l }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).isEmpty = t.isEmpty
-- Std.Time.Format.Modifier
Std.Time.instReprYear : Repr Std.Time.Year
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- We get a Galois insertion between `σ`-algebras on `α` and `Set (Set α)` by using `generate_from`
on one side and the collection of measurable sets on the other side.  -/
MeasurableSpace.giGenerateFrom : {α : Type u_1} → GaloisInsertion MeasurableSpace.generateFrom fun m => {t | MeasurableSet t}
-- Batteries.Data.List.Interleave
List.interleave.eq_2 : ∀ {α : Type u_1} (x : List α) (a : α) (l₁ : List α), (a :: l₁).interleave x = a :: x.interleave l₁
-- Init.Data.List.Basic
List.range'TR.go.eq_def : ∀ (step a a_1 : ℕ) (a_2 : List ℕ),
  List.range'TR.go step a a_1 a_2 =
    match a, a_1, a_2 with
    | 0, x, acc => acc
    | n.succ, e, acc => List.range'TR.go step n (e - step) ((e - step) :: acc)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'_add_left : ∀ (z τ : ℂ), jacobiTheta₂' (z + 1) τ = jacobiTheta₂' z τ
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instIsStableUnderRetractsOverCofibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts],
  (HomotopicalAlgebra.cofibrations (CategoryTheory.Over S)).IsStableUnderRetracts
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- **Alias** of `CategoryTheory.MorphismProperty.overPullbackMap`. -/
CategoryTheory.MorphismProperty.baseChange_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullbacksAlong f]
  {X Y : CategoryTheory.Over S} (g : X ⟶ Y),
  P (CategoryTheory.Over.Hom.left g) → P (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map g))
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.mem_perpBisector_iff_inner_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
  c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ inner ℝ (c -ᵥ p₁) (p₂ -ᵥ p₁) = dist p₁ p₂ ^ 2 / 2
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getThenInsertIfNew?_fst : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF → ∀ {k : α} {v : β}, (Std.DHashMap.Raw.Const.getThenInsertIfNew? m k v).1 = Std.DHashMap.Raw.Const.get? m k
-- Mathlib.Order.UpperLower.Prod
UpperSet.mem_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β} {s : UpperSet α} {t : UpperSet β},
  x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuousWithinAt_singleton_iff`. -/
ContinuousWithinAt.upperHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → UpperHemicontinuousWithinAt (fun x => {f x}) s x
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.mk.injEq : ∀ (content : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (priorParts : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
  (context : Array Lean.VersoModuleDocs.DocFrame✝) (content_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (priorParts_1 : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
  (context_1 : Array Lean.VersoModuleDocs.DocFrame✝),
  ({ content := content, priorParts := priorParts, context := context } =
      { content := content_1, priorParts := priorParts_1, context := context_1 }) =
    (content = content_1 ∧ priorParts = priorParts_1 ∧ context = context_1)
-- Mathlib.Condensed.Discrete.Module
/-- `CompHausLike.LocallyConstantModule.functorToPresheaves` lands in sheaves.  -/
CompHausLike.LocallyConstantModule.functor : {P : TopCat → Prop} →
  (R : Type (max u w)) →
    [inst : Ring R] →
      [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
        [inst_2 : CompHausLike.HasExplicitPullbacks P] →
          (hs :
              ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
                CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
            CategoryTheory.Functor (ModuleCat R)
              (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (ModuleCat R))
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_apply_eq_div : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : DivisionRing 𝔸] [inst_2 : Algebra 𝕂 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] (x : 𝔸) (n : ℕ),
  ((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = x ^ n / ↑n.factorial
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsEquivOfQuotEquiv.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f f_1 : R ⧸ I ≃+* A ⧸ J),
  f = f_1 → IsDedekindDomain.idealFactorsEquivOfQuotEquiv f = IsDedekindDomain.idealFactorsEquivOfQuotEquiv f_1
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
_private.Mathlib.Combinatorics.SetFamily.KruskalKatona.0.Finset.UV.UsefulCompression.instDecidableRel : {α : Type u_1} → [inst : LinearOrder α] → DecidableRel Finset.UV.UsefulCompression✝
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rii.isEmpty.eq_1 : ∀ {α : Type u} [inst : Std.PRange.Least? α] (x : Std.Rii α), x.isEmpty = Std.PRange.least?.isNone
-- Init.Data.BitVec.Bitblast
BitVec.not_sub_eq_not_add : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x - y) = ~~~x + y
-- Mathlib.Topology.Algebra.Group.Basic
IsClosed.rightCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {U : Set G},
  IsClosed U → ∀ (x : G), IsClosed (MulOpposite.op x • U)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndAdjunction_unit_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b),
  (CategoryTheory.Comma.costructuredArrowSndAdjunction L R b).unit.app X =
    CategoryTheory.CostructuredArrow.homMk
      { left := CategoryTheory.CategoryStruct.id X.left.left, right := X.hom, w := ⋯ } ⋯
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.copy_eq : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] (S : NonUnitalStarSubsemiring R) (s : Set R)
  (hs : s = ↑S), S.copy s hs = S
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- A local algebra homomorphism induces an algebra homomorphism on the residue fields.

See `mapAlgHom'` for a variant where the base ring `R` is also quotiented.  -/
IsLocalRing.ResidueField.mapAlgHom : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : IsLocalRing S] →
            [inst_3 : CommRing T] →
              [inst_4 : IsLocalRing T] →
                [inst_5 : Algebra R S] →
                  [inst_6 : Algebra R T] →
                    (e : S →ₐ[R] T) → [IsLocalHom e] → IsLocalRing.ResidueField S →ₐ[R] IsLocalRing.ResidueField T
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.compUnit.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b}
  (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂),
  adj₁.compUnit adj₂ =
    CategoryTheory.bicategoricalComp adj₁.unit
      (CategoryTheory.bicategoricalComp
        (CategoryTheory.Bicategory.whiskerLeft f₁ (CategoryTheory.Bicategory.whiskerRight adj₂.unit g₁))
        (CategoryTheory.CategoryStruct.id
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f₁ f₂)
            (CategoryTheory.CategoryStruct.comp g₂ g₁))))
-- Mathlib.Algebra.Group.Pi.Basic
Function.comp_ne_one_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : One β] [inst_1 : One γ] (f : α → β) {g : β → γ},
  Function.Injective g → g 1 = 1 → (g ∘ f ≠ 1 ↔ f ≠ 1)
-- Init.Data.SInt.Lemmas
Int32.toInt64_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int32.maxValue.toInt → (Int32.ofNat n).toInt64 = Int64.ofNat n
-- Mathlib.Algebra.Group.Ext
LeftCancelMonoid.ext_iff : ∀ {M : Type u} {m₁ m₂ : LeftCancelMonoid M}, m₁ = m₂ ↔ HMul.hMul = HMul.hMul
-- Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb : ∀ (X : AlgebraicGeometry.Scheme),
  CategoryTheory.IsGrothendieckAbelian.{u + 1, u + 1, u + 2}
    (CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.ProEt.topology X) Ab)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_nil_iff : ∀ {m n : ℕ}, (m...=n).toList = [] ↔ n < m
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.nonempty_algHom_iff_finrank_dvd : ∀ {F : Type u_3} {K : Type u_4} {L : Type u_5} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [inst_3 : Field L] [inst_4 : Algebra F L] [Finite L], Nonempty (K →ₐ[F] L) ↔ Module.finrank F K ∣ Module.finrank F L
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.proved.inj : ∀ {steps? steps?_1 : Option (Array Aesop.Script.LazyStep)},
  Aesop.NormRuleResult.proved steps? = Aesop.NormRuleResult.proved steps?_1 → steps? = steps?_1
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.BisimO.imp : ∀ {α : Type u} {R S : Stream'.WSeq α → Stream'.WSeq α → Prop},
  (∀ (s t : Stream'.WSeq α), R s t → S s t) →
    ∀ {o p : Option (α × Stream'.WSeq α)}, Stream'.WSeq.BisimO R o p → Stream'.WSeq.BisimO S o p
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.domRestrict_apply : ∀ {M : Type u_1} {σ : Type u_4} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] [inst_2 : SetLike σ M]
  [inst_3 : MulMemClass σ M] (f : M →ₙ* N) {S : σ} (x : ↥S), (f.domRestrict S) x = f ↑x
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.cokernelSequence_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.cokernelSequence f).Exact
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_nonempty : ∀ {G : Type u_1} [inst : AddGroup G] (s : AddSubgroup G), (↑s).Nonempty
-- Mathlib.Topology.EMetricSpace.Basic
/-- The triangle (polygon) inequality for sequences of points; `Finset.range` version.  -/
edist_le_range_sum_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (f : ℕ → α) (n : ℕ),
  edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.right_unitality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom)
      (CategoryTheory.CategoryStruct.comp (self.μIso X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))
-- Mathlib.Algebra.Order.Archimedean.Basic
le_of_forall_lt_rat_imp_le : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  (∀ (q : ℚ), y < ↑q → x ≤ ↑q) → x ≤ y
-- Batteries.Data.Fin.Lemmas
Fin.get_findRev?_maximal : ∀ {n : ℕ} {p : Fin n → Bool} (h : (Fin.findRev? p).isSome = true) (j : Fin n), (Fin.findRev? p).get h < j → p j = false
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.compIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasEqualizers C] [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.IsIso g],
  CategoryTheory.Limits.image.compIso f g =
    {
      hom :=
        CategoryTheory.Limits.image.lift
          (CategoryTheory.Limits.Image.monoFactorisation (CategoryTheory.CategoryStruct.comp f g)).ofCompIso,
      inv := CategoryTheory.Limits.image.lift ((CategoryTheory.Limits.Image.monoFactorisation f).compMono g),
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.image_eq : ∀ {Δ Δ' Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ Δ'} [CategoryTheory.Epi e] {i : Δ' ⟶ Δ''} [CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = φ → CategoryTheory.Limits.image φ = Δ'
-- Mathlib.Algebra.Homology.Homotopy
/-- the scalar multiplication of a homotopy  -/
Homotopy.smul : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            {f g : C ⟶ D} →
              {R : Type u_2} →
                [inst_2 : Semiring R] →
                  [inst_3 : CategoryTheory.Linear R V] → Homotopy f g → (a : R) → Homotopy (a • f) (a • g)
-- Init.Data.Nat.Lemmas
Nat.dvd_div_of_mul_dvd : ∀ {a b c : ℕ}, a * b ∣ c → b ∣ c / a
-- Mathlib.Analysis.Normed.Group.Ultra
/-- In an additive group with an ultrametric norm, closed balls around 0 of positive
radius are open subgroups.  -/
IsUltrametricDist.closedBall_openAddSubgroup : (S : Type u_1) → [inst : SeminormedAddGroup S] → [IsUltrametricDist S] → {r : ℝ} → 0 < r → OpenAddSubgroup S
-- Lean.Compiler.LCNF.Types
/-- `usize` represents the C `size_t` type. It has a separate representation because depending on the
target architecture it has a different width and we try to generate platform independent C code.

We generally assume that `sizeof(size_t) == sizeof(void)`.
 -/
Lean.Compiler.LCNF.ImpureType.usize : Lean.Expr
-- Init.Data.Int.Order
Int.le_neg_add_of_add_le : ∀ {a b c : ℤ}, a + b ≤ c → b ≤ -a + c
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_singleton_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {x y : P} {I : FractionalIdeal S P},
  y ∈ FractionalIdeal.spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.vadd : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} (a : M), IsSemilinearSet s → IsSemilinearSet (a +ᵥ s)
-- Init.Data.Vector.Lemmas
Vector.getElem_replace : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {n : ℕ} {a b : α} {xs : Vector α n} {i : ℕ} (h : i < n),
  (xs.replace a b)[i] = if (xs[i] == a) = true then if a ∈ xs.take i then a else b else xs[i]
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The setoid corresponding to commutative expressions modulo monoid Relations and identifications.
 -/
CommRingCat.Colimits.colimitSetoid : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → Setoid (CommRingCat.Colimits.Prequotient F)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- Both diagonal entries of an invertible lower-block-triangular matrix are invertible (by reading
off the diagonal entries of the inverse).  -/
Matrix.invertibleOfFromBlocksZero₁₂Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (C : Matrix n m α) →
                    (D : Matrix n n α) → [Invertible (Matrix.fromBlocks A 0 C D)] → Invertible A × Invertible D
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.toDual.congr_simp : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (B B_1 : LinearMap.BilinForm K V) (e_B : B = B_1) (b : B.Nondegenerate),
  B.toDual b = B_1.toDual ⋯
-- Mathlib.Order.SuccPred.Basic
Order.succ_lt_succ_iff_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  ¬IsMax a → ¬IsMax b → (Order.succ a < Order.succ b ↔ a < b)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zeta_prod_mk : ∀ (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : DecidableLE α] [inst_4 : DecidableLE β] (a₁ a₂ : α) (b₁ b₂ : β),
  (IncidenceAlgebra.zeta 𝕜) (a₁, b₁) (a₂, b₂) = (IncidenceAlgebra.zeta 𝕜) a₁ a₂ * (IncidenceAlgebra.zeta 𝕜) b₁ b₂
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_sInf_le : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set (Set M)),
  Submodule.span R (⋂₀ s) ≤ sInf (Submodule.span R '' s)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instInhabitedTacticParsedSnapshot : Inhabited Lean.Elab.Tactic.TacticParsedSnapshot
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a basemap
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.  -/
ContinuousWithinAt.clm_bundle_apply₂ : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)]
  {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)]
  [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)]
  [inst_19 : TopologicalSpace B] [inst_20 : TopologicalSpace M] [inst_21 : FiberBundle F₁ E₁]
  [inst_22 : VectorBundle 𝕜 F₁ E₁] [inst_23 : FiberBundle F₂ E₂] [inst_24 : VectorBundle 𝕜 F₂ E₂]
  [inst_25 : FiberBundle F₃ E₃] [inst_26 : VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M}
  {x : M} [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₃ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
  {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)},
  ContinuousWithinAt (fun m => ⟨b m, ψ m⟩) s x →
    ContinuousWithinAt (fun m => ⟨b m, v m⟩) s x →
      ContinuousWithinAt (fun m => ⟨b m, w m⟩) s x → ContinuousWithinAt (fun m => ⟨b m, ⋯ (w m)⟩) s x
-- Init.Data.BitVec.Lemmas
BitVec.udiv_self : ∀ {w : ℕ} {x : BitVec w}, x / x = if (x == 0#w) = true then 0#w else 1#w
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisRight.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq κ]
  (𝒞 : Module.Basis κ R N),
  TensorProduct.equivFinsuppOfBasisRight 𝒞 =
    (LinearEquiv.lTensor M 𝒞.repr).trans (TensorProduct.finsuppScalarRight R R M κ)