mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- The mates equivalence commutes with composition of squares of squares. These results form the
basis for an isomorphism of double categories to be proven later.
 -/
CategoryTheory.mateEquiv_square : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} {X : Type u₇} {Y : Type u₈}
  {Z : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] [inst_3 : CategoryTheory.Category.{v₄, u₄} D]
  [inst_4 : CategoryTheory.Category.{v₅, u₅} E] [inst_5 : CategoryTheory.Category.{v₆, u₆} F]
  [inst_6 : CategoryTheory.Category.{v₇, u₇} X] [inst_7 : CategoryTheory.Category.{v₈, u₈} Y]
  [inst_8 : CategoryTheory.Category.{v₉, u₉} Z] {G₁ : CategoryTheory.Functor A D} {H₁ : CategoryTheory.Functor B E}
  {K₁ : CategoryTheory.Functor C F} {G₂ : CategoryTheory.Functor D X} {H₂ : CategoryTheory.Functor E Y}
  {K₂ : CategoryTheory.Functor F Z} {L₁ : CategoryTheory.Functor A B} {R₁ : CategoryTheory.Functor B A}
  {L₂ : CategoryTheory.Functor B C} {R₂ : CategoryTheory.Functor C B} {L₃ : CategoryTheory.Functor D E}
  {R₃ : CategoryTheory.Functor E D} {L₄ : CategoryTheory.Functor E F} {R₄ : CategoryTheory.Functor F E}
  {L₅ : CategoryTheory.Functor X Y} {R₅ : CategoryTheory.Functor Y X} {L₆ : CategoryTheory.Functor Y Z}
  {R₆ : CategoryTheory.Functor Z Y} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (adj₄ : L₄ ⊣ R₄) (adj₅ : L₅ ⊣ R₅)
  (adj₆ : L₆ ⊣ R₆) (α : CategoryTheory.TwoSquare G₁ L₁ L₃ H₁) (β : CategoryTheory.TwoSquare H₁ L₂ L₄ K₁)
  (γ : CategoryTheory.TwoSquare G₂ L₃ L₅ H₂) (δ : CategoryTheory.TwoSquare H₂ L₄ L₆ K₂),
  (CategoryTheory.mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α.vComp β).hComp (γ.vComp δ)) =
    (((CategoryTheory.mateEquiv adj₂ adj₄) β).hComp ((CategoryTheory.mateEquiv adj₁ adj₃) α)).vComp
      (((CategoryTheory.mateEquiv adj₄ adj₆) δ).hComp ((CategoryTheory.mateEquiv adj₃ adj₅) γ))
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_1.eq_3 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → ℕ → Sort u_1) (a' : ONote) (h_1 : Unit → motive (Sum.inl none) 0)
  (h_2 : (m : ℕ) → motive (Sum.inl none) m.succ) (h_3 : (a' : ONote) → motive (Sum.inl (some a')) 0)
  (h_4 : (a' : ONote) → (m : ℕ) → motive (Sum.inl (some a')) m.succ) (h_5 : (f : ℕ → ONote) → motive (Sum.inr f) 0)
  (h_6 : (f : ℕ → ONote) → (m : ℕ) → motive (Sum.inr f) m.succ),
  (match Sum.inl (some a'), 0 with
    | Sum.inl none, 0 => h_1 ()
    | Sum.inl none, m.succ => h_2 m
    | Sum.inl (some a'), 0 => h_3 a'
    | Sum.inl (some a'), m.succ => h_4 a' m
    | Sum.inr f, 0 => h_5 f
    | Sum.inr f, m.succ => h_6 f m) =
    h_3 a'
-- Mathlib.Order.ModularLattice
IsWeakUpperModularLattice.mk : ∀ {α : Type u_2} [inst : Lattice α], (∀ {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b) → IsWeakUpperModularLattice α
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- The constant augmented simplicial object has an extra degeneracy.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X : C) → (CategoryTheory.SimplicialObject.Augmented.const.obj X).ExtraDegeneracy
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.forgetCocone_ι_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T)
  (self : CategoryTheory.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X)),
  (CategoryTheory.Over.forgetCocone X).ι.app self = self.hom
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f g : X ⟶ Y),
  f = g ↔ ∃ (h₁ : f.f = g.f), ∀ (i : X.I), CategoryTheory.CategoryStruct.comp (f.φ i) (CategoryTheory.eqToHom ⋯) = g.φ i
-- Mathlib.Probability.Independence.Kernel.Indep
/-- A family of sets of sets `π : ι → Set (Set Ω)` is independent with respect to a kernel `κ` and
a measure `μ` if for any finite set of indices `s = {i_1, ..., i_n}`, for any sets
`f i_1 ∈ π i_1, ..., f i_n ∈ π i_n`, then `∀ᵐ a ∂μ, κ a (⋂ i in s, f i) = ∏ i ∈ s, κ a (f i)`.
It will be used for families of π-systems.  -/
ProbabilityTheory.Kernel.iIndepSets : {α : Type u_1} →
  {Ω : Type u_2} →
    {ι : Type u_3} →
      {_mα : MeasurableSpace α} →
        {_mΩ : MeasurableSpace Ω} →
          (ι → Set (Set Ω)) →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.iIndepSets._auto_1 → Prop
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.comp_inv_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : Y ⟶ X) [inst_1 : CategoryTheory.IsIso α]
  {f : Z ⟶ X} {g : Z ⟶ Y},
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) = g ↔ f = CategoryTheory.CategoryStruct.comp g α
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.πObj_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {f g : CategoryTheory.Arrow C} (φ : f ⟶ g) {Z : C} (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.objMap I κ φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ g.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right φ) h)
-- Mathlib.Algebra.Module.LinearMap.Defs
AddMonoidHom.coe_toIntLinearMap : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] (f : M →+ M₂),
  ⇑f.toIntLinearMap = ⇑f
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (f g : X ⟶ Y),
  f.left = g.left → f = g
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (curr : ℕ) (h_1 : Unit → motive 0) (h_2 : (curr : ℕ) → motive curr.succ),
  (match curr.succ with
    | 0 => h_1 ()
    | curr.succ => h_2 curr) =
    h_2 curr
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
/-- `midpoint` does not depend on the ring `R`.  -/
midpoint_unique : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (R' : Type u_6) [inst_5 : Ring R'] [inst_6 : Invertible 2]
  [inst_7 : Module R' V] (x y : P), midpoint R x y = midpoint R' x y
-- Init.Data.Vector.Lemmas
Vector.back_pop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} [h : NeZero (n - 1)], xs.pop.back = xs[n - 2]
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Discharges assumptions of the form `∀ …, a = b` using `rfl`. This is particularly useful for higher
order assumptions of the form `∀ …, e = ?g x y` to instantiate a parameter `g` even if that does not
appear on the lhs of the rule.
 -/
Lean.Meta.Simp.dischargeRfl : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp h.p h.opcyclesIso.inv = S.pOpcycles
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_mcast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {a b : ℤ} {Γ' : Subgroup (GL (Fin 2) ℝ)} (heq : a = b) (hΓ : Γ' = Γ)
  (f : ModularForm Γ a), UpperHalfPlane.qExpansion h ⇑(ModularForm.mcast heq f hΓ) = UpperHalfPlane.qExpansion h ⇑f
-- Init.Data.String.Search
/-- Interprets a string as the decimal representation of a natural number, returning it. Panics if the
slice does not contain a decimal natural number.

A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
it are digits.

Use `isNat` to check whether `toNat!` would return a value. `toNat?` is a safer
alternative that returns `none` instead of panicking when the string is not a natural number.

Examples:

* `"0".toNat! = 0`

* `"5".toNat! = 5`

* `"587".toNat! = 587`
 -/
String.toNat! : String → ℕ
-- Mathlib.Topology.Order.DenselyOrdered
interior_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] [NoMaxOrder α] {a b : α}, interior (Set.Icc a b) = Set.Ioo a b
-- Lean.Meta.ArgsPacker
/-- Given unary types `(x : Aᵢ) → Rᵢ[x]`, and `(x : A₁ ⊕ A₂ …)`, calculate the packed codomain
```
match x with | inl x₁ => R₁[x₁] | inr x₂ => R₂[x₂] | …
```
This function assumes (and does not check) that `Rᵢ` all have the same level.
 -/
Lean.Meta.ArgsPacker.Mutual.mkCodomain : Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Icc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a : α i), Function.update f i '' Set.Icc a (f i) = Set.Icc (Function.update f i a) f
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_le : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b c : G),
  |a / c|ₘ ≤ |a / b|ₘ * |b / c|ₘ
-- Mathlib.Order.SuccPred.Limit
PredOrder.colimitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (isMin : (a : α) → IsMax a → motive a)
  (succ : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isSuccLimit : (a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a),
  PredOrder.colimitRecOn b isMin succ isSuccLimit =
    PredOrder.prelimitRecOn b succ fun a ha IH => if h : IsMax a then isMin a h else isSuccLimit a ⋯ IH
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false ↔ ∃ a, t.contains a = true
-- Mathlib.Algebra.Homology.DerivedCategory.KProjective
CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  {n : ℤ}
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  [inst_3 : K.IsKProjective]
  (b : CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n),
  CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective.symm b = Function.surjInv ⋯ b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.mk_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  (Q : CategoryTheory.MorphismProperty C) {F : CategoryTheory.Functor C D} {X : D} {A : C} (f : F.obj A ⟶ X) (hf : P f),
  (CategoryTheory.MorphismProperty.CostructuredArrow.mk Q f hf).hom = f
-- Mathlib.Algebra.Group.Shrink
Shrink.instIsCancelMul : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Mul α] [IsCancelMul α], IsCancelMul (Shrink.{v, u_2} α)
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instDecidableEqOffset : DecidableEq Std.Time.TimeZone.Offset
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Proposition that `toFun` is continuous  -/
ContinuousAddMonoidHom.continuous_toFun : ∀ {A : Type u_7} {B : Type u_8} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (self : A →ₜ+ B), Continuous (↑self.toAddMonoidHom).toFun
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instEpiσ : ∀ {n : ℕ} {i : Fin (n + 1)}, CategoryTheory.Epi (SimplexCategory.σ i)
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_prod : ∀ {T₁ : Type u} {T₂ : Type u'} {κ : Cardinal.{w}},
  Cardinal.aleph0 ≤ κ → HasCardinalLT T₁ κ → HasCardinalLT T₂ κ → HasCardinalLT (T₁ × T₂) κ
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- This is a wrapper around `Presieve.IsSheafFor.amalgamate` to be used below.
If `P` is a sheaf, `S` is a cover of `X`, and `x` is a collection of morphisms from `E`
to `P` evaluated at terms in the cover which are compatible, then we can amalgamate
the `x`s to obtain a single morphism `E ⟶ P.obj (op X)`.  -/
CategoryTheory.Presheaf.IsSheaf.amalgamate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          {E : A} →
            {X : C} →
              {P : CategoryTheory.Functor Cᵒᵖ A} →
                CategoryTheory.Presheaf.IsSheaf J P →
                  (S : J.Cover X) →
                    (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y)) →
                      (∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
                          CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) =
                            CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)) →
                        (E ⟶ P.obj (Opposite.op X))
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.degree_eq_degree_of_associated : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p q : Polynomial R}, Associated p q → p.degree = q.degree
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.tuple.inj : ∀ {ref : Lean.Syntax} {a : List Lean.Elab.Tactic.RCases.RCasesPatt} {ref_1 : Lean.Syntax}
  {a_1 : List Lean.Elab.Tactic.RCases.RCasesPatt},
  Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref a = Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref_1 a_1 →
    ref = ref_1 ∧ a = a_1
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularMono.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularMono f] (k : W ⟶ Y)
  (h :
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.left f) =
      CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.right f)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularMono.lift f k h) f = k
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sigma_indep_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I : Set ((i : ι) × α i)},
  (Matroid.sigma M).Indep I ↔ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
-- Mathlib.Topology.Order.ScottTopology
Topology.scottHausdorff.eq_1 : ∀ (α : Type u_3) (D : Set (Set α)) [inst : Preorder α],
  Topology.scottHausdorff α D =
    {
      IsOpen := fun u =>
        ∀ ⦃d : Set α⦄,
          d ∈ D →
            d.Nonempty →
              DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ u → ∃ b ∈ d, Set.Ici b ∩ d ⊆ u,
      isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis_helper : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (i : Fin n),
  Module.End.HasEigenvector T (↑(LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn i))
    ((LinearMap.IsSymmetric.unsortedEigenvectorBasis✝ hT hn) i)
-- Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
/-- Given two power-multiplicative ring seminorms `f, g` on `α`, if `f` is bounded by a positive
multiple of `g` and vice versa, then `f = g`.  -/
eq_seminorms : ∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : Ring α] [inst_1 : FunLike F α ℝ] [RingSeminormClass F α ℝ] {f g : F},
  IsPowMul ⇑f →
    IsPowMul ⇑g →
      (∃ r, ∃ (_ : 0 < r), ∀ (a : α), f a ≤ r * g a) → (∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a) → f = g
-- Mathlib.Algebra.Module.GradedModule
/-- `⨁ i, 𝓜 i` and `M` are isomorphic as `A`-modules.
"The internal version" and "the external version" are isomorphism as `A`-modules.
 -/
GradedModule.linearEquiv : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {A : Type u_4} →
      {M : Type u_5} →
        {σ : Type u_6} →
          {σ' : Type u_7} →
            [inst : AddMonoid ιA] →
              [inst_1 : AddAction ιA ιM] →
                [inst_2 : Semiring A] →
                  (𝓐 : ιA → σ') →
                    [inst_3 : SetLike σ' A] →
                      (𝓜 : ιM → σ) →
                        [inst_4 : AddCommMonoid M] →
                          [inst_5 : Module A M] →
                            [inst_6 : SetLike σ M] →
                              [inst_7 : AddSubmonoidClass σ' A] →
                                [inst_8 : AddSubmonoidClass σ M] →
                                  [inst_9 : SetLike.GradedSMul 𝓐 𝓜] →
                                    [inst_10 : DecidableEq ιA] →
                                      [inst_11 : DecidableEq ιM] →
                                        [inst_12 : GradedRing 𝓐] →
                                          [DirectSum.Decomposition 𝓜] → M ≃ₗ[A] DirectSum ιM fun i => ↥(𝓜 i)
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.getThenInsertIfNew? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {a : α} {b : β},
  m.WF → (m.getThenInsertIfNew? a b).2.WF
-- Mathlib.Order.Concept
Order.IsIntent.univ : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Order.IsIntent r Set.univ
-- Mathlib.LinearAlgebra.Reflection
/-- See also `Module.Dual.eq_of_preReflection_mapsTo'` for a variant of this lemma which
applies when `Φ` does not span.

This rather technical-looking lemma exists because it is exactly what is needed to establish various
uniqueness results for root data / systems. One might regard this lemma as lying at the boundary of
linear algebra and combinatorics since the finiteness assumption is the key.  -/
Module.Dual.eq_of_preReflection_mapsTo : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [CharZero R]
  [IsDomain R] [Module.IsTorsionFree R M] {x : M} {Φ : Set M},
  Φ.Finite →
    Submodule.span R Φ = ⊤ →
      ∀ {f g : Module.Dual R M},
        f x = 2 →
          Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ → g x = 2 → Set.MapsTo (⇑(Module.preReflection x g)) Φ Φ → f = g
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCongr_refl : ∀ {α : Type u_9} {β : Type u_10}, (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)
-- Mathlib.Data.Multiset.AddSub
Multiset.sub_add_cancel : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ≤ s → s - t + t = s
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  (CochainComplex.mappingConeCompTriangle f g).mor₂ =
    CochainComplex.mappingCone.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id X₃) ⋯
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det.congr_simp : ∀ {n : Type u_2} {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {R : Type v} [inst_3 : CommRing R]
  (M M_1 : Matrix n n R), M = M_1 → M.det = M_1.det
-- Aesop.RuleSet
Aesop.LocalRuleSet.containsGlobalSimpTheorem : Aesop.LocalRuleSet → Lean.Name → Bool
-- Init.Data.Fin.Lemmas
Fin.subsingleton_one : Subsingleton (Fin 1)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.leOnePart : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : Lattice β] [ContinuousSup β] [ContinuousInv β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x)⁻ᵐ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.β : Lean.Meta.Grind.InjectiveInfo → Lean.Expr
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_zero : ∀ {l w : ℕ} {x : BitVec (l * w)} {acc : BitVec w}, BitVec.addRecAux✝ x 0 acc = acc
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filter.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (f f_1 : (a : α) → β a → Bool),
  f = f_1 → ∀ (m m_1 : Std.ExtDHashMap α β), m = m_1 → Std.ExtDHashMap.filter f m = Std.ExtDHashMap.filter f_1 m_1
-- Init.Prelude
/-- Abbreviation for `DecidableRel (· < · : α → α → Prop)`.  -/
DecidableLT : (α : Type u) → [LT α] → Type (max 0 u)
-- Lean.Elab.InfoTree.Types
/-- Information about a user widget associated with a syntactic span.
This must be a panel widget.
A panel widget is a widget that can be displayed
in the infoview alongside the goal state.  -/
Lean.Elab.UserWidgetInfo : Type
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- Given an `IndParallelPairPresentation f g`, we can understand the parallel pair `(f, g)` as
the colimit of `(P.φ, P.ψ)` in `Ind C`.  -/
CategoryTheory.IndParallelPairPresentation.parallelPairIsoParallelPairCompIndYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : CategoryTheory.Ind C} →
      {f g : A ⟶ B} →
        (P :
            CategoryTheory.IndParallelPairPresentation ((CategoryTheory.Ind.inclusion C).map f)
              ((CategoryTheory.Ind.inclusion C).map g)) →
          CategoryTheory.Limits.parallelPair f g ≅
            (CategoryTheory.Limits.parallelPair P.φ P.ψ).comp (CategoryTheory.Ind.lim P.I)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm.congr_simp : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B B_1 : LinearMap.BilinForm R M} (e_B : B = B_1)
  (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q), CliffordAlgebra.changeForm h = CliffordAlgebra.changeForm ⋯
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix`.

---

`BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
`n`-by-`n` matrices with entries in `R`, if `b` is an `R`-basis for `M`.  -/
BilinForm.toMatrix : {R₁ : Type u_1} →
  {M₁ : Type u_2} →
    [inst : CommSemiring R₁] →
      [inst_1 : AddCommMonoid M₁] →
        [inst_2 : Module R₁ M₁] →
          {n : Type u_5} →
            [Fintype n] → [DecidableEq n] → Module.Basis n R₁ M₁ → LinearMap.BilinForm R₁ M₁ ≃ₗ[R₁] Matrix n n R₁
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) [inst_1 : DecidableEq σ],
  (MvPowerSeries.coeff n) 1 = if n = 0 then 1 else 0
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.below.inj : ∀ {decl : Lean.LocalDecl} {indName : Lean.Name} {vars : Array Lean.FVarId} {decl_1 : Lean.LocalDecl}
  {indName_1 : Lean.Name} {vars_1 : Array Lean.FVarId},
  Lean.Meta.IndPredBelow.NewDecl.below✝ decl indName vars =
      Lean.Meta.IndPredBelow.NewDecl.below✝ decl_1 indName_1 vars_1 →
    decl = decl_1 ∧ indName = indName_1 ∧ vars = vars_1