mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.RelClasses
Order.Preimage.instIsTrans : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [IsTrans α r] {f : β → α}, IsTrans β (f ⁻¹'o r)
-- Mathlib.RingTheory.Unramified.LocalRing
Algebra.instFormallyUnramifiedResidueField_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : IsLocalRing S] [inst_5 : IsLocalHom (algebraMap R S)]
  [Algebra.FormallyUnramified R S], Algebra.FormallyUnramified (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_of_nonneg_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightMono α] {a b : α}, 0 ≤ b → a ≤ b + a
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_pow' : ∀ {m n : ℕ}, n ≠ 0 → (Even (m ^ n) ↔ Even m)
-- Std.Data.ByteSlice
/-- Internal representation of `ByteSlice`, which is an abbreviation for `Slice ByteSliceData`.
 -/
Std.Slice.Internal.ByteSliceData : Type
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.coe_copy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {s : (X : C) → Set (CategoryTheory.Sieve X)} {h : J.sieves = s}, ⇑(J.copy s h) = s
-- Init.Data.Int.Gcd
Int.lcm_lcm_self_left_right : ∀ (m n : ℤ), (↑(n.lcm m)).lcm m = n.lcm m
-- Init.Data.AC
Lean.Data.AC.removeNeutrals.eq_2 : ∀ {α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α), Lean.Data.AC.removeNeutrals ctx [] = []
-- Mathlib.NumberTheory.Niven
/-- `2 sin(q * π)` for `q : ℚ` is integral over `ℤ`, using the complex `sin` function.  -/
Complex.isIntegral_two_mul_sin_rat_mul_pi : ∀ (q : ℚ), IsIntegral ℤ (2 * Complex.sin (↑q * ↑Real.pi))
-- Mathlib.Order.SupClosed
IsSublattice.preimage : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] {s : Set α}
  [inst_2 : FunLike F β α] [LatticeHomClass F β α], IsSublattice s → ∀ (f : F), IsSublattice (⇑f ⁻¹' s)
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.beq.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) →
    (Unit → motive Nat.zero Nat.zero) →
      ((n : ℕ) → motive Nat.zero n.succ) →
        ((n : ℕ) → motive n.succ Nat.zero) → ((n m : ℕ) → motive n.succ m.succ) → motive x x_1
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- Reinterpret `x : α` as an element of `Additive α`.  -/
Additive.ofMul : {α : Type u} → α ≃ Additive α
-- Mathlib.Algebra.DirectSum.Ring
/-- The `Ring` derived from `GSemiring A`.  -/
DirectSum.instRingOfNat : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommGroup (A i)] → [inst_1 : AddMonoid ι] → [DirectSum.GRing A] → Ring (A 0)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coeTail : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → CoeTail β (l.Germ β)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.hasPointwiseRightDerivedFunctor_of_inverts : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) {W : CategoryTheory.MorphismProperty C},
  W.IsInvertedBy F → F.HasPointwiseRightDerivedFunctor W
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_refl : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ↑(ContinuousLinearEquiv.refl R₁ M₁) = ContinuousLinearMap.id R₁ M₁
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Comonad.forget_additive : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (U : CategoryTheory.Comonad C) [inst_2 : U.Additive], U.forget.Additive
-- Mathlib.Order.Hom.Basic
OrderHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (toFun toFun_1 : α → β)
  (e_toFun : toFun = toFun_1) (monotone' : Monotone toFun),
  { toFun := toFun, monotone' := monotone' } = { toFun := toFun_1, monotone' := ⋯ }
-- Mathlib.Data.EReal.Inv
EReal.div_top : ∀ {a : EReal}, a / ⊤ = 0
-- Mathlib.Data.Seq.Computation
Computation.exists_of_liftRel_left : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β},
  Computation.LiftRel R ca cb → ∀ {a : α}, a ∈ ca → ∃ b ∈ cb, R a b
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mem_subgroupOfCoprimeConductor : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} [inst_1 : NeZero n] {d : ℕ} {χ : DirichletCharacter R n},
  χ ∈ DirichletCharacter.subgroupOfCoprimeConductor d ↔ d.Coprime χ.conductor
-- Mathlib.GroupTheory.Goursat
AddSubgroup.mem_goursatSnd : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {I : AddSubgroup (G × H)} {h : H},
  h ∈ I.goursatSnd ↔ (0, h) ∈ I
-- Init.Data.Vector.Erase
Vector.eraseIdx_set_gt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} {a : α} (h : i < j) {w : j < n},
  (xs.set i a ⋯).eraseIdx j w = (xs.eraseIdx j w).set i a ⋯
-- Mathlib.Data.Finset.Grade
Finset.erase_wcovBy : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), s.erase a ⩿ s
-- Mathlib.Topology.Algebra.Monoid
exists_open_nhds_zero_half : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [ContinuousAdd M] {s : Set M},
  s ∈ nhds 0 → ∃ V, IsOpen V ∧ 0 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.top_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (i : C), ⊤.obj i = ⊤
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.noConfusionType : Sort v✝ → Lean.Meta.ProjReductionKind → Lean.Meta.ProjReductionKind → Sort v✝
-- Mathlib.Data.PEquiv
PEquiv.ofSet_symm : ∀ {α : Type u} (s : Set α) [inst : DecidablePred fun x => x ∈ s], (PEquiv.ofSet s).symm = PEquiv.ofSet s
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.mk : ∀ {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₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₁ a).hom
        (CategoryTheory.Functor.whiskerRight τ (CategoryTheory.shiftFunctor D a)) =
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).whiskerLeft τ)
        (CategoryTheory.Functor.commShiftIso F₂ a).hom →
    CategoryTheory.NatTrans.CommShiftCore τ a
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SubgoalsResult.mk.injEq : ∀ (subgoals : List Lean.Expr) (instVal instTypeBody : Lean.Expr) (subgoals_1 : List Lean.Expr)
  (instVal_1 instTypeBody_1 : Lean.Expr),
  ({ subgoals := subgoals, instVal := instVal, instTypeBody := instTypeBody } =
      { subgoals := subgoals_1, instVal := instVal_1, instTypeBody := instTypeBody_1 }) =
    (subgoals = subgoals_1 ∧ instVal = instVal_1 ∧ instTypeBody = instTypeBody_1)
-- Mathlib.CategoryTheory.Shift.Induced
/-- When `F : C ⥤ D` is a functor satisfying suitable technical assumptions,
this is the induced term of type `HasShift D A` deduced from `[HasShift C A]`.  -/
CategoryTheory.HasShift.induced : {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) →
          (A : Type u_3) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                (s : A → CategoryTheory.Functor D D) →
                  ((a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F) →
                    [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] →
                      [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] → CategoryTheory.HasShift D A
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_of_pow : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), (FreeGroup.of a ^ n).toWord = List.replicate n (a, true)
-- Std.Data.HashMap.Lemmas
Std.HashMap.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α}, Std.HashMap.unitOfList l = ∅.insertManyIfNewUnit l
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.skewProd_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  {M₂ : Type u_3} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommGroup M₂] {M₃ : Type u_4}
  [inst_5 : TopologicalSpace M₃] [inst_6 : AddCommGroup M₃] {M₄ : Type u_5} [inst_7 : TopologicalSpace M₄]
  [inst_8 : AddCommGroup M₄] [inst_9 : Module R M] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R M₄] [inst_13 : IsTopologicalAddGroup M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄)
  (x : M₂ × M₄), (e.skewProd e' f).symm x = (e.symm x.1, e'.symm (x.2 - f (e.symm x.1)))
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.order_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ], HahnSeries.order 0 = 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.findRecAndParent?.go : Lean.Name → Option Lean.AsyncConst✝ → Lean.AsyncConsts✝ → Option (Lean.AsyncConst✝ × Option Lean.AsyncConst✝)
-- Mathlib.Algebra.Module.Torsion.Free
Module.IsTorsionFree.mk : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ ⦃r : R⦄, IsRegular r → IsSMulRegular M r) → Module.IsTorsionFree R M
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.instMonoidalEndMonoidalStarEndMonoidalStarFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).Monoidal
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- The canonical natural transformation `F ⟶ L ⋙ F.totalRightDerived L W`.  -/
CategoryTheory.Functor.totalRightDerivedUnit : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (F : CategoryTheory.Functor C H) →
              (L : CategoryTheory.Functor C D) →
                (W : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L.IsLocalization W] →
                    [inst_4 : F.HasRightDerivedFunctor W] → F ⟶ L.comp (F.totalRightDerived L W)
-- Mathlib.Computability.Encoding
/-- The natural inclusion of `Bool` in `Γ'`.  -/
Computability.inclusionBoolΓ' : Bool → Computability.Γ'
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.mono_of_source_iso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0), CategoryTheory.Mono f
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.indep_generateFrom_le_nat : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ProbabilityTheory.iIndepSet s μ →
      ∀ (n : ℕ),
        ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s (n + 1)})
          (MeasurableSpace.generateFrom {t | ∃ k ≤ n, s k = t}) μ
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_comp_reindex_symm : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11}
  [inst_3 : (i : ι) → AddCommMonoid (t i)] [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i)
  (e : ι ≃ ι₂),
  PiTensorProduct.map f ∘ₗ ↑(PiTensorProduct.reindex R s e).symm =
    ↑(PiTensorProduct.reindex R t e).symm ∘ₗ PiTensorProduct.map fun i => f (e.symm i)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.isTangentAt_touchpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (i : Fin (n + 1)),
      (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
-- Mathlib.Algebra.Homology.GrothendieckAbelian
HomologicalComplex.isGrothendieckAbelian : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] [c.HasNoLoop] [Small.{w, t} ι],
  CategoryTheory.IsGrothendieckAbelian.{w, max t v, max (max t u) v} (HomologicalComplex C c)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.mem_srange : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f : F} {y : S},
  y ∈ NonUnitalRingHom.srange f ↔ ∃ x, f x = y
-- Mathlib.SetTheory.ZFC.Class
Class.mem_univ_hom : ∀ (x : ZFSet.{u}), Class.univ x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.applySMulCommClass : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁], SMulCommClass R₁ (M₁ →L[R₁] M₁) M₁
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.commaFromOver_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Over X)),
  (CategoryTheory.WithTerminal.commaFromOver.obj K).right = X
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_get_EStateM_apply_eq : ∀ {ε σ : Type} {post : σ → σ → Prop} {epost : ε → σ → Prop},
  Std.Internal.Do.wp MonadStateOf.get post epost = fun s => post s s
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_coe : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] {F : Type u_2} [inst_6 : FunLike F A B] [inst_7 : NonUnitalAlgSemiHomClass F φ A B]
  (f : F), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.functor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShrinkHoms.functor C).map f = (equivShrink (X ⟶ Y)) f
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The presheaf `presheaf data G₀` extends `G₀`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          (X₀ : C₀) →
                            (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀).obj
                                (Opposite.op (F.obj X₀)) ≅
                              G₀.obj.obj (Opposite.op X₀)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.le_radius_of_summable_nnnorm : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, (Summable fun n => ‖p n‖₊ * r ^ n) → ↑r ≤ p.radius
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_1.eq_1 : ∀ (motive : Option (List Lean.MVarId) → Sort u_1) (goals' : List Lean.MVarId)
  (h_1 : (goals' : List Lean.MVarId) → motive (some goals')) (h_2 : Unit → motive none),
  (match some goals' with
    | some goals' => h_1 goals'
    | none => h_2 ()) =
    h_1 goals'
-- Mathlib.LinearAlgebra.Trace
LinearMap.id.eq_1 : ∀ {R : Type u_1} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.id = { toFun := fun x => x, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Data.Nat.ModEq
Nat.modEq_one : ∀ {a b : ℕ}, a ≡ b [MOD 1]
-- Init.Data.List.MapIdx
List.mapIdx_eq_cons_iff : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {l₂ : List β} {l : List α} {b : β},
  List.mapIdx f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f 0 a = b ∧ List.mapIdx (fun i => f (i + 1)) l₁ = l₂
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- A lax braided functor takes commutative monoid objects to commutative monoid objects.

That is, a lax braided functor `F : C ⥤ D` induces a functor `CommMon C ⥤ CommMon D`.
 -/
CategoryTheory.Functor.mapCommMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) →
                  [F.LaxBraided] → CategoryTheory.Functor (CategoryTheory.CommMon C) (CategoryTheory.CommMon D)
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. An integrable function is smaller than its integral on a set of
positive measure.  -/
MeasureTheory.measure_le_integral_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → 0 < μ {x | f x ≤ ∫ (a : α), f a ∂μ}
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.is_primitive_element_of_infinitePlace_lt : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.RingOfIntegers K}
  {w : NumberField.InfinitePlace K},
  x ≠ 0 → (∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) → w.IsReal ∨ |(w.embedding ↑x).re| < 1 → ℚ⟮↑x⟯ = ⊤
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_le_map_commutator : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {H₁ H₂ : Subgroup G} {f : G →* G'}
  {K₁ K₂ : Subgroup G'}, K₁ ≤ Subgroup.map f H₁ → K₂ ≤ Subgroup.map f H₂ → ⁅K₁, K₂⁆ ≤ Subgroup.map f ⁅H₁, H₂⁆
-- Init.Data.BitVec.Lemmas
BitVec.msb_setWidth'_of_lt : ∀ {m n : ℕ} (p : m < n) {x : BitVec m}, (BitVec.setWidth' ⋯ x).msb = false
-- Mathlib.Tactic.Sat.FromLRAT
/-- Parse a DIMACS format `.cnf` file.
This is not very robust; we assume the file has had comments stripped.  -/
Mathlib.Tactic.Sat.Parser.parseDimacs : Std.Internal.Parsec.String.Parser (ℕ × Array (Array ℤ))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (h : CategoryTheory.Limits.IsLimit s) {f g : W ⟶ s.pt},
  CategoryTheory.CategoryStruct.comp f s.fst = CategoryTheory.CategoryStruct.comp g s.fst →
    CategoryTheory.CategoryStruct.comp f s.snd = CategoryTheory.CategoryStruct.comp g s.snd → f = g
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.center_toSubmonoid : ∀ (R : Type u) [inst : NonAssocSemiring R],
  (Subsemiring.center R).toSubmonoid =
    { carrier := (NonUnitalSubsemiring.center R).carrier, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Data.Num.ZNum
Num.ofInt'_toZNum : ∀ (n : ℕ), (↑n).toZNum = ZNum.ofInt' ↑n
-- Init.Data.SInt.Bitwise
Int8.not_eq_neg_sub : ∀ (a : Int8), ~~~a = -a - 1
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.State.mk.sizeOf_spec : ∀ (perfect : Bool), sizeOf { perfect := perfect } = 1 + sizeOf perfect
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_spanRank : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R), I ≠ ⊤ → ↑I.height ≤ Submodule.spanRank I
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- `IsGaloisGroup` for rings implies `IsGaloisGroup` for their fraction fields.  -/
IsGaloisGroup.to_isFractionRing_of_isIntegral : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [inst : Group G] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : MulSemiringAction G B] [inst_4 : Algebra A B] [inst_5 : Field K] [inst_6 : Field L]
  [inst_7 : Algebra K L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : Algebra A L] [IsFractionRing A K]
  [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_15 : MulSemiringAction G L]
  [SMulDistribClass G B L] [Algebra.IsIntegral A B] [hGAB : IsGaloisGroup G A B], IsGaloisGroup G K L
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instVAddCommClass' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass M (Lex N) α
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.eq_1 : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t')
  (t : ℕ),
  SimpleGraph.ErdosStone.filter✝ K t = {v ∉ K.verts | ∀ p ∈ K.parts, ∃ s ∈ Finset.powersetCard t p, ∀ w ∈ s, G.Adj v w}
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projective_iff_subsingleton_ext_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  [inst_2 : CategoryTheory.HasExt C],
  CategoryTheory.Projective X ↔ ∀ ⦃Y : C⦄, Subsingleton (CategoryTheory.Abelian.Ext X Y 1)
-- Mathlib.Topology.Algebra.MulAction
/-- Eta-expanded form of `ContinuousOn.smul` -/
ContinuousOn.fun_smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {s : Set Y},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun i => f i • g i) s
-- Lean.Meta.Tactic.Grind.Extension
/-- A theorem for heuristic instantiation based on E-matching.  -/
Lean.Meta.Grind.EMatchTheorem : Type
-- Init.Data.Nat.Lcm
Nat.lcm_eq_zero_iff : ∀ {m n : ℕ}, m.lcm n = 0 ↔ m = 0 ∨ n = 0
-- Lean.Parser.Basic
Lean.Parser.takeUntilFn : (Char → Bool) → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom : ∀ {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] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D)
  (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))),
  ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).hom =
    CategoryTheory.CostructuredArrow.hom P.fiber