mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.smul'_mul : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {T : Type u_1} [inst_1 : CommSemiring T] [inst_2 : Algebra R T]
  [inst_3 : IsLocalization S T] {A : Type u_3} [inst_4 : Semiring A] [inst_5 : Algebra R A] (x : T)
  (p₁ p₂ : LocalizedModule S A), x • p₁ * p₂ = x • (p₁ * p₂)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
HasOuterApproxClosed.indicator_le_apprSeq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ℕ),
  (F.indicator fun x => 1) ≤ ⇑(hF.apprSeq n)
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_one : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : One M], sInf 1 = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.head?_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [Std.LawfulEqOrd α],
  t.WF → t.keys.head? = t.minKey?
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1
-- Mathlib.Order.Filter.Pi
Filter.eventually_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {p : (i : ι) → α i → Prop} [Finite ι],
  (∀ (i : ι), ∀ᶠ (x : α i) in f i, p i x) → ∀ᶠ (x : (i : ι) → α i) in Filter.pi f, ∀ (i : ι), p i (x i)
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (a : K) (b : J) {Z : C}
  (h : (CategoryTheory.Limits.colimit F.flip).obj b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.limit F) a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitIso F).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.colimit F.flip) b)
          h)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι F.flip a).app b) h)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.nsmul : {α : Type u} →
  [inst : Lean.Grind.NatModule α] → ℕ → Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α
-- Mathlib.FieldTheory.Separable
Polynomial.separable_X_add_C : ∀ {R : Type u} [inst : CommSemiring R] (a : R), (Polynomial.X + Polynomial.C a).Separable
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_neg_Ici : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : AddCommGroup G] [IsOrderedAddMonoid G] [MeasurableNeg G] [μ.IsNegInvariant]
  {c : G} {f : G → F},
  MeasureTheory.IntegrableOn f (Set.Iic (-c)) μ → MeasureTheory.IntegrableOn (fun x => f (-x)) (Set.Ici c) μ
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  (X : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A) (X_1 : Cᵒᵖ),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.counitIso.hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj X_1)
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms a list of keys into a tree map.  -/
Std.ExtDTreeMap.Const.unitOfList : {α : Type u} →
  List α →
    (cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap.Const.unitOfList._auto_1) →
      Std.ExtDTreeMap α (fun x => Unit) cmp
-- Mathlib.Topology.Category.LightProfinite.Injective
/-- This is the key statement for the inductive proof of injectivity of light profinite spaces.
Given a commutative square
```
X >-f->  Y
|g       |g'
v        v
S -f'->> T
```
where `Y` is profinite, `S` is finite, `f` is injective and `f'` is surjective,
there exists a diagonal map `k : Y → S` making the diagram commute.
 -/
Profinite.exists_lift_of_finite_of_injective_of_surjective : ∀ {X : Type u_1} {Y : Type u_2} {S : Type u_3} {T : Type u_4} [inst : TopologicalSpace X] [CompactSpace X]
  [inst_2 : TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace Y] [inst_6 : TopologicalSpace S]
  [T2Space S] [Finite S] [inst_9 : TopologicalSpace T] [T2Space T] (f : X → Y),
  Continuous f →
    Function.Injective f →
      ∀ (f' : S → T),
        Function.Surjective f' →
          ∀ (g : X → S),
            Continuous g → ∀ (g' : Y → T), Continuous g' → g' ∘ f = f' ∘ g → ∃ k, Continuous k ∧ f' ∘ k = g' ∧ k ∘ f = g
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.map_mem_map : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (S : IntermediateField K L) (f : L →ₐ[K] L') {x : L},
  f x ∈ IntermediateField.map f S ↔ x ∈ S
-- Mathlib.Algebra.GCDMonoid.Finset
/-- Least common multiple of a finite set  -/
Finset.lcm : {α : Type u_2} → {β : Type u_3} → [inst : CommMonoidWithZero α] → [NormalizedGCDMonoid α] → Finset β → (β → α) → α
-- Std.Do.WP.SimpLemmas
Std.Do.WP.readThe_MonadReaderOf : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ : Type u} {Q : Std.Do.PostCond ρ ps} [inst : MonadReaderOf ρ m]
  [inst_1 : Std.Do.WP m ps], (Std.Do.wp (readThe ρ)).apply Q = (Std.Do.wp MonadReaderOf.read).apply Q
-- Mathlib.Algebra.Free
FreeSemigroup.of_tail : ∀ {α : Type u} (x : α), (FreeSemigroup.of x).tail = []
-- Init.Data.SInt.Lemmas
Int16.zero_ne_one : 0 ≠ 1
-- Mathlib.Analysis.Convex.Between
Wbtw.sameRay_vsub_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z → SameRay R (y -ᵥ x) (z -ᵥ x)
-- Mathlib.Topology.MetricSpace.Isometry
/-- On pseudometric spaces, a map is an isometry if and only if it preserves nonnegative
distances.  -/
isometry_iff_nndist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y
-- Lean.ProjFns
Lean.addProjectionFnInfo : Lean.Environment → Lean.Name → Lean.Name → ℕ → ℕ → Bool → Lean.Environment
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.div_sInter_subset : ∀ {α : Type u_2} [inst : Div α] (s : Set α) (T : Set (Set α)), s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- The localizer morphism that is given by the "inclusion functor"
`HomotopyCategory.Plus (InjectiveObject C) ⥤ HomotopyCategory.Plus C`.
The target category is equipped with the class of quasi-isomorphisms while
the source category `HomotopyCategory.Plus (InjectiveObject C)` is equipped
with the class of isomorphisms (which is exactly the same as quasi-isomorphisms).  -/
HomotopyCategory.Plus.localizerMorphism : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.LocalizerMorphism
        (CategoryTheory.MorphismProperty.isomorphisms (HomotopyCategory.Plus (CategoryTheory.InjectiveObject C)))
        (HomotopyCategory.Plus.quasiIso C)
-- Mathlib.Tactic.CrossRefAttribute
/-- The `wikidata` attribute.
Use it as `@[wikidata Q12345 "Optional comment"]` to associate a Mathlib declaration with
the corresponding [Wikidata](https://www.wikidata.org) item.

The identifier must be the letter `Q` followed by one or more digits.
 -/
Mathlib.CrossRef.wikidataTag : Lean.ParserDescr
-- Init.Data.Nat.Basic
Nat.le_of_sub_eq_zero : ∀ {n m : ℕ}, n - m = 0 → n ≤ m
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncFinset_of_mem : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (p : MvPowerSeries σ R),
  x ∈ s → MvPolynomial.coeff x ((MvPowerSeries.truncFinset R s) p) = (MvPowerSeries.coeff x) p
-- Mathlib.Order.MinMax
Antitone.map_max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
  Antitone f → f (max a b) = min (f a) (f b)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.of.eq_1 : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : C), CategoryTheory.ForgetEnrichment.of W X = X
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.vadd' : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      [inst : AddMonoid R] →
        [inst_1 : AddAction R M] →
          [inst_2 : VAdd S R] → [inst_3 : VAdd S M] → [VAddAssocClass S R M] → (p : SubAddAction R M) → VAdd S ↥p
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app : ∀ {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_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] (X : C)
  (a b : A) (h : a + b = 0),
  F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).inv.app X))
        ((CategoryTheory.Functor.commShiftIso F b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)))
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.symm_subLeft : ∀ {G : Type u_5} [inst : AddCommGroup G] (a : G), (Equiv.subLeft a).symm = Equiv.subLeft a
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a positive multiple of a vector and a vector.  -/
InnerProductGeometry.angle_smul_left_of_pos : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
  0 < r → InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle x y
-- Mathlib.Order.RelIso.Basic
RelIso.injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), Function.Injective ⇑e
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_join_le_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R T : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) T →
    Lean.Order.PartialOrder.rel (Lean.Order.meet P R) T →
      Lean.Order.PartialOrder.rel (Lean.Order.meet P (Lean.Order.join Q R)) T
-- Init.Data.List.Basic
/-- The list has no duplicates: it contains every element at most once.

It is defined as `Pairwise (· ≠ ·)`: each element is unequal to all other elements.
 -/
List.Nodup : {α : Type u} → List α → Prop
-- Mathlib.Algebra.Group.Basic
eq_inv_iff_mul_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a = b⁻¹ ↔ a * b = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_list_unit : ∀ {α : Type u} [inst : BEq α] {l : List ((_ : α) × Unit)} {k : α},
  Std.Internal.List.getValue? k l = if Std.Internal.List.containsKey k l = true then some () else none
-- Lean.Expr
Lean.instHashableBinderInfo : Hashable Lean.BinderInfo
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.isCompact_closedBall : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K] [IsNonarchimedeanLocalField K]
  (γ : ValuativeRel.ValueGroupWithZero K), IsCompact {x | (ValuativeRel.valuation K) x ≤ γ}
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Restricting scalars along the identity is isomorphic to the identity.  -/
AlgCat.restrictScalarsId' : {R : Type u_1} →
  [inst : CommRing R] →
    (f : R →+* R) → f = RingHom.id R → (AlgCat.restrictScalars f ≅ CategoryTheory.Functor.id (AlgCat R))
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wPathDestRight_wPathCasesOn : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B a → P.last.W}
  (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α),
  P.wPathDestRight (P.wPathCasesOn g' g) = g
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The map `f ↦ (x ↦ g x • f x)` as a continuous `𝕜`-linear map on Schwartz space,
where `g` is a function of temperate growth.  -/
SchwartzMap.smulLeftCLM : {𝕜 : Type u_2} →
  {E : Type u_5} →
    (F : Type u_6) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : NontriviallyNormedField 𝕜] →
                [inst_5 : NormedAlgebra ℝ 𝕜] →
                  [inst_6 : NormedSpace 𝕜 F] → (E → 𝕜) → SchwartzMap E F →L[𝕜] SchwartzMap E F
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_add : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2]
  (f g : P1 →ᵃ[k] V2), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_map_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  {Y X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L')}
  (f : Y ⟶ X),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.map f).left =
    CategoryTheory.CategoryStruct.id Y.left
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientAtFilter_iff_isLittleO : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F},
  HasGradientAtFilter f f' x L ↔ (fun x' => f x' - f x - inner 𝕜 f' (x' - x)) =o[L] fun x' => x' - x
-- Mathlib.Algebra.Free
FreeMagma.length_toFreeSemigroup : ∀ {α : Type u} (x : FreeMagma α), (FreeMagma.toFreeSemigroup x).length = x.length
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.add_right : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T} (α β : u ⟶ v),
  CategoryTheory.Arrow.Hom.right (α + β) = CategoryTheory.Arrow.Hom.right α + CategoryTheory.Arrow.Hom.right β
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_eq_univ : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ↑H = Set.univ ↔ H = ⊤
-- Mathlib.Algebra.Quaternion
/-- There is a natural equivalence when swapping the first and third coefficients of a
quaternion algebra if `c₂` is 0.  -/
QuaternionAlgebra.swapEquiv : {R : Type u_3} → (c₁ c₃ : R) → [inst : CommRing R] → QuaternionAlgebra R c₁ 0 c₃ ≃ₐ[R] QuaternionAlgebra R c₃ 0 c₁
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- At every point `x`, for all `y > x` sufficiently close to `x`,
we have `toIocDiv hp a y = toIcoDiv hp a x`.

Note that we use different functions on the LHS and on the RHS.
 -/
eventuallyEq_toIocDiv_nhdsGT : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  toIocDiv hp a =ᶠ[nhdsWithin x (Set.Ioi x)] fun x_1 => toIcoDiv hp a x
-- Mathlib.RingTheory.KrullDimension.Polynomial
/-- If `R` is Noetherian, `dim R[X₁, ..., Xₙ] = dim R + n`.  -/
MvPolynomial.ringKrullDim_of_isNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {ι : Type u_2} [Finite ι],
  ringKrullDim (MvPolynomial ι R) = ringKrullDim R + ↑(Nat.card ι)
-- Mathlib.Algebra.Order.Group.Equiv
coe_ofLexAddEquiv : ∀ (α : Type u_1) [inst : Add α], ⇑(ofLexAddEquiv α) = ⇑ofLex
-- Init.Data.SInt.Lemmas
Int8.toInt16_le : ∀ {a b : Int8}, a.toInt16 ≤ b.toInt16 ↔ a ≤ b
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- Reduction lemma for integral FixedDetMatrices.  -/
FixedDetMatrices.reduce_rec : {m : ℤ} →
  {C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3} →
    ((A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A) →
      ((A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (FixedDetMatrices.reduceStep A) → C A) →
        (A : FixedDetMatrix (Fin 2) ℤ m) → C A
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- A natural transformation gives a natural transformation between the pushforward functors.  -/
SheafOfModules.pushforwardNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F G : CategoryTheory.Functor C D} →
              {T : CategoryTheory.Sheaf J RingCat} →
                {S : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    [inst_3 : G.IsContinuous J K] →
                      (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) →
                        (α : F ⟶ G) →
                          SheafOfModules.pushforward φ ⟶
                            SheafOfModules.pushforward
                              (CategoryTheory.CategoryStruct.comp φ
                                ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans α RingCat J K).app S))
-- Mathlib.Algebra.Star.StarProjection
/-- **Alias** of the forward direction of `isStarProjection_one_sub_iff`. -/
IsStarProjection.of_one_sub : ∀ {R : Type u_1} {p : R} [inst : NonAssocRing R] [inst_1 : StarRing R], IsStarProjection (1 - p) → IsStarProjection p
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp f =
    CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp f
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_finset_sup_eq_iInter : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ},
  0 ≤ r → (s.sup p).closedBall x r = ⋂ i ∈ s, (p i).closedBall x r
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsAtom.nonempty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  K < 1 → S.Nonempty → Finset.IsAtom✝ K S A → A.Nonempty
-- Mathlib.Algebra.Torsor.Defs
AddTorsor.subsingleton_iff : ∀ (G : Type u_1) (P : Type u_2) [inst : AddGroup G] [AddTorsor G P], Subsingleton G ↔ Subsingleton P
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The morphisms between two vertices `x`, `y` in `HomotopyCategory₂ A` are homotopy classes
of edges between `x` and `y`.
 -/
SSet.Truncated.HomotopyCategory₂.Hom : {A : SSet.Truncated 2} → [A.Quasicategory₂] → A.HomotopyCategory₂ → A.HomotopyCategory₂ → Type u_1
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.nontrivial_of_three_le_card : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], 3 ≤ Nat.card α → Nontrivial ↥(alternatingGroup α)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isRadical_iInf : ∀ {R : Type u} [inst : CommSemiring R] {ι : Sort u_2} (I : ι → Ideal R),
  (∀ (i : ι), (I i).IsRadical) → (⨅ i, I i).IsRadical
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.refl : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.AbsolutelyContinuous μ
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : IsDedekindDomain S] [q.LiesOver p],
  Ideal.map (algebraMap R S) p ≠ ⊥ →
    q.ramificationIdx R = Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) p))
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
pairSelfAdjointMatricesSubmodule.eq_1 : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J J₂ : Matrix n n R)
  [inst_2 : DecidableEq n],
  pairSelfAdjointMatricesSubmodule J J₂ =
    Submodule.map (↑LinearMap.toMatrix')
      (((Matrix.toLinearMap₂' R) J).isPairSelfAdjointSubmodule ((Matrix.toLinearMap₂' R) J₂))
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.zero_lt_pairingIn_iff' : ∀ {ι : 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) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [IsStrictOrderedRing S] [inst_8 : Algebra S R] [FaithfulSMul S R]
  [inst_10 : Module S M] [IsScalarTower S R M] [inst_12 : P.IsValuedIn S] {i j : ι} [Finite ι],
  0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i
-- Init.SimpLemmas
Lean.arrow_true_congr : ∀ (α : Sort u) (p : Prop), p = True → Lean.Arrow α p = True
-- Mathlib.Algebra.Group.Submonoid.MulAction
/-- The action by a submonoid is the action by the underlying monoid.  -/
Submonoid.mulAction : {M' : Type u_1} → {α : Type u_2} → [inst : Monoid M'] → [MulAction M' α] → (S : Submonoid M') → MulAction (↥S) α
-- Init.Data.Array.InsertIdx
Array.getElem_insertIdx_of_gt : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (w : k ≤ xs.size) (h : k > i), (xs.insertIdx i x ⋯)[k] = xs[k - 1]
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod : ∀ {n : ℕ} {R : Type u_1} [inst : CommRing R] (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R},
  (∀ (i j : Fin n), f i j = -f j i) → ∏ i, ∏ j > i, f (σ i) (σ j) = ↑↑(Equiv.Perm.sign σ) * ∏ i, ∏ j > i, f i j
-- Mathlib.RingTheory.Finiteness.Basic
/-- Finitely generated submodules are precisely compact elements in the submodule lattice.  -/
Submodule.fg_iff_compact : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Submodule R M), s.FG ↔ IsCompactElement s
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
/-- An n x n matrix over a field has a finite spectrum.  -/
Matrix.finite_spectrum : ∀ {n : Type u_1} {R : Type u_2} [inst : Field R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n R),
  (spectrum R A).Finite
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- Tensoring an exact pair on the right gives an exact pair  -/
rTensor_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q],
  Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → Function.Exact ⇑(LinearMap.rTensor Q f) ⇑(LinearMap.rTensor Q g)