mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.RelativeGluing
/-- The glued scheme of a relative gluing datum is the colimit over the `Xᵢ`. For the
structure map, see `AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase` and the isomorphisms
with the preimages `AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase`.
 -/
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰 →
          [Small.{u, u_1} 𝒰.I₀] → [Quiver.IsThin 𝒰.I₀] → AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.liftOrderHom_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : M → α) (h : ∀ (a b : M), ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → f a ≤ f b)
  (a : M), (ArchimedeanClass.liftOrderHom f h) (ArchimedeanClass.mk a) = f a
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i : C}
  {η : h ⟶ i}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g h ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g i}
  {η₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj g h) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj g i)}
  {η₃ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj g h) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) i}
  {η₄ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) h ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) i},
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft g η = η₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η₁ = η₂ →
      CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.MonoidalCategoryStruct.associator f g i).inv = η₃ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator f g h).hom η₃ = η₄ →
          CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) η = η₄
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_singleton_one : ∀ {R : Type u} [inst : NonAssocSemiring R], Subsemiring.closure {1} = ⊥
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map_surjective_of_surjOn : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q},
  Set.SurjOn ⇑g ↑S ↑T → Function.Surjective ⇑g → Function.Surjective ⇑(f.map hy k)
-- Lean.Elab.Term.TermElabM
/-- Throws `Exception.postpone`, if `expectedType?` contains unassigned metavariables.
If `mayPostpone == false`, it throws error `msg`.
 -/
Lean.Elab.Term.tryPostponeIfHasMVars : Option Lean.Expr → String → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Computability.Primrec.List
Primrec.list_flatten : ∀ {α : Type u_1} [inst : Primcodable α], Primrec List.flatten
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.succ : Turing.ToPartrec.Code
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.eq_of_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {a b : 𝒳} (f : p.obj a ⟶ p.obj b) (φ : a ⟶ b) [p.IsHomLift f φ], f = p.map φ
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.isOrthogonal_reflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  (self : P.InvariantForm) (i : ι), LinearMap.IsOrthogonal self.form ⇑(P.reflection i)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.presheaf.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R),
  M.presheaf =
    { obj := fun X => (CategoryTheory.forget₂ (ModuleCat ↑(R.obj X)) Ab).obj (M.obj X),
      map := fun {X Y} f => AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(CategoryTheory.ConcreteCategory.hom (M.map f)) ⋯),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.FieldTheory.Relrank
Subfield.rank_comap : ∀ {E : Type v} [inst : Field E] (A : Subfield E) {L : Type v} [inst_1 : Field L] (f : L →+* E),
  Module.rank (↥(Subfield.comap f A)) L = A.relrank f.fieldRange
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.ebound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F),
  ∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖ₑ ≤ ↑C * ‖x‖ₑ
-- Mathlib.Data.List.Rotate
List.rotate_eq_nil_iff : ∀ {α : Type u} {l : List α} {n : ℕ}, l.rotate n = [] ↔ l = []
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_equivariantMap.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (s : Set α),
  SubMulAction.ofFixingSubgroup_equivariantMap M s = { toFun := fun x => ↑x, map_smul' := ⋯ }
-- Init.Data.SInt.Lemmas
Int64.toInt_maxValue : Int64.maxValue.toInt = 2 ^ 63 - 1
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- This gives the first pair of coefficients of the continued fraction of a non-integer `v`.
 -/
GenContFract.of_s_head : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K},
  Int.fract v ≠ 0 → (GenContFract.of v).s.head = some { a := 1, b := ↑⌊(Int.fract v)⁻¹⌋ }
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.is_pow_of_dvd_count : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a : Associates α},
  a ≠ 0 → ∀ {k : ℕ}, (∀ (p : Associates α), Irreducible p → k ∣ p.count a.factors) → ∃ b, a = b ^ k
-- Mathlib.CategoryTheory.Filtered.Basic
/-- A category `IsFilteredOrEmpty` if
1. for every pair of objects there exists another object "to the right", and
2. for every pair of parallel morphisms there exists a morphism to the right so the compositions
   are equal.
 -/
CategoryTheory.IsFilteredOrEmpty : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_inter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_naturality_middle_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g' h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h)) h_1)
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.zero_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] (f : ZeroHom M N),
  ZeroHom.comp 0 f = 0
-- 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},
  (∀ (i : ι), DifferentiableOn 𝕜 (fun x => Φ x i) s) → DifferentiableOn 𝕜 Φ s
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instInhabited : (M : Type u_4) → [inst : MulOne M] → Inhabited (Monoid.End M)
-- Lean.ProjFns
Lean.ProjectionFunctionInfo.mk : Lean.Name → ℕ → ℕ → Bool → Lean.ProjectionFunctionInfo
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_sqrt_nnreal : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A} {x : NNReal},
  autoParam (0 ≤ a) CFC.rpow_sqrt_nnreal._auto_1 → CFC.sqrt a ^ ↑x = a ^ (↑x / 2)
-- Mathlib.Algebra.GroupWithZero.Basic
ne_zero_and_ne_zero_of_mul : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] {a b : M₀}, a * b ≠ 0 → a ≠ 0 ∧ b ≠ 0
-- Mathlib.Data.Real.Basic
Real.mk_add : ∀ {f g : CauSeq ℚ abs}, Real.mk (f + g) = Real.mk f + Real.mk g
-- Mathlib.Algebra.Lie.TraceForm
/-- A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian.  -/
LieModule.isLieAbelian_of_ker_traceForm_eq_bot : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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]
  [LieRing.IsNilpotent L] [IsDomain R] [Module.Free R M] [Module.Finite R M],
  LinearMap.ker (LieModule.traceForm R L M) = ⊥ → IsLieAbelian L
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.instOne : {R : Type u_1} → {M : Type u_2} → [inst : Monoid R] → [inst_1 : MulAction R M] → [One M] → One (SubMulAction R M)
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_inv : ∀ {ι : Type u_1} {G : Type u_7} [inst : Inv G] (a : G), (Function.const ι a)⁻¹ = Function.const ι a⁻¹
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_pi_of_finite`. -/
lowerCentralSeries_pi_of_finite : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [Finite η] (Ss : (i : η) → Subgroup (Gs i))
  (n : ℕ), (Subgroup.pi Set.univ Ss).lowerCentralSeries n = Subgroup.pi Set.univ fun i => (Ss i).lowerCentralSeries n
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany? : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] (n : ℕ) (a : α),
  Std.PRange.succMany? (n + 1) a = (Std.PRange.succ? a).bind fun x => Std.PRange.succMany? n x
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mk.congr_simp : ∀ {K : Type u} [inst : DivisionRing K] (toSubring toSubring_1 : Subring K) (e_toSubring : toSubring = toSubring_1)
  (inv_mem' : ∀ x ∈ toSubring.carrier, x⁻¹ ∈ toSubring.carrier),
  { toSubring := toSubring, inv_mem' := inv_mem' } = { toSubring := toSubring_1, inv_mem' := ⋯ }
-- Mathlib.RingTheory.Etale.Finite
/-- Construct a morphism in `FiniteEtale R` from an algebra map.  -/
CommAlgCat.FiniteEtale.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {S T : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : CommRing T] →
          [inst_3 : Algebra R S] →
            [inst_4 : Algebra R T] →
              [inst_5 : Module.Finite R S] →
                [inst_6 : Algebra.Etale R S] →
                  [inst_7 : Module.Finite R T] →
                    [inst_8 : Algebra.Etale R T] →
                      (S →ₐ[R] T) → (CommAlgCat.FiniteEtale.of R S ⟶ CommAlgCat.FiniteEtale.of R T)
-- Mathlib.Order.Category.BddDistLat
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
BddDistLat.Hom.Simps.hom : (X Y : BddDistLat) → X.Hom Y → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_assoc_X_pow : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] (m n : ℕ),
  p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
-- Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.exists_desc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms]
  [F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)]
  [inst_10 : CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj X₂)]
  (s :
    CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))),
  ∃ l,
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂)
        (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) l) =
      CategoryTheory.Limits.Cofork.π s
-- Lean.Server.Requests
Lean.Server.RequestContext : Type
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Morphisms between `𝒪ₓ`-modules. Use `Hom.app` to act on sections.  -/
AlgebraicGeometry.Scheme.Modules.Hom : {X : AlgebraicGeometry.Scheme} → X.Modules → X.Modules → Type u
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), (↑x).imJ = 0
-- Mathlib.RingTheory.Idempotents
/-- A system of complete orthogonal idempotents lift along nil ideals.  -/
CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {I : Type u_3} [inst_2 : Fintype I],
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ {e : I → S},
      CompleteOrthogonalIdempotents e →
        (∀ (i : I), e i ∈ f.range) → ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
Lean.commandDeclare_uint_simprocs_ : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.fixedPoint_unique : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α] {x : α}, Function.IsFixedPt f x → x = ContractingWith.fixedPoint f hf
-- Mathlib.Algebra.Algebra.Basic
/-- If `R →+* S` is surjective, then `R`-linear isomorphisms are also `S`-linear.  -/
LinearEquiv.extendScalarsOfSurjective : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {M : Type u_3} →
            {N : Type u_4} →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module S M] →
                      [IsScalarTower R S M] →
                        [inst_8 : Module R N] →
                          [inst_9 : Module S N] →
                            [IsScalarTower R S N] → Function.Surjective ⇑(algebraMap R S) → (M ≃ₗ[R] N) → M ≃ₗ[S] N
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.birdDet.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i))
  [inst_1 : I.IsPrime],
  (Localization.AtPrime.mapPiEvalRingHom I).comp
      (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) =
    (algebraMap (R i) (Localization.AtPrime I)).comp (Pi.evalRingHom R i)
-- Mathlib.Tactic.Simps.NotationClass
/-- The `@[notation_class]` attribute specifies that this is a notation class,
and this notation should be used instead of projections by `@[simps]`.
  * This is only important if the projection is written differently using notation, e.g.
    `+` uses `HAdd.hAdd`, not `Add.add` and `0` uses `OfNat.ofNat` not `Zero.zero`.
    We also add it to non-heterogeneous notation classes, like `Neg`, but it doesn't do much for any
    class that extends `Neg`.
  * `@[notation_class* <projName> Simps.findCoercionArgs]` is used to configure the
    `SetLike` and `DFunLike` coercions.
  * The first name argument is the projection name we use as the key to search for this class
    (default: name of first projection of the class).
  * The second argument is the name of a declaration that has type
    `findArgType` which is defined to be `Name → Name → Array Expr → MetaM (Array (Option Expr))`.
    This declaration specifies how to generate the arguments of the notation class from the
    arguments of classes that use the projection.  -/
notation_class : Lean.ParserDescr
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_sub : ∀ {α : Type u} (x y : FreeRing α), ↑(x - y) = ↑x - ↑y
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The canonical morphism `S.cycles ⟶ S.homology` for a short complex `S` that has homology.  -/
CategoryTheory.ShortComplex.homologyπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasHomology] → S.cycles ⟶ S.homology
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.closure_eq_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] {s : Set α},
  closure s = ↑(upperClosure s)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- A structure on an oplax functor that promotes an oplax functor to a pseudofunctor.

See `Pseudofunctor.mkOfOplax`.  -/
CategoryTheory.OplaxFunctor.PseudoCore : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.OplaxFunctor B C → Type (max (max u₁ v₁) w₂)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.spectrum_subset_slitPlane_iff_norm_lt_two : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : A}, u ∈ unitary A → (spectrum ℂ u ⊆ Complex.slitPlane ↔ ‖u - 1‖ < 2)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp k t.min!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isMulLeftInvariant_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G]
  {H : Type u_3} [inst_3 : MeasurableSpace H] [inst_4 : Mul H] [MeasurableMul H] [μ.IsMulLeftInvariant] (f : G →ₙ* H),
  Measurable ⇑f → Function.Surjective ⇑f → (MeasureTheory.Measure.map (⇑f) μ).IsMulLeftInvariant
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- Auxiliary lemma for `rnDeriv_add_right_of_mutuallySingular`.  -/
MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [μ.HaveLebesgueDecomposition (ν + ν')] [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν → ν.MutuallySingular ν' → μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : ↑(X.presheaf.obj (Opposite.op U))) (g : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))),
      ∃ f', X.basicOpen f' = X.basicOpen g
-- Mathlib.Data.Multiset.MapFold
Multiset.foldl_zero : ∀ {α : Type u_1} {β : Type v} (f : β → α → β) [inst : RightCommutative f] (b : β), Multiset.foldl f b 0 = b
-- Mathlib.Order.Lattice
/-- Prove distributivity of an existing lattice from the dual distributive law.  -/
DistribLattice.ofInfSupLe : {α : Type u} → [inst : Lattice α] → (∀ (a b c : α), a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c) → DistribLattice α
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.bipartiteBelow.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Finset α) (b : β) [inst : (a : α) → Decidable (r a b)],
  Finset.bipartiteBelow r s b = {a ∈ s | r a b}
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Cache mapping expressions (by pointer equality) to their simplified results.  -/
Lean.Meta.Sym.DSimp.Cache : Type
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instContinuousAddWeakSpace : ∀ (𝕜 : Type u_2) (E : Type u_1) [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  ContinuousAdd (WeakSpace 𝕜 E)
-- Mathlib.Analysis.Normed.Field.Basic
nndist_inv_inv₀ : ∀ {α : Type u_2} [inst : NormedDivisionRing α] {z w : α}, z ≠ 0 → w ≠ 0 → nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊)
-- Mathlib.NumberTheory.FLT.Basic
not_fermatLastTheoremFor_two : ¬FermatLastTheoremFor 2
-- Init.Data.Sum.Lemmas
Sum.isLeft_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.isLeft = true ↔ ∃ y, x = Sum.inl y
-- Mathlib.Order.Category.BoolAlg
boolAlg_dual_comp_forget_to_bddDistLat : BoolAlg.dual.comp (CategoryTheory.forget₂ BoolAlg BddDistLat) =
  (CategoryTheory.forget₂ BoolAlg BddDistLat).comp BddDistLat.dual
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.liftAux_map_mul : ∀ (R : Type u) {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L)
  (a b : FreeNonUnitalNonAssocAlgebra R X),
  (FreeLieAlgebra.liftAux R f) (a * b) = ⁅(FreeLieAlgebra.liftAux R f) a, (FreeLieAlgebra.liftAux R f) b⁆
-- Mathlib.Algebra.Star.Module
selfAdjointPart_apply_coe : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] (x : A), ↑((selfAdjointPart R) x) = ⅟2 • (x + star x)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_subset_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  a₁ ∈ Set.Icc a₂ b₂ → b₁ ∈ Set.Icc a₂ b₂ → Set.uIoo a₁ b₁ ⊆ Set.Ioo a₂ b₂