mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depthUB_le_two_depthLB : ∀ (c : RBTree.RBColor) (n : ℕ), RBTree.RBNode.depthUB c n ≤ 2 * RBTree.RBNode.depthLB c n
-- Mathlib.Algebra.Category.ModuleCat.Ext.Basic
/-- If `r • N = 0`, then `r • 𝟙 M` induces the zero endomorphism on `Ext M N n`.  -/
CategoryTheory.Abelian.Ext.postcomp_smul_id_eq_zero_of_mem_annihilator : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] {M N : ModuleCat R} {r : R},
  r ∈ Module.annihilator R ↑N →
    ∀ (n : ℕ),
      AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ (r • CategoryTheory.CategoryStruct.id M)).postcomp N ⋯) = 0
-- Mathlib.FieldTheory.AbelRuffini
/-- The intermediate field of elements solvable by radicals, defined as the smallest subfield which
is closed under `n`-th roots.  -/
solvableByRad : (F : Type u_1) → (E : Type u_2) → [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E
-- Mathlib.Algebra.Order.Star.Basic
StarOrderedRing.nonneg_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The complement sequence `Wᶜ : ℤ × ℕ → R` for a normalised EDS `W : ℤ → R` that witnesses
`W(k) ∣ W(n * k)`. In other words, `W(k) * Wᶜ(k, n) = W(n * k)` for all `k, n ∈ ℤ`.

This is defined in terms of `normEDS` and agrees with `complEDS₂` when `n = 2`.  -/
complEDS' : {R : Type u_1} → [CommRing R] → R → R → R → ℤ → ℕ → R
-- Mathlib.Analysis.Calculus.DSlope
continuousWithinAt_dslope_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜},
  b ≠ a → (ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b)
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.exists_not_orthogonal_self : ∀ {F : Type u_1} [inst : Field F] {m : Type u_2} [inst_1 : Fintype m] (v : Projectivization F (m → F)),
  ∃ w, ¬w.orthogonal v
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The `grw` discrimination tree root.  -/
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.grw : Mathlib.Tactic.ClickSuggestions.PreDiscrTrees →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.symm_image_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → ↑e.symm '' (e.target ∩ t) = e.source ∩ s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
CovariantClass.mk : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Covariant M N μ r → CovariantClass M N μ r
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedInverseImage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {D : Type u_2} [inst_6 : CategoryTheory.Category.{v_2, u_2} D] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : CategoryTheory.Limits.HasZeroObject D] [inst_9 : CategoryTheory.HasShift D ℤ]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [inst_12 : F.CommShift ℤ] [F.IsTriangulated]
  [P.IsClosedUnderIsomorphisms] [P.IsTriangulated], (P.inverseImage F).IsTriangulated
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_diff_eq_size_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.primitive_mul_isPrimitive : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ}
  (ψ : DirichletCharacter R m), (χ.primitive_mul ψ).IsPrimitive
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseZero : Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.stronglyAdapted_martingalePart : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ f → MeasureTheory.StronglyAdapted ℱ (MeasureTheory.martingalePart f ℱ μ)
-- Init.Data.SInt.Bitwise
Int16.zero_or : ∀ {a : Int16}, 0 ||| a = a
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_mono : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] {s t : Set σ},
  s ⊆ t → MvPolynomial.supported R s ≤ MvPolynomial.supported R t
-- Mathlib.Algebra.BigOperators.Finprod
map_finsetProd : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {α : Type u_7} {F : Type u_8}
  [inst_2 : Fintype α] [inst_3 : EquivLike F M N] [MulEquivClass F M N] (f : F) (g : α → M), f (∏ i, g i) = ∏ i, f (g i)
-- Init.Data.BitVec.Lemmas
BitVec.neg_neg : ∀ {w : ℕ} {x : BitVec w}, - -x = x
-- Mathlib.Algebra.Module.Torsion.Prod
Prod.moduleIsTorsionFree : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.IsTorsionFree R M] [Module.IsTorsionFree R N],
  Module.IsTorsionFree R (M × N)
-- Mathlib.Data.Seq.Computation
/-- Recursor based on membership  -/
Computation.memRecOn : {α : Type u} →
  {C : Computation α → Sort v} →
    {a : α} → {s : Computation α} → a ∈ s → C (Computation.pure a) → ((s : Computation α) → C s → C s.think) → C s
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, min c d ≤ b → Set.Iio b ∪ Set.Ico c d = Set.Iio (max b d)
-- Mathlib.Tactic.NormNum.Result
Int.rawCast.eq_1 : ∀ {α : Type u} [inst : Ring α] (n : ℤ), n.rawCast = ↑n
-- Mathlib.Data.List.Intervals
List.Ico.eq_nil_of_le : ∀ {n m : ℕ}, m ≤ n → List.Ico n m = []
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.unop_id : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : Cᵒᵖ},
  (CategoryTheory.CategoryStruct.id X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop X)
-- Init.Data.Ord.Basic
List.isLE_compare_nil_left : ∀ {α : Type u_1} [inst : Ord α] {xs : List α}, (compare [] xs).isLE = true
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_C_ite : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (a : R),
  (LaurentPolynomial.C a).degree = if a = 0 then ⊥ else 0
-- Mathlib.RingTheory.Coprime.Basic
/-- `IsCoprime` is not a useful definition for `PNat`; consider using `Nat.Coprime` instead.  -/
PNat.isCoprime_iff : ∀ {m n : ℕ+}, IsCoprime ↑m ↑n ↔ m = 1 ∨ n = 1
-- Mathlib.Analysis.Convex.Strong
StrongConcaveOn.strictConcaveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m : ℝ},
  StrongConcaveOn s m f → 0 < m → StrictConcaveOn ℝ s f
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType.Changed.sizeOf_spec : sizeOf Lean.Lsp.FileChangeType.Changed = 1
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_injective_of_injective : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'},
  Function.Injective ⇑f → Function.Injective (LieSubmodule.map f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insertIfNew!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey ⋯ = k
-- Batteries.Data.AssocList
/-- `O(n)`. Run monadic function `f` on all elements in the list, from head to tail.  -/
Batteries.AssocList.forM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} → [Monad m] → (α → β → m PUnit.{u_1 + 1}) → Batteries.AssocList α β → m PUnit.{u_1 + 1}
-- Mathlib.Algebra.Order.Module.Defs
/-- Binary **rearrangement inequality**.  -/
smul_add_smul_le_smul_add_smul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_7 : Module α β]
  [PosSMulMono α β] {a₁ a₂ : α} {b₁ b₂ : β}, a₂ ≤ a₁ → b₂ ≤ b₁ → a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeries.match_1.splitter : (motive : ℕ → Sort u_1) →
  (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((x : ℕ) → (x = 0 → False) → (x = 1 → False) → motive x) → motive x
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute : Type → Type
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.instNontrivialColoringOfNonempty : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Nonempty (G.Coloring α)] [Nontrivial α] [Nonempty V],
  Nontrivial (G.Coloring α)
-- Std.Internal.Do.WP.Basic
_private.Std.Internal.Do.WP.Basic.0.EStateM.bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s : σ) → motive (EStateM.Result.ok a s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- A real normed vector space is strictly convex provided that the unit ball is strictly convex.  -/
StrictConvexSpace.of_strictConvex_unitClosedBall : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [LinearMap.CompatibleSMul E E 𝕜 ℝ],
  StrictConvex 𝕜 (Metric.closedBall 0 1) → StrictConvexSpace 𝕜 E
-- Mathlib.RingTheory.AlgebraTower
/-- Suppose that `R → S → A` is a tower of algebras.
If an element `r : R` is invertible in `S`, then it is invertible in `A`.  -/
IsScalarTower.Invertible.algebraTower : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra S A] →
                [inst_5 : Algebra R A] →
                  [IsScalarTower R S A] → (r : R) → [Invertible ((algebraMap R S) r)] → Invertible ((algebraMap R A) r)
-- Mathlib.Analysis.Convex.Extreme
/-- A useful restatement using `segment`: `x` is an extreme point iff the only (closed) segments
that contain it are those with `x` as one of their endpoints.  -/
mem_extremePoints_iff_forall_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] {A : Set E} {x : E},
  x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart.mk.inj : ∀ {value : String} {tooltip? : Option String} {location? : Option Lean.Elab.InlayHintLinkLocation} {value_1 : String}
  {tooltip?_1 : Option String} {location?_1 : Option Lean.Elab.InlayHintLinkLocation},
  { value := value, tooltip? := tooltip?, location? := location? } =
      { value := value_1, tooltip? := tooltip?_1, location? := location?_1 } →
    value = value_1 ∧ tooltip? = tooltip?_1 ∧ location? = location?_1
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- In a linearly ordered monoid, we are happy for `bot_eq_zero` to be a `@[simp]` lemma  -/
bot_eq_zero' : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : OrderBot α], ⊥ = 0
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLeast? : Std.PRange.Least? UInt8
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ofHom_id : ∀ {X : Type u} [inst : AddCommGroup X],
  AddCommGrpCat.ofHom (AddMonoidHom.id X) = CategoryTheory.CategoryStruct.id (AddCommGrpCat.of X)
-- Batteries.Data.HashMap.Basic
/-- Given a key `a`, returns a key-value pair in the map whose key compares equal to `a`.
Note that the returned key may not be identical to the input, if `==` ignores some part
of the value.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findEntry? "one" = some ("one", 1)
hashMap.findEntry? "three" = none
```
 -/
Std.HashMap.findEntry? : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → α → Option (α × β)
-- Init.Data.SInt.Lemmas
ISize.eq_iff_ofBitVec_eq : ∀ {a b : BitVec System.Platform.numBits}, a = b ↔ ISize.ofBitVec a = ISize.ofBitVec b
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.mulValuation_toFun : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]), Padic.mulValuation x = if x = 0 then 0 else WithZero.exp (-x.valuation)
-- Mathlib.Order.Filter.Map
Filter.eventually_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {P : β → Prop},
  (∀ᶠ (b : β) in Filter.map m f, P b) ↔ ∀ᶠ (a : α) in f, P (m a)
-- Mathlib.Topology.Instances.RatLemmas
Rat.dense_compl_compact : ∀ {s : Set ℚ}, IsCompact s → Dense sᶜ
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constMonoidHom_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : MulOneClass β] (a : β) (a_1 : α),
  (Pi.constMonoidHom α β) a a_1 = Function.const α a a_1
-- Mathlib.Order.Bounds.Basic
bddAbove_def : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove s ↔ ∃ x, ∀ y ∈ s, y ≤ x
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainTopCoeff_le_chainLength : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  LieModule.chainTopCoeff (⇑α) β ≤ LieAlgebra.IsKilling.chainLength α β
-- Mathlib.Data.Prod.Lex
Prod.Lex.toLex_le_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LE β] {x y : α × β},
  toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedReturnCont : Inhabited Lean.Elab.Do.ReturnCont
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.toList_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.toList = t₂.toList
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (curr : ℕ)
  (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f]
  (idx : ℕ) (hidx : idx < curr),
  (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Rco α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Rco α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_bijective : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}, Function.Bijective ModuleCat.Hom.hom
-- Lean.Meta.Tactic.Grind.EMatch
/-- Given a proposition `prop` corresponding to an equational theorem.
Annotate the conditions using `Grind.MatchCond`. See `MatchCond.lean`.

Only hypotheses that have the `match`-condition shape `∀ …, _ = _ → … → False` are
annotated (see `isMatchCondCandidate`). Equational theorems may have other propositional
hypotheses (e.g., the discriminant equalities of a `match` with proof discriminants),
and the `MatchCond` propagators assume the annotated conditions have this shape.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.annotateEqnTypeConds : Lean.Expr → optParam (Lean.Expr → Lean.Meta.Grind.EMatch.M Lean.Expr) pure → Lean.Meta.Grind.EMatch.M Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
CategoryTheory.frobeniusMorphism_mate : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  (h : L ⊣ F) (A : C),
  (CategoryTheory.conjugateEquiv (h.comp (CategoryTheory.ihom.adjunction A))
        ((CategoryTheory.ihom.adjunction (F.obj A)).comp h))
      (CategoryTheory.frobeniusMorphism F h A).natTrans =
    (CategoryTheory.expComparison F A).natTrans
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Smoothness of a `C^n` section on `s` can be determined
using any trivialisation whose `baseSet` contains `s`.  -/
Bundle.Trivialization.contMDiffOn_section_iff : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} {a : Set B} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [MemTrivializationAtlas e],
  IsOpen a →
    a ⊆ e.baseSet →
      (ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) a ↔
        ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n (fun x => (↑e ⟨x, s x⟩).2) a)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- If `f = g`, then cobase change along `f` is naturally isomorphic to cobase change along `g`.  -/
CategoryTheory.MorphismProperty.Under.pushoutCongr : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          {f : X ⟶ Y} →
            [inst_2 : P.HasPushoutsAlong f] →
              [inst_3 : P.IsStableUnderCobaseChangeAlong f] →
                [inst_4 : Q.IsStableUnderCobaseChange] →
                  {g : X ⟶ Y} →
                    (h : f = g) →
                      CategoryTheory.MorphismProperty.Under.pushout P Q f ≅
                        CategoryTheory.MorphismProperty.Under.pushout P Q g
-- Mathlib.RingTheory.Noetherian.Orzech
/-- **Orzech's theorem** for Noetherian modules: if `R` is a ring (not necessarily commutative),
`M` and `N` are `R`-modules, `M` is Noetherian, `i : N →ₗ[R] M` is injective,
`f : N →ₗ[R] M` is surjective, then `f` is also injective. The proof here is adapted from
Djoković's paper *Epimorphisms of modules which must be isomorphisms* [djokovic1973],
utilizing `LinearMap.iterateMapComap`.
See also Orzech's original paper: *Onto endomorphisms are isomorphisms* [orzech1971].  -/
IsNoetherian.injective_of_surjective_of_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsNoetherian R M] (i f : N →ₗ[R] M),
  Function.Injective ⇑i → Function.Surjective ⇑f → Function.Injective ⇑f
-- Init.Data.UInt.Bitwise
UInt32.toUInt16_shiftLeft : ∀ (a b : UInt32), b < 16 → (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
_private.Mathlib.LinearAlgebra.QuadraticForm.Radical.0.QuadraticMap.lift_aux : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} {N : Submodule R M},
  N ≤ Q.radical → ∀ (m m' : M), N.quotientRel m m' → Q m = Q m'
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.infty_notMem_image_coe : ∀ {X : Type u_1} {s : Set X}, OnePoint.infty ∉ OnePoint.some '' s
-- Mathlib.Analysis.Calculus.VectorField
Filter.EventuallyEq.lieBracketWithin_vectorField_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
  V₁ =ᶠ[nhdsWithin x s] V →
    V₁ x = V x →
      W₁ =ᶠ[nhdsWithin x s] W →
        W₁ x = W x → VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods : Type
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasFDerivAt_list_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] [Finite ι] {l : List ι} {x : ι → 𝔸'},
  HasFDerivAt (fun x => (List.map x l).prod)
    (∑ i,
      (List.map x (List.take (↑i) l)).prod •
        MulOpposite.op (List.map x (List.drop (↑i).succ l)).prod • ContinuousLinearMap.proj l[i])
    x
-- Mathlib.Data.List.NatAntidiagonal
List.Nat.antidiagonal_succ : ∀ {n : ℕ}, List.Nat.antidiagonal (n + 1) = (0, n + 1) :: List.map (Prod.map Nat.succ id) (List.Nat.antidiagonal n)
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_lt_d4 : Real.pi < 3.1416
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.unmopFunctor_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.unmopFunctor C) X Y = (β_ X.unmop Y.unmop).hom
-- Mathlib.Data.NNReal.Basic
NNReal.bddAbove_range_natCast_iff : ∀ {ι : Sort u_3} (f : ι → ℕ), BddAbove (Set.range fun x => ↑(f x)) ↔ BddAbove (Set.range f)
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- *Dirichlet's approximation theorem:*
For any real number `ξ` and positive natural `n`, there is a fraction `q`
such that `q.den ≤ n` and `|ξ - q| ≤ 1/((n+1)*q.den)`.

See also `AddCircle.exists_norm_nsmul_le`.  -/
Real.exists_rat_abs_sub_le_and_den_le : ∀ (ξ : ℝ) {n : ℕ}, 0 < n → ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'_add : ∀ {α : Type u_1} (P Q : RegularExpression α), (P + Q).matches' = P.matches' + Q.matches'
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsShortComplex_shortExact : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{w, u, v} k G) (S : Subgroup G)
  [inst_2 : S.Normal], (A.coinvariantsShortComplex S).ShortExact
-- Mathlib.Analysis.Normed.Group.Basic
normGroupSeminorm.eq_1 : ∀ (E : Type u_5) [inst : SeminormedGroup E],
  normGroupSeminorm E = { toFun := norm, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop : ∀ {w : ℕ} (x : BitVec w), x.cpop.toNat = x.cpopNatRec w 0
-- Mathlib.Data.Finset.Lattice.Basic
Finset.sup_eq_union' : ∀ {α : Type u_1} [inst : DecidableEq α], max = Union.union