mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CongrExclamation
/-- The transparency level to use when applying a congruence theorem.
By default this is `.reducible`, which prevents unfolding of most definitions.  -/
Congr!.Config.transparency : Congr!.Config → Lean.Meta.TransparencyMode
-- Mathlib.AlgebraicTopology.CechNerve
/-- A helper function used in defining the Čech conerve adjunction.  -/
CategoryTheory.CosimplicialObject.equivalenceLeftToRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
      (F : CategoryTheory.Arrow C) →
        (X : CategoryTheory.CosimplicialObject.Augmented C) →
          (F.augmentedCechConerve ⟶ X) → (F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_sSup_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U : Submodule 𝕜 E} {V : Set (Submodule 𝕜 E)}, U ⟂ sSup V ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ
-- Mathlib.Probability.Kernel.Posterior
/-- The posterior is unique up to a `κ ∘ₘ μ`-null set.  -/
ProbabilityTheory.ae_eq_posterior_of_compProd_eq : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] {η : ProbabilityTheory.Kernel 𝓧 Ω}
  [ProbabilityTheory.IsFiniteKernel η],
  (μ.bind ⇑κ).compProd η = MeasureTheory.Measure.map Prod.swap (μ.compProd κ) →
    ⇑η =ᵐ[μ.bind ⇑κ] ⇑(ProbabilityTheory.posterior κ μ)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.IsBimonHom.toIsMonHom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {M N : C} {inst_3 : CategoryTheory.BimonObj M}
  {inst_4 : CategoryTheory.BimonObj N} {f : M ⟶ N} [self : CategoryTheory.IsBimonHom f], CategoryTheory.IsMonHom f
-- Mathlib.Data.Set.Card
Nat.card_coe_set_eq : ∀ {α : Type u_1} (s : Set α), Nat.card ↑s = s.ncard
-- Mathlib.Order.Monotone.Monovary
Monovary.comp_right : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
  {g : ι → β}, Monovary f g → ∀ (k : ι' → ι), Monovary (f ∘ k) (g ∘ k)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.unbox.sizeOf_spec : ∀ (x : Lean.IR.VarId), sizeOf (Lean.IR.Expr.unbox x) = 1 + sizeOf x
-- Mathlib.Order.Heyting.Basic
sdiff_eq_sdiff_iff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = b \ a ↔ a = b
-- Init.Data.UInt.Lemmas
UInt32.ofNat_mul : ∀ (a b : ℕ), UInt32.ofNat (a * b) = UInt32.ofNat a * UInt32.ofNat b
-- Mathlib.LinearAlgebra.SesquilinearForm.Star
LinearMap.isSymm_iff_isHermitian_toMatrix : ∀ {R : Type u_1} {M : Type u_2} {n : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Fintype n] [inst_5 : DecidableEq n] {B : M →ₗ⋆[R] M →ₗ[R] R} (b : Module.Basis n R M),
  B.IsSymm ↔ ((LinearMap.toMatrix₂ b b) B).IsHermitian
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the second quadrant. Let `f g : ℂ → E` be functions such that

* `f` and `g` are differentiable in the open second quadrant and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open second
  quadrant for some `A`, `B`, and `c < 2`;
* `f` is equal to `g` on the boundary of the second quadrant.

Then `f` is equal to `g` on the closed second quadrant.  -/
PhragmenLindelof.eqOn_quadrant_II : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
  DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Ioi 0) →
        (∃ c < 2,
            ∃ B,
              g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
          (∀ x ≤ 0, f ↑x = g ↑x) →
            (∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | z.re ≤ 0 ∧ 0 ≤ z.im}
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq' : Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.smul : {R : Type u} → {ι : Type u_4} → {M : Type u_5} → (ι → M) → ι → R → M → exteriorPower.presentation.Rels R ι M
-- Mathlib.Algebra.Quaternion
Quaternion.re_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (star a).re = a.re
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.compBilinForm_apply_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {R' : Type u_7}
  [inst_3 : CommSemiring R'] [inst_4 : Algebra R' R] [inst_5 : Module R' M] [inst_6 : IsScalarTower R' R M]
  (f : R →ₗ[R'] R') (B : LinearMap.BilinForm R M) (x x_1 : M), ((f.compBilinForm B) x) x_1 = f ((B x) x_1)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.StrongHomClass.toEmbedding_toFun : ∀ {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : FunLike F M N] [inst_3 : EmbeddingLike F M N] [inst_4 : L.StrongHomClass F M N] (a : F) (a_1 : M),
  (FirstOrder.Language.StrongHomClass.toEmbedding a) a_1 = a a_1
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N'),
  AddMonoid.Coprod.map f g =
    AddMonoid.Coprod.clift (AddMonoid.Coprod.mk.comp (FreeAddMonoid.map (Sum.map ⇑f ⇑g))) ⋯ ⋯ ⋯ ⋯
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadMap_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u} [Monad m] [inst : Std.Do.WP m ps]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ExceptT ε m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  (Std.Do.wp (MonadFunctor.monadMap (fun {β} => f) x)).apply Q =
    (Std.Do.wp (f x.run)).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_unique : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Unique ι] (f : ι → M),
  ∑ x, f x = f default
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The composition of lift linear map `lift I f h : M →ₗ[R] N` with the canonical
projection `N →ₗ[R] N ⧸ (I ^ n • ⊤)` is `f n`.
 -/
IsAdicComplete.mkQ_comp_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsAdicComplete I N]
  {f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤} (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m)
  (n : ℕ), (I ^ n • ⊤).mkQ ∘ₗ IsAdicComplete.lift I f ⋯ = f n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.condition : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.coequalizer.π f g) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.coequalizer.π f g)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instGroup : {α : Type u} → Group (FreeGroup α)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.denoteExpr : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.GoalM Lean.Expr
-- Init.Grind.Ordered.Int
Lean.Grind.instOrderedAddInt : Lean.Grind.OrderedAdd ℤ
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which monovary together on `s`, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together on `s`. Stated by permuting the entries of `g`.  -/
MonovaryOn.sum_mul_comp_perm_lt_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s)
-- Init.Prelude
Nat.div_rec_fuel_lemma : ∀ {x y fuel : ℕ}, 0 < y → y ≤ x → x < fuel + 1 → x - y < fuel
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Config.mk.sizeOf_spec : ∀ (maxSteps maxDischargeDepth : ℕ),
  sizeOf { maxSteps := maxSteps, maxDischargeDepth := maxDischargeDepth } =
    1 + sizeOf maxSteps + sizeOf maxDischargeDepth
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_naturality_app : ∀ {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]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F H G : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (ℌ :
    CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H)
  {G' H' : CategoryTheory.Functor C V} [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G'] (η : G ⟶ G')
  (ℌ' :
    CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G') H'),
  CategoryTheory.CategoryStruct.comp η ℌ'.coev_app =
    CategoryTheory.CategoryStruct.comp ℌ.coev_app
      (ℌ.map (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) η) ℌ')
-- Mathlib.Computability.Language
/-- Symbols for use by all kinds of grammars.  -/
Symbol : Type u_4 → Type u_5 → Type (max u_4 u_5)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mkPostcomp_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y''),
  CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.comp g g') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mkPostcomp f g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.StructuredArrow.mkPostcomp (CategoryTheory.CategoryStruct.comp f (T.map g)) g')
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.GroupTheory.Nilpotent
/-- The lower central series of a group is a descending central series.  -/
Subgroup.lowerCentralSeries_isDescendingCentralSeries : ∀ {G : Type u_1} [inst : Group G], Subgroup.IsDescendingCentralSeries ⊤.lowerCentralSeries
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.inverseCompIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E}
  {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D),
  i.inverseCompIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instPartialOrder : {G : Type u_1} → [inst : AddGroup G] → PartialOrder (FiniteIndexNormalAddSubgroup G)
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atBot.eq_1 : ∀ {α : Type u_3} [inst : Preorder α], Filter.atBot = ⨅ a, Filter.principal (Set.Iic a)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceL_eq_balanceL! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size},
  Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceL! k v l r
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.mk.inj : ∀ {R : Type u} {a₁ a₂ a₃ a₄ a₆ a₁_1 a₂_1 a₃_1 a₄_1 a₆_1 : R},
  { a₁ := a₁, a₂ := a₂, a₃ := a₃, a₄ := a₄, a₆ := a₆ } =
      { a₁ := a₁_1, a₂ := a₂_1, a₃ := a₃_1, a₄ := a₄_1, a₆ := a₆_1 } →
    a₁ = a₁_1 ∧ a₂ = a₂_1 ∧ a₃ = a₃_1 ∧ a₄ = a₄_1 ∧ a₆ = a₆_1
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.coe_primesOverFinset`. -/
coe_primesOverFinset : ∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A},
  p ≠ ⊥ →
    ∀ [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B] [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B]
      [IsDomain A] [Module.IsTorsionFree A B], ↑(IsDedekindDomain.primesOverFinset p B) = p.primesOver B
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop},
  μ.InnerRegularWRT p q → ∀ (c : ENNReal), (c • μ).InnerRegularWRT p q
-- Mathlib.NumberTheory.Harmonic.Bounds
log_le_harmonic_floor : ∀ (y : ℝ), 0 ≤ y → Real.log y ≤ ↑(harmonic ⌊y⌋₊)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.mem_brange_self : ∀ {α : Type u_1} {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → α) (i : Ordinal.{u_3}) (hi : i < o),
  f i hi ∈ o.brange f
-- Mathlib.Algebra.Star.Free
FreeMonoid.instStarMul : {α : Type u_1} → StarMul (FreeMonoid α)
-- Mathlib.Data.Multiset.Bind
Multiset.product_zero : ∀ {α : Type u_1} {β : Type v} (s : Multiset α), s ×ˢ 0 = 0
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mk.inj : ∀ {G : Type u_3} {inst : Group G} {toSubmonoid : Submonoid G}
  {inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier} {toSubmonoid_1 : Submonoid G}
  {inv_mem'_1 : ∀ {x : G}, x ∈ toSubmonoid_1.carrier → x⁻¹ ∈ toSubmonoid_1.carrier},
  { toSubmonoid := toSubmonoid, inv_mem' := inv_mem' } = { toSubmonoid := toSubmonoid_1, inv_mem' := inv_mem'_1 } →
    toSubmonoid = toSubmonoid_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.insert k).max? = some (t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Init.Data.Nat.Lcm
Nat.lcm_mul_right_left : ∀ (m n : ℕ), (n * m).lcm n = n * m
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence : ∀ {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) [F.IsEquivalence],
  F.EffectivelyEnough
-- Mathlib.Data.Complex.Basic
Complex.re_nsmul : ∀ (n : ℕ) (z : ℂ), (n • z).re = n • z.re
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_union : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s t : Set A),
  Algebra.adjoin R (s ∪ t) = Algebra.adjoin R s ⊔ Algebra.adjoin R t
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.FG.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] (p : SubMulAction R M),
  p.FG = ∃ s, s.Finite ∧ p = SubMulAction.closure R s
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.alreadyVisited : {α : Type u_1} → α → Lean.Meta.Grind.Arith.CollectDecVarsM Bool
-- Mathlib.Data.WSeq.Defs
Stream'.WSeq.toList_terminates : ∀ {α : Type u} (s : Stream'.WSeq α) [h : s.IsFinite], s.toList.Terminates
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tsum_pi_single : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : DecidableEq β] (b : β)
  (a : α), ∑' (b' : β), Pi.single b a b' = a
-- Mathlib.RingTheory.WittVector.Frobenius
/-- An auxiliary polynomial over the integers, that satisfies
`p * (frobeniusPolyAux p n) + X n ^ p = frobeniusPoly p n`.
This makes it easy to show that `frobeniusPoly p n` is congruent to `X n ^ p`
modulo `p`.  -/
WittVector.frobeniusPolyAux : ℕ → ℕ → MvPolynomial ℕ ℤ
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.zeroAdd : FirstOrder.Field.FieldAxiom
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α ≃o β} {s : LowerSet α} {b : β},
  b ∈ (LowerSet.map f) s ↔ f.symm b ∈ s
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.mk.injEq : ∀ (imports : Array Lean.Import) (pos : String.Pos.Raw) (badModifier : Bool) (error? : Option String)
  (isModule isMeta isExported importAll : Bool) (imports_1 : Array Lean.Import) (pos_1 : String.Pos.Raw)
  (badModifier_1 : Bool) (error?_1 : Option String) (isModule_1 isMeta_1 isExported_1 importAll_1 : Bool),
  ({ imports := imports, pos := pos, badModifier := badModifier, error? := error?, isModule := isModule,
        isMeta := isMeta, isExported := isExported, importAll := importAll } =
      { imports := imports_1, pos := pos_1, badModifier := badModifier_1, error? := error?_1, isModule := isModule_1,
        isMeta := isMeta_1, isExported := isExported_1, importAll := importAll_1 }) =
    (imports = imports_1 ∧
      pos = pos_1 ∧
        badModifier = badModifier_1 ∧
          error? = error?_1 ∧
            isModule = isModule_1 ∧ isMeta = isMeta_1 ∧ isExported = isExported_1 ∧ importAll = importAll_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.mem_of_mem_roi : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : LT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {a b : α}, r.lower ≤ b → a ∈ b<...* → a ∈ r
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.functoriality_obj_π : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) (j : J),
  ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).π j = G.map (A.π j)
-- Init.Data.List.Sublist
List.reverse_sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse.Sublist l₂.reverse ↔ l₁.Sublist l₂
-- Mathlib.Topology.Perfect
/-- A topological space `X` is said to be perfect if its universe is a perfect set.
Equivalently, this means that `𝓝[≠] x ≠ ⊥` for every point `x : X`.
 -/
PerfectSpace : (α : Type u_1) → [TopologicalSpace α] → Prop
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type Dₙ.

The corresponding Coxeter-Dynkin diagram is:
```
    o
     \
      o --- o ⬝ ⬝ ⬝ ⬝ o --- o
     /
    o
```
 -/
CoxeterMatrix.D : (n : ℕ) → CoxeterMatrix (Fin n)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_mul : ∀ {x : ℝ}, 0 ≤ x → ∀ (y z : ℝ), x ^ (y * z) = (x ^ y) ^ z
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
SubalgebraClass.toAlgebra : {S : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : SetLike S A] →
              [inst_4 : SubsemiringClass S A] → [hSR : SMulMemClass S R A] → (s : S) → Algebra R ↥s
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.

We give here a version of this statement within a set at a point.  -/
ContMDiffWithinAt.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {n : WithTop ℕ∞} {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M} {x : M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  ContMDiffWithinAt IM (IB.prod ⋯) n (fun m => ⋯) s x →
    ContMDiffWithinAt IM ⋯ n (fun m => ⟨b m, v m⟩) s x → ContMDiffWithinAt IM ⋯ n ⋯ s x
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear maps on the right preserves `C^n` functions on domains.  -/
ContDiffOn.comp_continuousLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f s → ∀ (g : G →L[𝕜] E), ContDiffOn 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.freeAddGroupCongr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β),
  FreeAddGroup.freeAddGroupCongr e =
    { toFun := ⇑(FreeAddGroup.map ⇑e), invFun := ⇑(FreeAddGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.RingTheory.Unramified.LocalStructure
Algebra.IsUnramifiedAt.instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S], Algebra.QuasiFinite R S
-- Mathlib.Topology.NhdsWithin
Pi.instNeBotNhdsWithinIoi : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] [Nonempty ι]
  [inst_2 : (i : ι) → Preorder (X i)] {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (Set.Ioi (x i))).NeBot],
  (nhdsWithin x (Set.Ioi x)).NeBot
-- Mathlib.Topology.UniformSpace.Closeds
prod_mem_hausdorffEntourage_entourageProd : ∀ {α : Type u_1} {β : Type u_2} (U₁ : SetRel α α) (U₂ : SetRel β β) {s₁ t₁ : Set α} {s₂ t₂ : Set β},
  (s₁, t₁) ∈ hausdorffEntourage U₁ →
    (s₂, t₂) ∈ hausdorffEntourage U₂ → (s₁ ×ˢ s₂, t₁ ×ˢ t₂) ∈ hausdorffEntourage (entourageProd U₁ U₂)
-- Init.Control.Lawful.Instances
OptionT.seq_eq : ∀ {m : Type u → Type u_1} {α β : Type u} [inst : Monad m] (mf : OptionT m (α → β)) (x : OptionT m α),
  mf <*> x = do
    let f ← mf
    f <$> x
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E},
  HasFDerivWithinAt f f' t x → t ∈ nhdsWithin x s → HasFDerivWithinAt f f' s x
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.rightHom_section : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (σ : S.Section) (g : G), S.rightHom (σ g) = g