mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Ring.Basic
List.norm_prod_le' : ∀ {α : Type u_2} [inst : SeminormedRing α] {l : List α}, l ≠ [] → ‖l.prod‖ ≤ (List.map norm l).prod
-- Mathlib.Data.Int.ModEq
/-- Cancel left multiplication on both sides of the `≡` and in the modulus.

For cancelling left multiplication in the modulus, see `Int.ModEq.of_mul_left`.  -/
Int.ModEq.mul_left_cancel' : ∀ {m a b c : ℤ}, c ≠ 0 → c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m]
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.smul_coroot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x), (B x) x • LinearMap.IsReflective.coroot B hx = 2 • B x
-- Init.Data.UInt.IntToBitVec
USize.le_iff_toBitVec32_le : ∀ {a b : USize} (h : System.Platform.numBits = 32), a ≤ b ↔ a.toBitVec32 h ≤ b.toBitVec32 h
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- If every nonconstant polynomial over `k` has a root, then `k` is algebraically closed.
 -/
IsAlgClosed.of_exists_root : ∀ (k : Type u) [inst : Field k],
  (∀ (p : Polynomial k), p.Monic → Irreducible p → ∃ x, Polynomial.eval x p = 0) → IsAlgClosed k
-- Lean.Elab.Syntax
Lean.Elab.Command.checkRuleKind : Lean.SyntaxNodeKind → Lean.SyntaxNodeKind → Bool
-- Mathlib.NumberTheory.Padics.PadicIntegers
_private.Mathlib.NumberTheory.Padics.PadicIntegers.0.PadicInt.cauSeq_to_rat_cauSeq : {p : ℕ} → [hp : Fact (Nat.Prime p)] → CauSeq ℤ_[p] norm → CauSeq ℚ_[p] fun a => ‖a‖
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.π_comp_map : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M), solution.π ∘ₗ relations.map = 0
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.IntInterval.lo?.match_1.eq_4 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.ii with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_4 ()
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.sub_nat_iff : ∀ {p x : ℝ} {n : ℕ}, LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- `sInf s < b` when there is an element `a` in `s` with `a < b`, when `s` is bounded below.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness below for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case.  -/
csInf_lt_of_lt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α}, BddBelow s → a ∈ s → a < b → sInf s < b
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.mapCoeffs_monomial : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (d : Derivation R A M) (n : ℕ) (x : A),
  d.mapCoeffs ((Polynomial.monomial n) x) = PolynomialModule.single A n (d x)
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.ZMod.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Analysis.Calculus.Deriv.Comp
deriv.scomp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {g₁ : 𝕜' → F} {y : 𝕜'},
  DifferentiableAt 𝕜' g₁ y → DifferentiableAt 𝕜 h x → y = h x → deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.prod_iff : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] {x : α × β},
  IsOfFinOrder x ↔ IsOfFinOrder x.1 ∧ IsOfFinOrder x.2
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.lintegral_condKernel_mem : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] (a : α) {s : Set (β × Ω)},
  MeasurableSet s → ∫⁻ (x : β), (κ.condKernel (a, x)) (Prod.mk x ⁻¹' s) ∂κ.fst a = (κ a) s
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
/-- The Radon-Nikodym theorem for signed measures.  -/
MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ],
  MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure ↔ μ.withDensityᵥ (s.rnDeriv μ) = s
-- Mathlib.Testing.Plausible.Functions
_private.Mathlib.Testing.Plausible.Functions.0.List.dlookup.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List (Sigma β) → Sort u_3) →
      (x : List (Sigma β)) →
        (Unit → motive []) → ((a' : α) → (b : β a') → (l : List (Sigma β)) → motive (⟨a', b⟩ :: l)) → motive x
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.natCast : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R] (d : ℕ), d ≠ 0 → (↑d).PosDef
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.main : Lean.Expr → Lean.CollectLevelParams.Visitor
-- Mathlib.CategoryTheory.Limits.Types.Filtered
/-- Recognizing filtered colimits of types. The injectivity condition here is
slightly easier to check as compared to `isColimitOf`.  -/
CategoryTheory.Limits.Types.FilteredColimit.isColimitOf' : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) →
      [CategoryTheory.IsFilteredOrEmpty J] →
        (t : CategoryTheory.Limits.Cocone F) →
          (∀ (x : t.pt), ∃ i xi, x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi) →
            (∀ (i : J) (x y : (fun X => X) (F.obj i)),
                (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x =
                    (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y →
                  ∃ k f,
                    (CategoryTheory.ConcreteCategory.hom (F.map f)) x =
                      (CategoryTheory.ConcreteCategory.hom (F.map f)) y) →
              CategoryTheory.Limits.IsColimit t
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldRedeclInfo.mk.injEq : ∀ (stx stx_1 : Lean.Syntax), ({ stx := stx } = { stx := stx_1 }) = (stx = stx_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toArray.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] (r r_1 : Std.Roi α), r = r_1 → r.toArray = r_1.toArray
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coe_aeval_eq_evalRingHom : ∀ {R : Type u} [inst : CommSemiring R] (x : R), ↑(Polynomial.aeval x) = Polynomial.evalRingHom x
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.isNilpotent_sub : ∀ {R : Type u_1} {x y : R} [inst : Ring R], Commute x y → IsNilpotent x → IsNilpotent y → IsNilpotent (x - y)
-- Mathlib.Order.Monotone.Basic
Int.rel_of_forall_rel_succ_of_le : ∀ {β : Type v} (r : β → β → Prop) [Std.Refl r] [IsTrans β r] {f : ℤ → β},
  (∀ (n : ℤ), r (f n) (f (n + 1))) → ∀ ⦃a b : ℤ⦄, a ≤ b → r (f a) (f b)
-- Lean.Parser.Types
Lean.Parser.InputContext.input : Lean.Parser.InputContext → String
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Under.instCreatesFiniteColimitsTopUnderForget : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [CategoryTheory.Limits.HasPushouts T] →
          [P.IsStableUnderComposition] →
            [P.ContainsIdentities] →
              [P.IsStableUnderCobaseChange] →
                [P.HasOfPrecompProperty P] →
                  CategoryTheory.Limits.CreatesFiniteColimits (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity.0.SimpleGraph.Walk.IsTrail.isEdgeReachable_two_of_isEdgeReachable_two_aux : ∀ {V : Type u_1} {G : SimpleGraph V} {u v x : V} {w : G.Walk u v},
  w.IsTrail → G.IsEdgeReachable 2 u v → x ∈ w.support → G.IsEdgeReachable 2 u x
-- Init.WF
/-- `Acc` is the accessibility predicate. Given some relation `r` (e.g. `<`) and a value `x`,
`Acc r x` means that `x` is accessible through `r`:

`x` is accessible if there exists no infinite sequence `... < y₂ < y₁ < y₀ < x`.
 -/
Acc : {α : Sort u} → (α → α → Prop) → α → Prop
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.symm_symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X}
  (F : f₀.HomotopyRel f₁ S), F.symm.symm = F
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.directedOn : ∀ {α : Type u_2} {s : Set α} [inst : SemilatticeSup α], CountableSupClosed s → DirectedOn (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The strict width of the cusp `∞`, i.e. the `x` such that `𝒢.strictPeriods = zmultiples x`, or
0 if no such `x` exists.  -/
Subgroup.strictWidthInfty : Subgroup (GL (Fin 2) ℝ) → ℝ
-- Mathlib.Algebra.Opposites
MulOpposite.op_zero : ∀ {α : Type u_1} [inst : Zero α], MulOpposite.op 0 = 0
-- Mathlib.Topology.DenseEmbedding
isClosed_property : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β} {p : β → Prop},
  DenseRange e → IsClosed {x | p x} → (∀ (a : α), p (e a)) → ∀ (b : β), p b
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.eqToHom_comp_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {j j' : J} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.biproduct.ι f j') =
    CategoryTheory.Limits.biproduct.ι f j
-- Mathlib.Data.Rat.Lemmas
Rat.natCast_div : ∀ (a b : ℕ), b ∣ a → ↑(a / b) = ↑a / ↑b
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_left_square : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' X : C} {Y Y' : D} (f : X' ⟶ X)
  (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k →
    CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y') g) =
      CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k)
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.weightedOrder_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [NoZeroDivisors R] (w : σ → ℕ) (f g : MvPowerSeries σ R),
  MvPowerSeries.weightedOrder w (f * g) = MvPowerSeries.weightedOrder w f + MvPowerSeries.weightedOrder w g
-- Mathlib.Data.List.GetD
List.getI_append : ∀ {α : Type u} [inst : Inhabited α] (l l' : List α), ∀ n < l.length, (l ++ l').getI n = l.getI n
-- Mathlib.Order.Filter.Map
Filter.map_id' : ∀ {α : Type u_1} {f : Filter α}, Filter.map (fun x => x) f = f
-- Mathlib.Topology.Order.OrderClosed
Ioo_mem_nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Ioo b a ∈ nhdsWithin b (Set.Ioi b)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_additive : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α], IsAddCyclic (Additive α)
-- Init.System.IO
/-- Checks whether the indicated path points to a file that exists. This function will traverse
symlinks.
 -/
System.FilePath.pathExists : System.FilePath → BaseIO Bool
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.lt_csInf_iff : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {a : α},
  s.Finite → s.Nonempty → (a < sInf s ↔ ∀ x ∈ s, a < x)
-- Init.Data.SInt.Bitwise
Int16.toInt8_and : ∀ (a b : Int16), (a &&& b).toInt8 = a.toInt8 &&& b.toInt8
-- Mathlib.Data.Set.Card
Set.coe_ncard_eq_encard : ∀ {α : Type u_1} (s : Set α) [Finite ↑s], ↑s.ncard = s.encard
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_smul_vsub_vadd_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {p₁ p₂ : P} (x : P), p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, t ≤ 0 → s.WOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_commute : ∀ {α : Type u_3} [inst : DivisionSemiring α] (q : ℚ≥0) (a : α), Commute (↑q) a
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- Given commutative rings `A` and `B` with respective localizations `IsLocalization M K` and
`IsLocalization N L`, and a ring homomorphism `f : A →+* B` satisfying `M ≤ Submonoid.comap f N`, a
fractional ideal `I` of `A` can be extended along `f` to a fractional ideal of `B`.  -/
FractionalIdeal.extended : {A : Type u_1} →
  [inst : CommRing A] →
    {B : Type u_2} →
      [inst_1 : CommRing B] →
        {f : A →+* B} →
          {K : Type u_3} →
            {M : Submonoid A} →
              [inst_2 : CommRing K] →
                [inst_3 : Algebra A K] →
                  [IsLocalization M K] →
                    (L : Type u_4) →
                      {N : Submonoid B} →
                        [inst_5 : CommRing L] →
                          [inst_6 : Algebra B L] →
                            [IsLocalization N L] → M ≤ Submonoid.comap f N → FractionalIdeal M K → FractionalIdeal N L
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instMin : (M : Type u_1) → [inst : MulOneClass M] → Min (SaturatedSubmonoid M)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_mem_pointwise_smul_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] {a : α}
  {S : Subgroup G} {x : G}, a • x ∈ a • S ↔ x ∈ S
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Ici' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Iio a).Nonempty → frontier (Set.Ici a) = {a}
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_lt_ofENat : ∀ {m n : ℕ∞}, ↑m < ↑n ↔ m < n
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.polynomial_mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β]
  [ContinuousAdd β] [ContinuousMul β],
  Asymptotics.SuperpolynomialDecay l k f →
    ∀ (p : Polynomial β), Asymptotics.SuperpolynomialDecay l k fun x => Polynomial.eval (k x) p * f x
-- Mathlib.Logic.Equiv.Prod
/-- The type of dependent functions on a sum type `ι ⊕ ι'` is equivalent to the type of pairs of
functions on `ι` and on `ι'`. This is a dependent version of `Equiv.sumArrowEquivProdArrow`.  -/
Equiv.sumPiEquivProdPi : {ι : Type u_10} →
  {ι' : Type u_11} →
    (π : ι ⊕ ι' → Type u_9) → ((i : ι ⊕ ι') → π i) ≃ ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The function x ↦ ∑ a_i b_i^x is injective. This implies the uniqueness of `p`.  -/
AkraBazziRecurrence.injective_sumCoeffsExp : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), Function.Injective fun p => ∑ i, a i * b i ^ p
-- Lean.Meta.Tactic.Grind.SimpUtil
/-- Returns the simplification context used by `grind`.  -/
Lean.Meta.Grind.getSimpContext : Lean.Grind.Config → Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.GroupTheory.GroupAction.Basic
isCancelVAdd_iff_stabilizer_eq_bot : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α],
  IsCancelVAdd G α ↔ ∀ (a : α), AddAction.stabilizer G a = ⊥
-- Mathlib.RingTheory.DedekindDomain.Dvr
/-- The localization of a Dedekind domain is a Dedekind domain.  -/
IsLocalization.isDedekindDomain : ∀ (A : Type u_1) [inst : CommRing A] [IsDomain A] [IsDedekindDomain A] {M : Submonoid A},
  M ≤ nonZeroDivisors A →
    ∀ (Aₘ : Type u_2) [inst_3 : CommRing Aₘ] [IsDomain Aₘ] [inst_5 : Algebra A Aₘ] [IsLocalization M Aₘ],
      IsDedekindDomain Aₘ
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The external product of `CompStruct` between edges of `2`-truncated simplicial sets.  -/
SSet.Truncated.Edge.CompStruct.tensor : {X Y : SSet.Truncated 2} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} →
    {e₀₁ : SSet.Truncated.Edge x₀ x₁} →
      {e₁₂ : SSet.Truncated.Edge x₁ x₂} →
        {e₀₂ : SSet.Truncated.Edge x₀ x₂} →
          e₀₁.CompStruct e₁₂ e₀₂ →
            {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} →
              {e'₀₁ : SSet.Truncated.Edge y₀ y₁} →
                {e'₁₂ : SSet.Truncated.Edge y₁ y₂} →
                  {e'₀₂ : SSet.Truncated.Edge y₀ y₂} →
                    e'₀₁.CompStruct e'₁₂ e'₀₂ → (e₀₁.tensor e'₀₁).CompStruct (e₁₂.tensor e'₁₂) (e₀₂.tensor e'₀₂)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mk.sizeOf_spec : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : SizeOf R] [inst_6 : SizeOf L] [inst_7 : SizeOf M]
  (toSubmodule : Submodule R M) (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier),
  sizeOf { toSubmodule := toSubmodule, lie_mem := lie_mem } = 1 + sizeOf toSubmodule
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq.eq_3 : ∀ (x x_1 : Int.Internal.Linear.Poly),
  (∀ (a b : ℤ), x = Int.Internal.Linear.Poly.num a → x_1 = Int.Internal.Linear.Poly.num b → False) →
    (∀ (a : ℤ) (a_1 : Int.Internal.Linear.Var) (a_2 : Int.Internal.Linear.Poly) (b : ℤ) (b_1 : Int.Internal.Linear.Var)
        (b_2 : Int.Internal.Linear.Poly),
        x = Int.Internal.Linear.Poly.add a a_1 a_2 → x_1 = Int.Internal.Linear.Poly.add b b_1 b_2 → False) →
      Int.Internal.Linear.instBEqPoly.beq x x_1 = false
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or
uppercase letters.  -/
Mathlib.CrossRef.stacksTagFn : Lean.Parser.ParserFn
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyD_eq_getKeyDₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) (fallback : α),
  l.getKeyD k fallback = Std.DTreeMap.Internal.Impl.getKeyDₘ k l fallback
-- Mathlib.Topology.Algebra.Order.Floor
FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K]
  [inst_4 : TopologicalSpace K] [OrderTopology K] (a c : K) (d : ℕ),
  Filter.Tendsto (fun n => a * c ^ n / ↑(n - d).factorial) Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.neg_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant], -MeasureTheory.ae μ = MeasureTheory.ae μ
-- Mathlib.Topology.Spectral.Hom
SpectralMap.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Order.Category.Semilat
SemilatSupCat.Iso.mk_inv_toFun : ∀ {α β : SemilatSupCat} (e : α.X ≃o β.X) (a : β.X), (SemilatSupCat.Iso.mk e).inv a = e.symm a
-- Mathlib.Algebra.Group.Units.Opposite
IsAddUnit.op : ∀ {M : Type u_2} [inst : AddMonoid M] {m : M}, IsAddUnit m → IsAddUnit (AddOpposite.op m)
-- Mathlib.RepresentationTheory.Character
FDRep.char_linHom : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Group G] (V W : FDRep k G) (g : G),
  (FDRep.of (Representation.linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_const : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E], m ≤ m₀ → ∀ (c : E) [MeasureTheory.IsFiniteMeasure μ], μ[fun x => c | m] = fun x => c
-- Mathlib.LinearAlgebra.Dimension.Basic
lift_rank_map_le : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (p : Submodule R M),
  Cardinal.lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ Cardinal.lift.{v', v} (Module.rank R ↥p)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurry0_curry0 : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×0]→L[𝕜] G'),
  ContinuousMultilinearMap.uncurry0 𝕜 G f.curry0 = f
-- Init.Data.Bool
Bool.and_not_eq_right_iff_and : ∀ {a b : Bool}, (a && !b) = b ↔ (!a) = true ∧ (!b) = true
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
MulAction.isMultiplyPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {n : ℕ},
  MulAction.IsMultiplyPretransitive G α n ↔ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
-- Mathlib.Data.Fintype.Sigma
Set.biUnion_finsetSigma_univ : ∀ {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_3} [inst : (i : ι) → Fintype (κ i)] (s : Finset ι)
  (f : Sigma κ → Set α), ⋃ ij ∈ s.sigma fun x => Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- Given a finite subset `A` of a group `G` and a subgroup `H ≤ G`, there exists a subset `Z ⊆ A`
such that `H * Z = H * A` and the cosets `Hz` are disjoint as `z` runs over `Z`.  -/
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.exists_subset_mul_eq_mul_injOn : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (A : Finset G),
  ∃ Z ⊆ A, ↑H * ↑Z = ↑H * ↑A ∧ Set.InjOn (fun x => MulOpposite.op x • ↑H) ↑Z
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hom_ext : ∀ {X Y : GrpCat} {f g : X ⟶ Y}, GrpCat.Hom.hom f = GrpCat.Hom.hom g → f = g
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto a complete subspace, as an
unbundled function. This definition is only intended for use in
setting up the bundled version `orthogonalProjection` and should not
be used once that is defined.  -/
Submodule.orthogonalProjectionFn : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → {K : Submodule 𝕜 E} → [K.HasOrthogonalProjection] → E → E
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.IsInternal.toBaseChange_bijective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (ℳ : ι → Submodule R M) [inst_3 : DecidableEq ι] [inst_4 : CommSemiring S]
  [inst_5 : Algebra R S], DirectSum.IsInternal ℳ → ∀ (i : ι), Function.Bijective ⇑(Submodule.toBaseChange S (ℳ i))