mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.Closeds.lipschitz_sup`. -/
EMetric.Closeds.lipschitz_sup : ∀ {α : Type u_1} [inst : EMetricSpace α], LipschitzWith 1 fun p => p.1 ⊔ p.2
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanServerCapabilities.mk.inj : ∀ {moduleHierarchyProvider? : Option Lean.Lsp.ModuleHierarchyOptions} {rpcProvider? : Option Lean.Lsp.RpcOptions}
  {moduleHierarchyProvider?_1 : Option Lean.Lsp.ModuleHierarchyOptions} {rpcProvider?_1 : Option Lean.Lsp.RpcOptions},
  { moduleHierarchyProvider? := moduleHierarchyProvider?, rpcProvider? := rpcProvider? } =
      { moduleHierarchyProvider? := moduleHierarchyProvider?_1, rpcProvider? := rpcProvider?_1 } →
    moduleHierarchyProvider? = moduleHierarchyProvider?_1 ∧ rpcProvider? = rpcProvider?_1
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSectionsOn.comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} {γ : Type u_4}
  [inst_1 : TopologicalSpace γ] {g : γ → α} {t : Set γ},
  HasOpenLowerSectionsOn f s → ContinuousOn g t → Set.MapsTo g t s → HasOpenLowerSectionsOn (f ∘ g) t
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.saveAltVarsInfo : Lean.MVarId → Lean.Syntax → Array Lean.FVarId → Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.instIsProperOfNonsingular : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [X.Nonsingular], h.IsProper
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_zero : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B : TopRep k G),
  TopRep.Hom.hom 0 = 0
-- Mathlib.Topology.Semicontinuity.Defs
/-- A relation `r : α → β → Prop` is semicontinuous on `s` if it is semicontinuous within `s` at
each `x ∈ s`.  -/
SemicontinuousOn : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → (α → β → Prop) → Set α → Prop
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_uniformContinuous_ofLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : UniformSpace α] [inst_1 : UniformSpace β],
  UniformContinuous WithLp.ofLp
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrRightₐ_symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [inst_1 : CommSemiring R]
  [inst_2 : Semiring Y] [inst_3 : Algebra R Y] [inst_4 : Semiring Z] [inst_5 : Algebra R Z] (e : Y ≃ₐ[R] Z)
  (g : LocallyConstant X Z) (a : X), ((LocallyConstant.congrRightₐ R e).symm g) a = e.symm (g a)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterMapWithPostcondition.eq_1 : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {m : Type w → Type w'} [inst_1 : Monad m]
  (f : β → Std.Iterators.PostconditionT m (Option γ)) (it : Std.Iter β),
  Std.Iter.filterMapWithPostcondition f it = Std.IterM.filterMapWithPostcondition f it.toIterM
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₂.injEq : ∀ (a : List ℕ) (a_1 : Turing.ToPartrec.Cont) (a_2 : List ℕ) (a_3 : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.cons₂ a a_1 = Turing.ToPartrec.Cont.cons₂ a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_indep_iff_of_disjoint : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis I X → Disjoint X J → ((M.contract X).Indep J ↔ M.Indep (J ∪ I))
-- Mathlib.Order.Filter.Prod
Filter.prod_bot : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α}, f ×ˢ ⊥ = ⊥
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, (Std.TreeMap.Raw.map f t).size = t.size
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.instIsLocalizationIdIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.Functor.id C).IsLocalization (CategoryTheory.MorphismProperty.isomorphisms C)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite products, then `F.unop : C ⥤ D` preserves finite
coproducts.  -/
CategoryTheory.Limits.preservesFiniteCoproducts_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteProducts F],
  CategoryTheory.Limits.PreservesFiniteCoproducts F.unop
-- Mathlib.Tactic.GRewrite.Elab
/-- `grewrite [e₁, ..., eₙ]` uses each expression `eᵢ : Rᵢ aᵢ bᵢ` (where `Rᵢ` is any two-argument
relation) as a generalized rewrite rule on the main goal, replacing occurrences of `aᵢ` with `bᵢ`.
Use `grewrite [← eᵢ]` to rewrite in the other direction, replacing occurrences of `bᵢ` with `aᵢ`.

If an expression `e` is a defined constant, then the equational theorems associated with `e` are
used. This provides a convenient way to unfold `e`. If `e` has parameters, the tactic will try to
fill these in by unification with the matching part of the target. Parameters are only filled in
once per rule, restricting which later rewrites can be found. Parameters that are not filled in
after unification will create side goals.

To be able to use `grewrite`, the relevant lemmas need to be tagged with `@[gcongr]`.
To rewrite inside a transitive relation, you can also give it an `IsTrans` instance.

Rewriting with a strict inequality `a < b` may change a constant in the goal,
such as changing `<` to `≤`. If this is not possible, then `a < b` is treated the same as `a ≤ b`.

`grw` is like `grewrite` but tries to close the goal afterwards by "cheap" (reducible) `rfl`.
To rewrite only in the `n`-th position, use `nth_grewrite n`.
`apply_rewrite [e₁, ..., eₙ]` is a shorthand for `grewrite +implicationHyp [e₁, ..., eₙ]`: it
interprets `· → ·` as a relation instead of adding the hypothesis as a side condition.

* `grewrite [← e]` applies the rewrite rule `e : R a b` in the reverse direction, replacing
  occurrences of `b` with `a`.
* `grewrite (config := cfg) [e₁, ..., eₙ]` uses `cfg` as configuration. See `GRewrite.Config` for
  details.
  * To let `grewrite` unfold more aggressively, as in `erw`, use
    `grewrite (transparency := default) [e₁, ..., eₙ]`.
  * `grewrite +implicationHyp [e₁, ..., eₙ]` interprets `· → ·` as a relation (see `apply_rewrite`).
* `grewrite [e₁, ..., eₙ] at l` rewrites at the location(s) `l`.
 -/
Mathlib.Tactic.GRewrite.evalGRewriteSeq : Lean.Elab.Tactic.Tactic
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.below.startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) →
        String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_1 → Prop},
  String.Slice.Pattern.Model.IsValidRevSearchFrom.below ⋯
-- Mathlib.Data.Num.Basic
/-- Subtraction of two `Num`s, producing a `ZNum`.  -/
Num.sub' : Num → Num → ZNum
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getThenInsertIfNew?_fst : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {k : α} {v : β},
  (Std.DHashMap.Const.getThenInsertIfNew? m k v).1 = Std.DHashMap.Const.get? m k
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Model.revPositionsFrom.eq_1 : ∀ {s : String} (p : s.Pos),
  String.Model.revPositionsFrom p =
    if h : p = s.startPos then [] else ⟨p.prev h, ⋯⟩ :: String.Model.revPositionsFrom (p.prev h)
-- Mathlib.RingTheory.HahnSeries.Addition
/-- `addOppositeEquiv` is an additive monoid isomorphism between
Hahn series over `Γ` with coefficients in the opposite additive monoid `Rᵃᵒᵖ`
and the additive opposite of Hahn series over `Γ` with coefficients `R`.
 -/
HahnSeries.addOppositeEquiv : {Γ : Type u_1} →
  {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddMonoid R] → HahnSeries Γ Rᵃᵒᵖ ≃+ (HahnSeries Γ R)ᵃᵒᵖ
-- Init.Data.UInt.Lemmas
UInt16.mod_lt : ∀ (a : UInt16) {b : UInt16}, 0 < b → a % b < b
-- Mathlib.Data.List.Cycle
List.prev_next : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (x : α) (hx : x ∈ l), l.prev (l.next x hx) ⋯ = x
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
/-- **Alias** of the reverse direction of `Subgroup.zpowers_le`. -/
Subgroup.zpowers_le_of_mem : ∀ {G : Type u_1} [inst : Group G] {g : G} {H : Subgroup G}, g ∈ H → Subgroup.zpowers g ≤ H
-- Mathlib.CategoryTheory.Retract
/-- ```
  X -------> Z -------> X
  |          |          |
  f          g          f
  |          |          |
  v          v          v
  Y -------> W -------> Y

```
A morphism `f : X ⟶ Y` is a retract of `g : Z ⟶ W` if there are morphisms `i : f ⟶ g`
and `r : g ⟶ f` in the arrow category such that `i ≫ r = 𝟙 f`.  -/
CategoryTheory.RetractArrow : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y Z W : C} → (X ⟶ Y) → (Z ⟶ W) → Type v
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_inj : ∀ {x y : ℤ}, pentagonal x = pentagonal y ↔ x = y
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_map_natCast : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℕ), (A.map Nat.cast).den = 1
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.instInhabited : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → Inhabited (CategoryTheory.Comonad C)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → (q ∈ s ∧ q ∈ as ↔ q = p)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.eq_iff : ∀ (K : Type u) [inst : CommRing K] [IsReduced K] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP K p]
  (x y : ℕ × K),
  PerfectClosure.mk K p x = PerfectClosure.mk K p y ↔ (⇑(frobenius K p))^[y.1] x.2 = (⇑(frobenius K p))^[x.1] y.2
-- Batteries.Tactic.Instances
/-- `#instances term` prints all the instances for the given class.
For example, `#instances Add _` gives all `Add` instances, and `#instances Add Nat` gives the
`Nat` instance. The `term` can be any type that can appear in `[...]` binders.

Trailing underscores can be omitted, and `#instances Add` and `#instances Add _` are equivalent;
the command adds metavariables until the argument is no longer a function.

The `#instances` command is closely related to `#synth`, but `#synth` does the full
instance synthesis algorithm and `#instances` does the first step of finding potential instances.  -/
Batteries.Tactic.Instances.instancesCmd : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ [Inhabited α] {k fallback : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.RingTheory.Etale.Finite
/-- The object property of étale `R`-algebras.  -/
CommAlgCat.etale : (R : Type u) → [inst : CommRing R] → CategoryTheory.ObjectProperty (CommAlgCat R)
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff.sum : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ι : Type u_2}
  (s : Finset ι) (f : ι → AddCircle T → E),
  (∀ i ∈ s, MeasureTheory.Integrable (f i) AddCircle.haarAddCircle) →
    fourierCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, fourierCoeff (f i)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLift_p2 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s)
      (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) =
    s.snd
-- Mathlib.Data.List.DropRight
List.rdrop_append_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, (l₁ ++ l₂).rdrop l₂.length = l₁
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_ofNat : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)] (n : ℕ) [inst_4 : n.AtLeastTwo],
  (OfNat.ofNat n).toAddMonoidAlgebra = OfNat.ofNat n
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_ite_of_false : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p],
  (∀ x ∈ s, ¬p x) → ∀ (f g : ι → M), (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, g x
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.comap_comap : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)) (U : TopologicalSpace.Opens γ),
  (TopologicalSpace.Opens.comap f) ((TopologicalSpace.Opens.comap g) U) = (TopologicalSpace.Opens.comap (g.comp f)) U
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.inclusion_self : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {E : IntermediateField K L},
  IntermediateField.inclusion ⋯ = AlgHom.id K ↥E
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.comp_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (g : L.Equiv N P) (f : L.Equiv M N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.Topology.Order.OrderClosed
Dense.orderDual : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, Dense s → Dense (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.instNormedAddCommGroup : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] → NormedAddCommGroup (TensorProduct 𝕜 E F)
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
/-- **Alias** of the reverse direction of `associated_abs_left_iff`. -/
Associated.abs_left : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] {x y : R}, Associated x y → Associated |x| y
-- Mathlib.Topology.MetricSpace.Polish
PolishSpace.iInf : ∀ {α : Type u_1} {ι : Type u_3} [Countable ι] {t : ι → TopologicalSpace α},
  (∃ i₀, ∀ (i : ι), t i ≤ t i₀) → (∀ (i : ι), PolishSpace α) → PolishSpace α
-- Lean.EnvExtension
Lean.MapDeclarationExtension.mk.inj : ∀ {α : Type}
  {toPersistentEnvExtension toPersistentEnvExtension_1 :
    Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)},
  { toPersistentEnvExtension := toPersistentEnvExtension } =
      { toPersistentEnvExtension := toPersistentEnvExtension_1 } →
    toPersistentEnvExtension = toPersistentEnvExtension_1
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
continuousAt_gaussian_integral : ∀ (b : ℂ), 0 < b.re → ContinuousAt (fun c => ∫ (x : ℝ), Complex.exp (-c * ↑x ^ 2)) b
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- If `M` is a faithfully flat `R`-module and `N` is `R`-linearly isomorphic to `M`, then
`N` is faithfully flat.  -/
Module.FaithfullyFlat.of_linearEquiv : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_1}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FaithfullyFlat R M] (e : N ≃ₗ[R] M), Module.FaithfullyFlat R N
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_le_of_measure_le_smul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  {c : ENNReal} {μ μ' : MeasureTheory.Measure α},
  μ' ≤ c • μ →
    ∀ {f : α → ε} {p : ENNReal}, MeasureTheory.eLpNorm f p μ' ≤ c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.ε_η : ∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k],
  (Representation.LinearizeMonoidal.ε k G).comp (Representation.LinearizeMonoidal.η k G) =
    Representation.IntertwiningMap.id
      (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforward_uncurry_curry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} {f : I ⟶ J}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X : CategoryTheory.Over I} {A : CategoryTheory.Over J}
  (u : (CategoryTheory.ChosenPullbacksAlong.pullback f).obj A ⟶ X),
  CategoryTheory.ExponentiableMorphism.pushforwardUncurry (CategoryTheory.ExponentiableMorphism.pushforwardCurry u) = u
-- Mathlib.RingTheory.Flat.Basic
LinearMap.baseChangeHom_injective : ∀ (R : Type u) (M : Type v) {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (S : Type u_4) [inst_5 : Semiring S] [inst_6 : Algebra R S]
  [FaithfulSMul R S] [Module.Flat R N], Function.Injective ⇑(LinearMap.baseChangeHom R S M N)
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.monotone_normalizer : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  Monotone LieSubmodule.normalizer
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The morphism `F.obj (A₁ ×_X A₂) ×_{A₁} (A₁ ×_X A₃) ⟶ X`.  -/
CategoryTheory.Functor.relativelyRepresentable.pullback₃.π : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : F.Full] →
            {A₁ A₂ A₃ : C} →
              {X : D} →
                {f₁ : F.obj A₁ ⟶ X} →
                  (hf₁ : F.relativelyRepresentable f₁) →
                    (f₂ : F.obj A₂ ⟶ X) →
                      (f₃ : F.obj A₃ ⟶ X) →
                        [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] →
                          F.obj (hf₁.pullback₃ f₂ f₃) ⟶ X
-- Mathlib.Algebra.Group.Int.Even
/-- `IsSquare` can be decided on `ℤ` by checking against the square root.  -/
Int.instDecidablePredIsSquare : DecidablePred IsSquare
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance1.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z d)
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c)) z d)
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (match RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d with
    | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d => h_1 a x b y c z d
    | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d => h_2 a x b y c z d
    | a, x, b => h_3 a x b) =
    h_1 a x b y c z d
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_insert : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.insert k v p) =
    Int.Internal.Linear.Poly.denote ctx p + k * Int.Internal.Linear.Var.denote ctx v
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `w₁ w₂` are words such that `w₁` reduces to `w₂`, then `w₂` is a sublist of `w₁`.  -/
FreeAddGroup.Red.sublist : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red L₁ L₂ → L₂.Sublist L₁
-- Mathlib.Topology.Order.OrderClosed
instSecondCountableTopologyOrderDual : ∀ {α : Type u} [inst : TopologicalSpace α] [h : SecondCountableTopology α], SecondCountableTopology αᵒᵈ
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg.instSigmaFinite : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SigmaFinite μ], MeasureTheory.SigmaFinite μ.neg
-- Init.Data.SInt.Lemmas
Int8.toInt_div_of_ne_left : ∀ (a b : Int8), a ≠ Int8.minValue → (a / b).toInt = a.toInt.tdiv b.toInt
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_alter_eq_add_one : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {k : α} {f : Option β → Option β},
  m.WF →
    k ∉ m → (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true → (Std.DHashMap.Raw.Const.alter m k f).size = m.size + 1
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be locally uniformly approximated by continuous functions is continuous.  -/
continuous_of_locally_uniform_approx_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : α → β},
  (∀ (x : α), ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) → Continuous f
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.cocycle_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j k : self.J)
  (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) {Z : C}
  (h : CategoryTheory.Limits.pullback (self.f i j hij) (self.f i k ⋯) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk)
      (CategoryTheory.CategoryStruct.comp (self.t' j k i hjk ⋯ ⋯)
        (CategoryTheory.CategoryStruct.comp (self.t' k i j ⋯ ⋯ hij) h)) =
    h
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_mul_replicateCol_apply : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Fintype m] [inst_1 : Mul α] [inst_2 : AddCommMonoid α]
  (v w : m → α) (i j : ι), (Matrix.replicateRow ι v * Matrix.replicateCol ι w) i j = v ⬝ᵥ w
-- Init.Data.Fin.Basic
Fin.val_le_of_ge : ∀ {n : ℕ} {a b : Fin n}, a ≥ b → ↑b ≤ ↑a
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.iterM_equiv_iterM_toList : ∀ {α : Type w} {array : Array α} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m],
  (array.iterM m).Equiv (array.toList.iterM m)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_map : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.FiniteMeasure Ω) (f : Ω → Ω'), ↑(ν.map f) = MeasureTheory.Measure.map f ↑ν
-- Mathlib.Data.Finset.Union
Finset.coe_biUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β],
  ↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_lt_iff_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → (a - b < c ↔ a < c + b)
-- Init.Internal.Order.Basic
Lean.Order.PProd.monotone_fst : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} [inst : Lean.Order.PartialOrder α] [inst_1 : Lean.Order.PartialOrder β]
  [inst_2 : Lean.Order.PartialOrder γ] {f : γ → α ×' β}, Lean.Order.monotone f → Lean.Order.monotone fun x => (f x).fst