mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.det_eq_one : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (u : SpecialLinearGroup R V), LinearMap.det ↑↑u = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involute_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (m : M), CliffordAlgebra.involute ((CliffordAlgebra.ι Q) m) = -(CliffordAlgebra.ι Q) m
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_add : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {s : Finset ι}
  {x y : (i : ↑↑s) → β ↑i}, DFinsupp.mk s (x + y) = DFinsupp.mk s x + DFinsupp.mk s y
-- Mathlib.Topology.Defs.Basic
WithTopology.toTopology.injEq : ∀ {X : Type u_1} (t : TopologicalSpace X) (ofTopology ofTopology_1 : X),
  (WithTopology.toTopology t ofTopology = WithTopology.toTopology t ofTopology_1) = (ofTopology = ofTopology_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.hasPushout_of_preservesPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.Limits.HasPushout (G.map f) (G.map g)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.id.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.id f) = 1 + sizeOf a + sizeOf b + sizeOf f
-- Mathlib.GroupTheory.Generators
/-- The transport of a generating family along an equivalence of index types.  -/
Group.Generators.reindex : {G : Type u_1} →
  {ι : Type u_3} → {ι' : Type u_4} → [inst : Group G] → Group.Generators G ι → ι' ≃ ι → Group.Generators G ι'
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_iff_right : ∀ {n a b c d : ℕ}, c ≡ d [MOD n] → (a + c ≡ b + d [MOD n] ↔ a ≡ b [MOD n])
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RocSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- In a compactly generated space `X`, a set `s` is open when `f ⁻¹' s` is
open for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
CompactlyGeneratedSpace.isOpen' : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X},
  (∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
      Continuous f → IsOpen (f ⁻¹' s)) →
    IsOpen s
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.diam_image : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (s : Set α),
  Metric.diam (⇑h '' s) = Metric.diam s
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_iInf : ∀ {ι : Sort u_1} {G : Type u_2} [inst : Group G] (S : ι → Subgroup Gᵐᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso_add'_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n m mn : A) (hnm : m + n = mn)
  (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C),
  (F.shiftIso mn a a'' ⋯).inv.app X =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X))
        ((CategoryTheory.shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X)))
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckLeftact : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
notMem_nonZeroDivisors_iff_right : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {r : M₀}, r ∉ nonZeroDivisors M₀ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS_neg : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k n : ℤ), complEDS b c d k (-n) = -complEDS b c d k n
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- `E^n₁(f₁, f₂, f₃)` identifies to the cokernel
of `δToCycles : H^{n₀}(f₃) ⟶ Z^{n₁}(f₁, f₂)`.  -/
CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex : {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 j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ :
                          autoParam (n₀ + 1 = n₁)
                            CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_1) →
                        (hn₂ :
                            autoParam (n₁ + 1 = n₂)
                              CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_3) →
                          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData
-- Lean.Elab.ConfigEval.Util
_private.Lean.Elab.ConfigEval.Util.0.Lean.Elab.ConfigEval.planDerivation.useDepTypes : Lean.Name →
  (Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)) →
    Array Lean.Expr → Lean.ExprSet → Array Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.Analysis.Seminorm
/-- The image of a ball under addition with a singleton is another ball.  -/
Seminorm.vadd_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x y : E}
  {r : ℝ} (p : Seminorm 𝕜 E), x +ᵥ p.ball y r = p.ball (x +ᵥ y) r
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Coframe.MinimalAxioms.sup_iInf_eq : ∀ {α : Type u} {ι : Sort w} [inst : CompleteLattice α],
  Order.Coframe.MinimalAxioms α → ∀ (a : α) (f : ι → α), a ⊔ ⨅ i, f i = ⨅ i, a ⊔ f i
-- Init.Data.String.Lemmas.Slice
String.Slice.beq_list_eq_false_iff : ∀ {l l' : List String.Slice}, (l == l') = false ↔ List.map String.Slice.copy l ≠ List.map String.Slice.copy l'
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.toContinuousMap : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : Zero R] →
        [inst_2 : TopologicalSpace X] → [inst_3 : TopologicalSpace R] → ContinuousMapZero X R → C(X, R)
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_union_compl_iff_inter_subset : ∀ {α : Type u_1} {s t u : Set α}, s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_bot : ∀ {α : Type u_1} [inst : CompleteLattice α], ⊥.limsSup = ⊥
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_empty_of_one_mem : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {s : Set A}, 1 ∈ s → ProjectiveSpectrum.zeroLocus 𝒜 s = ∅
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.mk.sizeOf_spec : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  [inst_2 : SizeOf J] [inst_3 : SizeOf C] (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt)
  (fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsWeakLimit.fac._autoParam),
  sizeOf { lift := lift, fac := fac } = 1
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The full set is a block.  -/
AddAction.IsBlock.univ : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X], AddAction.IsBlock G Set.univ
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.silentDiagnosticSupport : Lean.Lsp.ClientCapabilities → Bool
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_smul : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {R : Type u_3} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R) (m : MeasureTheory.Measure α) (f : α → MeasureTheory.Measure β),
  (c • m).bind f = c • m.bind f
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.toLocallyConvexSpace : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : NormedSpace ℝ 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : Module ℝ E] [IsScalarTower ℝ 𝕜 E]
  [inst_6 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι}, WithSeminorms p → LocallyConvexSpace ℝ E
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.paths.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  (x x_1 : CategoryTheory.Paths C) (p : x ⟶ x_1), W.paths p = Quiver.Path.rec True (fun {b c} x f P => P ∧ W f) p
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_diagonal : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] {d : n → R},
  (Matrix.diagonal d).permanent = ∏ i, d i
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.spec : (m : Type u_1 → Type u_1) → MLList.Spec✝ m
-- Init.Data.UInt.Lemmas
UInt32.toNat_mod_size : ∀ (n : UInt32), n.toNat % UInt32.size = n.toNat
-- Mathlib.RingTheory.Polynomial.Ideal
Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {a : R} {b : Polynomial R} {P : Polynomial (Polynomial R)},
  P ∈ Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C a), Polynomial.X - Polynomial.C b} ↔
    Polynomial.eval a (Polynomial.eval b P) = 0
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.associator_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  {H : CategoryTheory.Functor C V} [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_6 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_7 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F' G' H' : CategoryTheory.Functor C V} [inst_10 : CategoryTheory.MonoidalCategory.DayConvolution F' G']
  [inst_11 : CategoryTheory.MonoidalCategory.DayConvolution G' H']
  [inst_12 :
    CategoryTheory.MonoidalCategory.DayConvolution F'
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution G' H')]
  [inst_13 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F' G')
      H']
  (f : F ⟶ F') (g : G ⟶ G') (h : H ⟶ H'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.MonoidalCategory.DayConvolution.map f g) h)
      (CategoryTheory.MonoidalCategory.DayConvolution.associator F' G' H').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom
      (CategoryTheory.MonoidalCategory.DayConvolution.map f (CategoryTheory.MonoidalCategory.DayConvolution.map g h))
-- Mathlib.LinearAlgebra.DFinsupp
Submodule.dfinsuppSum_mem : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] {β : ι → Type u_7} [inst_4 : (i : ι) → Zero (β i)]
  [inst_5 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (S : Submodule R N) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → N),
  (∀ (c : ι), f c ≠ 0 → g c (f c) ∈ S) → f.sum g ∈ S
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
  (mem : k ∈ m) {h : k ∈ m.insertMany l}, (m.insertMany l).get k h = m.get k mem
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciSup_set : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : β → α} {s : Set β},
  BddAbove (f '' s) → ∀ {c : β}, c ∈ s → f c ≤ ⨆ i, f ↑i
-- Std.Http.Protocol.H1
/-- Replaces only the writer state variant while preserving pending user/output data.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.setWriterState : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Writer.State → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.iInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set (Set Ω)} {s' : Set (Set Ω)}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  (∃ n, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) → ProbabilityTheory.Kernel.IndepSets (⋂ n, s n) s' κ μ
-- Init.Data.UInt.Lemmas
UInt64.eq_sub_iff_add_eq : ∀ {a b c : UInt64}, a = c - b ↔ a + b = c
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp_supports : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {k : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.contSupp k ⊆ S → Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.contSupp k) S
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMon_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.Bimon.toMon C).comp (CategoryTheory.Mon.forget C) = CategoryTheory.Bimon.forget C
-- Init.GrindInstances.ToInt
Lean.Grind.instAddInt64SintOfNatNat : Lean.Grind.ToInt.Add Int64 (Lean.Grind.IntInterval.sint 64)
-- Init.Data.UInt.Lemmas
UInt16.toFin_toBitVec : ∀ (x : UInt16), x.toBitVec.toFin = x.toFin
-- Std.Http.Data.Headers.Basic
Std.Http.Header.ContentLength.mk.inj : ∀ {length length_1 : ℕ}, { length := length } = { length := length_1 } → length = length_1
-- Mathlib.Data.List.Sigma
List.ne_key : ∀ {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)}, a ∉ l.keys ↔ ∀ s ∈ l, a ≠ s.fst
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
-- Mathlib.NumberTheory.NumberField.DirichletDensity
NumberField.Set.primeIdealZetaSum.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S S_1 : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))),
  S = S_1 → ∀ (s s_1 : ℝ), s = s_1 → NumberField.Set.primeIdealZetaSum S s = NumberField.Set.primeIdealZetaSum S_1 s_1
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.mk : Lean.MVarId → Array Lean.FVarId → Array Lean.FVarId → Lean.Meta.FVarSubst → Lean.Meta.CaseArraySizesSubgoal
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_const_iff : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {C : ε'},
  autoParam (‖C‖ₑ ≠ ⊤) MeasureTheory.integrableOn_const_iff._auto_1 →
    (MeasureTheory.IntegrableOn (fun x => C) s μ ↔ ‖C‖ₑ = 0 ∨ μ s < ⊤)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.instDistribMulActionSpecialLinearGroupForall : {F : Type u_1} →
  [inst : CommRing F] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] → [inst_2 : Fintype ι] → DistribMulAction (Matrix.SpecialLinearGroup ι F) (ι → F)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.mkENodeCore : Lean.Expr → Bool → Bool → ℕ → Bool → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.ofIsoSelf_hom : ∀ {R : Type u} [inst : CommRing R] (M : CommBialgCat R), M.ofIsoSelf.hom = CategoryTheory.CategoryStruct.id M
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inl_XIsoBiprod_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).inv =
    HomologicalComplex.homotopyCofiber.inlX φ i j hij
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore condition of a fraction, expressed in terms of `oreNum` and `oreDenom`.  -/
OreLocalization.ore_eq : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s : ↥S),
  ↑(OreLocalization.oreDenom r s) * r = OreLocalization.oreNum r s * ↑s
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Complex.measurableEquivPi_apply : ∀ (a : ℂ), Complex.measurableEquivPi a = ![a.re, a.im]
-- Init.System.IO
_private.Init.System.IO.0.IO.FS.Handle.readBinToEndInto.loop : IO.FS.Handle → ByteArray → IO ByteArray
-- Mathlib.Topology.Compactness.CompactSystem
IsCompactSystem.of_nonempty_iInter : ∀ {α : Type u_1} {S : Set (Set α)},
  (∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (Set.dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) →
    IsCompactSystem S
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_le_deg_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y), r.degHom f ≤ r.deg X
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPushout.map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F]
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F],
  (sq.map F).IsPushout ↔ sq.IsPushout
-- Mathlib.Data.List.Dedup
List.replicate_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {x : α} {k : ℕ}, k ≠ 0 → (List.replicate k x).dedup = [x]
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedPoly.default : Lean.Grind.CommRing.Poly
-- Mathlib.Analysis.InnerProductSpace.Laplacian
InnerProductSpace.laplacianWithin.eq_1 : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f : E → F) (s : Set E) (x : E),
  InnerProductSpace.laplacianWithin f s x =
    (tensorIteratedFDerivWithinTwo ℝ f s x) (InnerProductSpace.canonicalCovariantTensor E)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_filter : ∀ {α β δ : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {f : β → Bool} {g : δ → β → δ} {init : δ} {it : Std.Iter β},
  Std.Iter.fold g init (Std.Iter.filter f it) = Std.Iter.fold (fun d b => if f b = true then g d b else d) init it
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorRight.eq_1 : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) (α : Type w') [inst_6 : DecidableEq α],
  σ.finsuppTensorRight ρ α = Representation.Equiv.mk (TensorProduct.finsuppRight k k V W α) ⋯
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.i_compHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {c₁ c₂ c₃ : R} (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (F : A →ₐ[R] B),
  (q.compHom F).i = F q.i
-- Lean.Elab.ElabRules
Lean.Elab.Command.elabElabRules : Lean.Elab.Command.CommandElab
-- Mathlib.GroupTheory.PushoutI
/-- Define a homomorphism out of the pushout of monoids by defining it on each object in the
diagram  -/
Monoid.PushoutI.lift : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      {K : Type u_4} →
        [inst : Monoid K] →
          [inst_1 : (i : ι) → Monoid (G i)] →
            [inst_2 : Monoid H] →
              {φ : (i : ι) → H →* G i} →
                (f : (i : ι) → G i →* K) → (k : H →* K) → (∀ (i : ι), (f i).comp (φ i) = k) → Monoid.PushoutI φ →* K
-- Mathlib.Topology.Sets.Closeds
/-- The equivalence `IrreducibleCloseds α ≃ { x : Set α // IsIrreducible x ∧ IsClosed x }` is an
order isomorphism.  -/
TopologicalSpace.IrreducibleCloseds.orderIsoSubtype : (α : Type u_2) →
  [inst : TopologicalSpace α] → TopologicalSpace.IrreducibleCloseds α ≃o { x // IsIrreducible x ∧ IsClosed x }
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instPreadditive : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → (c : ComplexShape ι) → CategoryTheory.Preadditive (HomotopyCategory V c)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Walk.IsCycle.adj_toSubgraph_iff_of_isCycles : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [G.LocallyFinite] {u : V} {p : G.Walk u u},
  p.IsCycle → G.IsCycles → v ∈ p.toSubgraph.verts → ∀ (w : V), p.toSubgraph.Adj v w ↔ G.Adj v w
-- Mathlib.Data.Option.Basic
Option.elim_none_some : ∀ {α : Type u_1} {β : Type u_2} (f : Option α → β) (i : Option α), i.elim (f none) (f ∘ some) = f i
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_eq_nil_iff : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {p : G.Walk u u},
  SimpleGraph.Walk.map f p = SimpleGraph.Walk.nil ↔ p = SimpleGraph.Walk.nil
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_orthogonal_val : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (u : E), Kᗮ.starProjection u = u - K.starProjection u