mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Yoneda
/-- Yoneda's lemma as a bijection `(uliftYoneda.{w}.obj X ⟶ F) ≃ F.obj (op X)`
for any presheaf of type `F : Cᵒᵖ ⥤ Type (max w v₁)` for some
auxiliary universe `w`.  -/
CategoryTheory.uliftYonedaEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} →
        (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.op X)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.prod_sup_eq_top : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ι → Ideal R},
  (∀ i ∈ s, J i ⊔ I = ⊤) → (∏ i ∈ s, J i) ⊔ I = ⊤
-- Mathlib.Data.Finsupp.Defs
/-- The natural `Finsupp` induced by the function `f` given that it has finite support.  -/
Finsupp.ofSupportFinite : {α : Type u_1} → {M : Type u_4} → [inst : Zero M] → (f : α → M) → (Function.support f).Finite → α →₀ M
-- Mathlib.Order.Heyting.Basic
inf_compl_eq_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, a ⊓ aᶜ = ⊥
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- An infinite place `w` of `L / K` lies over the infinite place `v` of `K` if `v` is the
restriction of `w` to `K`.  -/
NumberField.InfinitePlace.LiesOver : {K : Type u_1} →
  [inst : Field K] →
    {L : Type u_2} →
      [inst_1 : Field L] → [Algebra K L] → NumberField.InfinitePlace L → NumberField.InfinitePlace K → Prop
-- Mathlib.Analysis.Normed.Group.Defs
enorm_le_coe : ∀ {E : Type u_8} [inst : NNNorm E] {x : E} {r : NNReal}, ‖x‖ₑ ≤ ↑r ↔ ‖x‖₊ ≤ r
-- Aesop.Forward.PremiseIndex
Aesop.instDecidableEqPremiseIndex.decEq : (x x_1 : Aesop.PremiseIndex) → Decidable (x = x_1)
-- Mathlib.GroupTheory.Congruence.Defs
/-- There exists an element of the quotient of an `AddMonoid` by a congruence relation
(namely 0).  -/
AddCon.Quotient.inhabited : {M : Type u_1} → [inst : Add M] → [Zero M] → {c : AddCon M} → Inhabited c.Quotient
-- Mathlib.CategoryTheory.Abelian.CommSq
CategoryTheory.Abelian.instIsStableUnderBaseChangeEpimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  (CategoryTheory.MorphismProperty.epimorphisms C).IsStableUnderBaseChange
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.subtypeVal_coe : ∀ {β : Type u_3} [inst : SemilatticeInf β] [inst_1 : OrderTop β] {P : β → Prop} (Ptop : P ⊤)
  (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)), ⇑(InfTopHom.subtypeVal Ptop Pinf) = Subtype.val
-- Mathlib.Algebra.Ring.AddAut
AddAut.mulRight_apply : ∀ {R : Type u_1} [inst : Semiring R] (u : Rˣ) (x : R), (AddAut.mulRight u) x = x * ↑u
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_fun_mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸},
  DifferentiableAt 𝕜 a x →
    DifferentiableAt 𝕜 b x → fderiv 𝕜 (fun y => a y * b y) x = a x • fderiv 𝕜 b x + MulOpposite.op (b x) • fderiv 𝕜 a x
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eval_zero_of_odd : ∀ (R : Type u_1) [inst : CommRing R] {n : ℤ}, Odd n → Polynomial.eval 0 (Polynomial.Chebyshev.U R n) = 0
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftTCoreMMetaM_batteries : LawfulMonadLiftT Lean.CoreM Lean.MetaM
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.instSubsingletonOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk : ∀ (X : SSet.Truncated 2)
  [Subsingleton (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }))],
  Subsingleton X.HomotopyCategory
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.param_zpow_mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    Asymptotics.SuperpolynomialDecay l k f → ∀ (z : ℤ), Asymptotics.SuperpolynomialDecay l k fun a => k a ^ z * f a
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeries_summable_aux₃ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  ↑r < p.radius → ∀ (k : ℕ), Summable fun l => ‖p.changeOriginSeries k l‖₊ * r ^ l
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.triangleOfDegreewiseSplit_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  (CochainComplex.triangleOfDegreewiseSplit S σ).obj₃ = S.X₃
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.subset_of_mem_compactNhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K K' : TopologicalSpace.Compacts α}, K' ∈ K.compactNhds → ↑K ⊆ ↑K'
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Nat.Partition.ofSymShapeEquiv.eq_1 : ∀ {n : ℕ} {σ : Type u_1} {τ : Type u_2} [inst : DecidableEq σ] [inst_1 : DecidableEq τ] (μ : n.Partition) (e : σ ≃ τ),
  μ.ofSymShapeEquiv e =
    { toFun := fun x => ⟨(Sym.equivCongr e) ↑x, ⋯⟩, invFun := fun x => ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Data.Set.Function
Set.bijOn_of_subsingleton' : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton α] [Subsingleton β] (f : α → β),
  (s.Nonempty ↔ t.Nonempty) → Set.BijOn f s t
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingStrat.eq_1 : ∀ {Ω : Type u_1} (a b : ℝ) (f : ℕ → Ω → ℝ) (N n : ℕ) (ω : Ω),
  MeasureTheory.upcrossingStrat a b f N n ω =
    ∑ k ∈ Finset.range N,
      (Set.Ico (MeasureTheory.lowerCrossingTime a b f N k ω)
            (MeasureTheory.upperCrossingTime a b f N (k + 1) ω)).indicator
        1 n
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitorNatIso_inv_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.weakEquivalence_postcomp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [HomotopicalAlgebra.WeakEquivalence g],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.CategoryStruct.comp f g) ↔ HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.Algebra.Homology.LocalCohomology
localCohomology.SelfLERadical.cast_isEquivalence : ∀ {R : Type u} [inst : CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical),
  (localCohomology.SelfLERadical.cast hJK).IsEquivalence
-- Mathlib.Topology.DiscreteSubset
Filter.codiscrete.eq_1 : ∀ (X : Type u_3) [inst : TopologicalSpace X], Filter.codiscrete X = Filter.codiscreteWithin Set.univ
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_def : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)),
  o.areaForm =
    have z := AlternatingMap.constLinearEquivOfIsEmpty.symm;
    have y := (LinearMap.llcomp ℝ E (E [⋀^Fin 0]→ₗ[ℝ] ℝ) ℝ) ↑z ∘ₗ AlternatingMap.curryLeftLinearMap;
    y ∘ₗ AlternatingMap.curryLeftLinearMap o.volumeForm
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENode.mk : Lean.Expr →
  Lean.Expr →
    Lean.Expr →
      Lean.Expr →
        Option Lean.Expr →
          Option Lean.Expr →
            Bool →
              ℕ →
                Bool →
                  Bool →
                    Bool →
                      Bool →
                        ℕ →
                          ℕ →
                            ℕ →
                              Lean.Meta.Grind.SolverTerms →
                                Bool → Lean.Meta.Grind.EMatchDiagSource → Lean.Meta.Grind.ENode
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.subset_complex`. -/
Topology.CWComplex.Subcomplex.subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), ↑E ⊆ C
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_apply : ∀ {n : Type u_3} {α : Type v} {ι : Type u_6} (v : n → α) (i : ι) (j : n), Matrix.replicateRow ι v i j = v j
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.splitCenterBoxEmb_apply : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι), I.splitCenterBoxEmb s = I.splitCenterBox s
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.prev_eq' : ∀ {ι : Type u_1} (c : ComplexShape ι) {i j : ι}, c.Rel j i → c.prev i = j
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb.eq_1 : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)) (t : ↑unitInterval), Set.Icc.convexComb x y t = ⟨(1 - ↑t) * ↑x + ↑t * ↑y, ⋯⟩
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.inv_mul : ∀ {R : Type u_2} [inst : Semifield R] {a₁ : R} {a₂ : ℕ} {a₃ b₁ b₃ c : R},
  a₁⁻¹ = b₁ → a₃⁻¹ = b₃ → b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c → (a₁ ^ a₂ * a₃)⁻¹ = c
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
/-- If `‖B x y‖ = ‖x‖ * ‖y‖` for all `x, y`, then the variation of a vector measure with
density `f` wrt `μ` is the measure with density `‖f‖ₑ` with respect to the variation of `μ`.

The condition on `B` is necessary: for a counterexample without it, let `B` be the scalar
product in `ℝ²` and `f x` everywhere horizontal and `μ s` everywhere vertical.
Then `μ.withDensity f B = 0` so its variation is zero, while the integral of `‖f‖ₑ` is not.
 -/
MeasureTheory.VectorMeasure.variation_withDensity : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G}
  [CompleteSpace G],
  μ.Integrable f →
    (∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊) →
      (μ.withDensity f B).variation = (μ.transpose B).variation.withDensity fun x => ‖f x‖ₑ
-- Init.Data.SInt.Bitwise
Int16.not_neg_one : ~~~(-1) = 0
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addLeft_symm : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G] (x : G),
  (IsometryEquiv.addLeft x).symm = IsometryEquiv.addLeft (-x)
-- Lean.Util.ShareCommon
Lean.ShareCommon.PShareCommonT : (Type u_1 → Type u_2) → Type u_1 → Type (max u_1 u_2)
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.twoCochain_val_apply : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (a : ↥(LieModule.Cohomology.twoCochain R L M)) (x : L), ↑a x = a x
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The subfield of elements `x : R` such that `f x = g x`, i.e.,
the equalizer of f and g as a subfield of R  -/
RingHom.eqLocusField : {K : Type u} → [inst : DivisionRing K] → {L : Type v} → [inst_1 : Semiring L] → (K →+* L) → (K →+* L) → Subfield K
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.sub_rat : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (r : ℚ), LiouvilleWith p (x - ↑r)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.degree_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] [Nontrivial S] {P : Polynomial R},
  P.Monic → ∀ (f : R →+* S), (Polynomial.map f P).degree = P.degree
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instDecidableLeOffset : {x y : Std.Time.Minute.Offset} → Decidable (x ≤ y)
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then
it is an additive Haar measure.  -/
MeasureTheory.Measure.isAddHaarMeasure_of_isCompact_nonempty_interior : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (K : Set G),
  IsCompact K → (interior K).Nonempty → μ K ≠ 0 → μ K ≠ ⊤ → μ.IsAddHaarMeasure
-- Lean.LibrarySuggestions.SineQuaNon
Lean.LibrarySuggestions.SineQuaNon.sineQuaNonTheorems : Lean.Name → Lean.CoreM (List (Lean.Name × Float))
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem' : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ),
  (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred 0
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_left' : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], (x \ y) \ z = x \ y ⊓ x \ z
-- Init.Data.SInt.Lemmas
Int16.toInt_le : ∀ (x : Int16), x.toInt ≤ Int16.maxValue.toInt
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.sumAux.eq_1 : ∀ {M : Type u_6} [inst : AddMonoid M], FreeAddMonoid.sumAux [] = 0
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.comap_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂}, f.range = ⊤ → Function.Injective (Submodule.comap f)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- See note [partially-applied ext lemmas].  -/
TensorAlgebra.hom_ext : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : TensorAlgebra R M →ₐ[R] A},
  f.toLinearMap ∘ₗ TensorAlgebra.ι R = g.toLinearMap ∘ₗ TensorAlgebra.ι R → f = g
-- Init.Notation
/-- Time the elaboration of a command, and print the result (in milliseconds).

Example usage:
```
set_option maxRecDepth 100000 in
#time example : (List.range 500).length = 500 := rfl
```
 -/
Lean.Parser.timeCmd : Lean.ParserDescr
-- Init.Data.Dyadic.Basic
Dyadic.toRat_ofIntWithPrec_eq_mkRat : ∀ {n k : ℤ}, (Dyadic.ofIntWithPrec n k).toRat = mkRat (n <<< (-k).toNat) (1 <<< k.toNat)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView!.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l' r' with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') =
    h_2 size k' v' l' r'
-- Mathlib.Order.Atoms
OrderIso.isSimpleOrder_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : α ≃o β), IsSimpleOrder α ↔ IsSimpleOrder β
-- Mathlib.Algebra.Ring.Prod
/-- Product of two commutative rings is a commutative ring.  -/
Prod.instCommRing : {R : Type u_1} → {S : Type u_3} → [CommRing R] → [CommRing S] → CommRing (R × S)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.toOpenPartialHomeomorph_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  ↑(HasStrictFDerivAt.toOpenPartialHomeomorph f hf) = f
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_mulRight : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  (MeasurableEquiv.mulRight g).symm = MeasurableEquiv.mulRight g⁻¹
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Qq-fied version of `Expr`. Here, we use it to store free variables introduced when unpacking
existential quantifiers.  -/
ExistsAndEq.VarQ : Type
-- Mathlib.Data.Nat.Prime.Basic
Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul : ∀ {p : ℕ},
  Nat.Prime p → ∀ {m n k l : ℕ}, p ^ k ∣ m → p ^ l ∣ n → p ^ (k + l + 1) ∣ m * n → p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
-- Lean.Meta.Tactic.Cases
/-- Apply `casesOn` using the free variable `majorFVarId` as the major premise (aka discriminant).
`givenNames` contains user-facing names for each alternative.

- `useNatCasesAuxOn` is a temporary hack for the `rcases` family of tactics.
  Do not use it, as it is subject to removal.
  It enables using `Nat.casesAuxOn` instead of `Nat.casesOn`,
  which causes case splits on `n : Nat` to be represented as `0` and `n' + 1` rather than as `Nat.zero` and `Nat.succ n'`.
 -/
Lean.MVarId.cases : Lean.MVarId →
  Lean.FVarId →
    optParam (Array Lean.Meta.AltVarNames) #[] →
      optParam Bool false → optParam (Option (Array Lean.Name)) none → Lean.MetaM (Array Lean.Meta.CasesSubgoal)
-- Mathlib.Order.Category.Frm
Frm.comp_apply : ∀ {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l}, (t.insertMany l)[k] = t[k]
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableOn_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  DifferentiableOn 𝕜 Φ s ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => Φ x i) s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (t.alter k f).size =
    if k ∈ t ∧ (f t[k]?).isNone = true then t.size - 1
    else if k ∉ t ∧ (f t[k]?).isSome = true then t.size + 1 else t.size
-- Mathlib.Algebra.Group.Pi.Lemmas
ZeroHom.single_apply : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] (i : I) (x : f i),
  (ZeroHom.single f i) x = Pi.single i x
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.sub_one_right_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, x ∣ y → IsRelPrime x (y - 1)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_surjective_of_surjective : ∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β},
  Function.Surjective f → Function.Surjective ⇑(FreeGroup.lift f)
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- **Alias** of the forward direction of `ContinuousLinearMap.isFredholm_iff_exists_isQuasiInverse`. -/
ContinuousLinearMap.IsFredholm.exists_isQuasiInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space E] [T2Space F] {u : E →L[𝕜] F},
  u.IsFredholm → ∃ v, (↑v).IsQuasiInverse ↑u
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.replaceEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k), Std.Internal.List.replaceEntry k v [] = []
-- Mathlib.Data.Int.ModEq
Int.ModEq.trans : ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]
-- Mathlib.LinearAlgebra.Eigenspace.Pi
/-- Given a family of endomorphisms `i ↦ f i` which are compatible in the sense that every maximal
generalised eigenspace of `f i` is invariant w.r.t. `f j`, if each `f i` is triangularizable, the
family is simultaneously triangularizable.  -/
Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo : ∀ {ι : Type u_1} {K : Type u_3} {M : Type u_4} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [FiniteDimensional K M] (f : ι → Module.End K M),
  (∀ (i j : ι) (φ : K), Set.MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
    (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_toList_rco : ∀ {m n : ℤ}, (m...=n).toList = (m...n + 1).toList
-- Mathlib.Algebra.Ring.Commute
Commute.neg_one_left : ∀ {R : Type u} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (a : R), Commute (-1) a
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_apply_ne_self_iff : ∀ {α : Sort u_1} [inst : DecidableEq α] {a b x : α}, (Equiv.swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → SemilatticeInf (J.Cover X)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.Hom.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f : P.X ⟶ Q.X)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f Q.p) = f)
      CategoryTheory.Idempotents.Karoubi.Hom.comm._autoParam)
  (f_1 : P.X ⟶ Q.X)
  (comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f_1 Q.p) = f_1)
      CategoryTheory.Idempotents.Karoubi.Hom.comm._autoParam),
  ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.gc_map_comap : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] (f : A →⋆ₐ[R] B),
  GaloisConnection (StarSubalgebra.map f) (StarSubalgebra.comap f)
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_inf : ∀ {R : Type u} [inst : LinearOrder R] (x y : R), Tropical.trop (min x y) = Tropical.trop x + Tropical.trop y
-- Mathlib.Algebra.Free
/-- Isomorphism between `AddMagma.AssocQuotient (FreeAddMagma α)` and
`FreeAddSemigroup α`.  -/
FreeAddMagmaAssocQuotientEquiv : (α : Type u) → AddMagma.FreeAddSemigroup (FreeAddMagma α) ≃+ FreeAddSemigroup α
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prodEquiv.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N),
  H.prodEquiv K = { toEquiv := Equiv.Set.prod ↑H ↑K, map_add' := ⋯ }
-- Mathlib.Algebra.Algebra.Operations
Submodule.instMulLeftMono : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A], MulLeftMono (Submodule R A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_toList : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  (Std.DTreeMap.Internal.Impl.Const.toList t).toArray = Std.DTreeMap.Internal.Impl.Const.toArray t