mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_7 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.neg with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_7 a
-- Mathlib.Order.Monotone.Basic
antitoneOn_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instIsArithmeticAdjoinNegOne : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic], 𝒢.adjoinNegOne.IsArithmetic
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_mul_of_one_mem : ∀ {α : Type u_2} [inst : Monoid α] {t : Set α}, 1 ∈ t → Set.univ * t = Set.univ
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.vcomp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ ι : F ⟶ G} (Γ : CategoryTheory.Oplax.OplaxTrans.Modification η θ)
  (Δ : CategoryTheory.Oplax.OplaxTrans.Modification θ ι) (a : B),
  (Γ.vcomp Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_right_strictMono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : WithTop α} [inst_2 : Preorder α]
  [PosMulStrictMono α], 0 < a → a ≠ ⊤ → StrictMono fun x => a * x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (p p_1 : X ⟶ X') (e_p : p = p_1) (q q_1 : Y ⟶ Y') (e_q : q = q_1)
  (w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f'),
  CategoryTheory.Limits.kernel.map f f' p q w = CategoryTheory.Limits.kernel.map f f' p_1 q_1 ⋯
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_one : UInt32.toBitVec 1 = 1#32
-- Mathlib.Logic.Relation
Relation.comp_iff : ∀ {α : Type u_1} {r : α → Prop → Prop}, (Relation.Comp r fun x1 x2 => x1 ↔ x2) = r
-- Init.Data.String.Defs
String.Pos.Raw.byteIdx_slice_add : ∀ {s : String.Slice} {p : String.Pos.Raw}, (s + p).byteIdx = s.utf8ByteSize + p.byteIdx
-- Lean.Elab.Term.TermElabM
/-- Append the argument name (if available) to the message.
Remark: if the argument name contains macro scopes we do not append it.  -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.MVarErrorInfo.logError.addArgName : Lean.Elab.Term.MVarErrorInfo → Lean.MessageData → optParam String "" → Lean.Elab.TermElabM Lean.MessageData
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insertWith.valid : ∀ {α : Type u_1} [inst : Preorder α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : DecidableLE α] (f : α → α) (x : α),
  (∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) → ∀ {t : Ordnode α}, t.Valid → (Ordnode.insertWith f x t).Valid
-- Mathlib.Data.PNat.Xgcd
/-- This is the main reduction step, which is used when u.r ≠ 0, or
equivalently b does not divide a.  -/
PNat.XgcdType.step : PNat.XgcdType → PNat.XgcdType
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt64HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- Infimum of a collection of additive group topologies  -/
AddGroupTopology.instInfSet : {α : Type u} → [inst : AddGroup α] → InfSet (AddGroupTopology α)
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.ipv4.sizeOf_spec : ∀ (ipv4 : Std.Net.IPv4Addr), sizeOf (Std.Http.URI.Host.ipv4 ipv4) = 1 + sizeOf ipv4
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filterMap.congr_simp : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] (f f_1 : (a : α) → β a → Option (γ a)),
  f = f_1 → ∀ (m m_1 : Std.ExtDHashMap α β), m = m_1 → Std.ExtDHashMap.filterMap f m = Std.ExtDHashMap.filterMap f_1 m_1
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
/-- The condition on pre-`0`-hypercovers for every object.  -/
CategoryTheory.PreZeroHypercoverFamily.property : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.PreZeroHypercoverFamily C →
      ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X)
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.pack.match_1.congr_eq_2 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (x : Float.Model.UnpackedFloat)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos))
  (s : Float.Model.UnpackedFloat.Sign),
  x = Float.Model.UnpackedFloat.infinity s →
    (match x with
      | Float.Model.UnpackedFloat.notANumber => h_1 ()
      | Float.Model.UnpackedFloat.infinity s => h_2 s
      | Float.Model.UnpackedFloat.zero s => h_3 s
      | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) ≍
      h_2 s
-- Init.Sym.Lemmas
Lean.Sym.UInt8.le_eq_true : ∀ (a b : UInt8), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Canonical valuation on the `WithVal v` type synonym.  -/
WithVal.valuation : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Valuation (WithVal v) Γ₀
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_sub : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [inst : CommRing R], ↑(x - y) = ↑x - ↑y
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_eq_sInf : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), I.radical = sInf {J | I ≤ J ∧ J.IsPrime}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- A functor `U : X ⥤ Y` (functorially) induces a functor
`CatCommSqOver F G Y ⥤ CatCommSqOver F G X` by whiskering left the underlying
categorical commutative square by U.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                {X : Type u₄} →
                  {Y : Type u₅} →
                    [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                      [inst_4 : CategoryTheory.Category.{v₅, u₅} Y] →
                        CategoryTheory.Functor (CategoryTheory.Functor X Y)
                          (CategoryTheory.Functor (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y)
                            (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X))
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.isAlgebraic_iff : ∀ (R : Type u_1) (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsAlgebraic R S] [FaithfulSMul R S] {a : A}, IsAlgebraic R a ↔ IsAlgebraic S a
-- Lean.MetavarContext
Lean.MetavarDecl.mk.injEq : ∀ (userName : Lean.Name) (lctx : Lean.LocalContext) (type : Lean.Expr) (depth : ℕ)
  (localInstances : Lean.LocalInstances) (kind : Lean.MetavarKind) (numScopeArgs index : ℕ) (userName_1 : Lean.Name)
  (lctx_1 : Lean.LocalContext) (type_1 : Lean.Expr) (depth_1 : ℕ) (localInstances_1 : Lean.LocalInstances)
  (kind_1 : Lean.MetavarKind) (numScopeArgs_1 index_1 : ℕ),
  ({ userName := userName, lctx := lctx, type := type, depth := depth, localInstances := localInstances, kind := kind,
        numScopeArgs := numScopeArgs, index := index } =
      { userName := userName_1, lctx := lctx_1, type := type_1, depth := depth_1, localInstances := localInstances_1,
        kind := kind_1, numScopeArgs := numScopeArgs_1, index := index_1 }) =
    (userName = userName_1 ∧
      lctx = lctx_1 ∧
        type = type_1 ∧
          depth = depth_1 ∧
            localInstances = localInstances_1 ∧ kind = kind_1 ∧ numScopeArgs = numScopeArgs_1 ∧ index = index_1)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR_go_eq : ∀ {α : Type u_1} {a : α} {acc : Array α} (i : ℕ) (l : List α),
  List.insertIdxTR.go✝ a i l acc = acc.toList ++ l.insertIdx i a
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcompPostcompIso_hom_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} E'] {A : Type u_5} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift D A] [inst_6 : CategoryTheory.HasShift E A] [inst_7 : CategoryTheory.HasShift E' A]
  (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) (G' : CategoryTheory.Functor E E')
  [inst_8 : G.CommShift A] [inst_9 : G'.CommShift A] (a : A) (x : C),
  ((F.postcompPostcompIso G G').hom.hom a).app x =
    CategoryTheory.CategoryStruct.id (G'.obj (G.obj ((F.functor a).obj x)))
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_iff_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (Z : Set (PrimeSpectrum R)), IsClosed Z ↔ ∃ s, Z = PrimeSpectrum.zeroLocus s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.filterMap_equiv_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a},
  m.WF → (Std.DHashMap.Raw.filterMap (fun k v => some (f k v)) m).Equiv (Std.DHashMap.Raw.map f m)
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm_zero_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [_i : Fact (Module.finrank ℝ E = 0)],
  positiveOrientation.volumeForm = AlternatingMap.constLinearEquivOfIsEmpty 1
-- Mathlib.CategoryTheory.Category.RelCat
/-- The essentially surjective faithful embedding
from the category of types and functions into the category of types and relations.  -/
CategoryTheory.RelCat.graphFunctor : CategoryTheory.Functor (Type u) CategoryTheory.RelCat
-- Mathlib.Combinatorics.Quiver.Push
Quiver.Push.lift.congr_simp : ∀ {V : Type u_1} [inst : Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [inst_1 : Quiver W'] (φ φ_1 : V ⥤q W')
  (e_φ : φ = φ_1) (τ τ_1 : W → W') (e_τ : τ = τ_1) (h : ∀ (x : V), φ.obj x = τ (σ x)),
  Quiver.Push.lift σ φ τ h = Quiver.Push.lift σ φ_1 τ_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.mul_smul_self_flip_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] (X : C) [inst_3 : CategoryTheory.ModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.ModObj.smul)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h))
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.scalarTensorEquiv_tmul : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : CommMonoid M] (a : A) (p : MonoidAlgebra R M),
  (MonoidAlgebra.scalarTensorEquiv R A) (a ⊗ₜ[R] p) = a • (MonoidAlgebra.mapAlgHom M (Algebra.ofId R A)) p
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.smul_inductionOn_pointwise : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (N : Submodule R M) [inst_5 : SMulCommClass S R M] {a : S}
  {p : (x : M) → x ∈ a • N → Prop},
  (∀ (s : M) (hs : s ∈ N), p (a • s) ⋯) →
    (∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯) →
      (∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯) →
        p 0 ⋯ → ∀ {x : M} (hx : x ∈ a • N), p x hx
-- Mathlib.Data.Set.NAry
Set.image2_union_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
  Set.image2 f s (t ∪ t') = Set.image2 f s t ∪ Set.image2 f s t'
-- Mathlib.RingTheory.Morita.Matrix
/-- The linear equiv induced by the equality `toMatrixModCat (toModuleCat M) = Mⁿ`  -/
toModuleCatFromModuleCatLinearEquiv : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (M : ModuleCat (Matrix ι ι R)) → (j : ι) → ↑M ≃ₗ[Matrix ι ι R] ι → ↥(MatrixModCat.toModuleCatObj R (↑M) j)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_18 : HSub Std.Time.Minute.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Order.Bounds.Basic
isGreatest_compl : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a : α), IsGreatest {w | Disjoint w a} aᶜ
-- Mathlib.Data.Complex.Basic
Complex.exists : ∀ {p : ℂ → Prop}, (∃ x, p x) ↔ ∃ a b, p { re := a, im := b }
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.tensorCotangentInvFun.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {P : Algebra.Extension R S}
  {Q : Algebra.Extension R T} (f f_1 : P.Hom Q) (e_f : f = f_1) [alg : Algebra P.Ring Q.Ring]
  (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
  (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))),
  Algebra.Extension.tensorCotangentInvFun f halg H = Algebra.Extension.tensorCotangentInvFun f_1 ⋯ ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rco : ∀ {m n i fallback : ℕ}, (m...n).toList.getD i fallback = if i < n - m then m + i else fallback
-- Mathlib.Data.ENNReal.Inv
/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.

See `ENNReal.mul_iInf'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`, and `ENNReal`.  -/
ENNReal.mul_iInf_of_ne : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a * ⨅ i, f i = ⨅ i, a * f i
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_one_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  Int.fract (1 + a) = Int.fract a
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- An isomorphism of rings induces an isomorphism of residue fields.  -/
Ideal.residueFieldAlgEquiv : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (J : Ideal A) →
                  (K : Ideal B) →
                    [inst_5 : J.IsPrime] →
                      [inst_6 : K.IsPrime] → (f : A ≃ₐ[R] B) → J = Ideal.comap f K → J.ResidueField ≃ₐ[R] K.ResidueField
-- Lean.MetavarContext
Lean.MetavarDecl.localInstances : Lean.MetavarDecl → Lean.LocalInstances
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.map_map_right : ∀ {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] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X Y : CategoryTheory.Comma L R} (φ : X ⟶ Y),
  ((CategoryTheory.Comma.map α β).map φ).right = F₂.map φ.right
-- Init.Data.Dyadic.Basic
/-- Returns the dyadic number representation of `i * 2 ^ (-exp)`.  -/
Dyadic.ofIntWithPrec : ℤ → ℤ → Dyadic
-- Std.Http.Data.Body.Stream
Std.Http.Body.Stream.instNextChunkAsync : Std.Http.Body.Stream.NextChunk Std.Async.Async
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.gcd_eq_0 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (g n m a b : ℤ), g = a * n + b * m → ↑n = 0 → ↑m = 0 → ↑g = 0
-- Init.Core
Sum.nonemptyRight : ∀ {α : Type u} {β : Type v} [h : Nonempty β], Nonempty (α ⊕ β)
-- Mathlib.Order.Closure
ClosureOperator.mk.injEq : ∀ {α : Type u_1} [inst : Preorder α] (toOrderHom : α →o α) (le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x)
  (idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x) (IsClosed : α → Prop)
  (isClosed_iff : autoParam (∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x) ClosureOperator.isClosed_iff._autoParam)
  (toOrderHom_1 : α →o α) (le_closure'_1 : ∀ (x : α), x ≤ toOrderHom_1.toFun x)
  (idempotent'_1 : ∀ (x : α), toOrderHom_1.toFun (toOrderHom_1.toFun x) = toOrderHom_1.toFun x) (IsClosed_1 : α → Prop)
  (isClosed_iff_1 :
    autoParam (∀ {x : α}, IsClosed_1 x ↔ toOrderHom_1.toFun x = x) ClosureOperator.isClosed_iff._autoParam),
  ({ toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := isClosed_iff } =
      { toOrderHom := toOrderHom_1, le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
        isClosed_iff := isClosed_iff_1 }) =
    (toOrderHom = toOrderHom_1 ∧ IsClosed = IsClosed_1)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.forget_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Factorisation f),
  CategoryTheory.Factorisation.forget.obj self = self.mid
-- Mathlib.Algebra.Field.Basic
one_div_mul_sub_mul_one_div_eq_one_div_add_one_div : ∀ {K : Type u_1} [inst : DivisionRing K] {a b : K}, a ≠ 0 → b ≠ 0 → 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.symm_symm : ∀ {ι : Type u_1} (c : ComplexShape ι), c.symm.symm = c
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.ppow_succ' : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R} {k : ℕ}, f.ppow (k + 1) = f.pmul (f.ppow k)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.instIsSerreClassTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C], ⊤.IsSerreClass
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_left_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ s₃ : Finset α), s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- Given a functor `F : D ⥤ C`, zero morphisms on `C` induce zero morphisms on
`D` by taking preimages.  -/
CategoryTheory.Functor.FullyFaithful.hasZeroMorphisms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        [CategoryTheory.Limits.HasZeroMorphisms C] →
          {F : CategoryTheory.Functor D C} → F.FullyFaithful → CategoryTheory.Limits.HasZeroMorphisms D
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m), m.getKey k₁ h₁ = m.getKey k₂ ⋯
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A finite orthonormal set that spans is an orthonormal basis  -/
OrthonormalBasis.mk : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              {v : ι → E} → Orthonormal 𝕜 v → ⊤ ≤ Submodule.span 𝕜 (Set.range v) → OrthonormalBasis ι 𝕜 E
-- Mathlib.Control.Fold
Traversable.foldlm_map : ∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {m : Type u → Type u}
  [inst_2 : Monad m] [LawfulMonad m] (g : β → γ) (f : α → γ → m α) (a : α) (l : t β),
  Traversable.foldlm f a (g <$> l) = Traversable.foldlm (fun x y => f x (g y)) a l
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat.copy
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorHomEquiv.congr_simp : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂],
  CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V = CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V
-- Init.Data.SInt.Lemmas
ISize.mul_two : ∀ {a : ISize}, a * 2 = a + a
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- If `M` and `P` are semilinearly equivalent and `N` and `Q` are semilinearly equivalent
then `M ⊗ N` and `P ⊗ Q` are semilinearly equivalent.  -/
TensorProduct.congr : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {M : Type u_7} →
            {N : Type u_8} →
              {M₂ : Type u_12} →
                {N₂ : Type u_14} →
                  [inst_2 : AddCommMonoid M] →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : AddCommMonoid N₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R N] →
                              [inst_8 : Module R₂ M₂] →
                                [inst_9 : Module R₂ N₂] →
                                  {σ₂₁ : R₂ →+* R} →
                                    [inst_10 : RingHomInvPair σ₁₂ σ₂₁] →
                                      [inst_11 : RingHomInvPair σ₂₁ σ₁₂] →
                                        (M ≃ₛₗ[σ₁₂] M₂) →
                                          (N ≃ₛₗ[σ₁₂] N₂) → TensorProduct R M N ≃ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.coe_mul : ∀ {α : Type u} [inst : Mul α] (a b : α), ↑(a * b) = ↑a * ↑b