mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id._auto_1) {Z : C}
  (h : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀)
      (CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom h) =
    h
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_sum : ∀ {α : Type u_1} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] {p : α → Prop} [inst_1 : DecidablePred p]
  (s : Finset ι) (f : ι → α →₀ M), Finsupp.filter p (∑ a ∈ s, f a) = ∑ a ∈ s, Finsupp.filter p (f a)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- A morphism property `P` satisfies `P.RespectsLeft Q` if it is stable under
pre-composition with morphisms satisfying `Q`, i.e. whenever `P` holds for `f`
and `Q` holds for `i` then `P` holds for `i ≫ f`.  -/
CategoryTheory.MorphismProperty.RespectsLeft : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Star.CentroidHom
/-- The canonical \*-homomorphism from the center of a non-unital, non-associative \*-semiring
into the center of its centroid.  -/
CentroidHom.starCenterToCentroidCenter : {α : Type u_1} →
  [inst : NonUnitalNonAssocSemiring α] →
    [inst_1 : StarRing α] → ↥(NonUnitalStarSubsemiring.center α) →⋆ₙ+* ↥(Subsemiring.center (CentroidHom α))
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.map_distinguished_exact : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [inst_8 : F.IsHomological] (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact
-- Batteries.Data.UInt
USize.toUInt64_toNat : ∀ (x : USize), x.toUInt64.toNat = x.toNat
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A choice of an
[exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets)
of a weakly locally compact σ-compact space.  -/
CompactExhaustion.choice : (X : Type u_4) →
  [inst : TopologicalSpace X] → [WeaklyLocallyCompactSpace X] → [SigmaCompactSpace X] → CompactExhaustion X
-- Std.Http.Test.Helpers
/-- POST with Transfer-Encoding: chunked. `chunkedBody` is the pre-formatted body
(use `chunk` + `chunkEnd` to build it).
 -/
Std.Http.Internal.Test.mkChunked : String → String → optParam String "" → String
-- Mathlib.Data.NNRat.Floor
NNRat.floor_cast : ∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorSemiring K]
  (x : ℚ≥0), ⌊↑x⌋₊ = ⌊x⌋₊
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx'_eq_multiplicity : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊥ → P.IsPrime → p.ramificationIdx' P = multiplicity P (Ideal.map (algebraMap R S) p)
-- Mathlib.Data.Nat.Init
Nat.instNeZeroNatAbsOfInt_mathlib : ∀ (n : ℤ) [NeZero n], NeZero n.natAbs
-- Mathlib.LinearAlgebra.Finsupp.Defs
Module.End.ringEquivEndFinsupp_symm_apply_apply : ∀ {ι : Type u_4} {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (i : ι) (f : Module.End (Module.End R (ι →₀ M)) (ι →₀ M)) (m : M),
  ((Module.End.ringEquivEndFinsupp i).symm f) m = (f fun₀ | i => m) i
-- Mathlib.Data.Finset.Image
Finset.filter_attach : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α),
  {a ∈ s.attach | p ↑a} = Finset.map ((Function.Embedding.refl α).subtypeMap ⋯) (Finset.filter p s).attach
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.cancel_left : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] {g : ZeroHom N P}
  {f₁ f₂ : ZeroHom M N}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapAddEquiv.eq_1 : ∀ {R : Type u_3} {S : Type u_4} (M : Type u_6) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S),
  MonoidAlgebra.mapAddEquiv M e =
    { toFun := MonoidAlgebra.map ↑e, invFun := MonoidAlgebra.map ↑e.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Construct a `Mor₂` term from a lean expression.  -/
Mathlib.Tactic.BicategoryLike.MkMor₂.ofExpr : {m : Type → Type} → [self : Mathlib.Tactic.BicategoryLike.MkMor₂ m] → Lean.Expr → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isPath_mapLe`. -/
SimpleGraph.Walk.IsPath.mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  p.IsPath → (SimpleGraph.Walk.mapLe h p).IsPath
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_bot_one : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieSubmodule.ucs 1 ⊥ = LieModule.maxTrivSubmodule R L M
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isBasis_iff : ∀ {α : Type u_1} {M : Matroid α} {I D X : Set α}, (M.delete D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.isTheta_cpow_exp_re_mul_log : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → ∀ (a : ℂ), (fun x => x ^ a) =Θ[l] fun z => Real.exp (a.re * Real.log ‖z‖)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentPositionParams.toJson : Lean.Lsp.TextDocumentPositionParams → Lean.Json
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote : {α : Type u_1} → [Lean.Grind.Ring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Poly → α
-- Mathlib.Order.Filter.Pointwise
Filter.div_neBot_iff : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α}, (f / g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Mathlib.Data.List.SplitLengths
List.splitLengths.eq_1 : ∀ {α : Type u_1} (x : List α), [].splitLengths x = []
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.comp.eq_1 : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₁]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜₂ F]
  [inst_10 : AddCommGroup G] [inst_11 : TopologicalSpace G] [inst_12 : Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G)
  (f : E →SWOT[σ₁₂] F), g.comp f = ContinuousLinearMapWOT.ofCLM (g.toCLM ∘SL f.toCLM)
-- Init.Data.UInt.Lemmas
USize.le_of_eq : ∀ {a b : USize}, a = b → a ≤ b
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.LinarithData.mk.sizeOf_spec : ∀ (maxVar : ℕ) (comps : Mathlib.Tactic.Linarith.PCompSet),
  sizeOf { maxVar := maxVar, comps := comps } = 1 + sizeOf maxVar + sizeOf comps
-- Init.Data.Int.Order
Int.add_lt_add_left : ∀ {a b : ℤ}, a < b → ∀ (c : ℤ), c + a < c + b
-- Mathlib.Combinatorics.Hall.Basic
hallMatchingsOn.finite : ∀ {ι : Type u} {α : Type v} (t : ι → Finset α) (ι' : Finset ι), Finite ↑(hallMatchingsOn t ι')
-- Mathlib.Data.Set.Finite.Basic
/-- If a set `s` does not contain any triple of elements `x < y < z`, then `s` is finite.  -/
Set.finite_of_forall_not_lt_lt : ∀ {α : Type u} [inst : LinearOrder α] {s : Set α}, (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) → s.Finite
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_stabilizer_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : α} {g : G},
  g ∈ MulAction.stabilizer G a ↔ g • a = a
-- Init.Data.Fin.Lemmas
Fin.pred_inj : ∀ {n : ℕ} {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
-- Lean.Util.ParamMinimizer
/-- Search outcome (`missing`, `approx`, or `precise`)  -/
Lean.Util.ParamMinimizer.Result.status : Lean.Util.ParamMinimizer.Result → Lean.Util.ParamMinimizer.Status
-- Init.Data.String.Lemmas.Basic
String.pos!.eq_1 : ∀ (s : String) (off : String.Pos.Raw), s.pos! off = String.Pos.ofToSlice (s.toSlice.pos! off)
-- Mathlib.RingTheory.Henselian
/-- A ring `R` is *Henselian* at an ideal `I` if the following condition holds:
for every polynomial `f` over `R`, with a *simple* root `a₀` over the quotient ring `R/I`,
there exists a lift `a : R` of `a₀` that is a root of `f`.

(Here, saying that a root `b` of a polynomial `g` is *simple* means that `g.derivative.eval b` is a
unit. Warning: if `R/I` is not a field then it is not enough to assume that `g` has a factorization
into monic linear factors in which `X - b` shows up only once; for example `1` is not a simple root
of `X^2-1` over `ℤ/4ℤ`.)  -/
HenselianRing : (R : Type u_1) → [inst : CommRing R] → Ideal R → Prop
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_mk : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun),
  ⇑{ toAffineMap := f, cont := h } = ⇑f
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.to_finiteDimensional : ∀ {K : Type u_1} {inst : Field K} [self : NumberField K], FiniteDimensional ℚ K
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Iic : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0),
  NNRat.cast ⁻¹' Set.Iic ↑p = Set.Iic p
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instTrivialStar : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {R : Type u_5} [inst_1 : TopologicalSpace R]
  [inst_2 : Star R] [TrivialStar R] [inst_4 : ContinuousStar R], TrivialStar (α →ₘ[μ] R)
-- Init.Data.SInt.Basic
/-- Converts a 32-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.toInt : Int32 → ℤ
-- Mathlib.Algebra.Central.Matrix
Matrix.subalgebraCenter_eq_scalarAlgHom_map : ∀ {n : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n],
  Subalgebra.center R (Matrix n n A) = Subalgebra.map (Matrix.scalarAlgHom n R) (Subalgebra.center R A)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial] {Z : ModuleCat k}
  (h : ModuleCat.of k ↑A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 0)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H0IsoOfIsTrivial A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).hom h
-- Mathlib.Analysis.Convex.Function
ConcaveOn.openSegment_subset_strict_hypograph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f →
    ∀ (p q : E × β), p.1 ∈ s ∧ p.2 < f p.1 → q.1 ∈ s ∧ q.2 ≤ f q.1 → openSegment 𝕜 p q ⊆ {p | p.1 ∈ s ∧ p.2 < f p.1}
-- Std.Data.HashSet.Raw
/-- Internal implementation detail of the hash set.  -/
Std.HashSet.Raw.inner : {α : Type u} → Std.HashSet.Raw α → Std.HashMap.Raw α Unit
-- Mathlib.Data.Finset.SMulAntidiagonal
Set.IsWF.smul : ∀ {G : Type u_1} {P : Type u_2} [inst : LinearOrder G] [inst_1 : LinearOrder P] [inst_2 : SMul G P] [IsOrderedSMul G P]
  {s : Set G} {t : Set P}, s.IsWF → t.IsWF → (s • t).IsWF
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_const_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.variance (fun ω => c * X ω) μ = c ^ 2 * ProbabilityTheory.variance X μ
-- Mathlib.Order.RelIso.Basic
RelIso.cast_trans : ∀ {α β γ : Type u} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (h₁ : α = β) (h₁' : β = γ) (h₂ : r ≍ s)
  (h₂' : s ≍ t), (RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂') = RelIso.cast ⋯ ⋯
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.toAddCircle_X_eq_fourier_one : Polynomial.toAddCircle Polynomial.X = fourier 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.Cofan.inj.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Cofan f)
  (j : β), p.inj j = p.ι.app { as := j }
-- Aesop.Search.Queue
Aesop.LIFOQueue.mk : Array Aesop.GoalRef → Aesop.LIFOQueue
-- Batteries.Data.Fin.Coding
Fin.decodeOption.eq_1 : ∀ {n : ℕ}, Fin.decodeOption ⟨0, ⋯⟩ = none
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_compl : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α}, m.IsCaratheodory s₁ → m.IsCaratheodory s₁ᶜ
-- Mathlib.FieldTheory.Relrank
IntermediateField.lift_relrank_map_map : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : E →ₐ[F] L),
  Cardinal.lift.{v, w} ((IntermediateField.map f A).relrank (IntermediateField.map f B)) =
    Cardinal.lift.{w, v} (A.relrank B)
-- Init.Prelude
Zero.mk : {α : Type u} → α → Zero α
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.Precheck.Context.mk : Lean.NameSet → Lean.Elab.Term.Quotation.Precheck.Context
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : R),
  (AlgebraicGeometry.StructureSheaf.comap f U
        ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)
      ((algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))) x) =
    (algebraMap S
        ↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj
            (Opposite.op ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))
      (f x)
-- Init.Data.SInt.Lemmas
Int8.zero_mod : ∀ {a : Int8}, 0 % a = 0
-- Mathlib.RingTheory.AdicCompletion.Topology
IsHausdorff.congr_ringEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) (e : R ≃+* S),
  IsHausdorff (Ideal.map e I) S ↔ IsHausdorff I R
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_injective : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂],
  Function.Injective NormedAddGroupHom.toFun
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.mul_kroneckerTMul_mul : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {l' : Type u_15}
  {m' : Type u_16} {n' : Type u_17} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring α]
  [inst_2 : NonUnitalSemiring β] [inst_3 : Module R α] [inst_4 : Module R β] [inst_5 : IsScalarTower R α α]
  [inst_6 : SMulCommClass R α α] [inst_7 : IsScalarTower R β β] [inst_8 : SMulCommClass R β β] [inst_9 : Fintype m]
  [inst_10 : Fintype m'] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β),
  Matrix.kroneckerMap (TensorProduct.tmul R) (A * B) (A' * B') =
    Matrix.kroneckerMap (TensorProduct.tmul R) A A' * Matrix.kroneckerMap (TensorProduct.tmul R) B B'
-- Init.Data.String.Termination
String.Slice.Pos.prev_induction : ∀ {s : String.Slice} {C : s.Pos → Prop} (p : s.Pos),
  (∀ (x : s.Pos) (h : x ≠ s.startPos), C (x.prev h) → C x) → C s.startPos → C p
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- Typeclass expressing that a morphism property contains identities.  -/
CategoryTheory.MorphismProperty.ContainsIdentities : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitor_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.F =
    CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd
      (CategoryTheory.Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))
-- Init.SimpLemmas
Bool.true_and : ∀ (b : Bool), (true && b) = b
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ),
  (AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.inv.app X).f = AlgebraicTopology.DoldKan.PInfty
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.twoCocycleOf.congr_simp : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] (E : LieAlgebra.Extension R M L)
  {s s_1 : L →ₗ[R] E.L} (e_s : s = s_1) (hs : Function.LeftInverse ⇑E.proj ⇑s), E.twoCocycleOf hs = E.twoCocycleOf ⋯
-- Mathlib.Topology.Neighborhoods
Dense.inter_nhds_nonempty : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s t : Set X}, Dense s → t ∈ nhds x → (s ∩ t).Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S)
  {Z : C} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.equalizer.ι
          (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
          (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd s v) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g)
        (CategoryTheory.Limits.pullback.fst s v))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd s v) h)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Key.mk.inj : ∀ {w : ℕ} {expr : Std.Tactic.BVDecide.BVExpr w} {w_1 : ℕ} {expr_1 : Std.Tactic.BVDecide.BVExpr w_1},
  { w := w, expr := expr } = { w := w_1, expr := expr_1 } → w = w_1 ∧ expr ≍ expr_1
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.natCast.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℕ),
  Lean.Grind.Ring.OfSemiring.natCast n = Lean.Grind.Ring.OfSemiring.Q.mk (↑n, 0)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.edges = p.edges.reverse
-- Lean.Elab.Tactic.Try
/-- Evaluates a user-generated tactic and captures any "Try this" suggestions it produces
by walking the info tree for `TryThisInfo` nodes registered by `TryThis.addSuggestion`.

Returns an array of tactics: the original tactic followed by any extracted suggestions.
 -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.expandUserTactic : Lean.TSyntax `tactic → Lean.MVarId → Lean.MetaM (Array (Lean.TSyntax `tactic))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.stabilizer_of_subMul.addSubmonoid : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] {p : SubAddAction R M} (m : ↥p),
  AddAction.stabilizerAddSubmonoid R m = AddAction.stabilizerAddSubmonoid R ↑m
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
_private.Mathlib.Combinatorics.Additive.PluenneckeRuzsa.0.Finset.add_aux : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] {A B C : Finset G},
  A.Nonempty →
    A ⊆ B →
      (∀ A' ∈ B.powerset.erase ∅, ↑(A + C).card / ↑A.card ≤ ↑(A' + C).card / ↑A'.card) →
        ∀ A' ⊆ A, (A + C).card * A'.card ≤ (A' + C).card * A.card
-- Mathlib.Topology.UniformSpace.Defs
/-- The uniformity filter on the domain is the pullback of the uniformity filter on the codomain
under `Prod.map f f`.  -/
IsUniformInducing.comap_uniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α
-- Mathlib.CategoryTheory.Simple
/-- `X` is simple iff it has subobject lattice `{⊥, ⊤}`.  -/
CategoryTheory.simple_iff_subobject_isSimpleOrder : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C),
  CategoryTheory.Simple X ↔ IsSimpleOrder (CategoryTheory.Subobject X)
-- Init.Prelude
instInhabitedOfMonad : {α : Type u} → {m : Type u → Type v} → [Monad m] → [Inhabited α] → Inhabited (m α)
-- Mathlib.Data.List.Lookmap
List.perm_lookmap : ∀ {α : Type u_1} (f : α → Option α) {l₁ l₂ : List α},
  List.Pairwise (fun a b => ∀ c ∈ f a, ∀ d ∈ f b, a = b ∧ c = d) l₁ →
    l₁.Perm l₂ → (List.lookmap f l₁).Perm (List.lookmap f l₂)
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.mk.inj : ∀ {toElabInfo : Lean.Elab.ElabInfo} {mctxBefore : Lean.MetavarContext} {goalsBefore : List Lean.MVarId}
  {mctxAfter : Lean.MetavarContext} {goalsAfter : List Lean.MVarId} {toElabInfo_1 : Lean.Elab.ElabInfo}
  {mctxBefore_1 : Lean.MetavarContext} {goalsBefore_1 : List Lean.MVarId} {mctxAfter_1 : Lean.MetavarContext}
  {goalsAfter_1 : List Lean.MVarId},
  { toElabInfo := toElabInfo, mctxBefore := mctxBefore, goalsBefore := goalsBefore, mctxAfter := mctxAfter,
        goalsAfter := goalsAfter } =
      { toElabInfo := toElabInfo_1, mctxBefore := mctxBefore_1, goalsBefore := goalsBefore_1, mctxAfter := mctxAfter_1,
        goalsAfter := goalsAfter_1 } →
    toElabInfo = toElabInfo_1 ∧
      mctxBefore = mctxBefore_1 ∧ goalsBefore = goalsBefore_1 ∧ mctxAfter = mctxAfter_1 ∧ goalsAfter = goalsAfter_1
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctor_obj_d : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ)
  (K : CochainComplex C ℤ) (x x_1 : ℤ),
  ((CochainComplex.shiftFunctor C n).obj K).d x x_1 = n.negOnePow • K.d (x + n) (x_1 + n)