mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.exists_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    ∀ {W : C} (h : W ⟶ X) (k : W ⟶ Y),
      CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g →
        ∃ l, CategoryTheory.CategoryStruct.comp l fst = h ∧ CategoryTheory.CategoryStruct.comp l snd = k
-- Mathlib.Algebra.Tropical.Basic
Tropical.instGroupTropical : {R : Type u} → [AddGroup R] → Group (Tropical R)
-- Mathlib.Data.Fintype.Sets
Set.toFinset_eq_univ : ∀ {α : Type u_1} {s : Set α} [inst : Fintype α] [inst_1 : Fintype ↑s], s.toFinset = Finset.univ ↔ s = Set.univ
-- Init.Core
/-- The disjoint union of arbitrary sorts `α` `β`, or `α ⊕' β`.

It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts `Sort u` and `Sort v`,
instead of restricting them to `Type u` and `Type v`. This means that it can be used in situations
where one side is a proposition, like `True ⊕' Nat`. However, the resulting universe level
constraints are often more difficult to solve than those that result from `Sum`.
 -/
«term_⊕'_» : Lean.TrailingParserDescr
-- Mathlib.Order.SupIndep
/-- Bind operation for `SupIndep`.  -/
Finset.SupIndep.sup : ∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α]
  [inst_3 : DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
  (s.SupIndep fun i => (g i).sup f) → (∀ i' ∈ s, (g i').SupIndep f) → (s.sup g).SupIndep f
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.d_d_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_d._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_d._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_d._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.d_d._auto_7) {Z : C}
  (h : X.E f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
      (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_short_long : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R],
  P.pairingIn ℤ (RootPairing.EmbeddedG2.short P) (RootPairing.EmbeddedG2.long P) = -1
-- Mathlib.Topology.Maps.Basic
IsClosedMap.of_comp_surjective : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Function.Surjective f → Continuous f → IsClosedMap (g ∘ f) → IsClosedMap g
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], Function.Injective MonoidAlgebra.ofCoeff
-- Mathlib.RingTheory.Etale.QuasiFinite
Ideal.comap_fiberIsoOfBijectiveResidueField_symm : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : CommRing S]
  [inst_3 : Algebra R R'] [inst_4 : Algebra R S] {p : Ideal R} {q : Ideal R'} [inst_5 : p.IsPrime] [inst_6 : q.IsPrime]
  [inst_7 : q.LiesOver p] (H : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p q (Algebra.ofId R R') ⋯))
  (Q : ↑(p.primesOver S)),
  Ideal.comap ↑Algebra.TensorProduct.includeRight ↑((Ideal.fiberIsoOfBijectiveResidueField H).symm Q) = ↑Q
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The codomain of the truth morphism  -/
CategoryTheory.Subobject.Classifier.Ω : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Subobject.Classifier C → C
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.ι'_f_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X) {Z : C}
  (h : R.cochainComplex.X 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (R.ι'.f 0) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom
      (CategoryTheory.CategoryStruct.comp (R.ι.f 0)
        (CategoryTheory.CategoryStruct.comp
          (R.cochainComplexXIso 0 0 CategoryTheory.InjectiveResolution.ι'_f_zero._proof_1).inv h))
-- Mathlib.Tactic.GRewrite.Elab
/-- `apply_rewrite [e₁, ..., eₙ]` uses the expressions `e₁`, ..., `eₙ` as generalized rewrite rules, of
type `pᵢ → qᵢ`, on the main goal, replacing occurrences of `pᵢ` with `qᵢ`. The difference with
`grewrite` is that `grewrite` would turn `pᵢ` into a side goal and expect `qᵢ` to be a relation.

If an expression `e` is a defined constant, then the equational theorems associated with `e` are
used. This provides a convenient way to unfold `e`.

* `apply_rewrite [← e]` applies the rewrite rule `e : p → q` in the reverse direction, replacing
  occurrences of `q` with `p`.
* `apply_rewrite (config := cfg) [e₁, ..., eₙ]` uses `cfg` as configuration. See `GRewrite.Config`
  for details.
  To let `apply_rewrite` unfold more aggressively, as in `erw`, use
  `apply_rewrite (transparency := default) [e₁, ..., eₙ]`.
* `apply_rewrite [e₁, ..., eₙ] at l` rewrites at the location(s) `l`.
 -/
Mathlib.Tactic.GRewrite.tacticApply_rewrite___ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableAt.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → DifferentiableAt ℂ (fun x => Complex.sin (f x)) x
-- Mathlib.Order.RelIso.Basic
RelEmbedding.toEmbedding_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective RelEmbedding.toEmbedding
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.rciIterator.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound : α),
  Std.DTreeMap.Internal.rciIterator t lowerBound =
    { internalState := Std.DTreeMap.Internal.Zipper.prependMapGE t lowerBound Std.DTreeMap.Internal.Zipper.done }
-- Mathlib.Analysis.Complex.Trigonometric
Complex.two_cosh : ∀ (x : ℂ), 2 * Complex.cosh x = Complex.exp x + Complex.exp (-x)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotate_map_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.rotate C).map f).hom₁ = f.hom₂
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_zero_add_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), Metric.ball 0 δ + {x} = Metric.ball x δ
-- Init.Core
/-- `Identity op o` indicates `o` is a left and right identity of `op`.

This class does not require a proof that `o` is an identity, and is used
primarily for inferring the identity using class resolution.
 -/
Std.Identity : {α : Sort u} → (α → α → α) → outParam α → Prop
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The `n+1`-dimensional loops are in bijection with the loops in the space of
`n`-dimensional loops with base point `const`.
We allow an arbitrary indexing type `N` in place of `Fin n` here.  -/
GenLoop.loopHomeo : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} → [DecidableEq N] → (i : N) → ↑(GenLoop N X x) ≃ₜ LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj Y_1).right.as = PUnit.unit
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_eq_self_apply : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (Q : QuadraticMap R M N) (x : M),
  (((QuadraticMap.associatedHom S) Q) x) x = Q x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.ext_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A B : GL n R),
  A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxi.Iterator.toArray_eq_match : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {it : Std.Iter α},
  it.toArray =
    match it.internalState.next with
    | none => #[]
    | some a => #[a] ++ { internalState := { next := Std.PRange.succ? a } }.toArray
-- LeanSearchClient.Syntax
LeanSearchClient.stateSearchCache : IO.Ref (Std.HashMap (String × ℕ × String) (Array Lean.Json))
-- Mathlib.Order.Filter.Pointwise
Filter.smul_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α}, f • ⊥ = ⊥
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.coe_id : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : BoundedOrder α], ⇑(BoundedOrderHom.id α) = id
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map₂.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3}, WithZero.map₂ = Option.map₂
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.comp_comap_ofLE : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : H →g G),
  (SimpleGraph.Hom.comap (⇑f) G).comp (SimpleGraph.Hom.ofLE ⋯) = f
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram `D` to `F` is limit of `F`
evaluated at `D`. This version is for contravariant diagrams, see `colimitYonedaHomIsoLimit` for a
covariant version.  -/
CategoryTheory.Limits.colimitYonedaHomIsoLimit' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor I Cᵒᵖ) →
          (F : CategoryTheory.Functor Cᵒᵖ (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.leftOp.comp CategoryTheory.yoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.leftOp.comp CategoryTheory.yoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.not_congr : ∀ (x x' : Bool), x' = x → (!x') = !x
-- Init.Data.BitVec.Lemmas
BitVec.reverse_reverse_eq : ∀ {w : ℕ} {x : BitVec w}, x.reverse.reverse = x
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.set_support_mul_subset : ∀ {α : Type u_1} (p q : Equiv.Perm α), {x | (p * q) x ≠ x} ⊆ {x | p x ≠ x} ∪ {x | q x ≠ x}
-- Init.Data.UInt.Bitwise
USize.shiftRight_and : ∀ {a b c : USize}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → m.contains a = false
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- If for each `i : ι`, `f_i : R[X]` is transcendental over `R`, then `{f_i(X_i) | i : ι}`
in `MvPolynomial ι R` is algebraically independent over `R`.  -/
MvPolynomial.algebraicIndependent_polynomial_aeval_X : ∀ {ι : Type u_1} {R : Type u_3} [inst : CommRing R] (f : ι → Polynomial R),
  (∀ (i : ι), Transcendental R (f i)) → AlgebraicIndependent R fun i => (Polynomial.aeval (MvPolynomial.X i)) (f i)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : Option β → Option β},
  (t.alter k f).isEmpty = false →
    ((t.alter k f).maxKey! = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Init.Control.Lawful.Instances
ReaderT.instLawfulApplicative : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] [LawfulApplicative m], LawfulApplicative (ReaderT ρ m)
-- Mathlib.Tactic.DeriveTraversable
/-- Get `FVarId`s which is not implementation details in the current context.  -/
Mathlib.Deriving.Traversable.getFVarIdsNotImplementationDetails : Lean.MetaM (List Lean.FVarId)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keys_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Internal.Impl.map f t).keys = t.keys
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Constructor for cochains to `mappingCocone`.  -/
CochainComplex.mappingCocone.liftCochain : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {M : CochainComplex C ℤ} →
              {n m : ℤ} →
                CochainComplex.HomComplex.Cochain M K n →
                  CochainComplex.HomComplex.Cochain M L m →
                    m + 1 = n → CochainComplex.HomComplex.Cochain M (CochainComplex.mappingCocone φ) n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.instIsAddMonHomLift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N O : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N]
  [inst_4 : CategoryTheory.AddMonObj O] [inst_5 : CategoryTheory.BraidedCategory C] {f : M ⟶ N} {g : M ⟶ O}
  [CategoryTheory.IsAddMonHom f] [CategoryTheory.IsAddMonHom g],
  CategoryTheory.IsAddMonHom (CategoryTheory.CartesianMonoidalCategory.lift f g)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The cocone over the proposed colimit commutative monoid.  -/
CommMonCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J CommMonCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.add_isCompl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousAdd α] {s t : Set β},
  IsCompl s t → HasSum (f ∘ Subtype.val) a → HasSum (f ∘ Subtype.val) b → HasSum f (a + b)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.inv_sr : ∀ {n : ℕ} (i : ZMod n), (DihedralGroup.sr i)⁻¹ = DihedralGroup.sr i
-- Mathlib.Data.Sum.Basic
Sum.rec_update_right : ∀ {α : Type u} {β : Type v} {γ : α ⊕ β → Sort u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  (f : (a : α) → γ (Sum.inl a)) (g : (b : β) → γ (Sum.inr b)) (b : β) (x : γ (Sum.inr b)),
  (fun t => Sum.rec f (Function.update g b x) t) = Function.update (fun t => Sum.rec f g t) (Sum.inr b) x
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_rat_near : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {ε : K} (x : K),
  0 < ε → ∃ q, |x - ↑q| < ε
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
/-- A cocone in the category `PresheafOfModules R` is colimit if it is so after the application
of the functors `evaluation R X` for all `X`.  -/
PresheafOfModules.evaluationJointlyReflectsColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            (c : CategoryTheory.Limits.Cocone F) →
              ((X : Cᵒᵖ) → CategoryTheory.Limits.IsColimit ((PresheafOfModules.evaluation R X).mapCocone c)) →
                CategoryTheory.Limits.IsColimit c
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getHSMulNatFn? : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_trans_trans_symm : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (f : Equiv.Perm β) (e : α ≃ β), Equiv.Perm.sign ((e.trans f).trans e.symm) = Equiv.Perm.sign f
-- Mathlib.Algebra.Group.Equiv.Basic
Equiv.inv_symm : ∀ {G : Type u_14} [inst : InvolutiveInv G], Equiv.symm (Equiv.inv G) = Equiv.inv G
-- Mathlib.Tactic.ITauto
/-- * `ak = .and`: `(p: A ∧ B) ⊢ A`
* `ak = .iff`: `(p: A ↔ B) ⊢ A → B`
* `ak = .eq`: `(p: A = B) ⊢ A → B`
 -/
Mathlib.Tactic.ITauto.Proof.andLeft : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path of a simplicial set can be lifted to a subcomplex if the vertices
and arrows belong to this subcomplex.  -/
SSet.Subcomplex.liftPath : {X : SSet} →
  (A : X.Subcomplex) →
    {n : ℕ} →
      (p : X.Path n) →
        (∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op { len := 0 })) →
          (∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op { len := 1 })) → A.toSSet.Path n
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The trivial subgroup `{1}` is normal.  -/
Subgroup.normal_bot : ∀ {G : Type u_1} [inst : Group G], ⊥.Normal
-- Mathlib.Algebra.Group.Invertible.Defs
/-- Each element of a group is invertible.  -/
invertibleOfGroup : {α : Type u} → [inst : Group α] → (a : α) → Invertible a
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.equiv : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], Algebra.FiniteType R A → ∀ (e : A ≃ₐ[R] B), Algebra.FiniteType R B
-- Mathlib.Algebra.Order.Group.Action
pow_smul_le : ∀ {G : Type u_4} [inst : Monoid G] {α : Type u_5} [inst_1 : Preorder α] {g : G} {a : α} [inst_2 : MulAction G α]
  [CovariantClass G α HSMul.hSMul LE.le], g • a ≤ a → ∀ (n : ℕ), g ^ n • a ≤ a
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_bijective : ∀ (p : ENNReal) {V : Type u_4}, Function.Bijective (WithLp.toLp p)
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.le_isColocal_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (W : CategoryTheory.MorphismProperty C), W ≤ P.isColocal ↔ P ≤ W.isColocal
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.toExpr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.Expr
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.getInteractiveGoals : Lean.Lsp.PlainGoalParams → Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Widget.InteractiveGoals))
-- Std.Net.Addr
Std.Net.instInhabitedMACAddr.default : Std.Net.MACAddr
-- Init.Omega.IntList
Lean.Omega.IntList.get_map : ∀ {f : ℤ → ℤ} {i : ℕ} {xs : Lean.Omega.IntList}, f 0 = 0 → Lean.Omega.IntList.get (List.map f xs) i = f (xs.get i)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivWithinAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F}
  {s : Set (E × F)}, HasFDerivWithinAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) s p
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks
/-- `HasConicalPullbacks` represents the existence of conical pullbacks for every pair of
morphisms.
 -/
CategoryTheory.Enriched.HasConicalPullbacks : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) → [inst_2 : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EnrichedOrdinaryCategory V C] → Prop
-- Mathlib.LinearAlgebra.Dimension.Free
Algebra.instFiniteOfIsQuadraticExtension : ∀ (R : Type u_2) (S : Type u_3) [inst : CommSemiring R] [inst_1 : StrongRankCondition R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [Algebra.IsQuadraticExtension R S], Module.Finite R S
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Naturality of the `prodComparison` morphism in both arguments.  -/
CategoryTheory.Limits.prodComparison_natural_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D}
  (h : F.obj A' ⨯ F.obj B' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A' B') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) h)
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_erase_invOn : ∀ {α : Type u_1} {a : α}, Set.InvOn (insert a) (fun s => s \ {a}) {s | a ∈ s} {s | a ∉ s}
-- Lean.Message
Lean.MessageData.compose.inj : ∀ {a a_1 a_2 a_3 : Lean.MessageData}, a.compose a_1 = a_2.compose a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiff.neg : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f : M → G}, ContMDiff I' I n f → ContMDiff I' I n fun x => -f x
-- Init.Data.Int.Order
Int.min_eq_left : ∀ {a b : ℤ}, a ≤ b → min a b = a
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- If `P` is a property of objects for a pseudofunctor `F` to `Cat`, this is the
condition that all `P.prop : ObjectProperty (F.obj X)` for `X : B` are closed
under isomorphisms.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} → F.ObjectProperty → Prop
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Print a single cache entry as a string, without forcing it  -/
Lean.Elab.WF.GuessLex.RecCallCache.prettyEntry : Lean.Elab.WF.GuessLex.RecCallCache → ℕ → ℕ → Lean.MetaM String