mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Environment
Lean.PersistentEnvExtension.addImportedFn : {α β σ : Type} → Lean.PersistentEnvExtension α β σ → Array (Array α) → Lean.ImportM σ
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If three points lie in the affine span of two points, those five points are collinear.  -/
collinear_insert_insert_insert_of_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ p₅ : P},
  p₁ ∈ line[k, p₄, p₅] → p₂ ∈ line[k, p₄, p₅] → p₃ ∈ line[k, p₄, p₅] → Collinear k {p₁, p₂, p₃, p₄, p₅}
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.congr_arg : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e : M ≃ₛₗ[σ] M₂} {x x' : M},
  x = x' → e x = e x'
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropWhile_eq_sliceFrom_skipPrefixWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.dropWhile pat = s.sliceFrom (s.skipPrefixWhile pat)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F' : Type u_21} [inst_6 : NormedRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'}, MDiff p → MDiff q → MDiff (p * q)
-- Mathlib.Order.Hom.Lattice
LatticeHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (toSupHom : SupHom α β) (map_inf' : ∀ (a b : α), toSupHom.toFun (a ⊓ b) = toSupHom.toFun a ⊓ toSupHom.toFun b),
  sizeOf { toSupHom := toSupHom, map_inf' := map_inf' } = 1 + sizeOf toSupHom
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v w : MeasureTheory.VectorMeasure α M}, v = w → v.AbsolutelyContinuous w
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The preimage is the basic open in `X` defined by the same element `r`.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))),
  X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S)
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w :
    ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) e.hom)
  {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)}
  (w' :
    ∀ (i : ι), CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) = CategoryTheory.CategoryStruct.comp (f i) e.inv),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence F e w w').counitIso =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso F w' w (CategoryTheory.CategoryStruct.id S') ⋯ ⋯ ≪≫
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso F ⋯ ⋯ ≪≫
        CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso F S'
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.zero_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.Hom.τ₁ 0 = 0
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.finite_setOfPred_setGcd_dvd_and_mem_span : ∀ (s : Set ℕ), {n | Nat.setGcd s ∣ n ∧ n ∉ Ideal.span s}.Finite
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the largest element of the tree set, returning `fallback` if the tree set is empty.
 -/
Std.TreeSet.maxD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → α
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.instInhabited : {α : Type u} → [inst : Add α] → [Inhabited α] → Inhabited (AddMagma.FreeAddSemigroup α)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
stabilizer_empty_eq_top : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α], MulAction.stabilizer G ∅ = ⊤
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformRight_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformRight e x).1 = x.1 ∪ (AddOpposite.op e +ᵥ x.1)
-- Mathlib.Data.Set.Sups
Set.sups_left_comm : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t u : Set α), s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The identity functor is also the identity on group objects.  -/
CategoryTheory.Functor.mapGrpIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (CategoryTheory.Functor.id C).mapGrp ≅ CategoryTheory.Functor.id (CategoryTheory.Grp C)
-- Mathlib.ModelTheory.ElementarySubstructures
Set.Definable₁.eq_1 : ∀ {M : Type w} (A : Set M) (L : FirstOrder.Language) [inst : L.Structure M] (s : Set M),
  A.Definable₁ L s = A.Definable L {x | x 0 ∈ s}
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_insert_of_mem : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {v' : α} {cmp : α → α → Ordering} {v : α} {t : RBTree.RBNode α},
  t.Balanced c n → v' ∈ t → v' ∈ RBTree.RBNode.insert cmp t v ∨ cmp v v' = Ordering.eq
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.nextn.eq_1 : ∀ {s : String} (p : s.Pos) (n : ℕ), p.nextn n = String.Pos.ofToSlice (p.toSlice.nextn n)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k k' fallback : α} {f : β k → β k},
  (m.modify k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- If `C` acts monoidally on `D`, then every object of `D` is
canonically an additive module over the trivial additive monoid.  -/
CategoryTheory.AddModObj.instTensorAddUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (X : D) → CategoryTheory.AddModObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.ι_mul_ι_comm : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a b : M),
  (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) - (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a
-- ImportGraph.Imports.RequiredModules
/-- Return the names of the modules in which constants used transitively
in the specified declarations were defined.

Note that this will *not* account for tactics and syntax used in the declaration,
so the results may not suffice as imports.
 -/
Lean.NameSet.transitivelyRequiredModules : Lean.NameSet → Lean.Environment → Lean.CoreM Lean.NameSet
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionList.mk : Bool → Array Lean.Lsp.ResolvableCompletionItem → Lean.Lsp.ResolvableCompletionList
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_sup_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H K : AddSubgroup N),
  Function.Surjective ⇑f → AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAlt0.congr_simp : ∀ {α : Type u} {m n : ℕ} (hm : m = n + n) (v v_1 : Fin m → α),
  v = v_1 → ∀ (k k_1 : Fin n), k = k_1 → Matrix.vecAlt0 hm v k = Matrix.vecAlt0 hm v_1 k_1
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
ContDiffAt.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ} {a : E} {n : ℕ∞},
  ContDiffAt ℝ (↑n) c a →
    ContDiffAt ℝ (↑n) R a →
      ContDiffAt ℝ (↑n) x a → x a ≠ c a → ContDiffAt ℝ (↑n) (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) a
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instStarRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : NonUnitalNonAssocSemiring β] → [StarRing β] → StarRing (MeasureTheory.SimpleFunc α β)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.comp_continuousOn_iff : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] {α : Type u_8} [inst_10 : TopologicalSpace α] (e : M₁ ≃SL[σ₁₂] M₂)
  {f : α → M₁} {s : Set α}, ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
-- Lean.Parser.Term
Lean.Parser.Term.letOptPostponeValue.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_iter_comp_add : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (m : M) (n : ℕ)
  (y : M), (fwdDiff h)^[n] (fun r => f (r + m)) y = (fwdDiff h)^[n] f (y + m)
-- Mathlib.Data.Set.Image
Set.range_some_union_none : ∀ (α : Type u_5), Set.range some ∪ {none} = Set.univ
-- Mathlib.Topology.JacobsonSpace
mem_closedPoints_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, x ∈ closedPoints X ↔ IsClosed {x}
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  a ≤ b → nhdsSet (Set.Icc a b) = nhds a ⊔ nhds b ⊔ Filter.principal (Set.Ioo a b)
-- Mathlib.Data.Set.Card
Set.encard_le_coe_iff : ∀ {α : Type u_1} {s : Set α} {k : ℕ}, s.encard ≤ ↑k ↔ s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_neg : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] (a : A), CFC.abs (-a) = CFC.abs a
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryFinFinset_symm_apply_const : ∀ {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [inst : CommSemiring R] [inst_1 : AddCommMonoid M']
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M'] [inst_4 : Module R M₂] {k l n : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂))
  (x : M'), (((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) fun x_1 => x) = (f fun x_1 => x) fun x_1 => x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.forgetPreservesLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat),
  CategoryTheory.Limits.PreservesLimitsOfSize.{v₂, v, max u₁ v, max u₁ v, max (max (max u u₁) (v + 1)) v₁,
      max (max (max u u₁) (v + 1)) v₁}
    (SheafOfModules.forget R)
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- The equivalences `Mon (Type u) ≌ MonCat.{u}` and `CommMon (Type u) ≌ CommMonCat.{u}`
are naturally compatible with the forgetful functors to `MonCat` and `Mon (Type u)`.
 -/
commMonTypeEquivalenceCommMonForget : CommMonTypeEquivalenceCommMon.functor.comp (CategoryTheory.forget₂ CommMonCat MonCat) ≅
  (CategoryTheory.CommMon.forget₂Mon (Type u)).comp MonTypeEquivalenceMon.functor
-- Init.Data.Array.Lemmas
Array.prod_eq_foldr : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] {xs : Array α}, xs.prod = Array.foldr (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.singleHom_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (a : R × M),
  MonoidAlgebra.singleHom a = MonoidAlgebra.single a.2 a.1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  (Std.ExtDTreeMap.filterMap f t).size = t.size ↔ ∀ (a : α) (h : a ∈ t), (f a (t.get a h)).isSome = true
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.mk : ℝ → Tactic.ComputeAsymptotics.UnitMonomial → Tactic.ComputeAsymptotics.Monomial
-- Init.Data.String.Termination
String.Slice.Pos.ne_startPos_of_prev?_eq_some : ∀ {s : String.Slice} {p q : s.Pos}, p.prev? = some q → p ≠ s.startPos
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
spectrum_imaginaryPart' : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) spectrum_imaginaryPart'._auto_1 →
    spectrum ℝ ↑(imaginaryPart a) = Complex.im '' spectrum ℂ a
-- Mathlib.ModelTheory.Ultraproducts
FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast : ∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)]
  [∀ (a : α), Nonempty (M a)] {β : Type u_3} {n : ℕ} (φ : L.BoundedFormula β n) (x : β → (a : α) → M a)
  (v : Fin n → (a : α) → M a),
  (φ.Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) fun i => v i a
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.erase_mem_shadow : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  s ∈ 𝒜 → a ∈ s → s.erase a ∈ 𝒜.shadow
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.mkOnlyParams : Lean.Grind.Config → Lean.MetaM Lean.Meta.Grind.Params
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.instMkBEqCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkBEqCached
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
MeasureTheory.instIsZeroOrProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i))
  [∀ (n : ℕ), MeasureTheory.IsZeroOrProbabilityMeasure (μ n)] (I : Finset ℕ),
  MeasureTheory.IsZeroOrProbabilityMeasure (MeasureTheory.inducedFamily μ I)
-- Init.Data.Nat.Basic
Nat.pred_succ : ∀ (n : ℕ), n.succ.pred = n
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [inst_1 : CategoryTheory.EssentiallySmall.{v, v₂, u₂} C]
  (J : CategoryTheory.GrothendieckTopology C) (A : Type u₁) [inst_2 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_3 : CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian.{v, v₁, u₁} A]
  [∀ (X : Cᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape
        (CategoryTheory.StructuredArrow X (CategoryTheory.equivSmallModel C).inverse.op) A]
  [inst_6 : CategoryTheory.HasSheafify ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) A],
  CategoryTheory.IsGrothendieckAbelian.{v, max u₂ v₁, max (max (max u₁ u₂) v₁) v₂} (CategoryTheory.Sheaf J A)
-- Mathlib.GroupTheory.Transfer
Subgroup.transferTransversal_apply' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G)
  (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H))
  (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))),
  ↑(⋯.leftQuotientEquiv (g ^ k.cast • Quotient.out q)) = g ^ k.cast * Quotient.out (Quotient.out q)
-- Mathlib.Data.Set.Basic
Set.inter_def : ∀ {α : Type u} {s₁ s₂ : Set α}, s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂}
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- A nonzero vector equals a rotation of that vector if and only if the angle is zero.  -/
Orientation.eq_rotation_self_iff_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V}, x ≠ 0 → ∀ (θ : Real.Angle), x = (o.rotation θ) x ↔ θ = 0
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.tendsto_integral_Ico_integral_Iio : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E} (b : ℝ),
  MeasureTheory.IntegrableOn f (Set.Iio b) μ →
    Filter.Tendsto a l Filter.atBot →
      Filter.Tendsto (fun i => ∫ (x : ℝ) in Set.Ico (a i) b, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Iio b, f x ∂μ))
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv`.

---

The bijection between the sets of normalized factors of I and J induced by a ring
isomorphism `f : R/I ≅ A/J`.  -/
normalizedFactorsEquivOfQuotEquiv : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : IsDedekindDomain A] →
          {I : Ideal R} →
            {J : Ideal A} →
              [inst_3 : IsDedekindDomain R] →
                R ⧸ I ≃+* A ⧸ J →
                  I ≠ ⊥ →
                    J ≠ ⊥ →
                      ↑{L | L ∈ UniqueFactorizationMonoid.normalizedFactors I} ≃
                        ↑{M | M ∈ UniqueFactorizationMonoid.normalizedFactors J}
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_σ'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_σ'._auto_1),
  autoParam (↑j = ↑j' + i) CategoryTheory.SimplicialObject.σ₀Iter_σ'._auto_3 →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := m + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ₀Iter i hi) (CategoryTheory.CategoryStruct.comp (X.σ j) h) =
        CategoryTheory.CategoryStruct.comp (X.σ j') (CategoryTheory.CategoryStruct.comp (X.σ₀Iter i ⋯) h)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.hasFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.Limits.HasFiniteLimits (PresheafOfModules R)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instSMulSubtypeMem : {K : Type u} → [inst : DivisionRing K] → {X : Type u_1} → [SMul K X] → (F : Subfield K) → SMul (↥F) X
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The expression  -/
Lean.Meta.RefinedDiscrTree.ExprInfo.expr : Lean.Meta.RefinedDiscrTree.ExprInfo → Lean.Expr
-- Mathlib.Order.Antisymmetrization
Antisymmetrization.ind : ∀ {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] {p : Antisymmetrization α r → Prop},
  (∀ (a : α), p (toAntisymmetrization r a)) → ∀ (q : Antisymmetrization α r), p q
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.horn.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper], c.horn = c.horn
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
/-- Closed ball w.r.t. the Euclidean distance.  -/
Euclidean.closedBall : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : TopologicalSpace E] →
      [IsTopologicalAddGroup E] →
        [T2Space E] → [inst_4 : Module ℝ E] → [ContinuousSMul ℝ E] → [FiniteDimensional ℝ E] → E → ℝ → Set E
-- Mathlib.Data.Finset.Disjoint
Finset.disjUnion_singleton : ∀ {α : Type u_2} (s : Finset α) (a : α) (h : Disjoint s {a}), s.disjUnion {a} h = Finset.cons a s ⋯
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.toMultiplicative_toAdditive_symm_apply : ∀ {G : Type u_2} [inst : MulOneClass G] (a : G),
  MulEquiv.toMultiplicative_toAdditive.symm a = Multiplicative.ofAdd (Additive.ofMul a)
-- Init.Data.Int.Gcd
Int.lcm_mul_right_left : ∀ (a b : ℤ), (b * a).lcm b = b.natAbs * a.natAbs
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.hasBasis_seminorms : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F],
  (nhds 0).HasBasis (fun x => x ∈ (ContinuousLinearMapWOT.seminormFamily σ E F).basisSets) id
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))) {Z : Ab}
  (h : (M.restrict f).presheaf.obj (Opposite.op U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Modules.smul
          ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).hom) r))
        h)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.univ_sum_single_apply : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] [inst_1 : Fintype α] (i : α) (m : M),
  ∑ j, (fun₀ | i => m) j = m
-- Init.Data.String.PosRaw
String.Pos.Raw.sub_byteIdx : ∀ (p₁ p₂ : String.Pos.Raw), (p₁.unoffsetBy p₂).byteIdx = p₁.byteIdx - p₂.byteIdx
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsPreimmersion f]
  [AlgebraicGeometry.IsPreimmersion g], AlgebraicGeometry.IsPreimmersion (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.GroupTheory.OrderOfElement
zmultiples_equiv_zmultiples_apply : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G} [inst_1 : Finite G] (h : addOrderOf x = addOrderOf y) (n : ℕ),
  (zmultiplesEquivZMultiples h) ⟨n • x, ⋯⟩ = ⟨n • y, ⋯⟩
-- Init.Data.String.Basic
String.toList_inj : ∀ {s₁ s₂ : String}, s₁.toList = s₂.toList ↔ s₁ = s₂