mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_middle.inj : ∀ {lhs : Bool} {s₁ s₂ : Lean.Grind.AC.Seq} {c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr} {lhs_1 : Bool}
  {s₁_1 s₂_1 : Lean.Grind.AC.Seq} {c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.simp_middle lhs_1 s₁_1 s₂_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s₁ = s₁_1 ∧ s₂ = s₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.aeval_verschiebungPoly : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  (MvPolynomial.aeval x.coeff) (WittVector.verschiebungPoly n) = (WittVector.verschiebung x).coeff n
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.charFun_multivariateGaussian : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  S.PosSemidef →
    ∀ (x : EuclideanSpace ℝ ι),
      MeasureTheory.charFun (ProbabilityTheory.multivariateGaussian μ S) x =
        Complex.exp (↑(inner ℝ x μ) * Complex.I - ↑(x.ofLp ⬝ᵥ S.mulVec x.ofLp) / 2)
-- Init.Data.List.Sort.Lemmas
List.merge_perm_append : ∀ {α : Type u_1} (le : α → α → Bool) {xs ys : List α}, (xs.merge ys le).Perm (xs ++ ys)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_le_size_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.size ≤ (t.erase k).size + 1
-- Mathlib.Algebra.Group.Basic
zsmul_comm : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (m n : ℤ), n • m • a = m • n • a
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- If `I` is a two-sided ideal of `Rᵐᵒᵖ`, then `{x.unop | x ∈ I}` is a two-sided ideal in `R`.  -/
TwoSidedIdeal.unop : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → TwoSidedIdeal Rᵐᵒᵖ → TwoSidedIdeal R
-- Mathlib.Order.RelIso.Set
Subrel.relEmbedding_apply : ∀ {α : Type u_1} (r : α → α → Prop) (p : α → Prop) (a : Subtype p), (Subrel.relEmbedding r p) a = ↑a
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstHDivInt : Lean.Expr → Lean.MetaM Bool
-- Init.Data.List.Sublist
List.take_prefix : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.take i l <+: l
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.mem_finset_iff : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (l : Fin (d + 1)), l ∈ SSet.prodStdSimplex.pairingCore.finset x hd ↔ (x.cast hd).simplex.1 l = k.succ
-- Mathlib.SetTheory.Ordinal.Notation
ONote.sub.eq_1 : ∀ (x : ONote), ONote.zero.sub x = 0
-- Aesop.Frontend.RuleExpr
Lean.Parser.Category.Aesop.phase : Lean.Parser.Category
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsMatch.ne_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos → pos ≠ s.startPos
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.iterate : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → α},
  MeasureTheory.MeasurePreserving f μ μ → ∀ (n : ℕ), MeasureTheory.MeasurePreserving f^[n] μ μ
-- Init.Data.List.ToArray
List.idxOf_toArray : ∀ {α : Type u_1} [inst : BEq α] {as : List α} {a : α}, Array.idxOf a as.toArray = List.idxOf a as
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- While equal, the former has a convenient definitional reduction.  -/
MvPolynomial.homogeneousSubmodule_eq_finsupp_supported : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R] (n : ℕ),
  MvPolynomial.homogeneousSubmodule σ R n = AddMonoidAlgebra.supported R R {d | Finsupp.degree d = n}
-- Mathlib.Order.WithBot
WithTop.bot_eq_coe : ∀ {α : Type u_1} [inst : Bot α] {a : α}, ⊥ = ↑a ↔ ⊥ = a
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
_private.Mathlib.GroupTheory.FreeGroup.NielsenSchreier.0.IsFreeGroupoid.SpanningTree.homOfPath.match_1.eq_1 : ∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
  (motive :
    (x : G) →
      Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) x → Sort u_2)
  (h_1 :
    Unit →
      motive (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) Quiver.Path.nil)
  (h_2 :
    (x b : WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T) →
      (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) b) →
        (f : b ⟶ x) → motive x (p.cons f)),
  (match Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T), Quiver.Path.nil with
    | .(Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)), Quiver.Path.nil =>
      h_1 ()
    | x, p.cons f => h_2 x b p f) =
    h_1 ()
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateProjImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has cofiltered limits is said to have `AB5Star` (in literature `AB5*`)
provided that cofiltered limits are exact.
 -/
CategoryTheory.AB5StarOfSize : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w', v, u} C] → Prop
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- A finitely generated cancellative additive monoid with a single unit is generated by its
(finitely many) irreducible elements.  -/
AddSubmonoid.closure_addIrreducible : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] [Subsingleton (AddUnits M)] [AddMonoid.FG M],
  AddSubmonoid.closure {p | AddIrreducible p} = ⊤
-- Mathlib.ModelTheory.Satisfiability
/-- If a theory is complete all its models are elementarily equivalent.  -/
FirstOrder.Language.Theory.IsComplete.models_elementarily_equivalent : ∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete →
    ∀ (M : Type u_1) (N : Type u_2) [inst : L.Structure M] [inst_1 : L.Structure N] [M ⊨ T] [N ⊨ T] [Nonempty M]
      [Nonempty N], L.ElementarilyEquivalent M N
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.map_aux : ∀ {α : Type u_1} [inst : Preorder α] {β : Type u_2} [inst_1 : Preorder β] {f : α → β},
  StrictMono f →
    ∀ {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α},
      Ordnode.Valid' a₁ t a₂ →
        Ordnode.Valid' (Option.map f a₁) (Ordnode.map f t) (Option.map f a₂) ∧ (Ordnode.map f t).size = t.size
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.op_smul_eq_iff_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {c : Set G} {x : G},
  c ∈ MulAction.orbit Gᵐᵒᵖ ↑H → (x ∈ c ↔ MulOpposite.op x • ↑H = c)
-- Mathlib.Topology.Inseparable
/-- A map `f` between topological spaces is specializing if specializations lifts along `f`,
i.e. for each `f x' ⤳ y` there is some `x` with `x' ⤳ x` whose image is `y`.  -/
SpecializingMap : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Lean.Parser.Basic
/-- If the leading token is an identifier, then the parser just executes the parsers associated
with the auxiliary token “ident”, which parses identifiers.
 -/
Lean.Parser.LeadingIdentBehavior.default : Lean.Parser.LeadingIdentBehavior
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_lt_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x ^ z⁻¹ < y ↔ x < y ^ z)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (self : F ⊣₂ G) {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
  CategoryTheory.CategoryStruct.comp (self.adj X₁).unit
      (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) =
    CategoryTheory.CategoryStruct.comp (self.adj Y₁).unit ((F.obj Y₁).whiskerLeft (G.map f.op))
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.instSMulCommClass : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], SMulCommClass R R (PiTensorProduct R fun i => s i)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.ofMulEquiv : ∀ {G : Type u_1} [inst : Group G] [IsFreeGroup G] {H : Type u_2} [inst_2 : Group H] (e : G ≃* H), IsFreeGroup H
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.isStronglyProgressive_const`. -/
MeasureTheory.progMeasurable_const : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : Type u_3} [inst_1 : TopologicalSpace β]
  [inst_2 : MeasurableSpace ι] (f : MeasureTheory.Filtration ι m) (b : β),
  MeasureTheory.IsStronglyProgressive f fun x x_1 => b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k}
  {fallback : β k'},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (t.insertMany l).getD k' fallback = cast ⋯ v
-- Mathlib.Data.Fin.Tuple.Finset
Finset.card_snocEquiv_filter_piFinset : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α i.castSucc) → Prop)
  [inst : DecidablePred P],
  {r ∈ Fintype.piFinset S | P (Fin.init r)}.card =
    (S (Fin.last n)).card * {r ∈ Fintype.piFinset (Fin.init S) | P r}.card
-- Mathlib.Algebra.Ring.Commute
neg_one_pow_eq_pow_mod_two : ∀ {R : Type u} [inst : Ring R] (n : ℕ), (-1) ^ n = (-1) ^ (n % 2)
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.pf_mul_c : ∀ {α : Type u_1} {a b : α} [inst : Mul α], a = b → ∀ (c : α), a * c = b * c
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  [CategoryTheory.LocallySmall.{w, v, u} C], CategoryTheory.Limits.PreservesFiniteLimits Φ.fiber
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.range_sdiff_image_subset`. -/
Set.range_diff_image_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.range f \ f '' s ⊆ f '' sᶜ
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piEquivPiSubtypeProd_apply : ∀ {ι : Type u_7} (p : ι → Prop) (Y : ι → Type u_8) [inst : (i : ι) → TopologicalSpace (Y i)] [inst_1 : DecidablePred p]
  (f : (i : ι) → Y i), (Homeomorph.piEquivPiSubtypeProd p Y) f = (fun x => f ↑x, fun x => f ↑x)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instT0Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T0Space M], T0Space Mᵈᵐᵃ
-- Batteries.Data.List.Lemmas
List.diff_eq_foldl : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l₁ l₂ : List α), l₁.diff l₂ = List.foldl List.erase l₁ l₂
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.match_1.eq_1 : ∀ (motive : Option Lean.Syntax.Range → Sort u_1) (trail : Lean.Syntax.Range)
  (h_1 : (trail : Lean.Syntax.Range) → motive (some trail)) (h_2 : (x : Option Lean.Syntax.Range) → motive x),
  (match some trail with
    | some trail => h_1 trail
    | x => h_2 x) =
    h_1 trail
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.FarFromTriangleFree.lt_one : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [Nonempty α], G.FarFromTriangleFree ε → ε < 1
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.fderiv : ∀ {𝕜 : 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] {f : E → F}
  {x : E} (h : IsBoundedLinearMap 𝕜 f), fderiv 𝕜 f x = IsBoundedLinearMap.toContinuousLinearMap f h
-- Mathlib.Order.Interval.Basic
Interval.coe_dual : ∀ {α : Type u_1} [inst : PartialOrder α] (s : Interval α), ↑(Interval.dual s) = ⇑OrderDual.ofDual ⁻¹' ↑s
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
ContMDiffWithinAt.mdifferentiableWithinAt : ∀ {𝕜 : 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'] {f : M → M'} {x : M} {s : Set M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → n ≠ 0 → MDiffAt[s] f x
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_deriv_one_sub_smoothingFn : (deriv fun x => 1 - AkraBazziRecurrence.smoothingFn x) =ᶠ[Filter.atTop] fun x => x⁻¹ / Real.log x ^ 2
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- A function is `C^k` on a union of open sets `s i` iff it is `C^k` on each `s i`.  -/
contDiffOn_iUnion_iff_of_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞}
  {ι : Type u_5} {s : ι → Set E},
  (∀ (i : ι), IsOpen (s i)) → (ContDiffOn 𝕜 n f (⋃ i, s i) ↔ ∀ (i : ι), ContDiffOn 𝕜 n f (s i))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp ((t.insert k v).minKey ⋯) k).isLE = true
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.productEquiv_counitIso_hom_app : ∀ {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J × CategoryTheory.Discrete K),
  CategoryTheory.Discrete.productEquiv.counitIso.hom.app X =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Mathlib.Algebra.Order.Monoid.Units
Units.instMaxOfLinearOrder : {α : Type u_1} → [inst : Monoid α] → [LinearOrder α] → Max αˣ
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_inter : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.hom_inv_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (e : A ≅ B) (x : ↑B),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x
-- Mathlib.Topology.Compactness.Compact
/-- If a compact set belongs to a filter and this filter has a unique cluster point `y` in this set,
then the filter is less than or equal to `𝓝 y`.  -/
IsCompact.le_nhds_of_unique_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {l : Filter X} {y : X}, s ∈ l → (∀ x ∈ s, ClusterPt x l → x = y) → l ≤ nhds y
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeMapCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D}
  {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Functor.mapConeMapCone c =
    CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (H'.mapCone (H.mapCone c)).pt) ⋯
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.fixedReduce_eq_smul_iff : ∀ {R : Type u_4} {V : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (e : V ≃ₗ[R] V) (a : R),
  (∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x) ↔ ∀ (v : V), e v - a • v ∈ (↑e).fixedSubmodule
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_injective : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (f : P →ₐ[R] P'),
  Function.Injective ⇑f → Function.Injective (FractionalIdeal.map f)
-- Mathlib.Order.Filter.Pointwise
Filter.top_pow : ∀ {α : Type u_2} [inst : Monoid α] {n : ℕ}, n ≠ 0 → ⊤ ^ n = ⊤
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_pow : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : Ideal R) (n : ℕ), ↑(I ^ n) = ↑I ^ n
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.comp.match_1.eq_4 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : (x x_1 x_2 : CategoryTheory.Join C D) → x.Hom x_1 → x_1.Hom x_2 → Sort u_5) (_x _y _z : D)
  (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y))
  (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z))
  (h_1 :
    (_x _y _z : C) →
      (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
        (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z)) →
          motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.left _z) f g)
  (h_2 :
    (_x _y : C) →
      (_z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
          (x_1 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.right _z) x x_1)
  (h_3 :
    (_x : C) →
      (_y _z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y)) →
          (x_1 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) x x_1)
  (h_4 :
    (_x _y _z : D) →
      (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y)) →
        (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
          motive (CategoryTheory.Join.right _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) f g),
  (match CategoryTheory.Join.right _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, f, g with
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.left _z, f, g => h_1 _x _y _z f g
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.right _z, x, x_1 =>
      h_2 _x _y _z x x_1
    | CategoryTheory.Join.left _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, x, x_1 =>
      h_3 _x _y _z x x_1
    | CategoryTheory.Join.right _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, f, g =>
      h_4 _x _y _z f g) =
    h_4 _x _y _z f g
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.interSmaller : {α : Type u} → {β : α → Type v} → [BEq α] → List ((a : α) × β a) → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.Algebra.Homology.Augment
ChainComplex.truncate_obj_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) (i j : ℕ), (ChainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.eq : ∀ {M : Type u_1} [inst : Mul M] {a : M}, IsIdempotentElem a → a * a = a
-- Mathlib.Computability.Primrec.Basic
Primrec.option_map₁ : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
  Primrec f → Primrec (Option.map f)
-- Init.System.IO
/-- Runs an action with `stdin` emptied and `stdout` and `stderr` captured into a `String`. If
`isolateStderr` is `false`, only `stdout` is captured.
 -/
IO.FS.withIsolatedStreams : {m : Type → Type u_1} →
  {α : Type} → [Monad m] → [MonadFinally m] → [MonadLiftT BaseIO m] → m α → optParam Bool true → m (String × α)
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_right : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Ici ↑n)) (nhdsWithin (↑n) (Set.Ici ↑n))
-- Mathlib.FieldTheory.KummerExtension
autAdjoinRootXPowSubC_root : ∀ {K : Type u} [inst : Field K] {n : ℕ} (a : K) (η : ↥(rootsOfUnity n K)),
  ((autAdjoinRootXPowSubC n a) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) =
    ↑↑η • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonAddMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α],
  Finset.singletonAddMonoidHom = { toFun := Finset.singletonAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.reinsertAux.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : { d // 0 < d.size } → Sort u_3)
  (data : Array (Std.DHashMap.Internal.AssocList α β)) (hd : 0 < data.size)
  (h_1 : (data : Array (Std.DHashMap.Internal.AssocList α β)) → (hd : 0 < data.size) → motive ⟨data, hd⟩),
  (match ⟨data, hd⟩ with
    | ⟨data, hd⟩ => h_1 data hd) =
    h_1 data hd
-- Lean.Parser.Command
Lean.Parser.Command.initializeKeyword : Lean.Parser.Parser
-- Mathlib.Data.Finset.Basic
Finset.isEmpty_of_forall_eq_empty : ∀ {α : Type u_4}, (∀ (s : Finset α), s = ∅) → IsEmpty α
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_lt_logb_iff_of_base_lt_one : ∀ {b x y : ℝ}, 0 < b → b < 1 → 0 < x → 0 < y → (Real.logb b x < Real.logb b y ↔ y < x)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_smulₛₗ : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : R₁) (x : M₁), e (c • x) = σ₁₂ c • e x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldr_eq_foldr_toList : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α_1} {init : α_1} {t : RBTree.RBNode α},
  RBTree.RBNode.foldr f t init = List.foldr f init t.toList
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- A `NonUnitalSubring` is isomorphic to its image under an injective function  -/
NonUnitalSubring.equivMapOfInjective : {F : Type w} →
  {R : Type u} →
    {S : Type v} →
      [inst : NonUnitalNonAssocRing R] →
        [inst_1 : NonUnitalNonAssocRing S] →
          [inst_2 : FunLike F R S] →
            [inst_3 : NonUnitalRingHomClass F R S] →
              (s : NonUnitalSubring R) → (f : F) → Function.Injective ⇑f → ↥s ≃+* ↥(NonUnitalSubring.map f s)