mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.freeYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (X : C) (M : A) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.Presheaf.freeYoneda X M).map f =
    CategoryTheory.Limits.Sigma.map' ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yoneda.obj X).map f))
      fun x => CategoryTheory.CategoryStruct.id M
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
quadraticChar_apply : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] (a : F),
  (quadraticChar F) a = quadraticCharFun F a
-- Mathlib.Data.Finset.Grade
Finset.covBy_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s), s ⋖ Finset.cons a s ha
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.instReprError : Repr Std.Http.Protocol.H1.Error
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexLinearEquiv_comp_apply : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11)
  (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n')
  (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') (M : Matrix m n A),
  (Matrix.reindexLinearEquiv R A e₁' e₂') ((Matrix.reindexLinearEquiv R A e₁ e₂) M) =
    (Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) M
-- Mathlib.Analysis.Convex.Function
ConvexOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f → ConcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.range_eq_top_of_epi : ∀ {A B : CommGrpCat} (f : A ⟶ B) [CategoryTheory.Epi f], (CommGrpCat.Hom.hom f).range = ⊤
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.LaxBraidedFunctor C D),
  (CategoryTheory.CategoryStruct.id F).hom.hom = CategoryTheory.CategoryStruct.id F.toLaxMonoidalFunctor.toFunctor
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_eval_zero : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {n : ℕ}, n ≠ 0 → hI.dpow n 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- The underlying subset  -/
CategoryTheory.SimplicialThickening.Path.I : {J : Type u_1} → [inst : LinearOrder J] → {i j : J} → CategoryTheory.SimplicialThickening.Path i j → Set J
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (fallback : α × β) (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (fallback : α × β) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1,
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      fallback => h_3 size k v l size_2 k_2 v_2 l_1 r h r_2 fallback) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 fallback
-- Mathlib.Order.Category.BddOrd
/-- `OrderDual` as a functor.  -/
BddOrd.dual : CategoryTheory.Functor BddOrd BddOrd
-- Init.Data.SInt.Lemmas
Int64.toBitVec_maxValue : Int64.maxValue.toBitVec = BitVec.intMax 64
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive
constant, then `f` tends to `∞`.  -/
Filter.Tendsto.den : ∀ {α : Type u_4} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : TopologicalSpace K] [OrderTopology K] [ContinuousInv K] {f g : α → K} {l : Filter α},
  Filter.Tendsto f l Filter.atTop →
    ∀ {a : K}, 0 < a → Filter.Tendsto (fun x => f x / g x) l (nhds a) → Filter.Tendsto g l Filter.atTop
-- Mathlib.Data.Matrix.Mul
Matrix.neg_mulVec_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n] (v : n → α)
  (A : Matrix m n α), (-A).mulVec (-v) = A.mulVec v
-- Qq.ForLean.Do
Lean.Elab.Term.extractBind : Option Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Term.ExtractMonadResult
-- Mathlib.Order.Concept
/-- The intent consists of all elements related to all elements of the extent.  -/
Concept.upperPolar_extent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (self : Concept α β r), upperPolar r self.extent = self.intent
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instRepr : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Repr α] → [(a : α) → Repr (β a)] → Repr (Std.DTreeMap.Raw α β cmp)
-- Mathlib.CategoryTheory.Shift.Quotient
CategoryTheory.Quotient.liftCommShift_commShiftIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) (r : HomRel C) (A : Type w) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : r.IsCompatibleWithShift A]
  [inst_6 : F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A),
  CategoryTheory.Functor.commShiftIso (CategoryTheory.Quotient.lift r F hF) a =
    CategoryTheory.Quotient.LiftCommShift.iso F r hF a
-- Mathlib.Dynamics.Flow
Flow.fromIter_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] {g : α → α} (h : Continuous g) (n : ℕ) (x : α),
  (Flow.fromIter h).toFun n x = g^[n] x
-- Mathlib.CategoryTheory.Sites.Finite
/-- The finite precoverage on a category consists of finite presieves, i.e. a presieve with finitely
many maps after uncurrying.  -/
CategoryTheory.Precoverage.finite : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C
-- Init.Data.Vector.Extract
Vector.extract_replicate : ∀ {α : Type u_1} {a : α} {n i j : ℕ}, (Vector.replicate n a).extract i j = Vector.replicate (min j n - i) a
-- Mathlib.Data.PSigma.Order
/-- The lexicographical linear order on a sigma type.  -/
PSigma.Lex.boundedOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : PartialOrder ι] →
      [inst_1 : BoundedOrder ι] →
        [inst_2 : (i : ι) → Preorder (α i)] → [OrderBot (α ⊥)] → [OrderTop (α ⊤)] → BoundedOrder (Σₗ' (i : ι), α i)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instInterOfBEqOfHashable : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Inter (Std.DHashMap.Raw α β)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.ofObj.mk : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u'} {X : ι → C} (i : ι),
  CategoryTheory.ObjectProperty.ofObj X (X i)
-- Mathlib.Topology.Order.OrderClosed
isClosed_le_prod : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α], IsClosed {p | p.1 ≤ p.2}
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.mono : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α},
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ {ν : MeasureTheory.Measure α}, ν.AbsolutelyContinuous μ → MeasureTheory.IsFundamentalDomain G s ν
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.length_le : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red L₁ L₂ → L₂.length ≤ L₁.length
-- Mathlib.Order.WellFounded
WellFounded.not_rightTotal : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → ∀ [Nonempty α], ¬Relator.RightTotal r
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- The scalar product `ψ • s` of a `C^k` function `ψ : M → 𝕜` and a section `s` of a vector
bundle `V → M` is `C^k` once `s` is `C^k` on an open set containing `tsupport ψ`.

This is a vector bundle analogue of `contMDiff_of_tsupport`.  -/
ContMDiffOn.smul_section_of_tsupport : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {s : (x : M) → V x} {ψ : M → 𝕜},
  ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n ψ u →
    IsOpen u →
      tsupport ψ ⊆ u →
        ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u →
          ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, (ψ • s) x⟩
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
_private.Mathlib.MeasureTheory.Function.LpSpace.Basic.0.MeasureTheory.Lp.norm_LpToLpOfMeasureLeSMulₗ_apply_le : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {c : ENNReal} (hc : c ≠ ⊤)
  (h : μ ≤ c • ν) [Fact (1 ≤ p)] {f : ↥(MeasureTheory.Lp E p ν)},
  ‖(MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ✝ hc h) f‖ ≤ c.toReal ^ (1 / p).toReal * ‖f‖
-- Mathlib.Algebra.DirectSum.Internal
/-- The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of
`DirectSum.coeAlgHom`.  -/
Submodule.iSup_eq_toSubmodule_range : ∀ {ι : Type u_1} {S : Type u_3} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring S]
  [inst_3 : Semiring R] [inst_4 : Algebra S R] (A : ι → Submodule S R) [inst_5 : SetLike.GradedMonoid A],
  ⨆ i, A i = Subalgebra.toSubmodule (DirectSum.coeAlgHom A).range
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.ext : ∀ {x y : Std.Time.WallTime}, x.val = y.val → x = y
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The functor `pointwiseRightKanExtension L F` is a right Kan extension of `F` along `L`.  -/
CategoryTheory.Functor.pointwiseRightKanExtensionIsUniversal : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseRightKanExtension F] →
                  CategoryTheory.CostructuredArrow.IsUniversal
                    (CategoryTheory.Functor.RightExtension.mk (L.pointwiseRightKanExtension F)
                      (L.pointwiseRightKanExtensionCounit F))
-- Std.Sync.Mutex
Std.instNonemptyCondvar : Nonempty Std.Condvar
-- Mathlib.Topology.Algebra.MetricSpace.Lipschitz
LipschitzOnWith.cauchySeq_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s → ∀ {u : ℕ → α}, CauchySeq u → Set.range u ⊆ s → CauchySeq (f ∘ u)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_finite : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finite], (M.contract C).Finite
-- Std.Internal.Do.WP.Frame
Lean.Order.PreservesSup.frameClosure.eq_1 : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α) (k : (β → α) → α)
  (Q : β → α),
  Lean.Order.PreservesSup.frameClosure op k Q =
    Lean.Order.iInf fun r => Lean.Order.PreservesSup.upperAdjoint (op r) (k fun a => op r (Q a))
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.one : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.degree_hermite : ∀ (n : ℕ), (Polynomial.hermite n).degree = ↑n
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Ico_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c - b) (d - b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k fallback : α},
  Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union m₂ ⋯ ⋯).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.instZeroHom : {M N : SemiNormedGrp} → Zero (M ⟶ N)
-- Mathlib.Logic.Equiv.Defs
/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse.  -/
Equiv : Sort u_1 → Sort u_2 → Sort (max (max 1 u_1) u_2)
-- Mathlib.Data.Real.Basic
Real.ofCauchy_natCast : ∀ (n : ℕ), { cauchy := ↑n } = ↑n
-- Init.Data.List.Sublist
List.IsPrefix.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
-- Mathlib.Data.Multiset.Powerset
Multiset.pairwise_disjoint_powersetCard : ∀ {α : Type u_1} (s : Multiset α), Pairwise fun i j => Disjoint (Multiset.powersetCard i s) (Multiset.powersetCard j s)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.Hom.ext_iff : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X} {f g : A ⟶ B}, f = g ↔ f.right = g.right
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.partialOrder : {ι : Type u_1} → {I : BoxIntegral.Box ι} → PartialOrder (BoxIntegral.Prepartition I)
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.symm_fst : ∀ {X Y : TopPair} {f₀ f₁ : X ⟶ Y} (F : TopPair.Homotopy f₀ f₁), F.symm.fst = F.fst.symm
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- If `f` has derivative `f'` in the strict sense and `f x' = f₁ x'` near `x`,
then `f₁` has the same derivative in the strict sense.

Note that this lemma assumes `f =ᶠ[𝓝 x] f₁`, while other lemmas in this file assume `f₁ =ᶠ[𝓝 x] f`.
This is done for backward compatibility, and may change in the future.
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/MyProp.2Econgr_*.20lemmas.2C.20LHS.20vs.20RHS/with/572593573).
 -/
HasStrictDerivAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → f =ᶠ[nhds x] f₁ → HasStrictDerivAt f₁ f' x
-- Mathlib.Topology.Homeomorph.Lemmas
Continuous.continuous_symm_of_equiv_compact_to_t2 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] [T2Space Y]
  {f : X ≃ Y}, Continuous ⇑f → Continuous ⇑f.symm
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.prodMk_left : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α × β → γ}, UniformContinuous f → ∀ (b : β), UniformContinuous fun a => f (a, b)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X.Hom (AlgebraicGeometry.Spec A)) (I : Ideal ↑A)
  (hI :
    I ≤
      RingHom.ker
        (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop)))
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.liftQuotient I hI)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm.injEq : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly) (c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
  (e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr) (p_1 : Lean.Grind.CommRing.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm c_1 e_1 p_1) =
    (c = c_1 ∧ e = e_1 ∧ p = p_1)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Two finite Borel measures are equal if the integrals of all bounded continuous functions with
respect to both agree.  -/
MeasureTheory.FiniteMeasure.ext_of_forall_integral_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω]
  {μ ν : MeasureTheory.FiniteMeasure Ω},
  (∀ (f : BoundedContinuousFunction Ω ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν) → μ = ν
-- Mathlib.Data.List.Cycle
List.prev_eq_getElem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α} (ha : a ∈ l),
  l.prev a ha = l[(List.idxOf a l + (l.length - 1)) % l.length]
-- Mathlib.Data.Finset.Sups
Finset.sup_mem_sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α} {a b : α},
  a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldlM_eq_foldlM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.TreeMap.Raw.foldlM f init t = List.foldlM (fun a b => f a b.1 b.2) init t.toList
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forIn_eq_forIn : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ},
  Std.ExtDTreeMap.forIn f init t = forIn t init fun a b => f a.fst a.snd b
-- Init.Control.Basic
/-- A type that can be used to reconstruct both a returned value and any state used by the outer
monad.
 -/
MonadControl.stM : (m : semiOutParam (Type u → Type v)) → (n : Type u → Type w) → [self : MonadControl m n] → Type u → Type u
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- The submodule generated by a finite set is finite-dimensional.  -/
FiniteDimensional.span_of_finite : ∀ (K : Type u) {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {A : Set V},
  A.Finite → FiniteDimensional K ↥(Submodule.span K A)
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousSub.continuous_sub : ∀ {G : Type u_4} {inst : TopologicalSpace G} {inst_1 : Sub G} [self : ContinuousSub G], Continuous fun p => p.1 - p.2
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- enriched coyoneda functor `(X ⟶[V] _) : C ⥤ V`.  -/
CategoryTheory.eCoyoneda : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [CategoryTheory.EnrichedOrdinaryCategory V C] → C → CategoryTheory.Functor C V
-- Mathlib.Algebra.Ring.Equiv
/-- A ring isomorphism preserves addition.  -/
RingEquiv.map_add : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
  (x y : R), e (x + y) = e x + e y
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.mem_coeffs_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {c : R}, c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_counitIso_inv_app_hom_toFun : ∀ (X : TwoP) (a : ((TwoP.swap.comp TwoP.swap).obj X).toBipointed.X),
  (TwoP.swapEquiv.counitIso.inv.app X).hom.toFun a = a
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_ne_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n),
  Mathlib.Tactic.Order.ToInt.toInt val i ≠ Mathlib.Tactic.Order.ToInt.toInt val j ↔ val i ≠ val j
-- Mathlib.Topology.Connected.Basic
Continuous.image_connectedComponentIn_subset : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α} {a : α},
  Continuous f → a ∈ s → f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.grevlex_k_eq_grevlex : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), m₁.grevlex_k m₂ = m₁.grevlex m₂
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.below.inter : ∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → FiniteInter.finiteInterClosure S a → Prop} {s t : Set α}
  (a : FiniteInter.finiteInterClosure S s) (a_1 : FiniteInter.finiteInterClosure S t),
  FiniteInter.finiteInterClosure.below a →
    motive s a → FiniteInter.finiteInterClosure.below a_1 → motive t a_1 → FiniteInter.finiteInterClosure.below ⋯
-- Mathlib.CategoryTheory.Filtered.Small
/-- Implementation detail for the instance
`EssentiallySmall.{max v w} (FullSubcategory (cofilteredClosure f))`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] → (n : ℕ) → ((k : ℕ) → k < n → (t : Type (max v w)) × (t → C)) → Type (max v w)
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyLE.cardinal_iUnion : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α},
  Cardinal.mk ι < c → (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋃ i, s i ≤ᶠ[l] ⋃ i, t i
-- Mathlib.Algebra.Quaternion
/-- `ℍ[R,c₁,c₂,c₃]` has a basis over `R` given by `1`, `i`, `j`, and `k`.  -/
QuaternionAlgebra.basisOneIJK : {R : Type u_3} → (c₁ c₂ c₃ : R) → [inst : CommRing R] → Module.Basis (Fin 4) R (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.snd.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousMonoidHom.snd A B = { toMonoidHom := MonoidHom.snd A B, continuous_toFun := ⋯ }
-- Mathlib.Topology.Basic
isClosed_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (Set X)}, (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s)