mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Jordan
_private.Mathlib.GroupTheory.GroupAction.Jordan.0.IsPreprimitive.is_two_pretransitive' : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        MulAction.IsPreprimitive G α →
          {s : Set α} →
            {n : ℕ} →
              Nat.card ↑s = n + 1 →
                n + 1 < Nat.card α →
                  MulAction.IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
                    ProofWanted
                      (MulAction.IsMultiplyPretransitive (↥(Subgroup.normalClosure ↑(fixingSubgroup G s))) α 2)
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.add_right : ∀ {R : Type u} [inst : Distrib R] {a x y x' y' : R},
  SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x + x') (y + y')
-- Mathlib.Topology.Homotopy.Basic
/-- Casting a `HomotopyRel f₀ f₁ S` to a `HomotopyRel g₀ g₁ S` where `f₀ = g₀` and `f₁ = g₁`.
 -/
ContinuousMap.HomotopyRel.cast : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {S : Set X} → {f₀ f₁ g₀ g₁ : C(X, Y)} → f₀.HomotopyRel f₁ S → f₀ = g₀ → f₁ = g₁ → g₀.HomotopyRel g₁ S
-- Mathlib.Data.Finset.Update
Function.updateFinset_singleton : ∀ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {i : ι} {y : (i_1 : ↥{i}) → π ↑i_1},
  Function.updateFinset x {i} y = Function.update x i (y ⟨i, ⋯⟩)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.partialMatch_add_one_add_one_iff : ∀ {pat s : ByteArray} {stackPos needlePos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s (needlePos + 1) (stackPos + 1) ↔
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos ∧
      ∃ (h₁ : needlePos < pat.size) (h₂ : stackPos < s.size), pat[needlePos] = s[stackPos]
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N),
  (f.lift hg) z = g (f.sec z).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹
-- Mathlib.CategoryTheory.Adjunction.Opposites
/-- If `F` and `F'` are both adjoint to `G`, there is a natural isomorphism
`F.op ⋙ coyoneda ≅ F'.op ⋙ coyoneda`.
We use this in combination with `fullyFaithfulCancelRight` to show left adjoints are unique.
 -/
CategoryTheory.Adjunction.leftAdjointsCoyonedaEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F F' : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) → (F' ⊣ G) → (F.op.comp CategoryTheory.coyoneda ≅ F'.op.comp CategoryTheory.coyoneda)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitLower_eq_self : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, I.splitLower i x = ↑I ↔ I.upper i ≤ x
-- Aesop.Options.Public
/-- The transparency used by the `applyHyps` builtin rule. The rule applies a
hypothesis `h : T` if `T ≡ ∀ (x₁ : X₁) ... (xₙ : Xₙ), Y` at the given
transparency and if additionally the goal's target is defeq to `Y` at the
given transparency.
 -/
Aesop.Options.applyHypsTransparency : Aesop.Options → Lean.Meta.TransparencyMode
-- Mathlib.Topology.Algebra.Group.Quotient
/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.  -/
QuotientGroup.nhds_eq : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (N : Subgroup G) (x : G),
  nhds ↑x = Filter.map QuotientGroup.mk (nhds x)
-- Mathlib.Order.Filter.Lift
Filter.sInter_lift_sets : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β},
  Monotone g → ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x) (n : ℕ),
  a = Lean.Grind.CommRing.Expr.natCast n →
    (match a with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.intCast n => h_2 n
      | Lean.Grind.CommRing.Expr.natCast n => h_3 n
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | x => h_5 x) ≍
      h_3 n
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- `homₚ` and `hom` need to be compatible with `HomologyPretheory.iso`.  -/
TopPair.HomologyPretheory.Hom.iso_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (self : HP.Hom HP') (i : ι),
  CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (self.homₚ i)) =
    CategoryTheory.CategoryStruct.comp (self.hom i) (HP'.iso i).hom
-- Init.Data.String.Modify
String.remainingBytes_pastModify : ∀ {s : String} {p : s.Pos} {f : Char → Char} {hp : p ≠ s.endPos},
  (p.pastModify f hp).remainingBytes = (p.next hp).remainingBytes
-- Init.Data.UInt.Bitwise
UInt8.toUSize_shiftLeft_of_lt : ∀ (a b : UInt8), b < 8 → (a <<< b).toUSize = a.toUSize <<< b.toUSize % 256
-- Mathlib.Data.Nat.ModEq
Nat.odd_mul_odd : ∀ {n m : ℕ}, n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_some_getElem! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, a ∈ m → m[a]? = some m[a]!
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.strictAnti_eulerMascheroniSeq' : StrictAnti Real.eulerMascheroniSeq'
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
OneHom.withTopMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N] (f : OneHom M N),
  f.withTopMap = { toFun := WithTop.map ⇑f, map_one' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {coverings coverings_1 : (X : C) → Set (CategoryTheory.Presieve X)},
  { coverings := coverings } = { coverings := coverings_1 } → coverings = coverings_1
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_comm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} (x y : E),
  ((ProbabilityTheory.covarianceBilin μ) x) y = ((ProbabilityTheory.covarianceBilin μ) y) x
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.of_equiv : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} {B : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyUnramified R A] (e : A ≃ₐ[R] B),
  Algebra.FormallyUnramified R B
-- Lean.ScopedEnvExtension
Lean.registerSimpleScopedEnvExtension : {α σ : Type} → Lean.SimpleScopedEnvExtension.Descr α σ → IO (Lean.SimpleScopedEnvExtension α σ)
-- Lean.Meta.Tactic.Grind.Action
/-- Returns `true` if the tactic sequence `seq` closes `goal` starting at saved state `s?`.
If `s?` is `none` just returns `true`.
 -/
Lean.Meta.Grind.Action.checkSeqAt : Option Lean.Meta.Grind.SavedState → Lean.Meta.Grind.Goal → List Lean.Meta.Grind.TGrind → Lean.Meta.Grind.GrindM Bool
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_left_midpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), nndist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * nndist p₁ p₂
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_3),
  (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f =
    X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁
-- Mathlib.Topology.Inseparable
SeparationQuotient.instOne : {X : Type u_1} → [inst : TopologicalSpace X] → [One X] → One (SeparationQuotient X)
-- Lean.Meta.Tactic.Grind.EqResolution
/-- Sorts metavariables `ms` using topological sort.
There is an "edge" from `m₁` to `m₂` if type of `m₁` contains `m₂`.
We use this function to ensure that after applying equality resolution to
```
∀ x : Nat, p x a → ∀ y : Nat, p y b → x = y → False
```
we produce
```
∀ y, p y a → p y b → False
```
instead of
```
p ?y a → ∀ y, p y b → False
```
Recall that in equality resolution we create a meta-variable for each hypothesis.
Thus, we initially have
```
?x : Nat, ?h₁ : p ?x a, ?y : Nat, ?h₂ : p ?y b, ?h₃ : ?x = ?y
```
Then, we resolve `?h₃ : ?x = ?y` as `?y := ?x` and `?h₃ := Eq.refl ?y`.
But `?h₁` occurs before `?y`. We use topological sort to address this situation.
If a cycle is detected, it returns `none`.
 -/
_private.Lean.Meta.Tactic.Grind.EqResolution.0.Lean.Meta.Grind.topsortMVars? : Array Lean.Expr → Lean.MetaM (Option (Array Lean.Expr))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelπ_surjective : ∀ {X Y : SemiNormedGrp} {f : X ⟶ Y},
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (SemiNormedGrp.explicitCokernelπ f))
-- Mathlib.Data.Finsupp.SMul
Finsupp.mapDomain_smul : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [inst : AddCommMonoid M] [inst_1 : DistribSMul R M]
  {f : α → β} (b : R) (v : α →₀ M), Finsupp.mapDomain f (b • v) = b • Finsupp.mapDomain f v
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_ofReal_norm_sq_left_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v w : E}, inner 𝕜 v w = ↑‖v‖ ^ 2 ↔ inner 𝕜 v (v - w) = 0
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzOnWith.iff_le_add_mul : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {f : α → ℝ} {K : NNReal},
  LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y
-- Mathlib.Algebra.Group.Semiconj.Units
SemiconjBy.units_inv_right_iff : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a ↑x ↑y
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
/-- If `f : R →+* S` is a local ring hom, then `R` is a local ring if `S` is.  -/
RingHom.domain_isLocalRing : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f],
  IsLocalRing R
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- Notation for the Grothendieck category associated to a pseudofunctor `F`.  -/
CategoryTheory.Pseudofunctor.Grothendieck.«term∫_» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Support
/-- An inner regular measure has conull support when open sets are measurable.  -/
MeasureTheory.Measure.support_mem_ae_of_innerRegular : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] [μ.InnerRegular], μ.support ∈ MeasureTheory.ae μ
-- Mathlib.Order.Hom.Bounded
TopHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : OrderTop α] [inst_2 : LE β] [inst_3 : OrderTop β]
  [inst_4 : LE γ] [inst_5 : OrderTop γ] (g : TopHom β γ) (f : TopHom α β),
  TopHom.dual (g.comp f) = (TopHom.dual g).comp (TopHom.dual f)
-- Init.Data.Vector.Attach
Vector.back?_attachWith : ∀ {α : Type u_1} {n : ℕ} {P : α → Prop} {xs : Vector α n} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H).back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩
-- Mathlib.RingTheory.Henselian
Field.henselian : ∀ (K : Type u_1) [inst : Field K], HenselianLocalRing K
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.smul_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : SeminormedAddCommGroup Y] {C r : NNReal}
  {f : X → Y} {α : Type u_4} [inst_2 : SeminormedRing α] [inst_3 : Module α Y] [NormSMulClass α Y] (a : α),
  ‖a‖₊ ≠ 0 → (HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f)
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_comm : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] (f g : Π₀ (a : α), N a), f.neLocus g = g.neLocus f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.pow_subset_pow_right : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α} {m n : ℕ}, 1 ∈ s → m ≤ n → s ^ m ⊆ s ^ n
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.norm = NumberField.mixedEmbedding.norm
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal : ∀ (K : Type u_1) [inst : Field K] (x : NumberField.mixedEmbedding.realMixedSpace K) (w : { w // w.IsReal }),
  ((NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K) x).1 ↑w = x.1 w
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.rid_comp_includeLeftRingHom : ∀ (R : Type uR) (S : Type uS) (A : Type uA) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A],
  (↑(Algebra.TensorProduct.rid R S A)).comp Algebra.TensorProduct.includeLeftRingHom = RingHom.id A
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.of_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X n ⟶ X (n + 1)) (j : α), CochainComplex.of.d X d j (j + 1) = d j
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).isEmpty =
    ((m.isEmpty || m.size == 1 && m.contains k) && (f (Std.DHashMap.Const.get? m k)).isNone)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_sub : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B : TopRep k G)
  (f g : A ⟶ B), TopRep.Hom.hom (f - g) = TopRep.Hom.hom f - TopRep.Hom.hom g
-- Mathlib.Data.Nat.Factorization.Root
/-- Galois connection between `a ↦ a ^ n : ℕ → ℕ` and `floorRoot n : ℕ → ℕ` where `ℕ` is ordered
by divisibility.  -/
Nat.pow_dvd_iff_dvd_floorRoot : ∀ {a b n : ℕ}, a ^ n ∣ b ↔ a ∣ n.floorRoot b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
ContinuousWithinAt.arcsin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => Real.arcsin (f x)) s x
-- Mathlib.Algebra.Group.Graph
MonoidHom.graph.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (f : G →* H),
  f.graph = { toSubmonoid := f.mgraph, inv_mem' := ⋯ }
-- Mathlib.Order.Filter.Prod
Filter.bot_prod : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β}, ⊥ ×ˢ g = ⊥
-- Aesop.Builder.Cases
Aesop.RuleBuilderOptions.casesIndexTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceSingleton : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.ι_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (F : CategoryTheory.MonoidalCategory.DayFunctor C V),
  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V
          (CategoryTheory.MonoidalCategory.DayFunctor C V)).obj
      F =
    F.functor
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_9 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr) (k : ℕ)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.pow k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_9 a k
-- Mathlib.Data.List.MinMax
List.argmin.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] (f : α → β) (l : List α),
  List.argmin f l = List.foldl (List.argAux fun b c => f b < f c) none l
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.instFinCategoryOfFintypeOfIsThin : {J : Type u} → [Fintype J] → [inst : CategoryTheory.SmallCategory J] → [Quiver.IsThin J] → CategoryTheory.FinCategory J
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv
      (CategoryTheory.Limits.pullback.snd f g) =
    (CategoryTheory.Limits.pushout.inr f.op g.op).unop
-- Mathlib.Analysis.Calculus.Taylor
/-- A corollary of Taylor's theorem with the Lagrange form of the remainder.  -/
taylor_mean_remainder_lagrange_iteratedDeriv : ∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
  x₀ ≠ x →
    ContDiffOn ℝ (↑n + 1) f (Set.uIcc x₀ x) →
      ∃ x' ∈ Set.uIoo x₀ x,
        f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
          iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial