mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Functor.functorialityCompPostcompose α).hom.app X).hom = α.hom.app X.pt
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.mk.injEq : ∀ {w : ℕ} (wn wr : ℕ) (q r : BitVec w) (wn_1 wr_1 : ℕ) (q_1 r_1 : BitVec w),
  ({ wn := wn, wr := wr, q := q, r := r } = { wn := wn_1, wr := wr_1, q := q_1, r := r_1 }) =
    (wn = wn_1 ∧ wr = wr_1 ∧ q = q_1 ∧ r = r_1)
-- Lean.Compiler.LCNF.Types
Lean.Expr.isErased : Lean.Expr → Bool
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The determinant of the change-of-basis matrix between two orthonormal bases `a`, `b` has
unit length.  -/
OrthonormalBasis.det_to_matrix_orthonormalBasis : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E),
  ‖a.toBasis.det ⇑b‖ = 1
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instSMulCommClass_closedBall_left : SMulCommClass Complex.UnitClosedDisc Complex.UnitDisc Complex.UnitDisc
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Multiset.toDFinsupp (s ∪ t) = Multiset.toDFinsupp s ⊔ Multiset.toDFinsupp t
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pos.skip?_char_eq_skip?_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos}, pos.skip? c = pos.skip? fun x => x == c
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.coe_basis : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {φ : ι → Type u_4} (b : (i : ι) → Module.Basis (φ i) R M),
  ⇑(Finsupp.basis b) = fun ix => fun₀ | ix.fst => (b ix.fst) ix.snd
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- Map a kernel cone on the difference of two morphisms to the equalizer fork.  -/
CategoryTheory.Preadditive.forkOfKernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f g : X ⟶ Y} → CategoryTheory.Limits.KernelFork (f - g) → CategoryTheory.Limits.Fork f g
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_average : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] [MeasureTheory.IsFiniteMeasure μ] {f : α → ε},
  MeasureTheory.Integrable f ((μ Set.univ)⁻¹ • μ) ↔ MeasureTheory.Integrable f μ
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.cons_not : ∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool}, FreeAddGroup.Red.Step ((x, b) :: (x, !b) :: L) L
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofNat : ∀ {n : ℕ}, n < 4294967296 → (OfNat.ofNat n).toUInt64 = OfNat.ofNat n
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  (S : J.Cover X), ↑S ∈ J X
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_ne_zero : ∀ {K : Type u_1} [inst : RCLike K] {x : ℝ}, ↑x ≠ 0 ↔ x ≠ 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.keys_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β k}, (↑(m.insertIfNew k v)).keys.Perm (if m.contains k = true then (↑m).keys else k :: (↑m).keys)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The absolute value is nonnegative  -/
IsAbsoluteValue.abv_nonneg' : ∀ {S : Type u_5} {inst : Semiring S} {inst_1 : PartialOrder S} {R : Type u_6} {inst_2 : Semiring R} {f : R → S}
  [self : IsAbsoluteValue f] (x : R), 0 ≤ f x
-- Init.Data.Fin.Lemmas
Fin.subNat_one_succ : ∀ {n : ℕ} (i : Fin (n + 1)) (h : 1 ≤ ↑i), (Fin.subNat 1 i h).succ = i
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
IsAddTorsionFree.to_noZeroSMulDivisors_nat : ∀ {M : Type u_2} [inst : AddMonoid M] [IsAddTorsionFree M], NoZeroSMulDivisors ℕ M
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D],
  (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).unitIso =
    CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso
-- Mathlib.Data.Multiset.Defs
Multiset.coe_subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, ↑l₁ ⊆ ↑l₂ ↔ l₁ ⊆ l₂
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- **Alias** of `aeconst_of_dense_setOfPred_preimage_smul_eq`. -/
aeconst_of_dense_setOf_preimage_smul_eq : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g • x) ⁻¹' s = s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.CommComon.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Analysis.ConstantSpeed
/-- `f` has unit speed on `s` if it is linearly parameterized by `l = 1` on `s`.  -/
HasUnitSpeedOn : {E : Type u_2} → [PseudoEMetricSpace E] → (ℝ → E) → Set ℝ → Prop
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorUInt16 : LawfulXor UInt16
-- Mathlib.GroupTheory.Coset.Defs
/-- The equivalence relation corresponding to the partition of a group by right cosets of a
subgroup.  -/
QuotientGroup.rightRel : {α : Type u_1} → [inst : Group α] → Subgroup α → Setoid α
-- Mathlib.Order.WithBot
WithBot.instOrderTop.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α], WithBot.instOrderTop = { toTop := WithBot.instTop, le_top := ⋯ }
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.commute_all_of_involutive : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ → Function.Involutive ⇑φ → ∀ (g h : G), Commute g h
-- Lean.Elab.Tactic.SimpTrace
/-- Implementation of `dsimp?`.  -/
_private.Lean.Elab.Tactic.SimpTrace.0.Lean.Elab.Tactic.dsimpLocation'.go : Lean.Meta.Simp.Context →
  Lean.Meta.Simp.SimprocsArray → Array Lean.FVarId → Bool → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats
-- Mathlib.Tactic.CrossRefAttribute
/-- The formatter for Stacks Project Tags syntax.  -/
Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₁ : ∀ {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 b : ℤ) (h : a ≤ b) (j : C),
  ((t.triangleLTLTGELT a b h).obj j).mor₁ = (t.natTransTruncLTOfLE a b h).app j
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatCastNum : Lean.Meta.Simp.Simproc
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_pbind : ∀ {m : Type w → Type w'} {α : Type u} {β : Type v} [inst : Monad m] [LawfulMonad m] {x : Std.Iterators.HetT m α}
  {f : (a : α) → x.Property a → Std.Iterators.HetT m β},
  (x.pbind f).Property = fun b => ∃ a, ∃ (h : x.Property a), (f a h).Property b
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
max_div_min_eq_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] [MulRightMono α] (a b : α),
  max a b / min a b = |b / a|ₘ
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.image_inclusion : ∀ {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M α] (s : SubAddAction M α),
  Set.range ⇑s.inclusion = s.carrier
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, then `trace` and `algebraMap` commutes.
 -/
IntermediateField.LinearDisjoint.trace_algebraMap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [FiniteDimensional F E],
  A.LinearDisjoint ↥B →
    A ⊔ B = ⊤ → ∀ (x : ↥B), (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.contDiffAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E} {n : ℕ∞}, ContDiffAt ℝ (↑n) (↑f) x
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- A wrapper for promoting any category to a bicategory,
with the only 2-morphisms being equalities.
 -/
CategoryTheory.LocallyDiscrete : Type u → Type u
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.corecF.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)),
  MvQPF.corecF g = MvPFunctor.M.corec (MvQPF.P F) fun x => MvQPF.repr (g x)
-- Mathlib.Data.List.Sort
List.sublist_of_subperm_of_sortedLE : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α}, l₁.Subperm l₂ → l₁.SortedLE → l₂.SortedLE → l₁.Sublist l₂
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.stdSimplexHomeomorphI_vertex_one : TopCat.stdSimplexHomeomorphI (stdSimplex.vertex 1) = 1
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk'_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M.X ⟶ N.X)
  (smul_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
          CategoryTheory.ModObj.smul)
      CategoryTheory.Mod.Hom.mk'._auto_1),
  (CategoryTheory.Mod.Hom.mk' f smul_hom).hom = f
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat), IsLocalRing ↑(X.presheaf.stalk x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}, CategoryTheory.IsPushout f g inl inr → CategoryTheory.IsPushout g f inr inl
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The canonical isomorphism `S.unop.op ≅ S` for a short complex `S` in `Cᵒᵖ`  -/
CategoryTheory.ShortComplex.unopOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex Cᵒᵖ) → S.unop.op ≅ S
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE]
  [inst_8 : MetricSpace PF] [inst_9 : NormedAddTorsor F PF] [inst_10 : FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF),
  ⇑f.toHomeomorphOfFiniteDimensional.symm = ⇑f.symm
-- Mathlib.Algebra.Jordan.Basic
IsJordan.mk : ∀ {A : Type u_1} [inst : Mul A],
  (∀ (a b : A), a * b * a = a * (b * a)) →
    (∀ (a b : A), a * a * (a * b) = a * (a * a * b)) →
      (∀ (a b : A), a * a * (b * a) = a * a * b * a) →
        (∀ (a b : A), a * b * (a * a) = a * (b * (a * a))) →
          (∀ (a b : A), b * a * (a * a) = b * (a * a) * a) → IsJordan A
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_copy : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.hom_id : ∀ {R : CommSemiRingCat}, CommSemiRingCat.Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_surjective : ∀ {S : AlgebraicGeometry.Scheme} {Ω : Type u} [inst : Field Ω] [inst_1 : IsSepClosed Ω]
  (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) (X : S.Etale),
  Function.Surjective (AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage s hs₀)
-- Plausible.Gen
Plausible.GenError.genError.injEq : ∀ (a a_1 : String), (Plausible.GenError.genError a = Plausible.GenError.genError a_1) = (a = a_1)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (m : Lean.Grind.CommRing.Mon) (p_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.add k m p_2) =
    Lean.Grind.CommRing.denoteSInt k * Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denoteS ctx p_2
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.inradius.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.inradius = (s.exsphere ∅).radius
-- Mathlib.LinearAlgebra.Dimension.Finrank
Submodule.finrank_map_subtype_eq : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  (q : Submodule R ↥p), Module.finrank R ↥(Submodule.map p.subtype q) = Module.finrank R ↥q
-- Mathlib.Data.Fintype.Sets
/-- Construct a finset enumerating a set `s`, given a `Fintype` instance.  -/
Set.toFinset : {α : Type u_1} → (s : Set α) → [Fintype ↑s] → Finset α
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.refl_apply : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x : P₁), (AffineEquiv.refl k P₁) x = x
-- Mathlib.GroupTheory.Perm.Fin
Fin.insertNth_apply_cycleRange_symm : ∀ {n : ℕ} {α : Type u_1} (p : Fin (n + 1)) (a : α) (x : Fin n → α) (j : Fin (n + 1)),
  p.insertNth a x ((Equiv.symm p.cycleRange) j) = Fin.cons a x j
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset' : ∀ {A B : GrpCat} (f : A ⟶ B) (x b : ↑B),
  b ∈ (GrpCat.Hom.hom f).range →
    ((GrpCat.SurjectiveOfEpiAuxs.h f) x)
        (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(GrpCat.Hom.hom f).range, ⋯⟩) =
      GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(GrpCat.Hom.hom f).range, ⋯⟩
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.prepartition_tag : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] {ν : ι → ℤ} {B : BoxIntegral.Box ι},
  ν ∈ BoxIntegral.unitPartition.admissibleIndex n B →
    (BoxIntegral.unitPartition.prepartition n B).tag (BoxIntegral.unitPartition.box n ν) =
      BoxIntegral.unitPartition.tag n ν
-- Mathlib.GroupTheory.Perm.List
List.formPerm_cons_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (l : List α),
  (x :: y :: l).formPerm = Equiv.swap x y * (y :: l).formPerm
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation detail)
The inclusion map `V i j ⟶ F j` in the glue data associated to a locally directed diagram.  -/
AlgebraicGeometry.Scheme.IsLocallyDirected.tAux : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [Quiver.IsThin J] → (i j : J) → ↑(AlgebraicGeometry.Scheme.IsLocallyDirected.V F i j) ⟶ F.obj j
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.sup_def : ∀ {M : Type u_1} [inst : MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M},
  s₁ ⊔ s₂ = (s₁.toSubmonoid ⊔ s₂.toSubmonoid).saturation
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.id_comp : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ), (GradedRingHom.id ℬ).comp f = f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.TreeSet.ofList l cmp}, (Std.TreeSet.ofList l cmp).get k' h' = k
-- Init.Data.List.ToArray
List.forIn_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (l : List α) (b : β)
  (f : α → β → m (ForInStep β)), forIn l.toArray b f = forIn l b f
-- Mathlib.RepresentationTheory.Action
Representation.linearizeTrivialIso_apply : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] {X : Type w}
  (f : MonoidAlgebra k (Action.trivial G X).V), (Representation.linearizeTrivialIso k G X) f = f
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_orderEmbeddingToFun : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → LE (α i)],
  ⇑DFinsupp.orderEmbeddingToFun = DFunLike.coe
-- Batteries.Data.List.Lemmas
List.findIdxNth_le_findIdxNth_iff : ∀ {α : Type u_1} {p : α → Bool} {n m : ℕ} {xs : List α},
  List.findIdxNth p xs n ≤ List.findIdxNth p xs m ↔ List.countP p xs ≤ m ∨ n ≤ m
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.neg.sizeOf_spec : ∀ (a : ℕ), sizeOf (Sat.Literal.neg a) = 1 + sizeOf a
-- Mathlib.Data.Real.Star
/-- The real numbers are a \*-ring, with the trivial \*-structure.  -/
instStarRingReal : StarRing ℝ
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.coe_mk : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {f : E → F} {contDiff : ContDiff ℝ (↑n) f}
  {hasCompactSupport : HasCompactSupport f} {tsupport_subset : tsupport f ⊆ ↑Ω},
  ⇑{ toFun := f, contDiff' := contDiff, hasCompactSupport' := hasCompactSupport, tsupport_subset' := tsupport_subset } =
    f
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul_cancel_right' : ∀ {α : Type u} [inst : Monoid α] (a b : α) {x : Invertible b}, a * ⅟b * b = a
-- Mathlib.Algebra.Polynomial.Roots
/-- The set of roots of all polynomials of bounded degree and having coefficients in a finite set
is finite.  -/
Polynomial.bUnion_roots_finite : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : DecidableEq S]
  (m : R →+* S) (d : ℕ) {U : Set R},
  U.Finite → (⋃ f, ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑(Polynomial.map m f).roots.toFinset).Finite
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.rightHomologyFunctor C).obj S = S.rightHomology
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.mk : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    {s : optParam (Set M) Set.univ} →
                      (toFun : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) →
                        (LocallyFinite fun i => Function.support ⇑(toFun i)) →
                          (∀ (i : ι) (x : M), 0 ≤ (toFun i) x) →
                            (∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) →
                              (∀ (x : M), ∑ᶠ (i : ι), (toFun i) x ≤ 1) → SmoothPartitionOfUnity ι I M s
-- Mathlib.Lean.Name
_private.Mathlib.Lean.Name.0.isBlackListed : Lean.Name → Lean.CoreM Bool
-- Mathlib.Algebra.Polynomial.Derivation
Derivation.mk.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  (toLinearMap toLinearMap_1 : A →ₗ[R] M) (e_toLinearMap : toLinearMap = toLinearMap_1)
  (map_one_eq_zero' : toLinearMap 1 = 0)
  (leibniz' : ∀ (a b : A), toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a),
  { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' } =
    { toLinearMap := toLinearMap_1, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
-- Init.Data.UInt.Bitwise
USize.and_not_self : ∀ {a : USize}, a &&& ~~~a = 0
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instDistribSMulSubtypeAEEqFunMemAddSubgroupLp : {M : Type u_1} →
  {α : Type u_3} →
    {E : Type u_4} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {μ : MeasureTheory.Measure α} →
            {p : ENNReal} →
              [inst_2 : SMul M α] →
                [MeasureTheory.SMulInvariantMeasure M α μ] →
                  [MeasurableConstSMul M α] → DistribSMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Topology.Algebra.UniformConvergence
instNegUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Neg β],
  instNegUniformOnFun = { neg := instNegUniformOnFun._aux_1 }
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_right_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.right = sq.X₄
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_negDblY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).negDblY (⇑f ∘ P) = f (W'.negDblY P)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.congr : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f₁ =o[𝕜; l] g₁ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → f₂ =o[𝕜; l] g₂
-- Mathlib.Control.Bifunctor
Bifunctor.id_snd : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β),
  Bifunctor.snd id x = x