mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- `f : M → N` is called a **`C^n` local diffeomorphism on `s`** iff it is a local diffeomorphism
at each `x : s`.  -/
IsLocalDiffeomorphOn : {𝕜 : 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] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        ModelWithCorners 𝕜 E H₁ →
                          ModelWithCorners 𝕜 F H₂ →
                            {M : Type u_8} →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst : TopologicalSpace N] →
                                      [ChartedSpace H₂ N] → WithTop ℕ∞ → (M → N) → Set M → Prop
-- Init.Data.Int.Gcd
Int.gcd_add_self_left : ∀ (m n : ℤ), (n + m).gcd m = n.gcd m
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkip?_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.copy.revSkip? pat = Option.map String.Slice.Pos.copy (pos.revSkip? pat)
-- Batteries.Lean.AttributeExtra
/-- Gets the parameter of attribute `attr` associated to declaration `decl`,
or `none` if `decl` is not tagged.
 -/
Lean.ParametricAttributeExtra.getParam? : {α : Type} → [Inhabited α] → Lean.ParametricAttributeExtra α → Lean.Environment → Lean.Name → Option α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shiftLinearMap_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type u_1)
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a : ℤ)
  (a_1 : CochainComplex.HomComplex.Cochain K L n),
  (CochainComplex.HomComplex.Cochain.shiftLinearMap R K L n a) a_1 = a_1.shift a
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor `F` preserves finite coproducts if it reflects colimits of shape `Discrete J`
for finite `J`.

We require this for `J = Fin n` in the definition,
then generalize to `J : Type u` in the instance.
 -/
CategoryTheory.Limits.ReflectsFiniteCoproducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Batteries.Util.ProofWanted
/-- Reducible accessor so a binder of type `ProofWanted.Stmt foo` reduces to `foo`'s
statement. Used by the desugaring of `❰foo❱` when `foo` is a `proof_wanted`.  -/
ProofWanted.Stmt : {α : Sort u} → ProofWanted α → Sort u
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_mono : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  (∀ x ∈ quasispectrum R a, f x ≤ g x) →
    autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_mono._auto_1 →
      autoParam (ContinuousOn g (quasispectrum R a)) cfcₙ_mono._auto_3 →
        autoParam (f 0 = 0) cfcₙ_mono._auto_5 → autoParam (g 0 = 0) cfcₙ_mono._auto_7 → cfcₙ f a ≤ cfcₙ g a
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_pos : ∀ (n : ℕ), 0 < n.minFac
-- Mathlib.CategoryTheory.GlueData
/-- Indexing type of a glue data.  -/
CategoryTheory.GlueData'.J : {C : Type u₁} → [inst : CategoryTheory.Category.{v, u₁} C] → CategoryTheory.GlueData' C → Type v
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.A_mono : ∀ {𝕜 : 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}
  (L : E →L[𝕜] F) (r : ℝ) {ε δ : ℝ}, ε ≤ δ → FDerivMeasurableAux.A f L r ε ⊆ FDerivMeasurableAux.A f L r δ
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl.params : Lean.Elab.Term.Do.JPDecl → Array (Lean.Elab.Term.Do.Var × Bool)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.coe_toHomotopy : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P), ⇑F.toHomotopy = ⇑F
-- Mathlib.Data.Set.Lattice
Set.disjoint_iUnion_right : ∀ {α : Type u_1} {t : Set α} {ι : Sort u_12} {s : ι → Set α}, Disjoint t (⋃ i, s i) ↔ ∀ (i : ι), Disjoint t (s i)
-- Lean.Syntax
/-- Advance to the right sibling of the current node, if any.  -/
Lean.Syntax.Traverser.right : Lean.Syntax.Traverser → Lean.Syntax.Traverser
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.hcongr_5 : ∀ (motive motive' : ℕ → Sort u_1),
  motive = motive' →
    ∀ (x x' : ℕ),
      x = x' →
        ∀ (h_1 : Unit → motive 0) (h_1' : Unit → motive' 0),
          h_1 ≍ h_1' →
            ∀ (h_2 : Unit → motive 1) (h_2' : Unit → motive' 1),
              h_2 ≍ h_2' →
                ∀ (h_3 : (x : ℕ) → motive x) (h_3' : (x : ℕ) → motive' x),
                  h_3 ≍ h_3' →
                    (match x with
                      | 0 => h_1 ()
                      | 1 => h_2 ()
                      | x => h_3 x) ≍
                      match x' with
                      | 0 => h_1' ()
                      | 1 => h_2' ()
                      | x => h_3' x
-- Init.Data.SInt.Lemmas
Int8.ofIntClamp_bitVecToInt : ∀ (n : BitVec 8), Int8.ofIntClamp n.toInt = Int8.ofBitVec n
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabEndLocalScope : Lean.Elab.Command.CommandElab
-- Mathlib.RingTheory.Ideal.Maps
AlgHom.comap_ker : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {C : Type u_4} [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : B →ₐ[R] C) (g : A →ₐ[R] B), Ideal.comap g (RingHom.ker f) = RingHom.ker (f.comp g)
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.add_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsLowerSet s → IsLowerSet (s + t)
-- Mathlib.Topology.Sober
IsIrreducible.genericPoint_closure_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] {S : Set α} (hS : IsIrreducible S),
  closure {hS.genericPoint} = closure S
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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} (b : P.Base)
  [Finite ι] [IsAddTorsionFree M] [IsAddTorsionFree N],
  ∀ i ∈ b.support, ∀ (t : R), t • P.root i ∈ Set.range ⇑P.root → ∃ z, ↑z * t = 1
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Nest `p` in one pair of brackets, i.e. `x` becomes `(x)`.  -/
DyckWord.nest : DyckWord → DyckWord
-- Init.Data.Int.Order
Int.toNat_mul : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (a * b).toNat = a.toNat * b.toNat
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_iff_add : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J ↔ I + J = 1
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_succ_right_eq : ∀ (n k : ℕ), n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
-- Init.Grind.Ordered.Ring
/-- In a strict ordered semiring, we can multiply an inequality `a < b` on the left
by a positive element `0 < c` to obtain `c * a < c * b`.  -/
Lean.Grind.OrderedRing.mul_lt_mul_of_pos_left : ∀ {R : Type u} {inst : Lean.Grind.Semiring R} {inst_1 : LE R} {inst_2 : LT R} {inst_3 : Std.IsPreorder R}
  [self : Lean.Grind.OrderedRing R] {a b c : R}, a < b → 0 < c → c * a < c * b
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
CategoryTheory.Limits.isGrothendieckAbelian_ind : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} (CategoryTheory.Ind C)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_union₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      MeasureTheory.IntegrableOn f s μ →
        MeasureTheory.IntegrableOn f t μ → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
-- Mathlib.Algebra.Group.Ext
AddCommGroup.ext_iff : ∀ {G : Type u_1} {g₁ g₂ : AddCommGroup G}, g₁ = g₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMapIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  (CategoryTheory.ShortComplex.homologyMapIso e).inv = CategoryTheory.ShortComplex.homologyMap e.inv
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.eventually_meas_ne_zero : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X},
  IsFoelner G μ l F → ∀ᶠ (i : ι) in l, μ (F i) ≠ 0
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.alternatingFaceMapComplex.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  AlgebraicTopology.alternatingFaceMapComplex C =
    { obj := AlgebraicTopology.AlternatingFaceMapComplex.obj,
      map := fun {X Y} f => AlgebraicTopology.AlternatingFaceMapComplex.map f, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Data.List.Defs
List.Forall.eq_1 : ∀ {α : Type u_1} (p : α → Prop), List.Forall p [] = True
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.map_piecewise_smul : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] (c : ι → R) (m : (i : ι) → M₁ i) (s : Finset ι),
  f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
-- Mathlib.Order.InitialSeg
/-- Restrict the codomain of a principal segment embedding.  -/
PrincipalSeg.codRestrict : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        (p : Set β) →
          (f : PrincipalSeg r s) →
            (∀ (a : α), f.toRelEmbedding a ∈ p) → f.top ∈ p → PrincipalSeg r (Subrel s fun x => x ∈ p)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instFaithfulAddGrpFunctorOppositeAddGrpCatYonedaAddGrp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddGrp.Faithful
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instFiniteIdSearchStepOfStrictForwardPattern : ∀ {ρ : Type} (pat : ρ) {s : String.Slice} [inst : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.StrictForwardPattern pat],
  Std.Iterators.Finite (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat s) Id
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainRingHom_comp : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [inst : Semiring R] [inst_1 : AddMonoid M]
  [inst_2 : AddMonoid N] [inst_3 : AddMonoid O] (f : N →+ O) (g : M →+ N),
  AddMonoidAlgebra.mapDomainRingHom R (f.comp g) =
    (AddMonoidAlgebra.mapDomainRingHom R f).comp (AddMonoidAlgebra.mapDomainRingHom R g)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k fallback : α},
  (Std.ExtHashMap.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 m[x_2]).isSome).getD fallback
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_nc.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (m₁ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (pw : Lean.Grind.CommRing.Power) → motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit))
  (h_3 :
    (pw : Lean.Grind.CommRing.Power) → (m₁ : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult pw m₁))
  (pw : Lean.Grind.CommRing.Power) (m₁_1 : Lean.Grind.CommRing.Mon),
  m₁ = Lean.Grind.CommRing.Mon.mult pw m₁_1 →
    (m₁_1 = Lean.Grind.CommRing.Mon.unit → False) →
      (match m₁ with
        | Lean.Grind.CommRing.Mon.unit => h_1 ()
        | Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit => h_2 pw
        | Lean.Grind.CommRing.Mon.mult pw m₁ => h_3 pw m₁) ≍
        h_3 pw m₁_1
-- Init.Data.Nat.Lemmas
/-- The product of two natural numbers is greater than 1 if and only if
at least one of them is greater than 1 and both are positive.  -/
Nat.one_lt_mul_iff : ∀ {m n : ℕ}, 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
-- Mathlib.Tactic.Linter.PrivateModule
/-- The `privateModule` linter lints against nonempty modules that have only private declarations,
and suggests adding `@[expose] public section` or selectively marking declarations as `public`.  -/
Mathlib.Linter.linter.privateModule : Lean.Option Bool
-- Mathlib.Topology.UnitInterval
unitInterval.fract_mem : ∀ (x : ℝ), Int.fract x ∈ unitInterval
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.filterMap_eq_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {γ : α → Type w}
  (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β a → γ a),
  (↑m).WF → Std.DHashMap.Internal.Raw₀.filterMap (fun k v => some (f k v)) m = Std.DHashMap.Internal.Raw₀.map f m
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.map_left : ∀ {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] {J : CategoryTheory.Limits.MulticospanShape}
  (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (i : J.L),
  (d.map F).left i = F.obj (d.left i)
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_gcd_mul_of_dvd_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {m n k : α}, k ∣ m * n → k ∣ gcd k m * n
-- Mathlib.Combinatorics.Graph.Basic
Graph.incidenceSet_subset_edgeSet : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α), Graph.incidenceSet x ⊆ G.edgeSet
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.lift_coe : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : AddZeroClass β] (f : α →ₙ+ β) (x : α), (WithZero.lift f) ↑x = f x
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofNat_le_ofENat : ∀ {m : ℕ} [inst : m.AtLeastTwo] {n : ℕ∞}, OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- `Preregular` is preserved by equivalence of categories.  -/
CategoryTheory.Equivalence.preregular : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preregular C] (e : C ≌ D), CategoryTheory.Preregular D
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.OplaxTrans.Modification η θ) {b c : B}
  {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c) {Z : a' ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app b) (G.map g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app c)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) (G.map g))) h)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.le_int_module : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] (ctx : Lean.Grind.CommRing.Context α)
  (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx p ≤ 0 → Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p ≤ 0
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.prime_degree_dvd_card : ∀ {F : Type u_1} [inst : Field F] {p : Polynomial F} [CharZero F],
  Irreducible p → Nat.Prime p.natDegree → p.natDegree ∣ Nat.card p.Gal
-- Mathlib.Analysis.Normed.Group.Basic
NormedCommGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : CommGroup E] [inst_2 : NormedGroup F]
  [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f),
  NormedCommGroup.induced E F f h =
    { norm := fun a => ‖f a‖, toCommGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Init.Data.UInt.Bitwise
UInt8.toFin_shiftLeft : ∀ (a b : UInt8), b < 8 → (a <<< b).toFin = a.toFin <<< b.toFin
-- Mathlib.Tactic.NoncommRing
Mathlib.Tactic.NoncommRing.nat_lit_mul_eq_nsmul : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (r : R) (n : ℕ) [inst_1 : n.AtLeastTwo],
  OfNat.ofNat n * r = OfNat.ofNat n • r
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_eq_false_of_mod_ne_zero : ∀ {a b : ℤ}, (b % a != 0) = true → (a ∣ b) = False
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMapIso'_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  (CategoryTheory.ShortComplex.opcyclesMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.opcyclesMap' e.inv h₂ h₁
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∈ t₂ → (t₁ ∩ t₂)[k]! = t₁[k]!
-- Lean.DocString.Parser
Lean.Doc.Parser.InlineCtxt.mk.sizeOf_spec : ∀ (allowNewlines : Bool) (minIndent : ℕ) (boldDepth emphDepth : Option ℕ) (inLink : Bool),
  sizeOf
      { allowNewlines := allowNewlines, minIndent := minIndent, boldDepth := boldDepth, emphDepth := emphDepth,
        inLink := inLink } =
    1 + sizeOf allowNewlines + sizeOf minIndent + sizeOf boldDepth + sizeOf emphDepth + sizeOf inLink
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_span_singleton : ∀ {R : Type u} [inst : Semiring R] (r s : R) [(Ideal.span {r}).IsTwoSided],
  Ideal.span {r} * Ideal.span {s} = Ideal.span {r * s}
-- Mathlib.Topology.Separation.Basic
TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {b : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {x y : X}, x ≠ y → ∃ a ∈ b, x ∈ a ∧ y ∉ a
-- Mathlib.Algebra.Group.Defs
mul_inv_cancel_right : ∀ {G : Type u_1} [inst : Group G] (a b : G), a * b * b⁻¹ = a
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_eq : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p},
  (∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)) → f.norm = g.norm
-- Lean.Expr
Lean.instEmptyCollectionFVarIdHashSet : EmptyCollection Lean.FVarIdHashSet
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.eval_monoidalComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b} {η η' : f ⟶ g} {α : g ≅ h}
  {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i},
  η = η' →
    θ = θ' →
      CategoryTheory.CategoryStruct.comp α.hom θ' = αθ →
        CategoryTheory.CategoryStruct.comp η' αθ = ηαθ →
          CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRight_map_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  {X Y : CategoryTheory.MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapRight L r hr).map f).right =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).right
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- Note that `degreeOf_mul_eq` proves equality with `NoZeroDivisors R` and nonzero polynomials.
 -/
MvPolynomial.degreeOf_prod_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R),
  MvPolynomial.degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, MvPolynomial.degreeOf i (f j)
-- Mathlib.Util.Notation3
Mathlib.Notation3.BoundValueType.noConfusionType : Sort v✝ → Mathlib.Notation3.BoundValueType → Mathlib.Notation3.BoundValueType → Sort v✝
-- Lean.Meta.Tactic.Grind.Types
/-- Next unique index for creating ENodes  -/
Lean.Meta.Grind.GoalState.nextIdx : Lean.Meta.Grind.GoalState → ℕ
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.dpEqualizer.eq_1 : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I),
  hI.dpEqualizer hI' =
    { carrier := {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.contains_insertList_of_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k toInsert = true →
    Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true
-- Mathlib.Data.Int.Bitwise
Int.bitwise_or : Int.bitwise or = Int.lor
-- Init.RCases
/-- `x` is a pattern which binds `x`  -/
Lean.Parser.Tactic.rcasesPat.one : Lean.ParserDescr