mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Quandle
_private.Mathlib.Algebra.Quandle.0.Rack.toEnvelGroup.mapAux.match_1.eq_1 : ∀ {R : Type u_1} (motive : Rack.PreEnvelGroup R → Sort u_2) (h_1 : Unit → motive Rack.PreEnvelGroup.unit)
  (h_2 : (x : R) → motive (Rack.PreEnvelGroup.incl x)) (h_3 : (a b : Rack.PreEnvelGroup R) → motive (a.mul b))
  (h_4 : (a : Rack.PreEnvelGroup R) → motive a.inv),
  (match Rack.PreEnvelGroup.unit with
    | Rack.PreEnvelGroup.unit => h_1 ()
    | Rack.PreEnvelGroup.incl x => h_2 x
    | a.mul b => h_3 a b
    | a.inv => h_4 a) =
    h_1 ()
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.reflectionPerm_mem_rootSet_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [inst_5 : CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L)
  (α β : ↥LieSubalgebra.root), ((LieAlgebra.IsKilling.rootSystem H).reflectionPerm β) α ∈ I.rootSet ↔ α ∈ I.rootSet
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullback_fst_range : ∀ {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) =
    {x | ∃ y, (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- To check a polynomial `p` over a field is irreducible, it suffices to check there are no
divisors of degree `0 < d ≤ degree p / 2`.

See also: `Polynomial.Monic.irreducible_iff_natDegree'`.
 -/
Polynomial.irreducible_iff_lt_natDegree_lt : ∀ {R : Type u} [inst : Field R] {p : Polynomial R},
  p ≠ 0 →
    ¬IsUnit p → (Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p)
-- Mathlib.Combinatorics.Additive.Energy
Finset.le_card_add_mul_addEnergy : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α),
  s.card ^ 2 * t.card ^ 2 ≤ (s + t).card * s.addEnergy t
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.closure_ball : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] (x : E)
  {r : ℝ}, r ≠ 0 → closure (Euclidean.ball x r) = Euclidean.closedBall x r
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} [L.LeAtTop]
  [inst_3 : Fintype β] (f : β → α), ∏'[L] (b : β), f b = ∏ b, f b
-- Init.WFExtrinsicFix
_private.Init.WFExtrinsicFix.0.WellFounded.partialExtrinsicFix₃.eq_1 : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
  (F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c)
  (a : α) (b : β a) (c : γ a b),
  WellFounded.partialExtrinsicFix₃ R F a b c =
    WellFounded.extrinsicFix₃ (fun p q => R ⟨p.fst, ⟨p.snd.fst, ↑p.snd.snd⟩⟩ ⟨q.fst, ⟨q.snd.fst, ↑q.snd.snd⟩⟩)
      (fun a_1 b_1 c_1 recur => F a_1 b_1 ↑c_1 fun a' b' c' hR => recur a' b' ⟨c', ⋯⟩ hR) a b ⟨c, ⋯⟩
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.ExceptConds.entails.match_1.splitter : (motive : (ps : Std.Do.PostShape) → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Sort u_2) →
  (ps : Std.Do.PostShape) →
    (x y : Std.Do.ExceptConds ps) →
      ((x y : Std.Do.ExceptConds Std.Do.PostShape.pure) → motive Std.Do.PostShape.pure x y) →
        ((σ : Type u_1) →
            (ps : Std.Do.PostShape) →
              (x y : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps)) → motive (Std.Do.PostShape.arg σ ps) x y) →
          ((ε : Type u_1) →
              (ps : Std.Do.PostShape) →
                (x y : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)) → motive (Std.Do.PostShape.except ε ps) x y) →
            motive ps x y
-- Init.Data.Array.Extract
Array.set_eq_push_extract_append_extract : ∀ {α : Type u_1} {as : Array α} {i : ℕ} (h : i < as.size) {a : α},
  as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1)
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num_mul_den_eq_num_mul_den_iff_eq : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {x y : K},
  IsFractionRing.num A y * ↑(IsFractionRing.den A x) = IsFractionRing.num A x * ↑(IsFractionRing.den A y) ↔ x = y
-- Mathlib.Analysis.Complex.Schwarz
/-- The **Schwarz Lemma**.
Let `f : E → F` be a complex analytic on an open ball with center at the origin.
If `f` sends this ball to the closed ball with center `0` of the same radius and `f 0 = 0`,
then for any point `z` of this disk we have `‖f z‖ ≤ ‖z‖`.  -/
Complex.norm_le_norm_of_mapsTo_ball : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R : ℝ} {f : E → F} {z : E},
  DifferentiableOn ℂ f (Metric.ball 0 R) →
    Set.MapsTo f (Metric.ball 0 R) (Metric.closedBall 0 R) → f 0 = 0 → ‖z‖ < R → ‖f z‖ ≤ ‖z‖
-- Mathlib.Data.List.Lex
List.Lex.trichotomous : ∀ {α : Type u} (r : α → α → Prop) [Std.Trichotomous r], Std.Trichotomous (List.Lex r)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
instAddSemigroupTensorProduct : (R : Type u_3) →
  [inst : CommSemiring R] →
    (M : Type u_1) →
      (N : Type u_2) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → AddSemigroup (TensorProduct R M N)
-- Mathlib.Algebra.Algebra.Equiv
/-- The units group of `S →ₐ[R] S` is `S ≃ₐ[R] S`.
See `LinearMap.GeneralLinearGroup.generalLinearEquiv` for the linear map version.  -/
AlgEquiv.algHomUnitsEquiv : (R : Type u_1) →
  (S : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (S →ₐ[R] S)ˣ ≃* S ≃ₐ[R] S
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.CodeBlock.mk.injEq : ∀ (code : Lean.Elab.Term.Do.Code) (uvars : Lean.Elab.Term.Do.VarSet) (code_1 : Lean.Elab.Term.Do.Code)
  (uvars_1 : Lean.Elab.Term.Do.VarSet),
  ({ code := code, uvars := uvars } = { code := code_1, uvars := uvars_1 }) = (code = code_1 ∧ uvars = uvars_1)
-- Lean.Data.PPContext
Lean.PPContext.lctx : Lean.PPContext → Lean.LocalContext
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.ComplexConfig.mk : (out ctx : Type) →
  (Option ctx → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition ctx) →
    (Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → ctx → Lean.MVarId → Lean.Elab.Command.CommandElabM out) →
      (Lean.Syntax → List Lean.MVarId → ℕ → out → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)) →
        Mathlib.TacticAnalysis.ComplexConfig
-- Mathlib.Data.List.Cycle
Cycle.mk_eq_coe : ∀ {α : Type u_1} (l : List α), Quot.mk (⇑(List.IsRotated.setoid α)) l = ↑l
-- Lean.Meta.Sorry
Lean.Meta.SorryLabelView.decode? : Lean.Name → Option Lean.Meta.SorryLabelView
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.smul_torsionBy : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R)
  (x : ↥(Submodule.torsionBy R M a)), a • x = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- `f` is continuously differentiable if it is cont. differentiable at
each `x ∈ mulTSupport f`.  -/
contMDiff_of_mulTSupport : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  [inst_11 : One M'] {f : M → M'}, (∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x) → ContMDiff I I' n f
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.instInhabited : Inhabited SemiNormedGrp
-- Lean.Meta.SizeOf
/-- Construct minor premise proof for `mkSizeOfAuxLemmaProof`. `ys` contains fields and inductive hypotheses for the minor premise.  -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.mkMinorProof : Array Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.Structured.toJson : Lean.Json.Structured → Lean.Json
-- Init.Data.String.Lemmas.Intercalate
String.appendSlice_eq : ∀ {s : String} {t : String.Slice}, s ++ t = s ++ t.copy
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If a function is countably sub-additive then it is sub-additive on countable types  -/
rel_iSup_tsum : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Countable β]
  [inst_3 : CompleteLattice α] (m : α → M),
  m ⊥ = 0 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) → ∀ (s : β → α), R (m (⨆ b, s b)) (∑' (b : β), m (s b))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic.0.WeierstrassCurve.Affine.equation_zero_iff_nonsingular_zero_of_Δ_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R},
  WeierstrassCurve.Δ W ≠ 0 → (W.Equation 0 0 ↔ W.Nonsingular 0 0)
-- Init.Data.Vector.Find
Vector.findRev?_push_of_pos : ∀ {α : Type} {n : ℕ} {p : α → Bool} {a : α} {xs : Vector α n}, p a = true → Vector.findRev? p (xs.push a) = some a
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_prod_one : ∀ {ι : Type u_1} {κ : Type u_2} {M₀ : Type u_4} [inst : MulZeroOneClass M₀] {s : Set ι} {i : ι} {t : Set κ} {j : κ},
  (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- `M.map f` is the matrix obtained by applying `f` to each entry of the matrix `M`.  -/
CStarMatrix.map : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → {B : Type u_6} → CStarMatrix m n A → (A → B) → CStarMatrix m n B
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.dec.inj : ∀ {x : Lean.IR.VarId} {n : ℕ} {c persistent : Bool} {b : Lean.IR.FnBody} {x_1 : Lean.IR.VarId} {n_1 : ℕ}
  {c_1 persistent_1 : Bool} {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.dec x n c persistent b = Lean.IR.FnBody.dec x_1 n_1 c_1 persistent_1 b_1 →
    x = x_1 ∧ n = n_1 ∧ c = c_1 ∧ persistent = persistent_1 ∧ b = b_1
-- Mathlib.Algebra.Lie.Basic
LieHom.toLinearMap_comp : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L₃]
  [inst_6 : LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂), ↑(f.comp g) = ↑f ∘ₗ ↑g
-- Mathlib.Data.Int.ModEq
Int.ModEq.add_left_cancel' : ∀ {n a b : ℤ} (c : ℤ), c + a ≡ c + b [ZMOD n] → a ≡ b [ZMOD n]
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.Entry.info : Lean.Meta.Match.Extension.Entry → Lean.Meta.MatcherInfo
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast? k (List.filter (fun p => f p.fst p.snd) l) =
      Option.filter (f k) (Std.Internal.List.getValueCast? k l)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiff_finsetProd'`. -/
contMDiff_finset_prod' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n (∏ i ∈ t, f i)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.trans : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C} {f g h : X.Hom Y},
  CategoryTheory.FreeMonoidalCategory.HomEquiv f g →
    CategoryTheory.FreeMonoidalCategory.HomEquiv g h → CategoryTheory.FreeMonoidalCategory.HomEquiv f h
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- If a category has all coproducts then in particular it has finite coproducts.
 -/
CategoryTheory.Limits.hasFiniteCoproducts_of_hasCoproducts : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_coe_nhds_top_iff : ∀ {α : Type u_1} {f : α → ℝ} {l : Filter α},
  Filter.Tendsto (fun x => ↑(f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} {C : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C) → MeasureTheory.eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
-- Mathlib.Logic.Relation
Std.Refl.map : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Std.Refl r] {f : α → β},
  Function.Surjective f → Std.Refl (Relation.Map r f f)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.neg_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i) (i : ι), (-g) i = -g i
-- Mathlib.RingTheory.PowerBasis
PowerBasis.degree_minpoly : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] [Nontrivial A]
  (pb : PowerBasis A S), (minpoly A pb.gen).degree = ↑pb.dim
-- Mathlib.Data.Matrix.Diagonal
Matrix.intCast_apply : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddGroupWithOne α] {i j : n} {d : ℤ},
  ↑d i j = ↑(if i = j then d else 0)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.match_21.splitter : (aig : Std.Sat.AIG ℕ) →
  (upper : ℕ) →
    (h : upper < aig.decls.size) →
      (state : Std.Sat.AIG.toCNF.State✝ aig) →
        (lhs rhs : Std.Sat.AIG.Fanin) →
          (this : lhs.gate < upper ∧ rhs.gate < upper) →
            (motive : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state out lhs.gate ⋯ } → Sort u_1) →
              (x : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state out lhs.gate ⋯ }) →
                ((lstate : Std.Sat.AIG.toCNF.State✝ aig) →
                    (hlstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state lstate lhs.gate ⋯) →
                      motive ⟨lstate, hlstate⟩) →
                  motive x
-- Mathlib.Order.Filter.Prod
Filter.Eventually.prod_mk : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {pa : α → Prop},
  (∀ᶠ (x : α) in la, pa x) →
    ∀ {lb : Filter β} {pb : β → Prop}, (∀ᶠ (y : β) in lb, pb y) → ∀ᶠ (p : α × β) in la ×ˢ lb, pa p.1 ∧ pb p.2
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.lift_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) CategoryTheory.Limits.biprod.fst = f
-- Init.Data.String.Iter.Intercalate
/-- Appends all the elements in the iterator, in order.
 -/
Std.Iter.joinString : {α β : Type} → [Std.Iterator α Id β] → [ToString β] → Std.Iter β → String
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Given a `GrothendieckTopology` and a set of sieves `s` that is equal, form a new
`GrothendieckTopology` whose set of sieves is definitionally equal to `s`.  -/
CategoryTheory.GrothendieckTopology.copy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (s : (X : C) → Set (CategoryTheory.Sieve X)) → J.sieves = s → CategoryTheory.GrothendieckTopology C
-- Mathlib.Data.Set.Image
Subtype.preimage_val_subset_preimage_val_iff : ∀ {α : Type u_1} (s t u : Set α), Subtype.val ⁻¹' t ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.rename_msymm : ∀ {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : Fintype τ]
  [inst_3 : DecidableEq σ] [inst_4 : DecidableEq τ] {n : ℕ} (μ : n.Partition) (e : σ ≃ τ),
  (MvPolynomial.rename ⇑e) (MvPolynomial.msymm σ R μ) = MvPolynomial.msymm τ R μ
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Additive.ofMul_le`. -/
Additive.ofMul_mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Additive.ofMul a ≤ Additive.ofMul b
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
AlgHom.map_fieldRange : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] {L : Type u_4} [inst_5 : Field L] [inst_6 : Algebra F L] (f : E →ₐ[F] K)
  (g : K →ₐ[F] L), IntermediateField.map g f.fieldRange = (g.comp f).fieldRange
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.univ_eq_zero_iff : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α), m Set.univ = 0 ↔ m = 0
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.listItem.bulletFn : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Init.Data.UInt.Bitwise
UInt16.not_or_self : ∀ {a : UInt16}, ~~~a ||| a = -1
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.limitCone_isLimit_lift : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.CompleteLattice.limitCone F).isLimit.lift s = CategoryTheory.homOfLE ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_le_pow_right_of_le_one' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M} {n m : ℕ},
  a ≤ 1 → n ≤ m → a ^ m ≤ a ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Y_ne_zero_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Nonsingular P → P 2 = 0 → P 1 ≠ 0
-- Init.Data.List.Monadic
List.filterMapM.loop.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (x : List β) (a : α)
  (as : List α),
  List.filterMapM.loop f (a :: as) x = do
    let __do_lift ← f a
    match __do_lift with
      | none => List.filterMapM.loop f as x
      | some b => List.filterMapM.loop f as (b :: x)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
AffineEquiv.pointReflection_midpoint_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), (AffineEquiv.pointReflection R (midpoint R x y)) x = y
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittNeg_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.wittNeg p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.homomulFn? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Logic.Function.CompTypeclasses
/-- Class of composing triples  -/
CompTriple : {M : Type u_1} → {N : Type u_2} → {P : Type u_3} → (M → N) → (N → P) → outParam (M → P) → Prop
-- Init.Data.SInt.Bitwise
Int16.and_self : ∀ {a : Int16}, a &&& a = a
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c),
  I.fstSigmaMapOfIsColimit d hc =
    CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i =>
      CategoryTheory.CategoryStruct.comp (I.fst i) (d.inj (J.fst i))
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.equivNatAlgEquiv_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S),
  (RingEquiv.equivNatAlgEquiv R S) f = f.toNatAlgEquiv
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given an integrable function `f` with values in `ℝ≥0`, there exists an upper semicontinuous
function `g ≤ f` with integral arbitrarily close to that of `f`. Formulation in terms of
`integral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.exists_upperSemicontinuous_le_integral_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] (f : α → NNReal),
  MeasureTheory.Integrable (fun x => ↑(f x)) μ →
    ∀ {ε : ℝ},
      0 < ε →
        ∃ g,
          (∀ (x : α), g x ≤ f x) ∧
            UpperSemicontinuous g ∧
              MeasureTheory.Integrable (fun x => ↑(g x)) μ ∧ ∫ (x : α), ↑(f x) ∂μ - ε ≤ ∫ (x : α), ↑(g x) ∂μ
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The map `I₁ × I₂ → I₁₂` on indices given by `TotalComplexShape c₁ c₂ c₁₂`.  -/
ComplexShape.π : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) → (c₁₂ : ComplexShape I₁₂) → [TotalComplexShape c₁ c₂ c₁₂] → I₁ × I₂ → I₁₂
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- `rw??` is an interactive tactic that suggests rewrites for any expression selected by the user.
To use it, shift-click an expression in the goal or a hypothesis that you want to rewrite.
Clicking on one of the rewrite suggestions will paste the relevant rewrite tactic into the editor.

The rewrite suggestions are grouped and sorted by the pattern that the rewrite lemmas match with.
Rewrites that don't change the goal and rewrites that create the same goal as another rewrite
are filtered out, as well as rewrites that have new metavariables in the replacement expression.
To see all suggestions, click on the filter button (▼) in the top right.
 -/
Mathlib.Tactic.LibraryRewrite.tacticRw?? : Lean.ParserDescr
-- Mathlib.RingTheory.Algebraic.Basic
/-- If `x` is transcendental over `S`, then `x` is transcendental over `R` when `S` is an extension
of `R`, and the map from `R` to `S` is injective.  -/
Transcendental.restrictScalars : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A],
  Function.Injective ⇑(algebraMap R S) → ∀ {x : A}, Transcendental S x → Transcendental R x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α}, Std.DHashMap.Raw.Const.get? (m₁ ∩ m₂) k = if k ∈ m₂ then Std.DHashMap.Raw.Const.get? m₁ k else none
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk.sizeOf_spec : ∀ {M : Type u_3} [inst : MulOneClass M] [inst_1 : SizeOf M] (toSubsemigroup : Subsemigroup M)
  (one_mem' : 1 ∈ toSubsemigroup.carrier),
  sizeOf { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = 1 + sizeOf toSubsemigroup + sizeOf one_mem'
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintParams.toJson : Lean.Lsp.InlayHintParams → Lean.Json