mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_iter : ∀ {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_6 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {init : γ} {f : β → γ → m (ForInStep γ)}
  {it : Std.Iter β} (inv : Std.Internal.Do.Invariant it.toList γ Pred) {epost : EPred},
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList = pref ++ cur :: suff) (b : γ),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := it.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := it.toList, property := ⋯ } init ⦄ forIn it init f ⦃ fun b =>
      inv { «prefix» := it.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis_iff_isBasis'_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X ↔ M.IsBasis' I X ∧ X ⊆ M.E
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_trans_assoc : ∀ {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 F' F'' : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) {Z : CategoryTheory.Functor C D}
  (h : F'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj1.leftAdjointUniq adj2).hom
      (CategoryTheory.CategoryStruct.comp (adj2.leftAdjointUniq adj3).hom h) =
    CategoryTheory.CategoryStruct.comp (adj1.leftAdjointUniq adj3).hom h
-- Init.Data.UInt.Lemmas
UInt64.toNat_neg : ∀ (a : UInt64), (-a).toNat = (UInt64.size - a.toNat) % UInt64.size
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_const : ∀ (R : Type u_1) {V : Type u_2} {W : Type u_3} (P : Type u_4) {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (q : Q),
  ⇑(ContinuousAffineMap.const R P q) = Function.const P q
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Polynomial.cyclotomic.roots_eq_primitiveRoots_val : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [inst_1 : IsDomain R] [NeZero ↑n],
  (Polynomial.cyclotomic n R).roots = (primitiveRoots n R).val
-- Mathlib.Data.Subtype
Subtype.mk.hinj : ∀ {α : Sort u} {p : α → Prop} {val : α} {property : p val} {α_1 : Sort u} {p_1 : α_1 → Prop} {val_1 : α_1}
  {property_1 : p_1 val_1}, α = α_1 → p ≍ p_1 → ⟨val, property⟩ ≍ ⟨val_1, property_1⟩ → α = α_1 ∧ p ≍ p_1 ∧ val ≍ val_1
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_exact_iff_rTensor_exact : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    ∀ {N1 : Type (max u v)} [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type (max u v)}
      [inst_5 : AddCommGroup N2] [inst_6 : Module R N2] {N3 : Type (max u v)} [inst_7 : AddCommGroup N3]
      [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
      Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuous.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β},
  UpperSemicontinuous f → UpperSemicontinuous g → UpperSemicontinuous fun x => min (f x) (g x)
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.sigmaCongrRight_refl : ∀ {α : Type u_1} {β : α → Type u_2}, (Equiv.Perm.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
-- Aesop.Tree.Data
Aesop.GoalState.toNodeState : Aesop.GoalState → Aesop.NodeState
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofNatLT : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatLT n hn).toUInt32 = UInt32.ofNat n
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}), S.disjointed.set = disjointed S.set
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Weighted generalized mean inequality, version for sums over finite sets, with `ℝ≥0`-valued
functions and real exponents.  -/
NNReal.arith_mean_le_rpow_mean : ∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal),
  ∑ i ∈ s, w i = 1 → ∀ {p : ℝ}, 1 ≤ p → ∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
-- Init.Data.String.Search
/-- Checks whether the string can be interpreted as the decimal representation of an integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally `-` in front. Leading `+` characters are not allowed.

Use `String.toInt?` or `String.toInt!` to convert
such a string to an integer.

Examples:

* `"".isInt = false`

* `"-".isInt = false`

* `"0".isInt = true`

* `"-0".isInt = true`

* `"5".isInt = true`

* `"587".isInt = true`

* `"-587".isInt = true`

* `"+587".isInt = false`

* `" 5".isInt = false`

* `"2-3".isInt = false`

* `"0xff".isInt = false`
 -/
String.isInt : String → Bool
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- The cone itself  -/
CategoryTheory.Limits.WeakLimitCone.cone : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.WeakLimitCone F → CategoryTheory.Limits.Cone F
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_zero : ENNReal.toNNReal 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
CategoryTheory.MonoidalClosed.enrichedCategorySelf_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (X : C), CategoryTheory.eId C X = CategoryTheory.MonoidalClosed.id X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_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).toList = List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.ratio_le_opNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (x : E), ‖f x‖ / ‖x‖ ≤ ‖f‖
-- Mathlib.Algebra.Order.Nonneg.Floor
Nonneg.nat_ceil_coe : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedRing α] [inst_3 : FloorSemiring α]
  (a : { r // 0 ≤ r }), ⌈↑a⌉₊ = ⌈a⌉₊
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert!_le_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.minKey? = some km → (Std.DTreeMap.Internal.Impl.insert! k v t).minKey?.get ⋯ = kmi → (compare kmi km).isLE = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], a ∉ t → t.get! a = default
-- Mathlib.Data.Set.Inclusion
Set.inclusion_inclusion : ∀ {α : Type u_1} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) (x : ↑s),
  Set.inclusion htu (Set.inclusion hst x) = Set.inclusion ⋯ x
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.isScalarTower' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : DecidableEq β] [inst_2 : SMul α β]
  [inst_3 : SMul α γ] [inst_4 : SMul β γ] [IsScalarTower α β γ], IsScalarTower α (Finset β) (Finset γ)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀'_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₀'.Exact
-- Mathlib.Data.Finsupp.Multiset
Sym.coe_equivNatSumOfFintype_apply_apply : ∀ (α : Type u_1) [inst : DecidableEq α] (n : ℕ) [inst_1 : Fintype α] (s : Sym α n) (a : α),
  ↑((Sym.equivNatSumOfFintype α n) s) a = Multiset.count a ↑s
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- An explicit choice of cokernel, which has good properties with respect to the norm.  -/
SemiNormedGrp.explicitCokernel : {X Y : SemiNormedGrp} → (X ⟶ Y) → SemiNormedGrp
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_lt_combine_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.toSubsemigroup_closure : ∀ {A : Type u_5} [inst : Add A] (S : Set A),
  AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) = Subsemigroup.closure (⇑Multiplicative.toAdd ⁻¹' S)
-- Lean.Expr
/-- Return `true` if `e` contains the given free variable.  -/
Lean.Expr.containsFVar : Lean.Expr → Lean.FVarId → Bool
-- Aesop.Rule.Name
Aesop.instToJsonPhaseName.toJson : Aesop.PhaseName → Lean.Json
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.is_equiv_invariant : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [h : FirstOrder.Language.IsFraisse K]
  {M N : CategoryTheory.Bundled L.Structure}, Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_single : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b : β i),
  ‖PiLp.single p i b‖₊ = ‖b‖₊
-- Batteries.Data.String.Lemmas
String.take_eq : ∀ (s : String) (n : ℕ), String.Legacy.take s n = String.ofList (List.take n s.toList)
-- Lean.Elab.Match
/-- Collect problematic index for the "discriminant refinement feature". This method is invoked
when we detect a type mismatch at a pattern #`idx` of some alternative.  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.getIndexToInclude? : Lean.Expr → List ℕ → Lean.Elab.TermElabM (Option Lean.Expr)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertMin : ∀ {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced},
  (Std.DTreeMap.Internal.Impl.insertMin k v t h).impl.toListModel = ⟨k, v⟩ :: t.toListModel
-- Mathlib.Order.Category.Preord
Preord.inv_hom_apply : ∀ {X Y : Preord} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_w_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q₁ q₂ : ℕ) (hq : q₁ ≤ q₂) (i : ℤ)
  {Z : C}
  (h : ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q₁)).obj.mid.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₂).f i)
      (CategoryTheory.CategoryStruct.comp
        (((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).map (CategoryTheory.homOfLE hq).op).hom.h.f
          i)
        h) =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₁).f i) h
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Preregular C] [inst_3 : CategoryTheory.FinitaryExtensive C]
  [∀ (X : C), CategoryTheory.Projective X],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F
-- Mathlib.Analysis.Analytic.OfScalars
/-- This theorem combines the results of the special cases above, using `ENNReal` division to remove
the requirement that the ratio is eventually non-zero.  -/
FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto_ENNReal : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜) [NormOneClass E] {r : ENNReal},
  Filter.Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) Filter.atTop (nhds r) →
    (FormalMultilinearSeries.ofScalars E c).radius = r⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.instIsIsoCodiagonalOfEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f] [CategoryTheory.Epi f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pushout.codiagonal f)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k k' : α}, cmp k k' = Ordering.eq → t.getKey! k = t.getKey! k'
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.QuasiFiniteAt.of_isOpen_singleton_fiber : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (q : PrimeSpectrum S), IsOpen {⟨q, ⋯⟩} → Algebra.QuasiFiniteAt R q.asIdeal
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.restrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : CategoryTheory.Precoverage C} →
      {ι : C → Type w} →
        {X Y : C} →
          (X ⟶ Y) →
            CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y →
              CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι X
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_F : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i],
  (SSet.relativeCellComplexOfMono i).F = ⋯.functor.comp SSet.Subcomplex.toSSetFunctor
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Homotopy between morphisms of short complexes is compatible with subtraction.  -/
CategoryTheory.ShortComplex.Homotopy.sub : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            CategoryTheory.ShortComplex.Homotopy φ₃ φ₄ → CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₃) (φ₂ - φ₄)
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActionEntry.mk.inj : ∀ {declName : Lean.Name} {tacticKinds : Array Lean.Name} {declName_1 : Lean.Name} {tacticKinds_1 : Array Lean.Name},
  { declName := declName, tacticKinds := tacticKinds } = { declName := declName_1, tacticKinds := tacticKinds_1 } →
    declName = declName_1 ∧ tacticKinds = tacticKinds_1
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The two points of a bipointed type, bundled together as a pair.  -/
Bipointed.toProd : (self : Bipointed) → self.X × self.X
-- Init.Data.String.Basic
/-- Returns the character index that corresponds to the provided position (i.e. UTF-8 byte index) in a
string.

If the position is at the end of the string, then the string's length in characters is returned. If
the position is invalid due to pointing at the middle of a UTF-8 byte sequence, then the character
index of the next character after the position is returned.

Examples:
* `"L∃∀N".offsetOfPos ⟨0⟩ = 0`
* `"L∃∀N".offsetOfPos ⟨1⟩ = 1`
* `"L∃∀N".offsetOfPos ⟨2⟩ = 2`
* `"L∃∀N".offsetOfPos ⟨4⟩ = 2`
* `"L∃∀N".offsetOfPos ⟨5⟩ = 3`
* `"L∃∀N".offsetOfPos ⟨50⟩ = 4`
 -/
String.Pos.Raw.offsetOfPos : String → String.Pos.Raw → ℕ
-- Mathlib.Tactic.IntervalCases
/-- Given `a, b, b', p` where `p` proves `a ≱ b` and `b' := b-1`, prove `a ≤ b'`.  -/
Mathlib.Tactic.IntervalCases.Methods.roundDown : Mathlib.Tactic.IntervalCases.Methods → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Finset.Sort
Finset.min'_eq_sorted_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {h : s.Nonempty}, s.min' h = (s.sort fun a b => a ≤ b)[0]
-- Mathlib.Logic.Function.Basic
Function.update_comp_eq_of_forall_ne' : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {α' : Sort u_1} (g : (a : α) → β a) {f : α' → α} {i : α}
  (a : β i), (∀ (x : α'), f x ≠ i) → (fun j => Function.update g i a (f j)) = fun j => g (f j)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.get_skipWhile_char_ne : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {h : pos.skipWhile c ≠ s.endPos}, (pos.skipWhile c).get h ≠ c
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- A finite module can be realised as a quotient of `Fin n → R` (i.e. `R^n`).  -/
Module.Finite.exists_fin_quot_equiv : ∀ (R : Type u_3) (M : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M],
  ∃ n S, Nonempty (((Fin n → R) ⧸ S) ≃ₗ[R] M)
-- Mathlib.Order.RelSeries
RelSeries.last_drop : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)), (p.drop i).last = p.last
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.isoMk_inv_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] [inst_3 : Q.RespectsIso] [inst_4 : W.RespectsIso]
  {A B : P.Arrow Q W} (f : A.left ≅ B.left) (g : A.right ≅ B.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom B.hom = CategoryTheory.CategoryStruct.comp A.hom g.hom)
      CategoryTheory.MorphismProperty.Arrow.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Arrow.isoMk f g w).inv.left = f.inv
-- Init.Data.Vector.Lemmas
Vector.instDecidableExistsVectorZero : {α : Type u_1} → (P : Vector α 0 → Prop) → [Decidable (P #v[])] → Decidable (∃ xs, P xs)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter_subset_compl_verts : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t'),
  SimpleGraph.ErdosStone.filter✝ K t ⊆ K.vertsᶜ
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.hasColimit_of_small_quot : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J], Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F) → CategoryTheory.Limits.HasColimit F
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₁ : ∀ {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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_3),
  (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), Subsemigroup.comap f ⊤ = ⊤
-- Init.Prelude
Lean.Syntax.TSepArray.mk : {ks : Lean.SyntaxNodeKinds} → {sep : String} → Array Lean.Syntax → Lean.Syntax.TSepArray ks sep
-- Lean.Expr
Lean.Int.mkInstHPow : Lean.Expr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeWhisker_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C}
  {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconeWhisker.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- the underlying function of this section  -/
ContMDiffSection.toFun : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] → ContMDiffSection I F n V → (x : M) → V x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insert k v}, (t.insert k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq then k else t.getKey a ⋯
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If `(a : ℕ)` is a root of `cyclotomic n (ZMod p)`, then the multiplicative order of `a` modulo
`p` divides `n`.  -/
Polynomial.orderOf_root_cyclotomic_dvd : ∀ {n : ℕ} (hpos : 0 < n) {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ℕ}
  (hroot : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)),
  orderOf (ZMod.unitOfCoprime a ⋯) ∣ n
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
/-- If `α` has at least 5 elements, but not 6,
then the only nontrivial normal subgroup of `alternatingGroup α`
is `⊤`.  -/
alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_six : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  5 ≤ Nat.card α → Nat.card α ≠ 6 → ∀ {N : Subgroup ↥(alternatingGroup α)} [N.Normal], N = ⊥ ∨ N = ⊤
-- Mathlib.Logic.Equiv.Set
/-- The subtypes corresponding to equal sets are equivalent.  -/
Equiv.setCongr : {α : Type u_3} → {s t : Set α} → s = t → ↑s ≃ ↑t
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.instDecidableEqDihedralGroup.decEq.match_1.eq_4 : ∀ {n : ℕ} (motive : DihedralGroup n → DihedralGroup n → Sort u_1) (a b : ZMod n)
  (h_1 : (a b : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.r b))
  (h_2 : (a a_1 : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.sr a_1))
  (h_3 : (a a_1 : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.r a_1))
  (h_4 : (a b : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.sr b)),
  (match DihedralGroup.sr a, DihedralGroup.sr b with
    | DihedralGroup.r a, DihedralGroup.r b => h_1 a b
    | DihedralGroup.r a, DihedralGroup.sr a_1 => h_2 a a_1
    | DihedralGroup.sr a, DihedralGroup.r a_1 => h_3 a a_1
    | DihedralGroup.sr a, DihedralGroup.sr b => h_4 a b) =
    h_4 a b