mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffAt.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝕜' : Type u_6} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {f : E → 𝕜'} {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → ∀ (c : 𝕜'), ContDiffAt 𝕜 n (fun x => f x / c) x
-- Mathlib.Topology.AlexandrovDiscrete
alexandrovDiscrete_iff_isClosed : ∀ {α : Type u_3} [inst : TopologicalSpace α],
  AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed s) → IsClosed (⋃₀ S)
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- If `G` is a Galois group for `L/K` and the stabilizer of `P` in `G` is a Galois group for
`L/D`, then `D` is a decomposition field for `P`.
 -/
IsDecompositionField.of_isGaloisGroup : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (D : Type u_5) [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (G : Type u_7) [inst_7 : Group G] [Finite G] [inst_9 : MulSemiringAction G L]
  [IsGaloisGroup G K L] [inst_11 : MulSemiringAction G B] [inst_12 : Algebra B L] [IsFractionRing B L]
  [SMulDistribClass Gal(L/K) B L] [SMulDistribClass G B L] [h : IsGaloisGroup (↥(MulAction.stabilizer G P)) D L],
  IsDecompositionField K L P D
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupCohomologyIsoEven.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [h₀ : NeZero i] (hi : Even i),
  Rep.FiniteCyclicGroup.groupCohomologyIsoEven A g hg i hi = Rep.FiniteCyclicGroup.groupCohomologyIsoEven A g hg i hi
-- Mathlib.Algebra.Group.ULift
ULift.addZeroClass : {α : Type u} → [AddZeroClass α] → AddZeroClass (ULift.{u_1, u} α)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.πSummand A) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialObject.Splitting.summand s.N Δ A)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- Vertical composition of oplax transformations.  -/
CategoryTheory.Oplax.OplaxTrans.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Oplax.OplaxTrans F G →
            CategoryTheory.Oplax.OplaxTrans G H → CategoryTheory.Oplax.OplaxTrans F H
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_eq_inv : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), Ring.inverse a = a⁻¹
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a k : α} {v : β k}, (t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.inf_adj : ∀ {V : Type u_2} (x y : Digraph V) (v w : V), (x ⊓ y).Adj v w ↔ x.Adj v w ∧ y.Adj v w
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedProofInstInfo.default : Lean.Meta.Sym.ProofInstInfo
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.α : Lean.Meta.Grind.InjectiveInfo → Lean.Expr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {fallback : α},
  (t.modify k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Order.CompleteLattice.Lemmas
codisjoint_sInf_right : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α},
  Codisjoint b (sInf a) → ∀ {i : α}, i ∈ a → Codisjoint b i
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Theorems.eraseDecl : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.Name → Lean.MetaM (Lean.Meta.Grind.Theorems α)
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq'.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.AC.Expr → Sort u_1) (e : Lean.Grind.AC.Expr)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Expr.var x))
  (h_2 : (a b : Lean.Grind.AC.Expr) → motive (a.op b)) (a b : Lean.Grind.AC.Expr),
  e = a.op b →
    (match e with
      | Lean.Grind.AC.Expr.var x => h_1 x
      | a.op b => h_2 a b) ≍
      h_2 a b
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuous_real_rng : ∀ {E : Type u_6} {ι : Type u_9} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
  {p : ι → Seminorm ℝ E}, WithSeminorms p → ∀ (f : E →ₗ[ℝ] ℝ), (∃ s C, ∀ (x : E), f x ≤ (C • s.sup p) x) → Continuous ⇑f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_le_maxKeyD_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare (t.maxKeyD fallback) ((Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKeyD fallback)).isLE = true
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_mem_upperBounds : ∀ {r : NNReal} {s : Set NNReal}, ↑r ∈ upperBounds (ENNReal.ofNNReal '' s) ↔ r ∈ upperBounds s
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.symm : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, IsRelPrime x y → IsRelPrime y x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} [inst_1 : SizeOf C] (I₀ : Type w) (X : I₀ → C)
  (f : (i : I₀) → X i ⟶ S), sizeOf { I₀ := I₀, X := X, f := f } = 1 + sizeOf I₀
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_toLp_one : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] {f : SchwartzMap E F} {μ : MeasureTheory.Measure E}
  [hμ : μ.HasTemperateGrowth], ‖f.toLp 1 μ‖ = ∫ (x : E), ‖f x‖ ∂μ
-- Init.Data.Range.Polymorphic.Char
Char.instHasSize : Std.Rxc.HasSize Char
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.eval_injective : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_1}
  (b : Module.Basis ι R M), Function.Injective ⇑(Module.Dual.eval R M)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ},
  FiniteMultiplicity a b → (emultiplicity a b = ↑n ↔ multiplicity a b = n)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNeg : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Neg β] → Neg (MeasureTheory.SimpleFunc α β)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂),
  z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h
-- Init.Prelude
/-- Throws an exception of type `ε` to the nearest enclosing handler.
 -/
MonadExcept.throw : {ε : outParam (Type u)} → {m : Type v → Type w} → [self : MonadExcept ε m] → {α : Type v} → ε → m α
-- Mathlib.Analysis.Complex.Exponential
Real.exp_bound' : ∀ {x : ℝ},
  0 ≤ x →
    x ≤ 1 →
      ∀ {n : ℕ},
        0 < n → Real.exp x ≤ ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `X` represents a presheaf of monoids, then `X` is a monoid object.  -/
CategoryTheory.GrpObj.ofRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ GrpCat) →
          (F.comp (CategoryTheory.forget GrpCat)).RepresentableBy X → CategoryTheory.GrpObj X
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_desc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) {P : C} (k : (j : J) → g j ⟶ P),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) (CategoryTheory.Limits.biproduct.desc k) =
    CategoryTheory.Limits.biproduct.desc fun j => CategoryTheory.CategoryStruct.comp (p j) (k j)
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Mathlib.Order.Sublocale
nucleusIsoSublocale.symm_eq_toNucleus : ∀ {X : Type u_1} [inst : Order.Frame X], Sublocale.toNucleus = ⇑nucleusIsoSublocale.symm
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, the images of the components of
the natural transformation `H ⟶ F` under `G` are the components of the composition of counit of the
second adjunction with the unit of the first adjunction.  -/
CategoryTheory.Adjunction.Triple.map_rightToLeft_app_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 : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  (X : C) {Z : C} (h : G.obj (F.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (t.rightToLeft.app X)) h =
    CategoryTheory.CategoryStruct.comp (t.adj₂.counit.app X) (CategoryTheory.CategoryStruct.comp (t.adj₁.unit.app X) h)
-- Mathlib.Order.Filter.Ker
Filter.ker_pure : ∀ {α : Type u_2} (a : α), (pure a).ker = {a}
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.shearAddRight_coe : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  ⇑(Homeomorph.shearAddRight G) = fun z => (z.1, z.1 + z.2)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Generators.fg_ker_of_finitePresentation : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] {α : Type u_1} (P : Algebra.Generators R S α) [Finite α], P.ker.FG
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.H1Cotangent.map.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P'),
  Algebra.Extension.H1Cotangent.map f = (Algebra.Extension.Cotangent.map f).restrict ⋯
-- Mathlib.Data.Nat.Bits
_private.Mathlib.Data.Nat.Bits.0.Nat.boddDiv2.match_1.splitter : (motive : Bool × ℕ → Sort u_1) →
  (x : Bool × ℕ) → ((m : ℕ) → motive (false, m)) → ((m : ℕ) → motive (true, m)) → motive x
-- Mathlib.Tactic.Linarith.Frontend
/-- An extension of `linarith` with some preprocessing to allow it to solve some nonlinear arithmetic
problems. (Based on Coq's `nra` tactic.) See `linarith` for the available syntax of options,
which are inherited by `nlinarith`; that is, `nlinarith!` and `nlinarith only [h1, h2]` all work as
in `linarith`. The preprocessing is as follows:

* For every subterm `a ^ 2` or `a * a` in a hypothesis or the goal,
  the assumption `0 ≤ a ^ 2` or `0 ≤ a * a` is added to the context.
* For every pair of hypotheses `a1 R1 b1`, `a2 R2 b2` in the context, `R1, R2 ∈ {<, ≤, =}`,
  the assumption `0 R' (b1 - a1) * (b2 - a2)` is added to the context (non-recursively),
  where `R ∈ {<, ≤, =}` is the appropriate comparison derived from `R1, R2`.
 -/
Mathlib.Tactic.tacticNlinarith!_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is a monoid object, then `Hom(X, M)` has a monoid structure.  -/
CategoryTheory.Hom.monoid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → {M X : C} → [CategoryTheory.MonObj M] → Monoid (X ⟶ M)
-- Mathlib.Algebra.Notation.Prod
Prod.pow_snd : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : Pow α E] [inst_1 : Pow β E] (p : α × β) (c : E),
  (p ^ c).2 = p.2 ^ c
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_whiskerLeft_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g h : b ⟶ c) (θ : g ⟶ h),
  (CategoryTheory.Bicategory.whiskerLeft f θ).2 = CategoryTheory.Bicategory.whiskerLeft f.2 θ.2
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.hasseDualIso_apply : ∀ {α : Type u_1} [inst : Preorder α] (a : αᵒᵈ), SimpleGraph.hasseDualIso a = OrderDual.ofDual a
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_le_add_of_nonneg : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddZeroClass α] [AddLeftMono α] [AddRightMono α] {a b : α},
  0 ≤ a → 0 ≤ b → max a b ≤ a + b
-- Std.Http.Server.Handler
Std.Http.Server.StatelessHandler.mk.injEq : ∀ (onRequest : Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
  (onFailure : IO.Error → Std.Async.Async Unit) (onContinue : Std.Http.Request.Head → Std.Async.Async Bool)
  (onRequest_1 : Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
  (onFailure_1 : IO.Error → Std.Async.Async Unit) (onContinue_1 : Std.Http.Request.Head → Std.Async.Async Bool),
  ({ onRequest := onRequest, onFailure := onFailure, onContinue := onContinue } =
      { onRequest := onRequest_1, onFailure := onFailure_1, onContinue := onContinue_1 }) =
    (onRequest = onRequest_1 ∧ onFailure = onFailure_1 ∧ onContinue = onContinue_1)
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.ne_zero_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial A],
  minpoly A x ≠ 0 ↔ IsIntegral A x
-- Mathlib.Data.EReal.Operations
EReal.mul_nonneg_iff : ∀ {a b : EReal}, 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.commSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M],
  AddMonoidAlgebra.commSemiring = { toSemiring := AddMonoidAlgebra.semiring, mul_comm := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Notation for a `MulEquiv`.  -/
«term_≃*_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pullback a `MulActionWithZero` structure along an injective zero-preserving homomorphism.  -/
Function.Injective.mulActionWithZero : {M₀ : Type u_2} →
  {A : Type u_7} →
    {A' : Type u_8} →
      [inst : MonoidWithZero M₀] →
        [inst_1 : Zero A] →
          [inst_2 : MulActionWithZero M₀ A] →
            [inst_3 : Zero A'] →
              [inst_4 : SMul M₀ A'] →
                (f : ZeroHom A' A) →
                  Function.Injective ⇑f → (∀ (a : M₀) (b : A'), f (a • b) = a • f b) → MulActionWithZero M₀ A'
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_iff_mul_self_eq_of_pos : ∀ {x y : ℝ}, 0 < y → (√x = y ↔ y * y = x)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.eventually_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (x : X), ∀ᶠ (y : X) in nhds x, f y = f x
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_image_image : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) (s : Set P₁), ⇑e.symm '' ⇑e '' s = s
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- A non-zero power of a parabolic element is parabolic.  -/
Matrix.GeneralLinearGroup.IsParabolic.pow : ∀ {K : Type u_2} [inst : Field K] {g : GL (Fin 2) K},
  g.IsParabolic → ∀ [CharZero K] {n : ℕ}, n ≠ 0 → (g ^ n).IsParabolic
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_unit_of_unit : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (Ψ : CategoryTheory.LocalizerMorphism W₂ W₁) (ε₁ : CategoryTheory.Functor.id C₁ ⟶ Φ.functor.comp Ψ.functor)
  (ε₂ : CategoryTheory.Functor.id C₂ ⟶ Ψ.functor.comp Φ.functor),
  (∀ (X₁ : C₁), W₁ (ε₁.app X₁)) → (∀ (X₂ : C₂), W₂ (ε₂.app X₂)) → Φ.IsLocalizedEquivalence
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMonoid.eq_1 : ∀ {α : Type u} [inst : Semigroup α],
  WithOne.instMonoid =
    { toMul := WithOne.instMulOneClass.toMul, mul_assoc := ⋯, toOne := WithOne.instMulOneClass.toOne, one_mul := ⋯,
      mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }
-- Std.Internal.Do.WP.Lemmas
EStateM.modifyGet.eq_1 : ∀ {ε σ α : Type u} (f : σ → α × σ) (s : σ),
  EStateM.modifyGet f s =
    match f s with
    | (a, s) => EStateM.Result.ok a s
-- Init.Data.Option.Lemmas
Option.isSome_pfilter_iff : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  (o.pfilter p).isSome = true ↔ ∃ a, ∃ (ha : o = some a), p a ha = true
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_powerset_insert : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : Set α → M} {s : Set α} {a : α},
  s.Finite →
    a ∉ s →
      ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
        (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)
-- Mathlib.Geometry.Manifold.Immersion
/-- A choice of complement of the model normed space `E` of `M` in the model normed space
`E'` of `N`  -/
Manifold.IsImmersionAt.complement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} → {x : M} → Manifold.IsImmersionAt I J n f x → Type u
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.atomistic : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → ∀ a ≤ sSup S, ∃ T ⊆ S, a = sSup T
-- Mathlib.Tactic.NormNum.NatFib
/-- Auxiliary definition for `proveFib` extension.  -/
Mathlib.Meta.NormNum.IsFibAux : ℕ → ℕ → ℕ → Prop
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.withBotDegree 0 = ⊥
-- Init.Data.Int.Gcd
Int.gcd_mul_right_right_of_gcd_eq_one : ∀ {n m k : ℤ}, n.gcd m = 1 → n.gcd (m * k) = n.gcd k
-- Mathlib.Tactic.Linter.Style
/-- The "openClassical" linter emits a warning on `open Classical` statements which are not
scoped to a single declaration. A non-scoped `open Classical` can hide that some theorem statements
would be better stated with explicit decidability statements.
 -/
Mathlib.Linter.linter.style.openClassical : Lean.Option Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_union : ∀ {α : Type u_2} [inst : Add α] {s t₁ t₂ : Set α}, s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.pairwiseDisjoint_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] [IsLeftCancelVAdd α β] [inst_2 : DecidableEq β] {s : Set α}
  {t : Finset β}, (s.PairwiseDisjoint fun x => x +ᵥ t) ↔ Set.InjOn (fun p => p.1 +ᵥ p.2) (s ×ˢ ↑t)
-- Init.Data.Array.Lemmas
Array.mem_or_eq_of_mem_push : ∀ {α : Type u_1} {a b : α} {xs : Array α}, a ∈ xs.push b → a ∈ xs ∨ a = b
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
/-- When `A` is commutative, `Subalgebra.mul_toSubmodule_le` is strict.  -/
Subalgebra.mul_toSubmodule : ∀ {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S T : Subalgebra R A), Subalgebra.toSubmodule S * Subalgebra.toSubmodule T = Subalgebra.toSubmodule (S ⊔ T)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.resolve : {α : Type} → Std.CloseableChannel.Consumer✝ α → Option α → BaseIO Bool
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {x x_1 : B} (f : x ⟶ x_1),
  (CategoryTheory.CategoryStruct.id F).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The line derivative is additive, `∂_{v} (x + y) = ∂_{v} x + ∂_{v} y` for all `x y : E`
and `∂_{v + w} x = ∂_{v} x + ∂_{w} y` for all `v w : V`.

Note that `lineDeriv` on functions is not additive.
 -/
LineDerivAdd : (V : Type u) →
  (E : Type v) →
    (F : outParam (Type w)) → [AddCommGroup V] → [AddCommGroup E] → [AddCommGroup F] → [LineDeriv V E F] → Prop
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_ofLe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K'), (LieSubalgebra.ofLe h).toSubmodule = (Submodule.inclusion h).range
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_inverse_obj_π_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (t : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)) (a : J),
  ((CategoryTheory.WithTerminal.coneEquiv.inverse.obj t).π.app a).left = t.π.app (CategoryTheory.WithTerminal.of a)
-- Batteries.Data.List.Lemmas
List.countBefore_eq_count_take : ∀ {α : Type u_1} {xs : List α} {x : α} {i : ℕ} [inst : BEq α], List.countBefore x xs i = List.count x (List.take i xs)