mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.add_def : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f g : M →ₚₗ[R] N) (S : Type u) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S], (f + g).toFun' S = f.toFun' S + g.toFun' S
-- Mathlib.Algebra.Homology.QuasiIso
instIsIsoHomologyMapOfQuasiIsoAt : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [hf : QuasiIsoAt f i],
  CategoryTheory.IsIso (HomologicalComplex.homologyMap f i)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) {Z : CommRingCat} (h : X.residueField x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.Γevaluation (f x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop f)
      (CategoryTheory.CategoryStruct.comp (X.Γevaluation x) h)
-- Mathlib.Topology.Algebra.Monoid
continuousMul_iInf : ∀ {M : Type u_3} {ι' : Sort u_6} [inst : Mul M] {ts : ι' → TopologicalSpace M},
  (∀ (i : ι'), ContinuousMul M) → ContinuousMul M
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.field_closure_preimage_le : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Set L),
  Subfield.closure (⇑f ⁻¹' s) ≤ Subfield.comap f (Subfield.closure s)
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
AddMonoidAlgebra.instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsLeftCancelMulZero R] [inst_3 : Add A]
  [UniqueSums A], IsLeftCancelMulZero (AddMonoidAlgebra R A)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem
-- Mathlib.Data.Set.Sigma
Set.sigma_singleton : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {a : (i : ι) → α i}, (s.sigma fun i => {a i}) = (fun i => ⟨i, a i⟩) '' s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toList_toArray : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseEraShort : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Year.Era
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {fallback : α}, t₁.Equiv t₂ → t₁.maxKeyD fallback = t₂.maxKeyD fallback
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CnstrRHS.mk.injEq : ∀ (levelNames : Array Lean.Name) (numMVars : ℕ) (expr : Lean.Expr) (levelNames_1 : Array Lean.Name) (numMVars_1 : ℕ)
  (expr_1 : Lean.Expr),
  ({ levelNames := levelNames, numMVars := numMVars, expr := expr } =
      { levelNames := levelNames_1, numMVars := numMVars_1, expr := expr_1 }) =
    (levelNames = levelNames_1 ∧ numMVars = numMVars_1 ∧ expr = expr_1)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.forIn'_eq_if.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFinitelyAccessibleCategory C] (X : C),
  CategoryTheory.IsFiltered
    (CategoryTheory.CostructuredArrow (CategoryTheory.ObjectProperty.isFinitelyPresentable C).ι X)
-- Mathlib.CategoryTheory.IsoCat
/-- A functor which is an isomorphism of categories is faithful.  -/
CategoryTheory.Functor.IsIso.faithful : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} [self : F.IsIso], F.Faithful
-- Mathlib.Algebra.Group.End
Equiv.Perm.coe_pow : ∀ {α : Type u_4} (f : Equiv.Perm α) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.fun.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.FunDecl pu) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_5)
  (decl_1 : Lean.Compiler.LCNF.FunDecl pu) (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_5),
  (Lean.Compiler.LCNF.Code.fun decl k h = Lean.Compiler.LCNF.Code.fun decl_1 k_1 h_1) = (decl = decl_1 ∧ k = k_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.cfcₙHom_eq_restrict : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S]
  [inst_10 : NonUnitalRing A] [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A]
  [inst_14 : SMulCommClass S A A] [inst_15 : Algebra R S] [inst_16 : Module R A] [inst_17 : IsScalarTower R S A]
  [inst_18 : StarModule R S] [inst_19 : ContinuousSMul R S] [inst_20 : TopologicalSpace A]
  [inst_21 : NonUnitalContinuousFunctionalCalculus S A q] [inst_22 : IsScalarTower R A A]
  [inst_23 : SMulCommClass R A A] [inst_24 : NonUnitalContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] (f : C(S, R)) {a : A} (hpa : p a) (hqa : q a) (h : QuasispectrumRestricts a ⇑f),
  cfcₙHom hpa = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom hqa) h
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulRightLinearEquiv_apply : ∀ (R : Type u_9) {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a : Aˣ) (x : A), (Units.mulRightLinearEquiv R a) x = x * ↑a
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (f : M → N) (x y : M),
  QuadraticMap.polar f x y = f (x + y) - f x - f y
-- Mathlib.Logic.Basic
by_contradiction : ∀ {p : Prop}, (¬p → False) → p
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Auxiliary definition for `bifunctorComp₂₃Functor`.  -/
CategoryTheory.bifunctorComp₂₃FunctorObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄) →
                      CategoryTheory.Functor (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
                        (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)))
-- Batteries.Data.List.Basic
List.fillNones.eq_3 : ∀ {α : Type u_1} (as : List (Option α)), (none :: as).fillNones [] = as.reduceOption
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell_one : Nat.bell 1 = 1
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.left_invariant : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G] (g : G)
  (X : LeftInvariantDerivation I G),
  (hfdifferential ⋯) ((LeftInvariantDerivation.evalAt 1) X) = (LeftInvariantDerivation.evalAt g) X
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.map_constants : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.Embedding M N) (c : L.Constants), φ ↑c = ↑c
-- Init.Data.Ord.SInt
Int8.instLawfulOrderOrd : Std.LawfulOrderOrd Int8
-- Lean.Language.Basic
/-- Whitespace to be appended to contained syntax.  -/
Lean.Language.SnapshotTreeTransform.addTrailing : Lean.Language.SnapshotTreeTransform → Substring.Raw
-- Init.Control.Basic
/-- Right-to-left composition of Kleisli arrows. 

Conventions for notations in identifiers:

 * The recommended spelling of `<=<` in identifiers is `kleisliLeft`. -/
«term_<=<_» : Lean.TrailingParserDescr
-- Lean.Level
Lean.levelOne : Lean.Level
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.snoc.eq_1 : ∀ {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ Set.range ⇑x),
  Fin.Embedding.snoc x ha = { toFun := Fin.snoc (⇑x) a, inj' := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.emod_eq_iff : ∀ {a b c : ℤ}, b ≠ 0 → (a % b = c ↔ 0 ≤ c ∧ c < ↑b.natAbs ∧ b ∣ c - a)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.sup : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Max β]
  [ContinuousSup β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f ⊔ g)
-- Mathlib.Data.Finmap
Finmap.nodup_entries : ∀ {α : Type u} {β : α → Type v} (f : Finmap β), f.entries.Nodup
-- Mathlib.LinearAlgebra.Projection
Submodule.sub_projection_mem : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : E), x - (p.projection q h) x ∈ q
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
/-- **Harris-Kleitman inequality**: Any two lower sets of finsets correlate.  -/
IsLowerSet.le_card_inter_finset' : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s : Finset α},
  IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Antitone fun x => Set.Ioi (f x)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).obj₃ = X₂
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_8 : ∀ {C : Type u} (x x_1 Y : CategoryTheory.FreeMonoidalCategory C) (f : x.Hom Y) (g : Y.Hom x_1),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (f.comp g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeMonoidalCategory.normalizeMapAux f)
      (CategoryTheory.FreeMonoidalCategory.normalizeMapAux g)
-- Init.Data.Int.Gcd
Int.one_lcm : ∀ {a : ℤ}, Int.lcm 1 a = a.natAbs
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.mkFreshExprMVarAtCore : Lean.MVarId →
  Lean.LocalContext → Lean.LocalInstances → Lean.Expr → Lean.MetavarKind → Lean.Name → ℕ → Lean.MetaM Lean.Expr
-- Lean.Exception
Lean.instAddErrorMessageContextOfAddMessageContextOfMonad : (m : Type → Type) → [Lean.AddMessageContext m] → [Monad m] → Lean.AddErrorMessageContext m
-- Lean.Meta.Tactic.Grind.EMatch
/-- Performs one round of E-matching, and returns `true` if new instances were generated.
 -/
Lean.Meta.Grind.ematch : optParam (Array Lean.Meta.Grind.EMatchTheorem) #[] → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_neg`.

---

For `a - -b = a + b`, see `sub_neg_eq_add`.  -/
sub_neg_of_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, a < b → a - b < 0
-- Mathlib.Tactic.FinCases
/-- Implementation of the `fin_cases` tactic.  -/
Lean.Elab.Tactic.finCasesAt : Lean.MVarId → Lean.FVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MeasurePreserving.integrable_comp_emb : ∀ {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : MeasurableSpace δ] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε] {f : α → δ}
  {ν : MeasureTheory.Measure δ},
  MeasureTheory.MeasurePreserving f μ ν →
    MeasurableEmbedding f → ∀ {g : δ → ε}, MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable g ν
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, if an `AddCommMonoid`
map `g : M →+ P` induces a map `f.lift hg : N →+ P` then for all `z : N`, we have
`f.lift hg z + g y = g x`, where `x : M, y ∈ S` are such that `z + f y = f x`.  -/
AddSubmonoid.LocalizationMap.lift_add_right : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N),
  (f.lift hg) z + g ↑(f.sec z).2 = g (f.sec z).1
-- Mathlib.Data.Rat.Cast.Lemmas
Rat.cast_nnratCast : ∀ {K : Type u_2} [inst : DivisionRing K] (q : ℚ≥0), ↑↑q = ↑q
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Module.hom_ext : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] {g₁ g₂ : DirectLimit G f →ₗ[R] P},
  (∀ (i : ι), g₁ ∘ₗ DirectLimit.Module.of R ι G f i = g₂ ∘ₗ DirectLimit.Module.of R ι G f i) → g₁ = g₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α},
  t.erase k ≠ ∅ → ¬cmp k (t.maxKeyD fallback) = Ordering.eq → (t.erase k).maxKeyD fallback = t.maxKeyD fallback
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isValidRevSearchFrom_iff_isValidRevSearchFrom_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidRevSearchFrom pat pos l ↔
    String.Slice.Pattern.Model.IsValidRevSearchFrom pat.toSlice pos l
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_3.eq_2 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₂ m γ] (it₂ : Std.IterM m γ)
  (motive : it₂.Step → Sort u_3) (it₂' : Std.IterM m γ) (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂'))
  (h_1 :
    (it₂' : Std.IterM m γ) →
      (out : γ) → (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩)
  (h_2 :
    (it₂' : Std.IterM m γ) → (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩)
  (h_3 : (h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₂', h⟩ with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => h_1 it₂' out h
    | ⟨Std.IterStep.skip it₂', h⟩ => h_2 it₂' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₂' h
-- Lean.Meta.Tactic.Simp.Types
/-- Helper function for `simpAppUsingCongr`  -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.mkCongrArg' : Lean.Expr → Lean.Expr → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Lie.CartanExists
LieAlgebra.engel_isBot_of_isMin.lieCharpoly_natDegree : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x y : L) [Nontrivial R], (LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x y).natDegree = Module.finrank R M
-- Mathlib.CategoryTheory.Action.Monoidal
Action.whiskerRight_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] {X₁ X₂ : Action V G} (f : X₁ ⟶ X₂) (Y : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.V
-- Mathlib.Data.Int.Cast.Basic
Int.cast_negOfNat : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ), ↑(Int.negOfNat n) = -↑n
-- Mathlib.CategoryTheory.Sites.Continuous
/-- (Implementation) Use the more general `Functor.W_map_of_adjunction_of_isContinuous`.  -/
_private.Mathlib.CategoryTheory.Sites.Continuous.0.CategoryTheory.Functor.W_map_of_adjunction_of_isContinuous_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (F : CategoryTheory.Functor C D)
  (H :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))))
  (adj : H ⊣ (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op) [F.IsContinuous J K]
  {G G' : CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₁ u₂ v₂))} (f : G ⟶ G'), J.W f → K.W (H.map f)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_closure : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure (M.closure X) = M.closure X
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_centralizer : ∀ {R : Type u_1} [inst : Semiring R] (s : Set R), ↑(Subsemiring.centralizer s) = s.centralizer
-- Mathlib.Topology.ContinuousMap.Basic
/-- Evaluation at point as a bundled continuous map.  -/
ContinuousMap.eval : {I : Type u_5} → {X : I → Type u_7} → [inst : (i : I) → TopologicalSpace (X i)] → (i : I) → C((j : I) → X j, X i)
-- Mathlib.Data.Finset.NoncommProd
AddMonoidHom.pi_ext : ∀ {ι : Type u_2} {γ : Type u_5} [inst : AddMonoid γ] {M : ι → Type u_6} [inst_1 : (i : ι) → AddMonoid (M i)] [Finite ι]
  [inst_3 : DecidableEq ι] {f g : ((i : ι) → M i) →+ γ},
  (∀ (i : ι) (x : M i), f (Pi.single i x) = g (Pi.single i x)) → f = g
-- Mathlib.Algebra.Free
Magma.AssocQuotient.quot_mk_assoc_left : ∀ {α : Type u} [inst : Mul α] (x y z w : α),
  Quot.mk (Magma.AssocRel α) (x * (y * z * w)) = Quot.mk (Magma.AssocRel α) (x * (y * (z * w)))
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.of_aeval_monic : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x : A}
  {p : Polynomial R}, p.Monic → p.natDegree ≠ 0 → IsIntegral R ((Polynomial.aeval x) p) → IsIntegral R x
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightEq.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₂ ⟶ L₁) (h : l = l'),
  CategoryTheory.Comma.mapRightEq R l l' h =
    CategoryTheory.NatIso.ofComponents'
      (fun X =>
        CategoryTheory.Comma.isoMk._to_dual_1
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapRight R l).obj X).right)
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapRight R l).obj X).left) ⋯)
      ⋯
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_inf_stabilizer_le_stabilizer_union : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s t : Set α},
  MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s ∪ t)
-- Mathlib.Geometry.Manifold.Instances.Real
Icc_isBoundaryPoint_top : ∀ {x y : ℝ} [hxy : Fact (x < y)], (modelWithCornersEuclideanHalfSpace 1).IsBoundaryPoint ⊤
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Given the proof for a proposition to be used as an E-matching theorem,
infers its type, and preprocess it to identify generalized patterns.
Recall that we infer these generalized patterns automatically for
`match` congruence equations.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.inferEMatchProofType : Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Std.Data.ExtHashSet.Basic
/-- Computes the intersection of the given hash sets.

This function always iterates through the smaller set.
 -/
Std.ExtHashSet.inter : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → Std.ExtHashSet α → Std.ExtHashSet α
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_top : ∀ {α : Type u_1} [inst : Preorder α] [InfiniteDimensionalOrder α], Order.krullDim α = ⊤
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.topologyOfClosureOperator_close : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X))
  (pb :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X),
      (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S))
  (X : C) (S : CategoryTheory.Sieve X), (CategoryTheory.topologyOfClosureOperator c pb).close S = (c X) S
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
_private.Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential.0.UniqueMDiffWithinAt.bundle_preimage_aux : ∀ {𝕜 : 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] {s : Set M} {F : Type u_9} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {Z : M → Type u_10} [inst_8 : TopologicalSpace (Bundle.TotalSpace F Z)]
  [inst_9 : (b : M) → TopologicalSpace (Z b)] [inst_10 : FiberBundle F Z] {p : Bundle.TotalSpace F Z},
  UniqueMDiffAt[s] p.proj → s ⊆ (trivializationAt F Z p.proj).baseSet → UniqueMDiffAt[Bundle.TotalSpace.proj ⁻¹' s] p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {i : ℕ},
  i < r.toList.length → (Std.PRange.least?.bind (Std.PRange.succMany? i)).isSome = true
-- Mathlib.Algebra.GroupWithZero.Defs
/-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
equals zero.  -/
mul_eq_zero : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- `pullback` is a pullback of `f₁` and `f₂`  -/
CategoryTheory.Limits.ChosenPullback.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          (self : CategoryTheory.Limits.ChosenPullback f₁ f₂) →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk self.p₁ self.p₂ ⋯)