mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.equiv_trans : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_5} [inst_1 : Ring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M : Type u_6} {N : Type u_7}
  [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N] [inst_7 : Module R₂ N] (P : Submodule R M)
  (Q : Submodule R₂ N) {R₃ : Type u_8} {O : Type u_9} [inst_8 : Ring R₃] [inst_9 : AddCommGroup O]
  [inst_10 : Module R₃ O] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  [inst_11 : RingHomInvPair σ₂₃ σ₃₂] [inst_12 : RingHomInvPair σ₃₂ σ₂₃] [inst_13 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_14 : RingHomInvPair σ₃₁ σ₁₃] [inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_16 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  (S : Submodule R₃ O) (e : M ≃ₛₗ[σ₁₂] N) (f : N ≃ₛₗ[σ₂₃] O) (he : Submodule.map (↑e) P = Q)
  (hf : Submodule.map (↑f) Q = S) (hef : Submodule.map (↑(e.trans f)) P = S),
  Submodule.Quotient.equiv P S (e.trans f) hef =
    (Submodule.Quotient.equiv P Q e he).trans (Submodule.Quotient.equiv Q S f hf)
-- Mathlib.Algebra.Module.Submodule.Order
/-- A submodule of an ordered additive monoid is an ordered additive monoid.  -/
Submodule.toIsOrderedAddMonoid : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedAddMonoid M] [inst_4 : Module R M] (S : Submodule R M), IsOrderedAddMonoid ↥S
-- Mathlib.Data.Matrix.Mul
/-- `M *ᵥ v` (notation for `mulVec M v`) is the matrix-vector product of matrix `M` and vector `v`,
where `v` is seen as a column vector.

The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `dotProduct`,
so that `A *ᵥ v ⬝ᵥ B *ᵥ w` is parsed as `(A *ᵥ v) ⬝ᵥ (B *ᵥ w)`.
 -/
Matrix.mulVec : {m : Type u_2} →
  {n : Type u_3} → {α : Type v} → [NonUnitalNonAssocSemiring α] → [Fintype n] → Matrix m n α → (n → α) → m → α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.desc.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g}
  (hs hs_1 : CategoryTheory.Limits.IsColimit s),
  hs = hs_1 →
    ∀ {W : C} (k k_1 : Y ⟶ W) (e_k : k = k_1)
      (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k),
      CategoryTheory.Limits.Cofork.IsColimit.desc hs k h = CategoryTheory.Limits.Cofork.IsColimit.desc hs_1 k_1 ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {c : ℕ}, m.WF → (m.Equiv (Std.DHashMap.Raw.emptyWithCapacity c) ↔ m.isEmpty = true)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- A `C^n` manifold with `0` and `Inv` such that `fun x ↦ x⁻¹` is `C^n` at all nonzero points.
Any complete normed (semi)field has this property.  -/
ContMDiffInv₀ : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ →
                  (G : Type u_4) → [Inv G] → [Zero G] → [inst : TopologicalSpace G] → [ChartedSpace H G] → Prop
-- Mathlib.Data.Setoid.Partition
/-- index for type `α`  -/
IndexedPartition.index : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → IndexedPartition s → α → ι
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_basisFun`. -/
BilinForm.toMatrix_basisFun : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  LinearMap.BilinForm.toMatrix (Pi.basisFun R₁ n) = LinearMap.BilinForm.toMatrix'
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.tensorEquivSum_X_tmul_one : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (i : σ),
  (MvPolynomial.tensorEquivSum R σ ι S) (MvPolynomial.X i ⊗ₜ[R] 1) = MvPolynomial.X (Sum.inl i)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.eq_bot_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), p = ⊥ ↔ ∀ x ∈ p, x = 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_cons : ∀ (exp : ℝ) (tl : Tactic.ComputeAsymptotics.UnitMonomial) (basis_hd : ℝ → ℝ)
  (basis_tl : Tactic.ComputeAsymptotics.Basis),
  Tactic.ComputeAsymptotics.UnitMonomial.toLogFun (exp :: tl) (basis_hd :: basis_tl) =
    exp • Real.log ∘ basis_hd + tl.toLogFun basis_tl
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.LinearWeights.mk : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [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]
  [inst_7 : LieRing.IsNilpotent L],
  (∀ (χ : L → R), LieModule.genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y) →
    (∀ (χ : L → R), LieModule.genWeightSpace M χ ≠ ⊥ → ∀ (t : R) (x : L), χ (t • x) = t • χ x) →
      (∀ (χ : L → R), LieModule.genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ ⁅x, y⁆ = 0) → LieModule.LinearWeights R L M
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
exteriorPower.pairingDual_apply_apply_eq_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : LinearOrder ι] (x : ι → M) (f : ι → Module.Dual R M),
  (∀ (i : ι), (f i) (x i) = 1) →
    (∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0) →
      ∀ (n : ℕ) (a : Fin n ↪o ι),
        ((exteriorPower.pairingDual R M n) ((exteriorPower.ιMulti R n) (f ∘ ⇑a)))
            ((exteriorPower.ιMulti R n) (x ∘ ⇑a)) =
          1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.right_unitor_hom_inv : ∀ {B : Type u} [inst : Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.right_unitor f).vcomp (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f))
    (CategoryTheory.FreeBicategory.Hom₂.id (f.comp (CategoryTheory.FreeBicategory.Hom.id b)))
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_nsmul : ∀ (a : ENNReal) (n : ℕ), (n • a).toReal = n • a.toReal
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- Given a presieve `R` on `U`, we obtain a covering family of open sets in `X`, by taking as index
type the type of dependent pairs `(V, f)`, where `f : V ⟶ U` is in `R`.
 -/
TopCat.Presheaf.coveringOfPresieve : {X : TopCat} →
  (U : TopologicalSpace.Opens ↑X) →
    (R : CategoryTheory.Presieve U) → (V : TopologicalSpace.Opens ↑X) × { f // R f } → TopologicalSpace.Opens ↑X
-- Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
CategoryTheory.SimplicialObject.diagonal.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ},
  X.diagonal = X.map (SimplexCategory.diag n).op
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul_one_oreDiv_one_smul : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M] [inst_5 : IsScalarTower R M M]
  [inst_6 : IsScalarTower R M X] (r : R) (x : OreLocalization S X), (r • 1 /ₒ 1) • x = r • x
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.norm_comp_le_of_le' : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {f : NormedAddGroupHom V₁ V₂}
  {g : NormedAddGroupHom V₂ V₃} (C₁ C₂ C₃ : ℝ), C₃ = C₂ * C₁ → ‖g‖ ≤ C₂ → ‖f‖ ≤ C₁ → ‖g.comp f‖ ≤ C₃
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_one : ∀ {α : Type u} [inst : Lean.Grind.Semiring α], ↑1 = 1
-- Mathlib.Logic.Equiv.Set
/-- If `s` is a set in `range f`,
then its image under `rangeSplitting f` is in bijection (via `f`) with `s`.
 -/
Equiv.Set.rangeSplittingImageEquiv : {α : Type u_3} → {β : Type u_4} → (f : α → β) → (s : Set ↑(Set.range f)) → ↑(Set.rangeSplitting f '' s) ≃ ↑s
-- Mathlib.Data.Stream.Defs
/-- An auxiliary definition for `Stream'.cycle` corecursive def  -/
Stream'.cycleG : {α : Type u} → α × List α × α × List α → α × List α × α × List α
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
CategoryTheory.Functor.IsDenseAt.iff_of_final : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {C' : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} C']
  (G : CategoryTheory.Functor C' C) [(CategoryTheory.CostructuredArrow.pre G F Y).Final],
  (G.comp F).isDenseAt Y ↔ F.isDenseAt Y
-- Mathlib.Topology.Algebra.Monoid
mulHomOfTendsto.eq_1 : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Mul M₁]
  [inst_3 : Mul M₂] [inst_4 : ContinuousMul M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : MulHomClass F M₁ M₂]
  {l : Filter α} (f : M₁ → M₂) (g : α → F) [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)),
  mulHomOfTendsto f g h = mulHomOfMemClosureRangeCoe f ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.injective_of_map_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_6} {M' : Type u_7} {N : Type u_8}
  [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [IsLocalizedModule S f] [inst_6 : AddCommGroup N] [inst_7 : Module R N] {g : M' →ₗ[R] N},
  (∀ (m : M), g (f m) = 0 → f m = 0) → Function.Injective ⇑g
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S T : J.Cover X} (x : CategoryTheory.Meq P S) (y : CategoryTheory.Meq P T),
  CategoryTheory.GrothendieckTopology.Plus.mk x = CategoryTheory.GrothendieckTopology.Plus.mk y ↔
    ∃ W h1 h2, x.refine h1 = y.refine h2
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.of_edist_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  (∀ (x y : α), edist (f x) (f y) ≤ edist x y) → LipschitzWith 1 f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A continuous function with compact support is strongly measurable.  -/
Continuous.stronglyMeasurable_of_hasCompactMulSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : One β] {f : α → β},
  Continuous f → HasCompactMulSupport f → MeasureTheory.StronglyMeasurable f
-- Mathlib.Topology.DiscreteSubset
/-- In a `T1Space`, complements of singleton sets are codiscrete within any set.
 -/
compl_singleton_mem_codiscreteWithin : ∀ {X : Type u_3} [inst : TopologicalSpace X] [T1Space X] {s : Set X} (x : X), {x}ᶜ ∈ Filter.codiscreteWithin s
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_of_not_measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ],
  ¬Measurable (Function.uncurry f) → κ.withDensity f = 0
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.equivalence_isCohomologous : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C), Equivalence CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.continuousLinearEquiv_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)]
  [inst_3 : (i : ι) → TopologicalSpace (β i)] (a : WithLp p ((i : ι) → β i)) (i : ι),
  (PiLp.continuousLinearEquiv p 𝕜 β) a i = a.ofLp i
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.ULiftT.run_map : ∀ {n : Type (max u v) → Type v'} [inst : Monad n] {α β : Type u} {x : Std.Iterators.ULiftT n α} {f : α → β},
  (f <$> x).run = do
    let a ← x.run
    pure { down := f a.down }
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ici_add_Ioi_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrderTop α] (a b : α), Finset.Ici a + Finset.Ioi b ⊆ Finset.Ioi (a + b)
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorFlipCurriedTensorObjWhiskeringRightTensorBifunctor : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.Localization.Lifting₂
                        (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)
                        (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) W W
                        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.comp
                          ((CategoryTheory.Functor.whiskeringRight C C (CategoryTheory.LocalizedMonoidal L W ε)).obj
                            (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)))
                        (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).flip
-- Mathlib.Order.Sublattice
Sublattice.instInhabited : {α : Type u_2} → [inst : Lattice α] → Inhabited (Sublattice α)
-- Std.Time.Zoned.ZoneRules
/-- Distinguishes between universal time and local time.
 -/
Std.Time.TimeZone.LocalTimeType.utLocal : Std.Time.TimeZone.LocalTimeType → Std.Time.TimeZone.UTLocal
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.heq_comp_eqToHom_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W),
  g ≍ CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h) ↔ g ≍ f
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.coe_toAddEquiv : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S'), ⇑↑equiv = ⇑equiv
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.mk : (L : Type w) → (R : Type w') → (R → L) → (R → L) → CategoryTheory.Limits.MulticospanShape
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_counitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ), e.rightOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.unop X)).op
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.cofibrations_over_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y),
  HomotopicalAlgebra.Cofibration f ↔ HomotopicalAlgebra.Cofibration (CategoryTheory.Over.Hom.left f)
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.instIsMultiplyPretransitiveSpecialLinearGroupForallOfNatNat : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  MulAction.IsMultiplyPretransitive (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K)) 2
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.map.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_3 x
-- Mathlib.Data.List.Sort
List.sortedLT_range' : ∀ (a b : ℕ) {s : ℕ}, s ≠ 0 → (List.range' a b s).SortedLT
-- Mathlib.Tactic.Simps.Basic
/-- Auxiliary function of `getCompositeOfProjections`.  -/
Simps.getCompositeOfProjectionsAux : String → Lean.Expr → Array ℕ → Array Lean.Expr → Lean.MetaM (Lean.Expr × Array ℕ)
-- Init.Grind.Ring.Field
/-- The zeroth power of any element is one.  -/
Lean.Grind.Field.zpow_zero : ∀ {α : Type u} [self : Lean.Grind.Field α] (a : α), a ^ 0 = 1
-- Plausible.Gen
Plausible.Gen.up : {α : Type u} → Plausible.Gen α → Plausible.Gen (ULift.{v, u} α)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.nterm.injEq : ∀ (e : Lean.Expr) (n : Lean.Expr × ℤ) (x : ℕ × Lean.Expr) (a : Mathlib.Tactic.Abel.NormalExpr) (e_1 : Lean.Expr)
  (n_1 : Lean.Expr × ℤ) (x_1 : ℕ × Lean.Expr) (a_1 : Mathlib.Tactic.Abel.NormalExpr),
  (Mathlib.Tactic.Abel.NormalExpr.nterm e n x a = Mathlib.Tactic.Abel.NormalExpr.nterm e_1 n_1 x_1 a_1) =
    (e = e_1 ∧ n = n_1 ∧ x = x_1 ∧ a = a_1)
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.List.TProd.elim.match_1.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} (motive : (x : List ι) → List.TProd α x → (x_2 : ι) → x_2 ∈ x → Sort u_3) (i : ι)
  (is : List ι) (v : List.TProd α (i :: is)) (j : ι) (hj : j ∈ i :: is)
  (h_1 :
    (i : ι) → (is : List ι) → (v : List.TProd α (i :: is)) → (j : ι) → (hj : j ∈ i :: is) → motive (i :: is) v j hj),
  (match i :: is, v, j, hj with
    | i :: is, v, j, hj => h_1 i is v j hj) =
    h_1 i is v j hj
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_unitIso_inv_app_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X_1 : C) (X_2 : D),
  ((CategoryTheory.Functor.flipping.unitIso.inv.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.subgroup_eq_bot : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanClass.subgroup ⊤ = ⊥
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The projection `presheafObj data G₀ X ⟶ G₀.val.obj (op ((data X).X i))`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                    [inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                      (G₀ : CategoryTheory.Sheaf J₀ A) →
                        (X : C) →
                          (i : (data X).I₀) →
                            CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X ⟶
                              G₀.obj.obj (Opposite.op ((data X).X i))
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The morphism `reflection W Z κ : Z ⟶ reflectionObj W Z κ` is a transfinite
compositions of morphisms in `LeftBousfield.W W.isLocal`.  -/
CategoryTheory.OrthogonalReflection.transfiniteCompositionOfShapeReflection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasPushouts C] →
          [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
            [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
              [inst_4 :
                  ∀ (Z : C),
                    CategoryTheory.Limits.HasMulticoequalizer
                      (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                (κ : Cardinal.{w}) →
                  [inst_5 : OrderBot κ.ord.ToType] →
                    [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] →
                      W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType
                        (CategoryTheory.OrthogonalReflection.reflection W Z κ)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_eq' : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) (f : α → E), ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂(μ Set.univ)⁻¹ • μ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle.congr_simp : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι)
  (x x_1 : G i), x = x_1 → RestrictedProduct.mulSingle A i x = RestrictedProduct.mulSingle A i x_1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.decidableEq : {α : Type u_1} →
  [inst : CommMonoid α] → [IsCancelMul α] → {s : Submonoid α} → [DecidableEq α] → DecidableEq (Localization s)
-- Std.Sat.AIG.Relabel
_private.Std.Sat.AIG.Relabel.0.Std.Sat.AIG.Decl.relabel.match_1.eq_3 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (lhs rhs : Std.Sat.AIG.Fanin)
  (h_1 : Unit → motive Std.Sat.AIG.Decl.false) (h_2 : (a : α) → motive (Std.Sat.AIG.Decl.atom a))
  (h_3 : (lhs rhs : Std.Sat.AIG.Fanin) → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match Std.Sat.AIG.Decl.gate lhs rhs with
    | Std.Sat.AIG.Decl.false => h_1 ()
    | Std.Sat.AIG.Decl.atom a => h_2 a
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs) =
    h_3 lhs rhs