mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalizedModule.map_linearCombination : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_3} [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  {M' : Type u_4} [inst_6 : AddCommMonoid M'] [inst_7 : Module R M'] [inst_8 : Module A M']
  [inst_9 : IsScalarTower R A M'] (f : M →ₗ[R] M') {α : Type u_7} {v : α → M} [inst_10 : IsLocalizedModule S f],
  (IsLocalizedModule.map S (Finsupp.mapRange.linearMap (Algebra.linearMap R A)) f) (Finsupp.linearCombination R v) =
    ↑R (Finsupp.linearCombination A (⇑f ∘ v))
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore condition of a difference, expressed in terms of `oreMin` and `oreSubtra`.  -/
AddOreLocalization.AddOreSet.ore_eq : ∀ {R : Type u_1} {inst : AddMonoid R} {S : AddSubmonoid R} [self : AddOreLocalization.AddOreSet S] (r : R) (s : ↥S),
  ↑(AddOreLocalization.AddOreSet.oreSubtra r s) + r = AddOreLocalization.AddOreSet.oreMin r s + ↑s
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_3 : {α : Type u} → Std.Roc.Sliceable (Subarray α) ℕ (Subarray α)
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instIsCentralScalar : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : MulAction G β] [inst_2 : MulAction Gᵐᵒᵖ β]
  [IsCentralScalar G β], IsCentralScalar G (α ↪ β)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_succ_right_eq_append : ∀ {m n : ℤ}, m ≤ n + 1 → (m...=n + 1).toList = (m...=n).toList ++ [n + 1]
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_mem : ∀ {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent},
  SimpleGraph.ConnectedComponent.Represents s C → c ∈ C → (c.supp \ s).ncard = c.supp.ncard - 1
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isZeroOrProbabilityMeasure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.IsZeroOrProbabilityMeasure μ ↔ μ Set.univ = 0 ∨ μ Set.univ = 1
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.of_nhds_one' : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1) →
    Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) →
        (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x * x₀) (nhds 1)) → IsTopologicalGroup G
-- Lean.Util.Diff
Lean.Diff.instInhabitedAction.default : Lean.Diff.Action
-- Init.Data.List.Sublist
List.isSublist_iff_sublist : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α}, l₁.isSublist l₂ = true ↔ l₁.Sublist l₂
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C), self.L₁.Exact
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.mk : {α : Type u} →
  (ord : autoParam (Ord α) Std.Packages.LinearPreorderOfOrdArgs.ord._autoParam) →
    (transOrd : autoParam (Std.TransOrd α) Std.Packages.LinearPreorderOfOrdArgs.transOrd._autoParam) →
      (le :
          autoParam
            (let this := ord;
            LE α)
            Std.Packages.LinearPreorderOfOrdArgs.le._autoParam) →
        (lawfulOrderOrd :
            autoParam
              (let this := ord;
              let this_1 := transOrd;
              let this_2 := le;
              Std.LawfulOrderOrd α)
              Std.Packages.LinearPreorderOfOrdArgs.lawfulOrderOrd._autoParam) →
          autoParam
              (let this := ord;
              let this := le;
              have this_1 := lawfulOrderOrd;
              DecidableLE α)
              Std.Packages.LinearPreorderOfOrdArgs.decidableLE._autoParam →
            (lt :
                autoParam
                  (let this := ord;
                  LT α)
                  Std.Packages.LinearPreorderOfOrdArgs.lt._autoParam) →
              (lt_iff :
                  autoParam
                    (let this := ord;
                    let this_1 := le;
                    have this_2 := lawfulOrderOrd;
                    let this_3 := lt;
                    ∀ (a b : α), a < b ↔ compare a b = Ordering.lt)
                    Std.Packages.LinearPreorderOfOrdArgs.lt_iff._autoParam) →
                autoParam
                    (let this := ord;
                    let this := lt;
                    let this_1 := le;
                    have this_2 := lawfulOrderOrd;
                    have this_3 := lt_iff;
                    DecidableLT α)
                    Std.Packages.LinearPreorderOfOrdArgs.decidableLT._autoParam →
                  (beq :
                      autoParam
                        (let this := ord;
                        BEq α)
                        Std.Packages.LinearPreorderOfOrdArgs.beq._autoParam) →
                    autoParam
                        (let this := ord;
                        let this_1 := le;
                        have this_2 := lawfulOrderOrd;
                        let this_3 := beq;
                        ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq)
                        Std.Packages.LinearPreorderOfOrdArgs.beq_iff._autoParam →
                      Std.Packages.LinearPreorderOfOrdArgs α
-- Mathlib.RingTheory.HopfAlgebra.Convolution
LinearMap.antipode_mul_id : ∀ {R : Type u_1} {C : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring C] [inst_2 : HopfAlgebra R C],
  WithConv.toConv (HopfAlgebraStruct.antipode R) * WithConv.toConv LinearMap.id = 1
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- The set of column stochastic matrices is convex.  -/
Matrix.convex_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R], Convex R ↑(Matrix.colStochastic R n)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.lemma_congr : ∀ (x x' : Bool), x' = x → x = true → x' = true
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.powerRevlex : ℕ → ℕ → Ordering
-- Mathlib.SetTheory.Cardinal.Subfield
_private.Mathlib.SetTheory.Cardinal.Subfield.0.Subfield.rangeOfWType : {α : Type u} → (s : Set α) → [inst : DivisionRing α] → Subfield ↥(Subfield.closure s)
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.Context.mk.injEq : ∀ (exceptionSet : Lean.ExprSet) (kind : Lean.Meta.SplitKind) (exceptionSet_1 : Lean.ExprSet)
  (kind_1 : Lean.Meta.SplitKind),
  ({ exceptionSet := exceptionSet, kind := kind } = { exceptionSet := exceptionSet_1, kind := kind_1 }) =
    (exceptionSet = exceptionSet_1 ∧ kind = kind_1)
-- Init.Data.BitVec.Lemmas
BitVec.not_lt : ∀ {n : ℕ} {x y : BitVec n}, ¬x < y ↔ y ≤ x
-- Mathlib.Topology.Compactness.Lindelof
not_LindelofSpace_iff : ∀ {X : Type u} [inst : TopologicalSpace X], ¬LindelofSpace X ↔ NonLindelofSpace X
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instMonoidWithZero : {R : Type u_1} →
  [inst : MonoidWithZero R] →
    {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → MonoidWithZero (OreLocalization S R)
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.neg : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable (-f) s
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryGTD : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a → (a : α) × β a
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_vadd : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] {i : ι} (v : V) (b : AffineBasis ι k P),
  (v +ᵥ b).coord i = (b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.map : ∀ {α : Type u_1} {β : Type u_2} {n : Type u_4} [inst : Star α] [inst_1 : Star β] {A : Matrix n n α},
  A.IsHermitian → ∀ (f : α → β), Function.Semiconj f star star → (A.map f).IsHermitian
-- Mathlib.Algebra.Group.Basic
eq_neg_of_add_eq_zero_right : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a + b = 0 → b = -a
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier : ∀ {A : CommRingCat} [Nontrivial ↑A], Nonempty ↥(AlgebraicGeometry.Spec A)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {M N : QuadraticModuleCat R} {f g : M ⟶ N},
  f = g ↔ QuadraticModuleCat.Hom.toIsometry f = QuadraticModuleCat.Hom.toIsometry g
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_twoPow : ∀ {i j w : ℕ}, (BitVec.twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1))
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- If `0 < n`, then `DihedralGroup n` has `2n` elements.
 -/
DihedralGroup.card : ∀ {n : ℕ} [inst : NeZero n], Fintype.card (DihedralGroup n) = 2 * n
-- Mathlib.Data.Real.Basic
Real.instIsOrderedAddMonoid : IsOrderedAddMonoid ℝ
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A bounded variation function tends to its left-limit on its left.  -/
BoundedVariationOn.tendsto_leftLim : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : α → E},
  BoundedVariationOn f Set.univ → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.GammaIntegral_one : Complex.GammaIntegral 1 = 1
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearCoyoneda_map_app : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {Y₁ Y₂ : Cᵒᵖ} (f : Y₁ ⟶ Y₂) (X : C),
  ((CategoryTheory.linearCoyoneda R C).map f).app X = ModuleCat.ofHom (CategoryTheory.Linear.leftComp R X f.unop)
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.instAlgebra_1 : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → Algebra R (IsDedekindDomain.FiniteAdeleRing R K)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_eq_comap_of_inverse : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {g : N →+ G},
  Function.LeftInverse ⇑g ⇑f →
    Function.RightInverse ⇑g ⇑f → ∀ (H : AddSubgroup G), AddSubgroup.map f H = AddSubgroup.comap g H
-- Mathlib.Topology.DiscreteSubset
/-- A set `s` is discrete iff for every `t ⊆ s` there is a closed `u` with `u ∩ s = t`.  -/
isDiscrete_iff_forall_mem_exists_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X}, IsDiscrete S ↔ ∀ s ⊆ S, ∃ U, IsClosed U ∧ U ∩ S = s
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDeriv_fun_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {x : E} (c : 𝕜)
  (ω : E → E [⋀^Fin n]→L[𝕜] F), extDeriv (c • ω) x = c • extDeriv ω x
-- Mathlib.Order.Max
IsTop.not_isMin : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} [Nontrivial α], IsTop a → ¬IsMin a
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- An additive subsemigroup `S` includes `closure s` if and only if it includes `s`  -/
AddSubsemigroup.closure_le : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s ≤ S ↔ s ⊆ ↑S
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (braiding :
          (X Y : C) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) →
        autoParam
            (∀ (X : C) {Y Z : C} (f : Y ⟶ Z),
              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
                  (braiding X Z).hom =
                CategoryTheory.CategoryStruct.comp (braiding X Y).hom
                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
            CategoryTheory.BraidedCategory.braiding_naturality_right._autoParam →
          autoParam
              (∀ {X Y : C} (f : X ⟶ Y) (Z : C),
                CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
                    (braiding Y Z).hom =
                  CategoryTheory.CategoryStruct.comp (braiding X Z).hom
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f))
              CategoryTheory.BraidedCategory.braiding_naturality_left._autoParam →
            autoParam
                (∀ (X Y Z : C),
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
                      (CategoryTheory.CategoryStruct.comp
                        (braiding X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
                        (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (braiding X Y).hom Z)
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (braiding X Z).hom)))
                CategoryTheory.BraidedCategory.hexagon_forward._autoParam →
              autoParam
                  (∀ (X Y Z : C),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
                        (CategoryTheory.CategoryStruct.comp
                          (braiding (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
                          (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) =
                      CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (braiding Y Z).hom)
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (braiding X Z).hom Y)))
                  CategoryTheory.BraidedCategory.hexagon_reverse._autoParam →
                CategoryTheory.BraidedCategory C
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.lTensor_add : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f₁ f₂ : σ.IntertwiningMap τ),
  Representation.IntertwiningMap.lTensor ρ (f₁ + f₂) =
    Representation.IntertwiningMap.lTensor ρ f₁ + Representation.IntertwiningMap.lTensor ρ f₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.full_sheafPushforwardContinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) {A : Type u_4} [inst_2 : CategoryTheory.Category.{v_4, u_4} A]
  (G : CategoryTheory.Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] [inst_5 : G.IsContinuous J K],
  (G.sheafPushforwardContinuous A J K).Full
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_top : ∀ {X Y : SSet} (f : X ⟶ Y), ⊤.image f = SSet.Subcomplex.range f
-- Mathlib.Topology.Algebra.Field
/-- Compact Hausdorff topological fields are finite. This is not an instance, as it would apply to
every `Finite` goal, causing slowly failing typeclass search in some cases.  -/
DivisionRing.finite_of_compactSpace_of_t2Space : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : TopologicalSpace K] [IsTopologicalRing K] [CompactSpace K]
  [T2Space K], Finite K
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.liftExpand.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_3}
  [inst_2 : AddAction R X] {C : Sort u_2} (P : X → ↥S → C)
  (hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t + ↑s ∈ S), P r s = P (t +ᵥ r) ⟨t + ↑s, ht⟩),
  AddOreLocalization.liftExpand P hP = Quotient.lift (fun p => P p.1 p.2) ⋯
-- Batteries.Lean.LawfulMonadLift
StateRefT'.lift_pure : ∀ {m : Type → Type} {α ω σ : Type} [inst : Monad m] (a : α), StateRefT'.lift (pure a) = pure a
-- Mathlib.CategoryTheory.Simple
CategoryTheory.Biprod.isIso_inl_iff_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C),
  CategoryTheory.IsIso CategoryTheory.Limits.biprod.inl ↔ CategoryTheory.Limits.IsZero Y
-- Mathlib.Computability.Language
Symbol.nonterminal.sizeOf_spec : ∀ {T : Type u_4} {N : Type u_5} [inst : SizeOf T] [inst_1 : SizeOf N] (n : N),
  sizeOf (Symbol.nonterminal n) = 1 + sizeOf n
-- Mathlib.Data.List.Basic
List.head!_mem_head? : ∀ {α : Type u} [inst : Inhabited α] {l : List α}, l ≠ [] → l.head! ∈ l.head?
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.AddMon_tensor_add_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : C) [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add))
        (CategoryTheory.MonoidalCategoryStruct.tensorObj M N))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add
              CategoryTheory.AddMonObj.add)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)))
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.lift_mk : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  (ρ : Representation k G V) (f : V →ₗ[k] W) (h : ∀ (x : G), f ∘ₗ ρ x = f) (x : V),
  (Representation.Coinvariants.lift ρ f h) ((Representation.Coinvariants.mk ρ) x) = f x
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_ofNat : ∀ {r : ℝ} {n : ℕ} [inst : n.AtLeastTwo], r.toNNReal < OfNat.ofNat n ↔ r < OfNat.ofNat n
-- Mathlib.Algebra.Module.Torsion.Basic
/-- An `a`-torsion module is a module where every element is `a`-torsion.  -/
Module.IsTorsionBy : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → R → Prop
-- Mathlib.Data.Matrix.Basis
Matrix.single.congr_simp : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} {inst : DecidableEq m} [inst_1 : DecidableEq m] {inst_2 : DecidableEq n}
  [inst_3 : DecidableEq n] [inst_4 : Zero α] (i i_1 : m),
  i = i_1 →
    ∀ (j j_1 : n),
      j = j_1 →
        ∀ (a a_1 : α),
          a = a_1 →
            ∀ (a_2 a_3 : m),
              a_2 = a_3 → ∀ (a_4 a_5 : n), a_4 = a_5 → Matrix.single i j a a_2 a_4 = Matrix.single i_1 j_1 a_1 a_3 a_5
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₃_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF], W.a₃ = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.getKey! a = (m.getKey? a).get!
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.sdiv_eq.match_1.splitter : (motive : Bool → Bool → Sort u_1) →
  (x x_1 : Bool) →
    (Unit → motive false false) →
      (Unit → motive false true) → (Unit → motive true false) → (Unit → motive true true) → motive x x_1
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.eraseManyEntries : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type u_1} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  {t : Std.DTreeMap.Internal.Impl α β} {l : ρ} {h : t.Balanced}, t.WF → (↑(t.eraseManyEntries l h)).WF
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.erase : ∀ {α : Type u_1} [inst : LE α] {s : Set α} {a : α}, IsLowerSet s → (∀ b ∈ s, a ≤ b → b = a) → IsLowerSet (s \ {a})
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.diag2_decompose : ∀ {F : Type u_1} [inst : Field F] (a : F) (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2 a ha =
    Matrix.SpecialLinearGroup.transvection ⋯ a * Matrix.SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
            Matrix.SpecialLinearGroup.transvection ⋯ a *
          Matrix.SpecialLinearGroup.transvection ⋯ (-1) *
        Matrix.SpecialLinearGroup.transvection ⋯ 1 *
      Matrix.SpecialLinearGroup.transvection ⋯ (-1)
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.PlausibleStep.rejected : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β} {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    (P out).Property { down := false } → Std.Iterators.Types.TakeWhile.PlausibleStep it Std.IterStep.done
-- Lean.Elab.Tactic.Doc
Lean.Elab.Tactic.Doc.elabRegisterTacticTag : Lean.Elab.Command.CommandElab
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfectCompl.mk : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R} [inst_5 : p.IsPerfPair] {U : Submodule R M}
  {V : Submodule R N},
  IsCompl U (Submodule.map (↑p.toPerfPair.symm) V.dualAnnihilator) →
    IsCompl V (Submodule.map (↑p.flip.toPerfPair.symm) U.dualAnnihilator) → p.IsPerfectCompl U V