mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OrderOfElement
AddSubgroup.addOrderOf_mk : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (a : G) (ha : a ∈ H), addOrderOf ⟨a, ha⟩ = addOrderOf a
-- Init.Data.Int.Lemmas
Int.neg_inj : ∀ {a b : ℤ}, -a = -b ↔ a = b
-- Mathlib.Order.PropInstances
Pi.eq_top_iff_refl_of_subsingleton : ∀ {α : Type u_2} [Subsingleton α] {r : α → α → Prop}, r = ⊤ ↔ Std.Refl r
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_of_isColimit_cofan : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderFiniteCoproducts] {J : Type u_2} [Finite J] {f : J → C} {F : CategoryTheory.Limits.Cofan f}
  (hF : CategoryTheory.Limits.IsColimit F), (∀ (j : J), P (f j)) → P F.pt
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.WF
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCallHierarchyIncomingCall.default : Lean.Lsp.CallHierarchyIncomingCall
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasLimitsOfShape_thinSkeleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [Quiver.IsThin C] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.ThinSkeleton C)
-- Mathlib.Data.Finset.NoncommProd
/-- Proof used in definition of `Finset.noncommSum`  -/
Finset.noncommSum_lemma : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (f : α → β),
  (↑s).Pairwise (Function.onFun AddCommute f) → {x | x ∈ Multiset.map f s.val}.Pairwise AddCommute
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod.sizeOf_spec : ∀ (k : ℤ) (y? : Option Int.Internal.Linear.Var) (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod k y? c) = 1 + sizeOf k + sizeOf y? + sizeOf c
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.lift_fac_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsClosedImmersion f]
  (H : AlgebraicGeometry.Scheme.Hom.ker f ≤ AlgebraicGeometry.Scheme.Hom.ker g) {Z_1 : AlgebraicGeometry.Scheme}
  (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsClosedImmersion.lift f g H)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] (L : CategoryTheory.Functor C₂ D) [inst_3 : L.IsLocalization W₂]
  {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃),
  CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y =
    CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).hom.left =
    CategoryTheory.CategoryStruct.id (W ⟹ X.left)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.saveBVar : ℕ → Lean.Meta.Grind.NormalizePattern.M✝ Unit
-- Mathlib.Order.Filter.Germ.Basic
/-- Lift a relation `r : β → γ → Prop` to `Germ l β → Germ l γ → Prop`.  -/
Filter.Germ.LiftRel : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {l : Filter α} → (β → γ → Prop) → l.Germ β → l.Germ γ → Prop
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_apply : ∀ {A : Type u_1} [inst : AddMonoid A] [inst_1 : Finset.HasAntidiagonal A]
  (x : (n : A) × ↥(Finset.HasAntidiagonal.antidiagonal n)), Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd x = ↑x.snd
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.eq_pow_second_of_chain_of_has_chain : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [UniqueFactorizationMonoid M] {q : Associates M} {n : ℕ},
  n ≠ 0 →
    ∀ {c : Fin (n + 1) → Associates M},
      StrictMono c → (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → q ≠ 0 → q = c 1 ^ n
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.separable_cyclotomic : ∀ (n : ℕ) (K : Type u_2) [inst : Field K] [NeZero ↑n], (Polynomial.cyclotomic n K).Separable
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_mod_two : ∀ (b : Bool) (n : ℕ), Nat.bit b n % 2 = b.toNat
-- Init.Core
/-- Places a value into its squash type, in which it cannot be distinguished from any other.
 -/
Squash.mk : {α : Sort u} → α → Squash α
-- Mathlib.Topology.Algebra.Monoid
continuous_finsum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M},
  (∀ (i : ι), Continuous (f i)) →
    (LocallyFinite fun i => Function.support (f i)) → Continuous fun x => ∑ᶠ (i : ι), f i x
-- Mathlib.Tactic.ITauto
/-- Debug printer for the context.  -/
Mathlib.Tactic.ITauto.Context.format : Mathlib.Tactic.ITauto.Context → Std.Format
-- Mathlib.Data.Erased
Erased.instToString : (α : Type u) → ToString (Erased α)
-- Mathlib.Data.Nat.MaxPowDiv
_private.Mathlib.Data.Nat.MaxPowDiv.0.Nat.maxPowDvdDiv.match_1.eq_1 : ∀ (motive : ℕ × ℕ → Sort u_1) (e q : ℕ) (h_1 : (e q : ℕ) → motive (e, q)),
  (match (e, q) with
    | (e, q) => h_1 e q) =
    h_1 e q
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Two finite-dimensional topological vector spaces over a complete normed field are continuously
linearly equivalent if they have the same (finite) dimension.  -/
FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F]
  [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜]
  [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F],
  Module.finrank 𝕜 E = Module.finrank 𝕜 F → Nonempty (E ≃L[𝕜] F)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.atImInfty.eq_1 : UpperHalfPlane.atImInfty = Filter.comap UpperHalfPlane.im Filter.atTop
-- Mathlib.Data.Matrix.Reflection
Matrix.transposeᵣ.eq_2 : ∀ {α : Type u_1} (x n : ℕ) (A : Matrix (Fin x) (Fin (n + 1)) α),
  A.transposeᵣ = Matrix.of (Matrix.vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ).transposeᵣ)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_sum : ∀ (α : Type u) (β : Type v),
  Cardinal.mk (α ⊕ β) = Cardinal.lift.{v, u} (Cardinal.mk α) + Cardinal.lift.{u, v} (Cardinal.mk β)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.instRegularOfIsHaarMeasureOfCompactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] [CompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ], μ.Regular
-- Lean.ScopedEnvExtension
Lean.instInhabitedScopedEnvExtension.default : {α β σ : Type} → [Inhabited α] → Lean.ScopedEnvExtension α β σ
-- Mathlib.CategoryTheory.EpiMono
/-- There is a splitting  -/
CategoryTheory.IsSplitEpi.exists_splitEpi : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsSplitEpi f],
  Nonempty (CategoryTheory.SplitEpi f)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.mkIterator.eq_1 : ∀ (s : String), String.Legacy.mkIterator s = { s := s, i := 0 }
-- Lean.Environment
/-- Resulting "main branch" environment which contains the declaration name as an asynchronous
constant. Accessing the constant or kernel environment will block until the corresponding
`AddConstAsyncResult.commit*` function has been called.
 -/
Lean.Environment.AddConstAsyncResult.mainEnv : Lean.Environment.AddConstAsyncResult → Lean.Environment
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_finset_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} {s : Finset ι}, LinearIndepOn R v ↑s ↔ ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
-- Lean.Server.References
/-- Determines whether this transient worker ILean includes actual references.  -/
Lean.Server.TransientWorkerILean.hasRefs : Lean.Server.TransientWorkerILean → Bool
-- Init.Control.Except
/-- Monads that provide the ability to ensure an action happens, regardless of exceptions or other
failures.

`MonadFinally.tryFinally'` is used to desugar `try ... finally ...` syntax.
 -/
MonadFinally : (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.Analysis.Complex.Polynomial.GaussLucas
Polynomial.derivRootWeight.eq_1 : ∀ (P : Polynomial ℂ) (z w : ℂ),
  P.derivRootWeight z w =
    if Polynomial.eval z P = 0 then Pi.single z 1 w else ↑(Polynomial.rootMultiplicity w P) / ‖z - w‖ ^ 2
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The canonical linear map from the direct sum of the `A i` to the free product  -/
LinearAlgebra.FreeProduct.ι' : {I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] → (DirectSum I fun i => A i) →ₗ[R] LinearAlgebra.FreeProduct R A
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g)
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g)
  (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)),
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φQ = φ.τ₂
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_nil_cons : ∀ {α : Type u_1} (x : α) (s : Stream'.Seq α), dist Stream'.Seq.nil (Stream'.Seq.cons x s) = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff m₂ ⋯).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.lipschitzWith_ofFun_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] [inst_1 : PseudoEMetricSpace β]
  {f : γ → α → β} {K : NNReal},
  (LipschitzWith K fun x => UniformFun.ofFun (f x)) ↔ ∀ (c : α), LipschitzWith K fun x => f x c
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Cell.ofEq.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (k' : α) (v' : β k')
  (hcmp : ∀ [Std.OrientedOrd α], k k' = Ordering.eq),
  Std.DTreeMap.Internal.Cell.ofEq k' v' hcmp = { inner := some ⟨k', v'⟩, property := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_le_size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, t.size ≤ (Std.ExtDTreeMap.Const.insertMany t l).size
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.distribMulAction : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : Semiring R'] →
      [inst_1 : AddMonoid α] → [DistribMulAction R' α] → (S : Subsemiring R') → DistribMulAction (↥S) α
-- Mathlib.Order.Partition.Basic
Partition.instIsTransRel : ∀ {α : Type u_1} {u : Set α} (P : Partition u), IsTrans α P.Rel
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.faithful_linearYoneda : ∀ (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],
  (CategoryTheory.linearYoneda R C).Faithful
-- Mathlib.Topology.Algebra.Group.Basic
Prod.continuousNeg : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] [inst_3 : TopologicalSpace H]
  [inst_4 : Neg H] [ContinuousNeg H], ContinuousNeg (G × H)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.Augmented.σ₀Iter_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (Y : CategoryTheory.SimplicialObject.Augmented C)
  {n m : ℕ} (i : ℕ) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.Augmented.σ₀Iter_hom_app._auto_1)
  {Z : C} (h : Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.left.σ₀Iter i hi)
      (CategoryTheory.CategoryStruct.comp (Y.hom.app (Opposite.op { len := m })) h) =
    CategoryTheory.CategoryStruct.comp (Y.hom.app (Opposite.op { len := n })) h
-- Lean.Meta.Tactic.Grind.Types
/-- Sequential conjunction: executes both `x` and `y`.

- Runs `x` and always runs `y` afterward, regardless of whether `x` made progress.
- It is not applicable only if both `x` and `y` are not applicable.
 -/
Lean.Meta.Grind.Action.andAlso : Lean.Meta.Grind.Action → Lean.Meta.Grind.Action → Lean.Meta.Grind.Action
-- Mathlib.Data.Finite.Prod
Prod.finite_iff : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β], Finite (α × β) ↔ Finite α ∧ Finite β
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If a function is locally integrable in a second countable topological space,
then there exists a sequence of open sets covering the space on which it is integrable.  -/
MeasureTheory.LocallyIntegrable.exists_nat_integrableOn : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [SecondCountableTopology X],
  MeasureTheory.LocallyIntegrable f μ →
    ∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = Set.univ ∧ ∀ (n : ℕ), MeasureTheory.IntegrableOn f (u n) μ
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The sign at index `i` for Euler characteristic computations.  -/
ComplexShape.χ : {ι : Type u_1} → (c : ComplexShape ι) → [c.EulerCharSigns] → ι → ℤˣ
-- Mathlib.Data.PFunctor.Univariate.Basic
Functor.supp.eq_1 : ∀ {F : Type u → Type v} [inst : Functor F] {α : Type u} (x : F α),
  Functor.supp x = {y | ∀ ⦃p : α → Prop⦄, Functor.Liftp p x → p y}
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.preGNS_norm_def : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  (a : f.PreGNS), ‖a‖ = √(f (star (f.ofPreGNS a) * f.ofPreGNS a)).re
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.comp.congr_simp : ∀ {𝕜₁ : 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 g_1 : F →SWOT[σ₂₃] G),
  g = g_1 → ∀ (f f_1 : E →SWOT[σ₁₂] F), f = f_1 → g.comp f = g_1.comp f_1
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.Normal.conj_smul_eq_self : ∀ {G : Type u_2} [inst : Group G] (g : G) (H : Subgroup G) [h : H.Normal], MulAut.conj g • H = H
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda_inv_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) {Z : Type u₂} (h : (F.obj i ⟶ A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).inv
      (CategoryTheory.CategoryStruct.comp
        (TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i) g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) h
-- Init.Data.UInt.Lemmas
UInt8.not_le : ∀ {a b : UInt8}, ¬a ≤ b ↔ b < a
-- Mathlib.Data.Countable.Defs
instCountablePLift : ∀ {α : Sort u} [Countable α], Countable (PLift α)
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
RestrictedProduct.mk.congr_simp : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} (x x_1 : (i : ι) → R i) (e_x : x = x_1)
  (hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ A i), RestrictedProduct.mk x hx = RestrictedProduct.mk x_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toMatrix₂Aux_toLinearMap₂'Aux : ∀ (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : Semiring R₁] [inst_2 : Semiring S₁] [inst_3 : Semiring R₂]
  [inst_4 : Semiring S₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Module S₁ N₂]
  [inst_8 : Module S₂ N₂] [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂]
  [inst_11 : SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} [inst_12 : Fintype n] [inst_13 : Fintype m]
  [inst_14 : DecidableEq n] [inst_15 : DecidableEq m] (f : Matrix n m N₂),
  (LinearMap.toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) (Matrix.toLinearMap₂'Aux σ₁ σ₂ f) = f
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem_subset_self : ∀ {α : Type u_1} {S : Set (Set α)}, IsPiSystem S → generatePiSystem S ⊆ S
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.evalTactic : Lean.Meta.Grind.Methods → Lean.Meta.Grind.EvalTactic
-- Mathlib.Tactic.Linter.Style
/-- The "longLine" linter emits a warning on lines longer than
`linter.style.longLine.maxLineLength` (which defaults to 100) characters.
We allow lines containing URLs to be longer, though.  -/
Mathlib.Linter.linter.style.longLine : Lean.Option Bool
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.comp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8} {γ : ι → Type u_9}
  {mβ : (i : ι) → MeasurableSpace (β i)} {mγ : (i : ι) → MeasurableSpace (γ i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    ∀ (g : (i : ι) → β i → γ i),
      (∀ (i : ι), Measurable (g i)) → ProbabilityTheory.Kernel.iIndepFun (fun i => g i ∘ f i) κ μ
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_var : ∀ (ctx : Int.Internal.Linear.Context) (x y : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.of_var_eq_var_cert x y p = true →
    Int.Internal.Linear.Var.denote ctx x = Int.Internal.Linear.Var.denote ctx y →
      Int.Internal.Linear.Poly.denote' ctx p = 0
-- Mathlib.RingTheory.Polynomial.Ideal
Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S) (I : Ideal R),
  I ≠ ⊤ →
    ∀ [inst_3 : Invertible x],
      Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤ →
        ∃ p, p.leadingCoeff - 1 ∈ I ∧ (Polynomial.aeval ⅟x) p = 0
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step_cons_of_isLT : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β} [inst : Ord α] {upper : α} {h : (compare k upper).isLT = true},
  { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }.step =
    Std.IterStep.yield { internalState := { iter := Std.DTreeMap.Internal.Zipper.prependMap t it, upper := upper } }
      ⟨k, v⟩
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_lt_sub_iff_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c : α},
  -a < b - c ↔ c < a + b
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
/-- The basis on `ι →₀ R` with basis vectors `fun i ↦ single i 1`.  -/
Finsupp.basisSingleOne : {R : Type u_1} → {ι : Type u_3} → [inst : Semiring R] → Module.Basis ι R (ι →₀ R)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Triangulated.Octahedron.map_m₁ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] [inst_4 : CategoryTheory.Limits.HasZeroObject C]
  [inst_5 : CategoryTheory.Limits.HasZeroObject D] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : CategoryTheory.Preadditive D] [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃}
  {u₁₃ : X₁ ⟶ X₃} {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D)
  [inst_12 : F.CommShift ℤ] [inst_13 : F.IsTriangulated], (h.map F).m₁ = F.map h.m₁
-- Lean.Elab.Exception
Lean.Elab.mkMessageCore : String → Lean.FileMap → Lean.MessageData → Lean.MessageSeverity → String.Pos.Raw → String.Pos.Raw → Lean.Message
-- Lean.Elab.Do.Basic
Lean.Elab.Do.withDeadCode : {α : Type} → Lean.Elab.Do.CodeLiveness → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α