mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Finiteness
/-- If there exists a set `{ r }` of `R` that generates the unit ideal and such that `Mᵣ` is `Rᵣ`-finite
for each `r`, then `M` is a finite `R`-module.

General version for any modules `Mᵣ` and rings `Rᵣ` satisfying the correct universal properties.
See `Module.Finite.of_localizationSpan_finite` for the specialized version.
 -/
Module.Finite.of_localizationSpan' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type w} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (t : Set R),
  Ideal.span t = ⊤ →
    ∀ {Mₚ : ↑t → Type u_1} [inst_3 : (g : ↑t) → AddCommMonoid (Mₚ g)] [inst_4 : (g : ↑t) → Module R (Mₚ g)]
      {Rₚ : ↑t → Type u_2} [inst_5 : (g : ↑t) → CommSemiring (Rₚ g)] [inst_6 : (g : ↑t) → Algebra R (Rₚ g)]
      [h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)] [inst_7 : (g : ↑t) → Module (Rₚ g) (Mₚ g)]
      [∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)] (f : (g : ↑t) → M →ₗ[R] Mₚ g)
      [h₂ : ∀ (g : ↑t), IsLocalizedModule.Away (↑g) (f g)],
      (∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)) → Module.Finite R M
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.Monoidal.hexagon_reverse : ∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X Y Z : CategoryTheory.GradedObject I C)
  [inst_3 : CategoryTheory.BraidedCategory C] [inst_4 : X.HasTensor Y] [inst_5 : Y.HasTensor Z] [inst_6 : Z.HasTensor X]
  [inst_7 : Z.HasTensor Y] [inst_8 : X.HasTensor Z]
  [inst_9 : (CategoryTheory.GradedObject.Monoidal.tensorObj X Y).HasTensor Z]
  [inst_10 : X.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)]
  [inst_11 : Z.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X Y)]
  [inst_12 : (CategoryTheory.GradedObject.Monoidal.tensorObj Z X).HasTensor Y]
  [inst_13 : X.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Z Y)]
  [inst_14 : (CategoryTheory.GradedObject.Monoidal.tensorObj X Z).HasTensor Y] [inst_15 : X.HasGoodTensor₁₂Tensor Y Z]
  [inst_16 : X.HasGoodTensorTensor₂₃ Y Z] [inst_17 : Z.HasGoodTensor₁₂Tensor X Y]
  [inst_18 : Z.HasGoodTensorTensor₂₃ X Y] [inst_19 : X.HasGoodTensor₁₂Tensor Z Y]
  [inst_20 : X.HasGoodTensorTensor₂₃ Z Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.braiding (CategoryTheory.GradedObject.Monoidal.tensorObj X Y) Z).hom
        (CategoryTheory.GradedObject.Monoidal.associator Z X Y).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.whiskerLeft X (CategoryTheory.GradedObject.Monoidal.braiding Y Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X Z Y).inv
        (CategoryTheory.GradedObject.Monoidal.whiskerRight (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom Y))
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.nonempty : ∀ {ι : 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) [P.IsG2], Nonempty ι
-- Mathlib.Data.Matrix.Mul
Matrix.mul_zero : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (M : Matrix m n α), M * 0 = 0
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.SavedLocalContext.savedLocalContext : Lean.Elab.WF.GuessLex.SavedLocalContext → Lean.LocalContext
-- Mathlib.CategoryTheory.Subfunctor.Image
/-- If the image of a morphism falls in a subfunctor, then the morphism factors through it.  -/
CategoryTheory.Subfunctor.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C (Type w)} →
      (f : F' ⟶ F) → {G : CategoryTheory.Subfunctor F} → CategoryTheory.Subfunctor.range f ≤ G → (F' ⟶ G.toFunctor)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- Maps a nonzero fractional ideal to an integral representative in the class group.  -/
ClassGroup.integralRep : {R : Type u_1} → [inst : CommRing R] → FractionalIdeal (nonZeroDivisors R) (FractionRing R) → Ideal R
-- Mathlib.Order.Interval.Set.Infinite
/-- A nonempty preorder with no minimal element is infinite.  -/
NoMinOrder.infinite : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMinOrder α], Infinite α
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k : α} (h : k ∈ m),
  m.getKey k h = k
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.fixingAddSubgroup_of_insert : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (a : α)
  (s : Set ↥(SubAddAction.ofStabilizer M a)),
  fixingAddSubgroup M (insert a ((fun x => ↑x) '' s)) =
    AddSubgroup.map (AddAction.stabilizer M a).subtype (fixingAddSubgroup (↥(AddAction.stabilizer M a)) s)
-- Std.Http.Internal.ChunkedBuffer
/-- Turn the combined structure into a single contiguous ByteArray.
 -/
Std.Http.Internal.ChunkedBuffer.toByteArray : Std.Http.Internal.ChunkedBuffer → ByteArray
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.avgRisk_le_mul : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} (P : ProbabilityTheory.Kernel Θ 𝓧) [ProbabilityTheory.IsMarkovKernel P]
  (κ : ProbabilityTheory.Kernel 𝓧 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (π : MeasureTheory.Measure Θ)
  [MeasureTheory.IsProbabilityMeasure π] {C : NNReal},
  (∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C) → ProbabilityTheory.avgRisk ℓ P κ π ≤ ↑C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDeriv_odd_cosh : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Real.cosh = Real.sinh
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
uniqueDiffWithinAt_extChartAt_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  UniqueDiffWithinAt 𝕜 (extChartAt I x).target (↑(extChartAt I x) x)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instInhabitedStruct : Inhabited Lean.Meta.Grind.AC.Struct
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremArgs.comp.injEq : ∀ (fArgId gArgId fArgId_1 gArgId_1 : ℕ),
  (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId gArgId =
      Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId_1 gArgId_1) =
    (fArgId = fArgId_1 ∧ gArgId = gArgId_1)
-- Mathlib.Order.Sublattice
Sublattice.coe_mk : ∀ {α : Type u_2} [inst : Lattice α] {s : Set α} (h_sup : SupClosed s) (h_inf : InfClosed s),
  ↑{ carrier := s, supClosed' := h_sup, infClosed' := h_inf } = s
-- Mathlib.Data.Finset.NAry
Finset.image₂_inter_union_subset_union : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
  {t t' : Finset β} [inst_1 : DecidableEq α] [inst_2 : DecidableEq β],
  Finset.image₂ f (s ∩ s') (t ∪ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.mul_pos : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] {a b : R},
  0 < a * b ↔ 0 < a ∧ 0 < b
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.sub_zsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddGroup α] [inst_1 : SubtractionMonoid β],
  Function.Antiperiodic f c → ∀ (n : ℤ), f (x - n • c) = ↑n.negOnePow • f x
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.normalizer_mono : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {N₁ N₂ : LieSubmodule R L M}, N₁ ≤ N₂ → N₁.normalizer ≤ N₂.normalizer
-- Mathlib.Analysis.Normed.Module.Basic
instNonUnitalSeminormedCommRingRestrictScalars : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    {E : Type u_3} → [I : NonUnitalSeminormedCommRing E] → NonUnitalSeminormedCommRing (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Data.Finset.Filter
/-- `Finset.filter p s` is the set of elements of `s` that satisfy `p`.

For example, one can use `s.filter (· ∈ t)` to get the intersection of `s` with `t : Set α`
as a `Finset α` (when a `DecidablePred (· ∈ t)` instance is available).  -/
Finset.filter : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Finset α → Finset α
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.not_isBasis_of_ssubset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → J ⊂ I → ¬M.IsBasis J X
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.congr_simp : ∀ {X : SSet} (f₀ f₀_1 : SSet.stdSimplex.obj { len := 2 } ⟶ X) (e_f₀ : f₀ = f₀_1)
  (f₁ f₁_1 : SSet.stdSimplex.obj { len := 2 } ⟶ X) (e_f₁ : f₁ = f₁_1) (f₃ f₃_1 : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (e_f₃ : f₃ = f₃_1)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = SSet.horn₃₂.desc f₀_1 f₁_1 f₃_1 ⋯ ⋯ ⋯
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- An induction principle for closure membership for predicates with two arguments.  -/
NonUnitalSubsemiring.closure_induction₂ : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R}
  {p : (x y : R) → x ∈ NonUnitalSubsemiring.closure s → y ∈ NonUnitalSubsemiring.closure s → Prop},
  (∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (x : R) (hx : x ∈ NonUnitalSubsemiring.closure s), p 0 x ⋯ hx) →
      (∀ (x : R) (hx : x ∈ NonUnitalSubsemiring.closure s), p x 0 hx ⋯) →
        (∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s)
            (hz : z ∈ NonUnitalSubsemiring.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
          (∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s)
              (hz : z ∈ NonUnitalSubsemiring.closure s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
            (∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s)
                (hz : z ∈ NonUnitalSubsemiring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
              (∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s)
                  (hz : z ∈ NonUnitalSubsemiring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                ∀ {x y : R} (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s),
                  p x y hx hy
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNat_inv_one : ∀ {α : Type u_1} [inst : DivisionSemiring α] {a : α}, Mathlib.Meta.NormNum.IsNat a 1 → Mathlib.Meta.NormNum.IsNat a⁻¹ 1
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_eq' : ∀ (n : ℕ), (n ^ 2).sqrt = n
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecLin_submatrix : ∀ {R : Type u_1} [inst : CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5}
  [inst_1 : Fintype n] [inst_2 : Fintype l] (f₁ : m → k) (e₂ : n ≃ l) (M : Matrix k l R),
  (M.submatrix f₁ ⇑e₂).mulVecLin = LinearMap.funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ LinearMap.funLeft R R ⇑e₂.symm
-- Init.Data.Char.Lemmas
Char.lt_trans : ∀ {a b c : Char}, a < b → b < c → a < c
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.flipFunctor_obj : ∀ (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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)), (CategoryTheory.flipFunctor C D E).obj F = F.flip
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.State.mk.injEq : ∀ (keys results keys_1 results_1 : Array Lean.Expr),
  ({ keys := keys, results := results } = { keys := keys_1, results := results_1 }) =
    (keys = keys_1 ∧ results = results_1)
-- Mathlib.RingTheory.WittVector.Domain
_private.Mathlib.RingTheory.WittVector.Domain.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_sum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {ι : Type u_3}
  (f : ι → R → R) (a : A) (s : Finset ι),
  autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) cfc_sum._auto_1 → cfc (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (f i) a
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.compRight_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (f : M →ₗ[R] M) (v w : M), ((B.compRight f) v) w = (B v) (f w)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_OptionT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  (x : OptionT m α) (h : PUnit.{u_1 + 1} → OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp x post (EPost.Cons.mk✝ (Std.Internal.Do.wp (h PUnit.unit) post epost) epost.tail) ⦄
    MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_empty_list : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {l : List α},
  List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).size = l.length
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Variant of `posLog_add` for norms of elements in normed additive commutative groups, using
monotonicity of `log⁺` and the triangle inequality.
 -/
Real.posLog_norm_add_le : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (a b : E), ‖a + b‖.posLog ≤ ‖a‖.posLog + ‖b‖.posLog + Real.log 2
-- Batteries.Data.Array.Basic
/-- Fold a function `f` over the subarray from the right, returning the list of partial results.
 -/
Subarray.scanr : {α : Type u_1} → {β : Type u_2} → (α → β → β) → β → Subarray α → Array β
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The left homology data of `(K.extend e).sc' i' j' k'` that is deduced
from a left homology data of `K.sc' i j k`.  -/
HomologicalComplex.extend.leftHomologyData : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {i' j' k' : ι'} →
                        e.f j = j' →
                          c.prev j = i →
                            c'.prev j' = i' →
                              c.next j = k →
                                c'.next j' = k' →
                                  (K.sc' i j k).LeftHomologyData → ((K.extend e).sc' i' j' k').LeftHomologyData
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
MeasurableSpace.measurable_invariants_dom : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β] {f : α → α} {g : α → β},
  Measurable g ↔ Measurable g ∧ ∀ (s : Set β), MeasurableSet s → g ∘ f ⁻¹' s = g ⁻¹' s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF → (List.find? (fun x => compare x.fst k == Ordering.eq) t.toList = none ↔ k ∉ t)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Geometric progressions of length three are unchanged under `2`-Freiman isomorphisms.  -/
IsMulFreimanIso.threeGPFree_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s : Set α} {t : Set β} {f : α → β},
  IsMulFreimanIso 2 s t f → (ThreeGPFree s ↔ ThreeGPFree t)
-- Mathlib.Order.Heyting.Basic
gc_inf_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a : α}, GaloisConnection (fun x => a ⊓ x) fun x => a ⇨ x
-- Init.Data.Order.LemmasExtra
/-- This lemma derives a `LawfulOrderMax α` instance from a property involving an `Ord α` instance.
 -/
Std.LawfulOrderMax.of_ord : ∀ (α : Type u) [inst : Ord α] [inst_1 : Max α] [inst_2 : LE α] [Std.LawfulOrderOrd α],
  (∀ (a b c : α), (compare (a ⊔ b) c).isLE = true ↔ (compare a c).isLE = true ∧ (compare b c).isLE = true) →
    (∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b) → Std.LawfulOrderMax α
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mk.injEq : ∀ {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} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} (toComma : CategoryTheory.Comma L R)
  (prop : P toComma.hom) (toComma_1 : CategoryTheory.Comma L R) (prop_1 : P toComma_1.hom),
  ({ toComma := toComma, prop := prop } = { toComma := toComma_1, prop := prop_1 }) = (toComma = toComma_1)
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.codRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ {s : Set β} (hs : ∀ (x : α), f x ∈ s), AntilipschitzWith K (Set.codRestrict f s hs)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
/-- Let `A` be an `R`-algebra. If `B` is an etale `A`-algebra, there exists an
`R`-subalgebra of finite type `A₀` of `A` and an etale `A₀`-algebra `B₀` such that
`B ≃ₐ A ⊗[A₀] B₀`.
 -/
Algebra.Etale.exists_subalgebra_fg : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u) (B : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [Algebra.Etale A B],
  ∃ A₀ B₀ x x_1, A₀.FG ∧ Algebra.Etale (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.quasiIsoAt_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  (∀ i < n, QuasiIsoAt f i) →
    ∀ [CategoryTheory.Mono f] [CategoryTheory.Mono (HomologicalComplex.homologyMap f n)],
      ∀ q ≤ n, QuasiIsoAt (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι✝ f n) q
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.mul : Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly
-- Mathlib.Algebra.Notation.Prod
Prod.instSMul.eq_1 : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SMul E α] [inst_1 : SMul E β],
  Prod.instSMul = { smul := fun c p => (c • p.1, c • p.2) }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toArray_rio_eq : ∀ {n i : ℕ}, ((*...n).toArray[i]?.isSome = true) = (i < n)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((bs : List β) → motive [] bs) →
            ((a : α) → (as : List α) → motive (a :: as) []) →
              ((a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)) → motive x x_1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Hom.liftQuotient.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f f_1 : X.Hom (AlgebraicGeometry.Spec A)) (e_f : f = f_1)
  (I : Ideal ↑A)
  (hI :
    I ≤
      RingHom.ker
        (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop))),
  f.liftQuotient I hI = f_1.liftQuotient I ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_ne_zero_of_X_ne : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → P 0 * Q 2 ≠ Q 0 * P 2 → W'.addZ P Q ≠ 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
/-- Conditional expectation of a function in L2 with respect to a sigma-algebra  -/
MeasureTheory.condExpL2 : {α : Type u_1} →
  (E : Type u_2) →
    (𝕜 : Type u_7) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [CompleteSpace E] →
              {m m0 : MeasurableSpace α} →
                {μ : MeasureTheory.Measure α} →
                  m ≤ m0 → ↥(MeasureTheory.Lp E 2 μ) →L[𝕜] ↥(MeasureTheory.lpMeas E 𝕜 m 2 μ)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.span_maximal_of_irreducible : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} [Fact (Irreducible f)], (Ideal.span {f}).IsMaximal
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.limit.π.hcongr_7 : ∀ (J J' : Type u₁),
  J = J' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} J) (inst' : CategoryTheory.Category.{v₁, u₁} J'),
      inst ≍ inst' →
        ∀ (C C' : Type u),
          C = C' →
            ∀ (inst_1 : CategoryTheory.Category.{v, u} C) (inst'_1 : CategoryTheory.Category.{v, u} C'),
              inst_1 ≍ inst'_1 →
                ∀ (F : CategoryTheory.Functor J C) (F' : CategoryTheory.Functor J' C'),
                  F ≍ F' →
                    ∀ (inst_2 : CategoryTheory.Limits.HasLimit F) (inst'_2 : CategoryTheory.Limits.HasLimit F'),
                      inst_2 ≍ inst'_2 →
                        ∀ (j : J) (j' : J'),
                          j ≍ j' → CategoryTheory.Limits.limit.π F j ≍ CategoryTheory.Limits.limit.π F' j'
-- Mathlib.AlgebraicTopology.SimplicialObject.II
/-- The functor `SimplexCategory ⥤ SimplexCategoryᵒᵖ` (i.e. a cosimplicial
object in `SimplexCategoryᵒᵖ`) which sends `⦋n⦌` to the object in `SimplexCategoryᵒᵖ`
that is associated to the linearly ordered type `⦋n + 1⦌` (which could be
identified to the ordered type `⦋n⦌ →o ⦋1⦌`).  -/
SimplexCategory.II : CategoryTheory.CosimplicialObject SimplexCategoryᵒᵖ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_insertMany_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α},
  k ∈ m → k ∈ Std.DHashMap.Const.insertMany m l
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst_k : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.diff_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ), ↑(CochainComplex.HomComplex.Cocycle.diff K) = CochainComplex.HomComplex.Cochain.diff K
-- Mathlib.GroupTheory.PGroup
IsPGroup.iff_card : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite G], IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n
-- Mathlib.Data.ENat.Basic
instNoZeroDivisorsENat : NoZeroDivisors ℕ∞