mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
/-- The isomorphism between the sheafification of `P` composed with `F` and
the sheafification of `P ⋙ F`.

Use the lemmas `whisker_right_to_sheafify_sheafify_comp_iso_hom`,
`to_sheafify_comp_sheafify_comp_iso_inv` and `sheafify_comp_iso_inv_eq_sheafify_lift` to reduce
the components of this isomorphism to a state that can be handled using the universal property
of sheafification.  -/
CategoryTheory.GrothendieckTopology.sheafifyCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          {E : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
              (F : CategoryTheory.Functor D E) →
                [inst_3 :
                    ∀ (J : CategoryTheory.Limits.MulticospanShape),
                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] →
                  [inst_4 :
                      ∀ (J : CategoryTheory.Limits.MulticospanShape),
                        CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] →
                    [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                      [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] →
                        [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] →
                          [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
                                CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] →
                            (P : CategoryTheory.Functor Cᵒᵖ D) → (J.sheafify P).comp F ≅ J.sheafify (P.comp F)
-- Mathlib.RingTheory.DedekindDomain.GaussLemma
/-- **Gauss's Lemma:** given a polynomial `p` in `R[X]`, the content ideal of `p` is the whole ring
if and only if the `v`-adic Gauss norms of `p` are equal to 1 for all `v`.  -/
Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {b : NNReal} (hb : 1 < b) (p : Polynomial R),
  ¬IsField R →
    (p.contentIdeal = ⊤ ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), Polynomial.gaussNorm (v.intAdicAbv hb) 1 p = 1)
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprBehaviorIfUnchanged : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.natCast_cpow_natCast_mul : ∀ (n m : ℕ) (z : ℂ), ↑n ^ (↑m * z) = (↑n ^ m) ^ z
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instAdd : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → Add (E →ₛₗ.[σ] F)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- Any free, nontrivial `R`-module is flat.  -/
Module.FaithfullyFlat.instOfNontrivialOfFree : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [Module.Free R M], Module.FaithfullyFlat R M
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.rightInvSeq.match_1.eq_2 : ∀ {B : Type u_1} (motive : List B → Sort u_2) (i : B) (ω : List B) (h_1 : Unit → motive [])
  (h_2 : (i : B) → (ω : List B) → motive (i :: ω)),
  (match i :: ω with
    | [] => h_1 ()
    | i :: ω => h_2 i ω) =
    h_2 i ω
-- Lean.Data.Json.Basic
Lean.Json : Type
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctor_obj_obj : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₂ C)
  (X_1 : J₁ × J₂),
  ((CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₂ C).obj X).obj X_1 =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (X.1.obj X_1.1) (X.2.obj X_1.2)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.le_ae_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.ae μ ⊓ Filter.principal s ≤ MeasureTheory.ae (μ.restrict s)
-- Init.System.FilePath
/-- Separates the entries in the `$PATH` (or `%PATH%`) environment variable by the current
platform-dependent separator character.
 -/
System.SearchPath.parse : String → System.SearchPath
-- Mathlib.Data.Matrix.Composition
Matrix.compAddEquiv_apply : ∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) [inst : Add R]
  (M : Matrix I J (Matrix K L R)), (Matrix.compAddEquiv I J K L R) M = (Matrix.comp I J K L R) M
-- Mathlib.LinearAlgebra.Dimension.RankNullity
HasRankNullity.rank_quotient_add_rank : ∀ {R : Type v} {inst : Ring R} [self : HasRankNullity.{u, v} R] {M : Type u} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] (N : Submodule R M), Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.lowerSemicontinuousAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ}, ContinuousAt f x → LowerSemicontinuousAt f x
-- Mathlib.Topology.LocallyClosed
coborder_eq_union_closure_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, coborder s = s ∪ (closure s)ᶜ
-- Init.Data.BitVec.Lemmas
BitVec.ofInt_negSucc_eq_not_ofNat : ∀ {w n : ℕ}, BitVec.ofInt w (Int.negSucc n) = ~~~BitVec.ofNat w n
-- Mathlib.Logic.Basic
instDecidableFact : {p : Prop} → [Decidable p] → Decidable (Fact p)
-- Aesop.Options.Public
/-- Search strategies which Aesop can use.
 -/
Aesop.Strategy : Type
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_singleton : ∀ {x y : PSet.{u_1}}, x ∈ {y} ↔ x.Equiv y
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toSubring_subtype : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  (S : NonUnitalSubalgebra R A), NonUnitalSubringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)
-- Mathlib.Data.Set.Lattice
Set.nonempty_biUnion : ∀ {α : Type u_1} {β : Type u_2} {t : Set α} {s : α → Set β}, (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty
-- Lean.Compiler.IR.Basic
Lean.IR.VarId.mk.sizeOf_spec : ∀ (idx : Lean.IR.Index), sizeOf { idx := idx } = 1 + sizeOf idx
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- This is a version of `EisensteinSeries.qExpansion_identity` for positive naturals,
which shows that  `∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n : ℕ+, n ^ k q ^n`
where `q = cexp (2 π I z)`.  -/
EisensteinSeries.qExpansion_identity_pnat : ∀ {k : ℕ},
  1 ≤ k →
    ∀ (z : UpperHalfPlane),
      ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
        (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial *
          ∑' (n : ℕ+), ↑↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Filter out duplicate rewrites, reflexive rewrites
or rewrites that have metavariables in the replacement expression.  -/
Mathlib.Tactic.LibraryRewrite.filterRewrites : {α : Type} → Lean.Expr → Array α → (α → Lean.Expr) → (α → Bool) → Lean.MetaM (Array α)
-- Mathlib.Algebra.Order.Interval.Basic
instZeroInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], instZeroInterval = { zero := ↑0 }
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_map : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : μ'.IsAddHaarMeasure] (φ : G ≃ₜ+ G),
  (MeasureTheory.Measure.map (⇑φ) μ').addHaarScalarFactor (MeasureTheory.Measure.map (⇑φ) μ) = μ'.addHaarScalarFactor μ
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.mul_eq_add : ∀ {p q : ℝ}, p.HolderConjugate q → p * q = p + q
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Ioc_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c - b) (d - b)
-- Mathlib.Order.Hom.Basic
/-- One can lift an unbundled monotone function to a bundled one.  -/
OrderHom.canLift : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β],
  CanLift (α → β) (α →o β) DFunLike.coe Monotone
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_succ_succ : ∀ {m n : ℕ}, ((m + 1)<...n + 1).toList = List.map (fun x => x + 1) (m<...n).toList
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.IsClosedUnderLimitsOfShape J ↔ P.op.IsClosedUnderColimitsOfShape Jᵒᵖ
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.ofIso_iso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ≅ Y),
  (AlgebraicGeometry.Scheme.PartialIso.ofIso f).iso = X.topIso ≪≫ f ≪≫ Y.topIso.symm
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which monovary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together. Stated by permuting the entries of `g`.  -/
Monovary.sum_comp_perm_smul_lt_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Monovary f g → (∑ i, f (σ i) • g i < ∑ i, f i • g i ↔ ¬Monovary (f ∘ ⇑σ) g)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCancelCommMonoid : {α : Type u_1} → [CancelCommMonoid α] → CancelCommMonoid (Colex α)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (ha : MvPowerSeries.HasSubst a) (f : MvPowerSeries σ R),
  (MvPowerSeries.substAlgHom ha) f = MvPowerSeries.subst a f
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.insert' : ∀ {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X},
  R.IsSeparated s → (∀ y ∈ s, (x, y) ∈ R → x = y) → (∀ y ∈ s, (y, x) ∈ R → x = y) → R.IsSeparated (insert x s)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Auxiliary definition for `vComp`.  -/
CategoryTheory.Lax.LaxTrans.vCompApp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          CategoryTheory.Lax.LaxTrans F G → CategoryTheory.Lax.LaxTrans G H → (a : B) → F.obj a ⟶ H.obj a
-- Mathlib.GroupTheory.Congruence.Basic
Con.instSMul.eq_1 : ∀ {α : Type u_4} {M : Type u_5} [inst : MulOneClass M] [inst_1 : SMul α M] [inst_2 : IsScalarTower α M M] (c : Con M),
  c.instSMul = { smul := fun a => Quotient.map' (fun x => a • x) ⋯ }
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.ofHom_id : ∀ {X : Type u} [inst : PartialOrder X],
  PartOrdEmb.ofHom (RelEmbedding.refl fun x1 x2 => x1 ≤ x2) =
    CategoryTheory.CategoryStruct.id { carrier := X, str := inst }
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ClientInfo.mk.inj : ∀ {name : String} {version? : Option String} {name_1 : String} {version?_1 : Option String},
  { name := name, version? := version? } = { name := name_1, version? := version?_1 } →
    name = name_1 ∧ version? = version?_1
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The information needed for doing a rewrite.  -/
Mathlib.Tactic.ClickSuggestions.RwInfo : Type
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_equiv_eq_arrow_of_lift_eq : ∀ {α : Type u} {β' : Type v} [Infinite α],
  Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β') →
    Cardinal.mk (α ≃ β') = Cardinal.mk (α → β')
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The isomorphism between `zero` and `one` in `WalkingIso`.  -/
CategoryTheory.WalkingIso.iso : CategoryTheory.WalkingIso.zero ≅ CategoryTheory.WalkingIso.one
-- Mathlib.Order.Bounds.Basic
lowerBounds_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, lowerBounds (Set.Ici a) = Set.Iic a
-- Mathlib.Data.Real.ConjExponents
/-- Nonnegative real numbers `p q r : ℝ≥0` are said to be a **Hölder triple** if `p` and `q` are
positive and `p⁻¹ + q⁻¹ = r⁻¹`.  -/
NNReal.HolderTriple : NNReal → NNReal → NNReal → Prop
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associator_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.f =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)
        CategoryTheory.Limits.prod.snd)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.apply_symm_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : B × F}, x ∈ e.target → ↑e (↑e.symm x) = x
-- Mathlib.Data.NNReal.Defs
NNReal.coe_add : ∀ (r₁ r₂ : NNReal), ↑(r₁ + r₂) = ↑r₁ + ↑r₂
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.Etale f],
  AlgebraicGeometry.Etale (f ∣_ V)
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_apply : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] (f : A →ₗ[R] B) (L : CharacterModule B),
  (CharacterModule.dual f) L = AddMonoidHom.comp L f.toAddMonoidHom
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ) (X : C),
  (t.natTransTruncLTOfLE a a ⋯).app X = CategoryTheory.CategoryStruct.id ((t.truncLT a).obj X)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.sup : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → β}
  [inst : TopologicalSpace β] [inst_1 : Zero β] [inst_2 : SemilatticeSup β] [ContinuousSup β],
  MeasureTheory.FinStronglyMeasurable f μ →
    MeasureTheory.FinStronglyMeasurable g μ → MeasureTheory.FinStronglyMeasurable (f ⊔ g) μ
-- Mathlib.Algebra.Star.StarAlgHom
/-- Helper instance for cases where the inference via `EquivLike` is too hard.  -/
StarAlgEquiv.instFunLike : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Add A] →
        [inst_1 : Add B] →
          [inst_2 : Mul A] →
            [inst_3 : Mul B] →
              [inst_4 : SMul R A] →
                [inst_5 : SMul R B] → [inst_6 : Star A] → [inst_7 : Star B] → FunLike (A ≃⋆ₐ[R] B) A B
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) {p q n : ℤ} (h : p + n = q) (p' : ℤ)
  (hp' : p' + 1 = p), CochainComplex.HomComplex.Cocycle.toSingleMk 0 h p' hp' ⋯ = 0
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.norm : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} {f : X → E},
  MeasureTheory.LocallyIntegrableOn f s μ → MeasureTheory.LocallyIntegrableOn (fun x => ‖f x‖) s μ
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_trans : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} {ι'' : Type u_9} (σ₁ : ι ≃ ι')
  (σ₂ : ι' ≃ ι'') (f : M [⋀^ι]→ₗ[R] N),
  AlternatingMap.domDomCongr (σ₁.trans σ₂) f = AlternatingMap.domDomCongr σ₂ (AlternatingMap.domDomCongr σ₁ f)
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_getElem_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (hl : 1 < l.length), l.formPerm l[0] = l[1]
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, where the point on the right is constant and the
sum of the weights is 0.  -/
Finset.sum_smul_vsub_const_eq_weightedVSub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : P),
  ∑ i ∈ s, w i = 0 → ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSub p₁) w
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsMonHomHomAsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] {f : M ⟶ N} [inst_4 : CategoryTheory.IsIso f]
  [CategoryTheory.IsMonHom f], CategoryTheory.IsMonHom (CategoryTheory.asIso f).hom
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.contains (t.minKey he) = true
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go aig distance curr acc).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go aig distance curr acc).aig.decls[idx] = aig.decls[idx]
-- Lean.Data.SMap
Lean.SMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : BEq α} {inst_1 : Hashable α} {stage₁ : Bool} {map₁ : Std.HashMap α β}
  {map₂ : Lean.PHashMap α β} {stage₁_1 : Bool} {map₁_1 : Std.HashMap α β} {map₂_1 : Lean.PHashMap α β},
  { stage₁ := stage₁, map₁ := map₁, map₂ := map₂ } = { stage₁ := stage₁_1, map₁ := map₁_1, map₂ := map₂_1 } →
    stage₁ = stage₁_1 ∧ map₁ = map₁_1 ∧ map₂ = map₂_1
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.instForInOfMonad : {α : Type u} → {le : α → α → Bool} → {m : Type u_1 → Type u_2} → [Monad m] → ForIn m (Batteries.BinomialHeap α le) α
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_natCast_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a => a * ↑n
-- Mathlib.Data.UInt
USize.instCommMonoid : CommMonoid USize
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.toAddSubmonoid_mono : ∀ {G : Type u_1} [inst : AddGroup G], Monotone AddSubgroup.toAddSubmonoid
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Iic : ∀ {m n : ℕ} (h : m = n) (i : Fin n), Fin.cast h ⁻¹' Set.Iic i = Set.Iic (Fin.cast ⋯ i)
-- Mathlib.Data.Multiset.AddSub
Multiset.countP_sub : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α},
  t ≤ s →
    ∀ (p : α → Prop) [inst_1 : DecidablePred p], Multiset.countP p (s - t) = Multiset.countP p s - Multiset.countP p t
-- Mathlib.Topology.ContinuousMap.Interval
/-- The embedding into an interval from a sub-interval lying on the right, as a `ContinuousMap`.  -/
ContinuousMap.IccInclusionRight : {α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] → {a b c : α} → [Fact (a ≤ b)] → C(↑(Set.Icc b c), ↑(Set.Icc a c))
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- If `f : ℂ → ℂ` is measurable, then the Cartan kernel of integration is measurable as a function in
the two variables `α` and `β`.
 -/
ValueDistribution.Cartan.measurable_cartanKernel : ∀ {f : ℂ → ℂ} {R : ℝ}, Measurable f → Measurable fun p => ValueDistribution.Cartan.cartanKernel f R p.1 p.2
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
Matrix.HasOrthogonalRows.transpose_hasOrthogonalCols : ∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] {A : Matrix m n α}
  [inst_2 : Fintype n], A.HasOrthogonalRows → A.transpose.HasOrthogonalCols
-- Mathlib.GroupTheory.Exponent
orderOf_eq_two_iff : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent G = 2 → ∀ {x : G}, orderOf x = 2 ↔ x ≠ 1
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.smul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasStrictDerivAt c c' x → ∀ (f : F), HasStrictDerivAt (fun y => c y • f) (c' • f) x
-- Mathlib.Algebra.CharP.Two
CharTwo.sum_mul_self : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring R] [CharP R 2] (s : Finset ι) (f : ι → R),
  (∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, f i * f i
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.conjugator.cons_append : ∀ {α : Type u} [inst : DecidableEq α] {a b : α × Bool} (L : List (α × Bool)),
  FreeAddGroup.reduceCyclically.conjugator (a :: (L ++ [b])) =
    if b.1 = a.1 ∧ (!b.2) = a.2 then a :: FreeAddGroup.reduceCyclically.conjugator L else []
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonLambda : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.triangleRotateShortComplex_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangleRotateShortComplex φ).X₂ = (CochainComplex.mappingCone.triangle φ).rotate.obj₂
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.lintegral_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α)
  {g : γ → ENNReal}, Measurable g → ∫⁻ (c : γ), g c ∂(η.comp κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- If two maps of short complexes are homotopic, their opposites also are.  -/
CategoryTheory.ShortComplex.Homotopy.neg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ → CategoryTheory.ShortComplex.Homotopy (-φ₁) (-φ₂)