mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Like `.fn`, but unconditionally with `sizeOf` at the right type.
We use this one when in `evalRecCall`
 -/
Lean.Elab.WF.GuessLex.BasicMeasure.natFn : Lean.Elab.WF.GuessLex.BasicMeasure → Lean.Expr
-- Mathlib.Algebra.Group.Ext
AddCancelCommMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : AddCancelCommMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Burnside's lemma** : a (noncomputable) bijection between the disjoint union of all
`{x ∈ X | g • x = x}` for `g ∈ G` and the product `G × Ω`, where `G` is an additive group
acting on `X` and `Ω = X/G` denotes the quotient of `X` by the relation `orbitRel G X`.  -/
AddAction.sigmaFixedByEquivOrbitsProdAddGroup : (G : Type u) →
  (X : Type v) →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] → (g : G) × ↑(AddAction.fixedBy X g) ≃ Quotient (AddAction.orbitRel G X) × G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_fst_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {X_1 Y : X} (f : X_1 ⟶ Y),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).fst.map f =
    ψ.left.map (S.fst.map f)
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.Join.refl`. -/
Relation.reflexive_join : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], Std.Refl (Relation.Join r)
-- Mathlib.Tactic.FunProp.Core
/-- Prove function property of `fun f ↦ f x₁ ... xₙ`.  -/
Mathlib.Meta.FunProp.bvarAppCase : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Mathlib.Meta.FunProp.FunctionData →
      (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
        Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The image of the fractional ideal `I` in the mixed space.  -/
NumberField.mixedEmbedding.idealLattice : (K : Type u_2) →
  [inst : Field K] →
    (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ →
      Submodule ℤ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
DifferentiableAt.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} {x : E}
  [Finite ι],
  DifferentiableAt 𝕜 f x →
    (∀ (i : ι), DifferentiableAt 𝕜 (g i) x) → DifferentiableAt 𝕜 (fun x => (f x) fun x_1 => g x_1 x) x
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.symm_trans : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  {f₀ f₁ f₂ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (G : f₁.HomotopyWith f₂ P), (F.trans G).symm = G.symm.trans F.symm
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMap_comp_at : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {g : M' → M''} (p : TangentBundle I M),
  MDiffAt g (f p.proj) → MDiffAt f p.proj → tangentMap I I'' (g ∘ f) p = tangentMap I' I'' g (tangentMap I I' f p)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (a : ℤ)
  (K : CochainComplex C ℤ),
  (CochainComplex.shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K =
    (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map
      ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.foldl_eq_foldl_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {α_1 : Type u_3} {f : α_1 → α → β → α_1} {init : α_1}
  {t : RBTree.RBMap α β cmp}, RBTree.RBMap.foldl f init t = List.foldl (fun r p => f r p.1 p.2) init t.toList
-- Mathlib.Algebra.Ring.Action.Basic
/-- Each element of the monoid defines a semiring homomorphism.  -/
MulSemiringAction.toRingHom : (M : Type u_1) → [inst : Monoid M] → (R : Type v) → [inst_1 : Semiring R] → [MulSemiringAction M R] → M → R →+* R
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_eq_getElem!_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.minKey! = t.keysArray[0]!
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.foldr_eq_foldr_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {δ : Type w} [inst : Std.TransCmp cmp]
  {f : α → δ → δ} {init : δ}, Std.ExtTreeSet.foldr f init t = List.foldr f init t.toList
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.map_radical : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (I : Ideal R),
  Ideal.map (algebraMap R S) I.radical = (Ideal.map (algebraMap R S) I).radical
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_lt_coe : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {c : NNReal}, dist x y < ↑c ↔ nndist x y < c
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.mk_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n : N),
  ((TensorProduct.mk R M N) m) n = m ⊗ₜ[R] n
-- Mathlib.Tactic.Widget.SelectPanelUtils
SelectInsertParams.mk : Lean.Lsp.Position →
  Array Lean.Widget.InteractiveGoal → Array Lean.SubExpr.GoalsLocation → Lean.Lsp.Range → SelectInsertParams
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u_1, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupCohomology.mapShortComplexH2 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH2 (MonoidHom.id G) φ)
      (groupCohomology.mapShortComplexH2 (MonoidHom.id G) ψ)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] {X' : C} (s : X' ⟶ X) (hs : W s) (f : X' ⟶ Y),
  sizeOf { X' := X', s := s, hs := hs, f := f } = 1 + sizeOf X' + sizeOf s + sizeOf hs + sizeOf f
-- Init.Data.UInt.Lemmas
UInt16.ofNat_eq_iff_mod_eq_toNat : ∀ (a : ℕ) (b : UInt16), UInt16.ofNat a = b ↔ a % 2 ^ 16 = b.toNat
-- Mathlib.Topology.NhdsWithin
insert_mem_nhds_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, insert a s ∈ nhds a ↔ s ∈ nhdsWithin a {a}ᶜ
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- abstraction function for dependent products  -/
MvQPF.Pi.abs : {n : ℕ} →
  {A : Type u} →
    (F : A → TypeVec.{u} n → Type u) →
      [inst : (α : A) → MvQPF (F α)] → ⦃α : TypeVec.{u} n⦄ → ↑(MvQPF.Pi.P F) α → MvQPF.Pi F α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.get_eq_getValueCast : ∀ {α : Type u} {β : α → Type v} [instBEq : BEq α] [inst : Ord α] [inst_1 : Std.LawfulBEqOrd α] [inst_2 : Std.TransOrd α]
  [inst_3 : Std.LawfulEqOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β} {h : k ∈ t} (hto : t.Ordered),
  t.get k h = Std.Internal.List.getValueCast k t.toListModel ⋯
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
measurableSet_pi_polarCoord_target : ∀ {ι : Type u_1} [Finite ι], MeasurableSet (Set.univ.pi fun x => polarCoord.target)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_zero : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α], Interval.length 0 = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_5 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w l r : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr l)
  (rhs : Std.Tactic.BVDecide.BVExpr r) (h : w = l + r) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.append rhs h with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_5 w l r lhs rhs h
-- Lean.IdentifierSuggestion
/-- Create the extension mapping from existing identifiers to the incorrect alternatives for which we
want to provide suggestions. This is mostly equivalent to a `MapDeclarationExtension` or the
extensions underlying `ParametricAttribute` attributes, but it differs in allowing
`suggest_for` attributes to be assigned in files other than the ones where they were defined.
 -/
_private.Lean.IdentifierSuggestion.0.Lean.mkExistingToIncorrect : IO (Lean.PersistentEnvExtension (Lean.Name × Array Lean.Name) (Lean.Name × Array Lean.Name) (Lean.NameMap Lean.NameSet))
-- Mathlib.Topology.Constructions.SumProd
Topology.IsEmbedding.inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Topology.IsEmbedding Sum.inr
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.disjoint_val_image : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α}
  {t : Set ↥(SubMulAction.ofFixingSubgroup M s)}, Disjoint s (Subtype.val '' t)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.AdjoinPair.algebraMap_gen₂ : ∀ (K : Type u_1) {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x y : L),
  (algebraMap (↥K⟮x, y⟯) L) (IntermediateField.AdjoinPair.gen₂ K x y) = y
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instIsPreorderOpposite : ∀ {α : Type u_1} {i : LE α} [Std.IsPreorder α], Std.IsPreorder α
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.nonempty_type : ∀ {α : Type u_1} (M : Matroid α) [h : M.Nonempty], Nonempty α
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_const_smul : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {R : Type u_3}
  [inst_2 : Monoid R] [inst_3 : DistribMulAction R G] (r : R) (f : M → G), fwdDiff h (r • f) = r • fwdDiff h f
-- Aesop.Rule.Basic
Aesop.Rule.mapM : {m : Type → Type u_1} → {α β : Type} → [Monad m] → (α → m β) → Aesop.Rule α → m (Aesop.Rule β)
-- Mathlib.CategoryTheory.EqToHom
/-- We can push `eqToHom` to the left through families of morphisms.  -/
CategoryTheory.eqToHom_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b)
  {j j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (z j') h)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.continuous : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕),
  Continuous ⇑f
-- Std.Sync.Channel
/-- The buffer space for the channel. Slots with `some v` contain a value that is waiting for
consumption; the slots with `none` are free for enqueueing.

Note that this is a `Vector` of `IO.Ref (Option α)` as the `buf` itself is shared across threads
and would thus keep getting copied if it was a `Vector (Option α)` instead.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.buf : {α : Type} →
  (self : Std.CloseableChannel.Bounded.State✝ α) →
    Vector (IO.Ref (Option α)) (Std.CloseableChannel.Bounded.State.capacity✝ self)
-- Mathlib.Algebra.Module.PUnit
PUnit.instSMul_mathlib : {R : Type u_1} → SMul PUnit.{u_3 + 1} R
-- Lean.Util.Trace
Lean.trace.profiler.threshold.unitAdjusted : Lean.Options → Float
-- Batteries.Control.AlternativeMonad
/-- Lifting preserves `orElse`.  -/
LawfulAlternativeLift.monadLift_orElse : ∀ {m : semiOutParam (Type u → Type v)} {n : Type u → Type w} {inst : Alternative m} {inst_1 : Alternative n}
  {inst_2 : MonadLift m n} [self : LawfulAlternativeLift m n] {α : Type u} (x y : m α),
  monadLift (x <|> y) = (monadLift x <|> monadLift y)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor : ∀ (X Y : SSet.Truncated 2),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.iso X Y).inv.toFunctor =
    SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y
-- Mathlib.RingTheory.EssentialFiniteness
RingHom.essFiniteType_algebraMap : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).EssFiniteType ↔ Algebra.EssFiniteType R S
-- Mathlib.Topology.Bases
/-- In a separable space, a family of nonempty disjoint open sets is countable.  -/
Set.PairwiseDisjoint.countable_of_isOpen : ∀ {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} {a : Set ι},
  a.PairwiseDisjoint s → (∀ i ∈ a, IsOpen (s i)) → (∀ i ∈ a, (s i).Nonempty) → a.Countable
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_comp_rTensor : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} {k : Type u} [inst_1 : CommSemiring k] (f : X ⟶ Y)
  (Z : Action (Type w) G),
  (Representation.LinearizeMonoidal.μ Y Z).comp
      (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.linearizeMap f)) =
    (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)).comp
      (Representation.LinearizeMonoidal.μ X Z)
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context : Type
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.adjointify_η_ε_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G)
  (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X))
      (CategoryTheory.CategoryStruct.comp (ε.hom.app (F.obj X)) h) =
    h
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f g : T₁ ⟶ T₂},
  f = g ↔ f.app = g.app
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toLax_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C), F.toLax.toPrelaxFunctor = F.toPrelaxFunctor
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.ext_iff : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  {f g : R →ₑ+*[φ] S}, f = g ↔ ∀ (x : R), f x = g x
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varFinsetLeft.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : L.Term (α ⊕ β)),
  x.varFinsetLeft =
    match x with
    | FirstOrder.Language.var (Sum.inl i) => {i}
    | FirstOrder.Language.var (Sum.inr _i) => ∅
    | FirstOrder.Language.func _f ts => Finset.univ.biUnion fun i => (ts i).varFinsetLeft
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.ofNNReal_finsetProd : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Logic.Relation
Relation.ReflTransGen.stdSymm : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm (Relation.ReflTransGen r)
-- Mathlib.Algebra.Group.Defs
/-- `NPow` is an implementation detail of `Monoid`. It is needed because it is
impossible to extend `Pow M ℕ` and `Pow M ℤ` at the same time.  -/
NPow : Type u → Type u
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_eq_getD : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a fallback : α} {h' : a ∈ m}, m.get a h' = m.getD a fallback
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualAnnihilator_eq_top_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {W : Submodule R M}
  [Module.Projective R M], W.dualAnnihilator = ⊤ ↔ W = ⊥
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.of_comp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F} [inst_7 : TopologicalSpace G] [inst_8 : AddCommMonoid G] [inst_9 : Module R G]
  {g : F →L[R] G}, (g ∘SL f).HasRightInverse → g.HasRightInverse
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.div_apply : ∀ {M : Type u_2} {G : Type u_5} [inst : MulOneClass M] [inst_1 : CommGroup G] (f g : M →* G) (x : M),
  (f / g) x = f x / g x
-- Lean.Elab.Term.TermElabM
/-- Creates syntax for `(` <ident> `:` <type> `)`  -/
Lean.Elab.Term.mkExplicitBinder : Lean.TSyntax [`ident, `Lean.Parser.Term.hole] → Lean.Term → Lean.Syntax
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_int_le_pow_iff_dvd : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℤ} {n : ℕ}, ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.contains k = true → t.maxKey?.isSome = true
-- Mathlib.Topology.Order.Lattice
ContinuousSup.mk : ∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Max L], (Continuous fun p => p.1 ⊔ p.2) → ContinuousSup L
-- Mathlib.Analysis.Matrix.Hermitian
/-- A matrix is Hermitian iff the corresponding linear map on the Euclidean space is
symmetric.  -/
Matrix.isSymmetric_toEuclideanLin_iff : ∀ {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  (Matrix.toEuclideanLin A).IsSymmetric ↔ A.IsHermitian
-- Mathlib.Order.Filter.Partial
/-- Inverse map of a filter under a partial function. One generalization of `Filter.comap` to
partial functions.  -/
Filter.pcomap' : {α : Type u} → {β : Type v} → (α →. β) → Filter β → Filter α
-- Mathlib.Algebra.Colimit.Module
/-- A component that corresponds to zero in the direct limit is already zero in some
bigger module in the directed system.  -/
AddCommGroup.DirectLimit.of.zero_exact : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] [IsDirectedOrder ι]
  [DirectedSystem G fun i j h => ⇑(f i j h)] (i : ι) (x : G i),
  (AddCommGroup.DirectLimit.of G f i) x = 0 → ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_le_coe_ennreal_iff : ∀ {x y : ENNReal}, ↑x ≤ ↑y ↔ x ≤ y
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.ext : ∀ {α : Type w} {x y : Std.Iterators.Types.ArrayIterator α}, x.array = y.array → x.pos = y.pos → x = y
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
to the coinduced `H`-representation `coind' φ A`, with action on maps given by postcomposition.  -/
Rep.coindFunctor' : (k : Type u) →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] → (G →* H) → CategoryTheory.Functor (Rep.{max u w, u, v} k G) (Rep.{max u w, u, w} k H)
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmas : Type
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.lift_functor : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_5, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_7, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C E A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] (Φ : A → CategoryTheory.Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (a : A),
  (F.lift G Φ hΦ).functor a = Φ a