mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.Examples
CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl : ∀ (G : Type u) [inst : Group G] {X Y : Action FintypeCat G} (f : X ⟶ Y),
  CategoryTheory.Mono (CategoryTheory.FintypeCat.Action.imageComplementIncl G f)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) [inst_1 : E.Small],
  E.restrictIndexOfSmall.toPreZeroHypercover =
    E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_nsmul_subset : ∀ {α : Type u_2} [inst : AddMonoid α] {s t : Set α} {n : ℕ}, n • (s ∩ t) ⊆ n • s ∩ n • t
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  (Std.HashMap.filterMap f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.partition_one_parts : ∀ (p : Nat.Partition 1), p.parts = {1}
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.colon ↑⊥ = ⊤
-- Init.Data.Iterators.Basic
Std.PlausibleIterStep.skip.congr_simp : ∀ {α : Type u} {β : Type w} {IsPlausibleStep : Std.IterStep α β → Prop} (it' it'_1 : α) (e_it' : it' = it'_1)
  (h : IsPlausibleStep (Std.IterStep.skip it')), Std.PlausibleIterStep.skip it' h = Std.PlausibleIterStep.skip it'_1 ⋯
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.zero_tprodCoeff : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (f : (i : ι) → s i), PiTensorProduct.tprodCoeff R 0 f = 0
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- If `F : C → Type v`, then the data of a "type-theoretic" cofan of `F`
with a point in `Type v` is the same as the data of a cocone (in a categorical sense).  -/
CategoryTheory.Limits.Cofan.cofanTypes : {C : Type u} → {F : C → Type v} → CategoryTheory.Limits.Cofan F → CategoryTheory.Limits.CofanTypes F
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that the action of `M` on `α` has `MeasurableSMul` if for each `c` the map `x ↦ c • x`
is a measurable function and for each `x` the map `c ↦ c • x` is a measurable function.  -/
MeasurableSMul : (M : Type u_2) → (α : Type u_3) → [SMul M α] → [MeasurableSpace M] → [MeasurableSpace α] → Prop
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_mem_subspace_eq_self`.

---

The orthogonal projection sends elements of `K` to themselves.  -/
Submodule.orthogonalProjection_mem_subspace_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (v : ↥K), K.orthogonalProjectionOnto ↑v = v
-- Mathlib.Dynamics.OmegaLimit
/-- the ω-limit of a forward image of `s` is the same as the ω-limit of `s`.  -/
Flow.omegaLimit_image_eq : ∀ {τ : Type u_1} [inst : TopologicalSpace τ] [inst_1 : AddCommGroup τ] {α : Type u_2} [inst_2 : TopologicalSpace α]
  (f : Filter τ) (ϕ : Flow τ α) (s : Set α),
  (∀ (t : τ), Filter.Tendsto (fun x => x + t) f f) →
    ∀ (t : τ), omegaLimit f ϕ.toFun (ϕ.toFun t '' s) = omegaLimit f ϕ.toFun s
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F)
  (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)}
  (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) {Z : A}
  (h : (E.multicospanIndex P).left a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (CategoryTheory.CategoryStruct.comp (c.ι a) h) =
    CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (CategoryTheory.CategoryStruct.comp (P.map (f.h₀ a).op) h)
-- Mathlib.Algebra.Group.Defs
isAddLeftRegular_iff_isAddRegular : ∀ {G : Type u_1} [inst : AddCommMagma G] {a : G}, IsAddLeftRegular a ↔ IsAddRegular a
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_iff_isOpen_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : Preorder β],
  UpperSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Iio y)
-- Mathlib.Algebra.Group.Units.Hom
isLocalHom_of_leftInverse : ∀ {G : Type u_1} {R : Type u_2} {S : Type u_3} {F : Type u_5} [inst : Monoid R] [inst_1 : Monoid S]
  [inst_2 : FunLike F R S] [MonoidHomClass F R S] [inst_4 : FunLike G S R] [MonoidHomClass G S R] {f : F} (g : G),
  Function.LeftInverse ⇑g ⇑f → IsLocalHom f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.extensions : Lean.Meta.Grind.Context → Lean.Meta.Grind.ExtensionStateArray
-- Mathlib.RingTheory.Norm.Transitivity
/-- Let A/S/R be a tower of finite free tower of rings (with R and S commutative).
Then $\text{Norm}_{A/R} = \text{Norm}_{A/S} \circ \text{Norm}_{S/R}$.  -/
Algebra.norm_norm : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Free R S]
  {A : Type u_6} [inst_4 : Ring A] [inst_5 : Algebra R A] [inst_6 : Algebra S A] [IsScalarTower R S A] [Module.Free S A]
  {a : A}, (Algebra.norm R) ((Algebra.norm S) a) = (Algebra.norm R) a
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.fst : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {f : α → β × γ},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).1) μ
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
Subgroup.isClosed_of_discrete : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H : Subgroup G}
  [DiscreteTopology ↥H], IsClosed ↑H
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSMul.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → SMul R (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)],
  DirectLimit.instSMul = { smul := fun r => DirectLimit.map f f (fun x x_1 => r • x_1) ⋯ }
-- Mathlib.Condensed.Discrete.Basic
/-- A version of `LightCondensed.underlying` in the `LightCondSet` namespace  -/
LightCondSet.underlying : CategoryTheory.Functor (LightCondensed (Type u)) (Type u)
-- Mathlib.Algebra.DirectSum.Module
/-- The projection map onto one component, as a linear map.  -/
DirectSum.component : (R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      (M : ι → Type w) →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → (i : ι) → (DirectSum ι fun i => M i) →ₗ[R] M i
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), Function.Injective ⇑e
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- If `it` plausibly yields in its immediate next step, this step is a plausible `0`-th output step.  -/
Std.IterM.IsPlausibleNthOutputStep.zero_yield : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it' : Std.IterM m β} {out : β}
  {it : Std.IterM m β},
  it.IsPlausibleStep (Std.IterStep.yield it' out) → Std.IterM.IsPlausibleNthOutputStep 0 it (Std.IterStep.yield it' out)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.baseChangeToBaseChange_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (x : (Algebra.Generators.baseChange T P).toExtension.Ring),
  (P.baseChangeToBaseChange T).toRingHom x = (MvPolynomial.algebraTensorAlgEquiv R T).symm x
-- Mathlib.Topology.Algebra.Star
continuousOn_star : ∀ {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R] {s : Set R}, ContinuousOn star s
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂),
  CategoryTheory.CategoryStruct.comp self.f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ self.f₃
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_le_map_iff_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f → ∀ {S T : AddSubsemigroup M}, AddSubsemigroup.map f S ≤ AddSubsemigroup.map f T ↔ S ≤ T
-- Mathlib.Algebra.Homology.Opposite
/-- The natural isomorphism `K.op.opcycles i ≅ op (K.cycles i)`.  -/
HomologicalComplex.opcyclesOpNatIso : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          [inst_2 : CategoryTheory.CategoryWithHomology V] →
            (i : ι) →
              (HomologicalComplex.opFunctor V c).comp (HomologicalComplex.opcyclesFunctor Vᵒᵖ c.symm i) ≅
                (HomologicalComplex.cyclesFunctor V c i).op
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic.0.Std.Tactic.BVDecide.Gate.toString.match_1.eq_1 : ∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.and with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_1 ()
-- Init.Meta.Defs
Lean.TSyntax.instCoeIdentTerm : Coe Lean.Ident Lean.Term
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt.0.Int8.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int8)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasSplitMultiplicativeReduction.mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K}
  [toHasMultiplicativeReduction : WeierstrassCurve.HasMultiplicativeReduction R W],
  (Polynomial.map (algebraMap R (IsLocalRing.ResidueField R))
        (Polynomial.C (WeierstrassCurve.integralModel R W).c₄ * Polynomial.X ^ 2 +
            Polynomial.C ((WeierstrassCurve.integralModel R W).a₁ * (WeierstrassCurve.integralModel R W).c₄) *
              Polynomial.X -
          Polynomial.C
            (54 * (WeierstrassCurve.integralModel R W).b₆ -
                3 * (WeierstrassCurve.integralModel R W).b₂ * (WeierstrassCurve.integralModel R W).b₄ +
              (WeierstrassCurve.integralModel R W).a₂ * (WeierstrassCurve.integralModel R W).c₄))).Splits →
    WeierstrassCurve.HasSplitMultiplicativeReduction R W
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.map_id : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (self : CategoryTheory.EnrichedFunctor V C D) (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (self.map X X) = CategoryTheory.eId V (self.obj X)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ GrpCat) (α : (F.comp (CategoryTheory.forget GrpCat)).RepresentableBy X),
  (CategoryTheory.yonedaGrpObjIsoOfRepresentableBy X F α).hom =
    { app := fun X_1 => GrpCat.ofHom ↑{ toEquiv := α.homEquiv, map_mul' := ⋯ }, naturality := ⋯ }
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.instIsCocontinuousOverLeftIteratedSliceBackwardOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (f : CategoryTheory.Over X), f.iteratedSliceBackward.IsCocontinuous (J.over f.left) ((J.over X).over f)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_apply_of_not_continuousOn : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f : R → R} (a : A),
  ¬ContinuousOn f (quasispectrum R a) → cfcₙ f a = 0
-- Mathlib.RingTheory.KrullDimension.Module
support_of_supportDim_eq_zero : ∀ (R : Type u_1) [inst : CommRing R] (N : Type u_3) [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  [inst_3 : IsLocalRing R],
  Module.supportDim R N = 0 → Module.support R N = PrimeSpectrum.zeroLocus ↑(IsLocalRing.maximalIdeal R)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCases.default_1 : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
  (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) {Z_1 : C} (h : J.cocomplex.X 1 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d 1 2)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroOne f comm) h) =
    CategoryTheory.CategoryStruct.comp
      (f.f 1 -
        CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm)
          (J.cocomplex.d 0 1))
      h
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
for extensionality of the ring elements.  -/
IsAdjoinRoot.ext : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h h' : IsAdjoinRoot S f), h.root = h'.root → h = h'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k},
  (t.modify k f).get? k' = if h : cmp k k' = Ordering.eq then cast ⋯ (Option.map f (t.get? k)) else t.get? k'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.pentagon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.associator W X Y).hom
        (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator W (X ⨿ Y) Z).hom
        (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W)
          (CategoryTheory.Limits.coprod.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator (W ⨿ X) Y Z).hom
      (CategoryTheory.Limits.coprod.associator W X (Y ⨿ Z)).hom
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (ij : ι × ι'), (b.smulTower c) ij = b ij.1 • c ij.2
-- Mathlib.Topology.Germ
forall_restrictGermPredicate_of_forall : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y} {A : Set X}
  {P : (x : X) → (nhds x).Germ Y → Prop}, (∀ (x : X), P x ↑f) → ∀ (x : X), RestrictGermPredicate P A x ↑f
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_ground_union : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk (M.E ∪ X) = M.eRank
-- Mathlib.Order.Antichain
IsAntichain.eq : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → ∀ {a b : α}, a ∈ s → b ∈ s → r a b → a = b
-- Mathlib.AlgebraicGeometry.Group.Affine
CategoryTheory.OverClass.asOver.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X S : C) [inst_1 : CategoryTheory.OverClass X S],
  CategoryTheory.OverClass.asOver X S = CategoryTheory.Over.mk (X ↘ S)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ico_sub_one_right_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α}, a < b → insert (b - 1) (Finset.Ico a (b - 1)) = Finset.Ico a b
-- Init.Grind.Lint
/-- `#grind_lint inspect thm₁ …` analyzes the specified theorem(s) individually.

It always prints detailed statistics regardless of thresholds and is useful
for investigating specific `grind` lemmas that may generate excessive
instantiations.
Examples:
```
#grind_lint inspect Array.zip_map
```
You can use `set_option trace.grind.ematch.instance true` to instruct `grind` to display the
actual instances it produces.
 -/
Lean.Grind.grindLintInspect : Lean.ParserDescr
-- Mathlib.GroupTheory.Index
Subgroup.index_strictAnti : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H < K → ∀ [H.FiniteIndex], K.index < H.index
-- Mathlib.Tactic.Ring.Common
/-- `e'` is a monomial.  -/
Mathlib.Tactic.Ring.Common.ExtractCoeff.ve' : {e : Q(ℕ)} → (self : Mathlib.Tactic.Ring.Common.ExtractCoeff e) → Mathlib.Tactic.Ring.Common.ExProdNat self.e'
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.BiconeMorphism.mk.congr_simp : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  (hom hom_1 : A.pt ⟶ B.pt) (e_hom : hom = hom_1)
  (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π j) = A.π j)
  (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom = B.ι j),
  { hom := hom, wπ := wπ, wι := wι } = { hom := hom_1, wπ := ⋯, wι := ⋯ }
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  (Γ : Subgroup (Matrix.SpecialLinearGroup n R)), (Subgroup.map Matrix.SpecialLinearGroup.toGL Γ).HasDetOne
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.GAlgebra.map_one : ∀ {ι : Type uι} {R : Type uR} {A : ι → Type uA} {inst : CommSemiring R} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  {inst_2 : (i : ι) → Module R (A i)} {inst_3 : AddMonoid ι} {inst_4 : DirectSum.GSemiring A}
  [self : DirectSum.GAlgebra R A], DirectSum.GAlgebra.toFun 1 = GradedMonoid.GOne.one
-- Lean.Message
/-- See `MessageData.ofList`.  -/
Lean.MessageData.ofArray : Array Lean.MessageData → Lean.MessageData
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulHom.eq_of_eqOn_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N}, Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Mathlib.CategoryTheory.Action.Limits
Action.zsmul_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {X Y : Action V G} (n : ℤ) (f : X ⟶ Y), (n • f).hom = n • f.hom
-- Mathlib.Analysis.Complex.Basic
RCLike.hasSum_re : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜},
  HasSum f x L → HasSum (fun x => RCLike.re (f x)) (RCLike.re x) L
-- Mathlib.Algebra.Homology.Localization
/-- The homology functor `HomologicalComplexUpToQuasiIso C c ⥤ C` for each `i : ι`.  -/
HomologicalComplexUpToQuasiIso.homologyFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {ι : Type u_2} →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_2 : CategoryTheory.CategoryWithHomology C] →
            [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] →
              ι → CategoryTheory.Functor (HomologicalComplexUpToQuasiIso C c) C
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.ofPairingInThree_short : ∀ {ι : 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) [inst_5 : CharZero R]
  [inst_6 : P.IsCrystallographic] [inst_7 : P.IsReduced] (long short : ι) (h : P.pairingIn ℤ long short = 3),
  RootPairing.EmbeddedG2.short P = short
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.comp_add' : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B C : TopRep k G)
  (f : A ⟶ B) (g h : B ⟶ C),
  CategoryTheory.CategoryStruct.comp f (g + h) =
    CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h
-- Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
FirstOrder.Ring.termOfFreeCommRing.eq_1 : ∀ {α : Type u_1} (p : FreeCommRing α), FirstOrder.Ring.termOfFreeCommRing p = Classical.choose ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- the forward direction of a homotopy equivalence.  -/
CategoryTheory.ShortComplex.HomotopyEquiv.hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → S₁.HomotopyEquiv S₂ → (S₁ ⟶ S₂)
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm_zero_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [_i : Fact (Module.finrank ℝ E = 0)],
  (-positiveOrientation).volumeForm = -AlternatingMap.constLinearEquivOfIsEmpty 1
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The image of an additive group object under a monoidal functor is an additive group object.  -/
CategoryTheory.Functor.addGrpObjObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] → {G : C} → [CategoryTheory.AddGrpObj G] → CategoryTheory.AddGrpObj (F.obj G)