mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.tail.eq_2 : ∀ (p : Int.Internal.Linear.Poly),
  (∀ (a : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
      p = Int.Internal.Linear.Poly.add a v p_1 → False) →
    p.tail = p
-- Mathlib.CategoryTheory.Localization.Opposite
CategoryTheory.Localization.isoOfHom_op_inv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X Y : Cᵒᵖ} (w : X ⟶ Y) (hw : W.op w),
  (CategoryTheory.Localization.isoOfHom L.op W.op w hw).inv =
    (CategoryTheory.Localization.isoOfHom L W w.unop hw).inv.op
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.of_measure_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T : Set α → β} {C : ℝ} {μ' : MeasureTheory.Measure α},
  μ ≤ μ' → MeasureTheory.DominatedFinMeasAdditive μ T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive μ' T C
-- Std.Time.Date.Basic
Std.Time.instHSubOffset_6 : HSub Std.Time.Week.Offset Std.Time.Week.Offset Std.Time.Week.Offset
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_neg_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {i : ℕ}
  {f : E → F}, iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `K` is linearly ordered, the norm of a primitive root is `1` if `n` is odd.  -/
IsPrimitiveRoot.norm_eq_one_of_linearly_ordered : ∀ {n : ℕ} {L : Type v} [inst : CommRing L] {ζ : L},
  IsPrimitiveRoot ζ n →
    ∀ {K : Type u_1} [inst_1 : Field K] [inst_2 : LinearOrder K] [IsStrictOrderedRing K] [inst_4 : Algebra K L],
      Odd n → (Algebra.norm K) ζ = 1
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_sup : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Closeds α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- We can apply morphisms of concrete categories by first casting them down
to the base functions.
 -/
CategoryTheory.ConcreteCategory.instCoeFunHomForallToType : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X Y : C} → CoeFun (X ⟶ Y) fun x => CategoryTheory.ToType X → CategoryTheory.ToType Y
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_dep_iff : ∀ {α : Type u_1} {M : Matroid α} {R X : Set α}, (M.restrict R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The forgetful functor from `StructuredArrow K B` preserves any connected colimit.  -/
CategoryTheory.StructuredArrow.instPreservesColimitsOfShapeProjOfIsConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D}
  [CategoryTheory.IsConnected J] {B : D},
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.StructuredArrow.proj B K)
-- Mathlib.Order.Closure
LowerAdjoint.closure_inf_le : ∀ {α : Type u_1} {β : Type u_4} [inst : SemilatticeInf α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u)
  (x y : α), u (l.toFun (x ⊓ y)) ≤ u (l.toFun x) ⊓ u (l.toFun y)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.infDist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α}, Measurable f → ∀ {s : Set α}, Measurable fun x => Metric.infDist (f x) s
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fract_mem_fundamentalDomain : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (x : ι → ℕ),
  IsProperLinearSet.fract✝ hs x ∈ IsProperLinearSet.fundamentalDomain✝ hs
-- Mathlib.Data.Real.Basic
Real.instRatCast : RatCast ℝ
-- Mathlib.Topology.Gluing
TopCat.GlueData.preimage_image_eq_image : ∀ (D : TopCat.GlueData) (i j : D.J) (U : Set ↑(D.U i)),
  ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(CategoryTheory.ConcreteCategory.hom (D.f j i)) ''
      ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))) ⁻¹' U
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsAddLeftInvariant],
  μ'.addHaarScalarFactor μ = if ¬LocallyCompactSpace G then 1 else ⋯.choose
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey.mk : Lean.Parser.CacheableParserContext → Lean.Name → String.Pos.Raw → Lean.Parser.ParserCacheKey
-- Mathlib.Algebra.Group.Subgroup.Pointwise
coe_div_coe : ∀ {G : Type u_2} {S : Type u_4} [inst : SetLike S G] [inst_1 : DivisionMonoid G] [SubgroupClass S G] (H : S),
  ↑H / ↑H = ↑H
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.exists_modelType_is_realized_in : ∀ {L : FirstOrder.Language} (T : L.Theory) {α : Type w} (p : T.CompleteType α), ∃ M, p ∈ T.realizedTypes (↑M) α
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.neg.sizeOf_spec : sizeOf FirstOrder.ringFunc.neg = 1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkEMatchEqTheoremsForDef? : Lean.Name → optParam Bool false → Lean.MetaM (Option (Array Lean.Meta.Grind.EMatchTheorem))
-- Mathlib.Data.NNReal.Defs
NNReal.half_lt_self : ∀ {a : NNReal}, a ≠ 0 → a / 2 < a
-- Mathlib.Tactic.NormNum.Result
/-- A "raw nnrat cast" is an expression of the form:

* `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
* `(NNRat.rawCast n d : α)` where `n` is a raw nat literal, `d` is a raw nat literal, and `d` is not
  `1` or `0`.

This representation is used by tactics like `ring` to decrease the number of typeclass arguments
required in each use of a number literal at type `α`.
 -/
NNRat.rawCast : {α : Type u} → [DivisionSemiring α] → ℕ → ℕ → α
-- Mathlib.Data.List.Sort
List.sortedGT_iff_isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT ↔ List.IsChain (fun x1 x2 => x1 > x2) l
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  Topology.IsOpenEmbedding ⇑f →
    ∀ [∀ (x : ↥X), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)],
      AlgebraicGeometry.IsOpenImmersion f
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm : ∀ {V : Type u_1} {W : Type u_2} [inst : CategoryTheory.ReflQuiver W] [inst_1 : CategoryTheory.ReflQuiver V]
  {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} C] (F : V ⥤rq W) (G : W ⥤rq C),
  CategoryTheory.ReflQuiv.adj.homEquiv.symm (F ⋙rq G) =
    (CategoryTheory.Cat.freeReflMap F).comp (CategoryTheory.ReflQuiv.adj.homEquiv.symm G)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_comp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)),
  (f.lift hg).comp f.toAddMonoidHom = g
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_le_diam_pow : ∀ {ι : Type u_1} [inst : Fintype ι] (s : Set (ι → ℝ)), MeasureTheory.volume s ≤ Metric.ediam s ^ Fintype.card ι
-- Lean.Declaration
Lean.instInhabitedDeclaration : Inhabited Lean.Declaration
-- Mathlib.Combinatorics.Colex
/-- If `s ⊂ t`, then `s < t` in the colex order. Note the converse does not hold, as inclusion does
not form a linear order.  -/
Finset.Colex.toColex_strictMono : ∀ {α : Type u_1} [inst : PartialOrder α], StrictMono ⇑toColex
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_of_res_zero_of_qcqs_of_top : ∀ {X : AlgebraicGeometry.Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥X] {f s : ↑(X.presheaf.obj (Opposite.op ⊤))},
  TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = 0 → ∃ n, s ^ n * f = 0
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- If `c` is invertible, `c • f` is differentiable at `x` if and only if `f` is.  -/
differentiableAt_smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F] (c : R) [Invertible c], DifferentiableAt 𝕜 (c • f) x ↔ DifferentiableAt 𝕜 f x
-- Aesop.RuleTac.Forward.Basic
/-- Parse a name generated by `forwardImplDetailHypName`, obtaining the
`fwdHypName` and `depth`.
 -/
Aesop.matchForwardImplDetailHypName : Lean.Name → Option (ℕ × Lean.Name)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.tensorLineDerivTwo.congr_simp : ∀ (R : Type u_4) {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [inst : LineDeriv E V₁ V₂]
  [inst_1 : LineDeriv E V₂ V₃] [inst_2 : AddCommGroup V₁] [inst_3 : AddCommGroup V₂] [inst_4 : AddCommGroup V₃]
  [inst_5 : CommRing R] [inst_6 : AddCommGroup E] [inst_7 : Module R E] [inst_8 : Module R V₂] [inst_9 : Module R V₃]
  [inst_10 : LineDerivAdd E V₂ V₃] [inst_11 : LineDerivAdd E V₁ V₂] [inst_12 : LineDerivSMul R E V₂ V₃]
  [inst_13 : LineDerivLeftSMul R E V₁ V₂] [inst_14 : LineDerivLeftSMul R E V₂ V₃] (f f_1 : V₁),
  f = f_1 → LineDeriv.tensorLineDerivTwo R f = LineDeriv.tensorLineDerivTwo R f_1
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R₁ : Type u_1} {R₂ : Type u_2} [inst_3 : CommRing R₁] [inst_4 : CommRing R₂] [inst_5 : Algebra R₁ R₂]
  [inst_6 : Algebra R₁ S] [inst_7 : Algebra R₂ S] [inst_8 : Module R₁ P.Cotangent]
  [inst_9 : IsScalarTower R₁ S P.Cotangent] [inst_10 : Module R₂ P.Cotangent] [inst_11 : IsScalarTower R₂ S P.Cotangent]
  [IsScalarTower R₁ R₂ P.Cotangent], IsScalarTower R₁ R₂ P.H1Cotangent
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_self : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, (AdjoinRoot.mk f) f = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.mk.injEq : ∀ (id structId : ℕ) (type : Lean.Expr) (u : Lean.Level) (natModuleInst : Lean.Expr)
  (leInst? ltInst? lawfulOrderLTInst? isPreorderInst? orderedAddInst? isLinearInst? addRightCancelInst? :
    Option Lean.Expr)
  (rfl_q zero toQFn addFn smulFn : Lean.Expr) (termMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr))
  (id_1 structId_1 : ℕ) (type_1 : Lean.Expr) (u_1 : Lean.Level) (natModuleInst_1 : Lean.Expr)
  (leInst?_1 ltInst?_1 lawfulOrderLTInst?_1 isPreorderInst?_1 orderedAddInst?_1 isLinearInst?_1 addRightCancelInst?_1 :
    Option Lean.Expr)
  (rfl_q_1 zero_1 toQFn_1 addFn_1 smulFn_1 : Lean.Expr)
  (termMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)),
  ({ id := id, structId := structId, type := type, u := u, natModuleInst := natModuleInst, leInst? := leInst?,
        ltInst? := ltInst?, lawfulOrderLTInst? := lawfulOrderLTInst?, isPreorderInst? := isPreorderInst?,
        orderedAddInst? := orderedAddInst?, isLinearInst? := isLinearInst?, addRightCancelInst? := addRightCancelInst?,
        rfl_q := rfl_q, zero := zero, toQFn := toQFn, addFn := addFn, smulFn := smulFn, termMap := termMap } =
      { id := id_1, structId := structId_1, type := type_1, u := u_1, natModuleInst := natModuleInst_1,
        leInst? := leInst?_1, ltInst? := ltInst?_1, lawfulOrderLTInst? := lawfulOrderLTInst?_1,
        isPreorderInst? := isPreorderInst?_1, orderedAddInst? := orderedAddInst?_1, isLinearInst? := isLinearInst?_1,
        addRightCancelInst? := addRightCancelInst?_1, rfl_q := rfl_q_1, zero := zero_1, toQFn := toQFn_1,
        addFn := addFn_1, smulFn := smulFn_1, termMap := termMap_1 }) =
    (id = id_1 ∧
      structId = structId_1 ∧
        type = type_1 ∧
          u = u_1 ∧
            natModuleInst = natModuleInst_1 ∧
              leInst? = leInst?_1 ∧
                ltInst? = ltInst?_1 ∧
                  lawfulOrderLTInst? = lawfulOrderLTInst?_1 ∧
                    isPreorderInst? = isPreorderInst?_1 ∧
                      orderedAddInst? = orderedAddInst?_1 ∧
                        isLinearInst? = isLinearInst?_1 ∧
                          addRightCancelInst? = addRightCancelInst?_1 ∧
                            rfl_q = rfl_q_1 ∧
                              zero = zero_1 ∧
                                toQFn = toQFn_1 ∧ addFn = addFn_1 ∧ smulFn = smulFn_1 ∧ termMap = termMap_1)
-- Batteries.Data.List.Basic
List.zipWithLeft'.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α),
  List.zipWithLeft' f (a :: as) [] = (List.map (fun a => f a none) (a :: as), [])
-- Mathlib.MeasureTheory.Measure.MeasuredSets
/-- Given a ring of sets `C` covering the space modulo `0` and generating the measurable space
structure, any measurable set can be approximated by elements of `C`.  -/
MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)},
  MeasureTheory.IsSetRing C →
    (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) →
      mα = MeasurableSpace.generateFrom C →
        ∀ {s : Set α}, MeasurableSet s → ∀ {ε : ENNReal}, 0 < ε → ∃ t ∈ C, μ (symmDiff t s) < ε
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeDTR.go.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Array α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        (x_2 : Array α) →
          ((n : ℕ) → (x : α) → (xs : List α) → (acc : Array α) → motive n.succ (x :: xs) acc) →
            ((x : List α) → (acc : Array α) → motive 0 x acc) →
              ((n : ℕ) → (acc : Array α) → (n = 0 → False) → motive n [] acc) → motive x x_1 x_2
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_mul_comm : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f g : M →ₗ[R] M),
  (LinearMap.trace R M) (f * g) = (LinearMap.trace R M) (g * f)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.of_symm_smul_of_eq_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  (HahnModule.of R).symm (x • (HahnModule.of R) y) = x * y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addMap_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          ¬(P 0 * Q 2 = Q 0 * P 2 ∧ P 1 * Q 2 = W.negY Q * P 2) →
            W.addMap ⟦P⟧ ⟦Q⟧ =
              ⟦![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  1]⟧
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.eq_padicNorm : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ), ‖↑q‖ = ↑(padicNorm p q)
-- Mathlib.Algebra.Module.SpanRank
/-- The minimum cardinality of a generating set of a submodule as a cardinal.  -/
Submodule.spanRank : {R : Type u_1} →
  {M : Type u} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Cardinal.{u}
-- Mathlib.RingTheory.PicardGroup
/-- An `R`-module `M` is invertible if the canonical map `Mᵛ ⊗[R] M → R` is an isomorphism,
where `Mᵛ` is the `R`-dual of `M`.  -/
Module.Invertible : (R : Type u) → (M : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_of_isUnit : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {U : X.Opens} [inst_2 : Nonempty ↥↑U]
  {f : ↑(X.presheaf.obj (Opposite.op U))},
  IsUnit f →
    ∀ {x : ↥X},
      x ∈ U → AlgebraicGeometry.Scheme.ord ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestChainTac : Lean.Elab.Tactic.Try.TryTactic
-- Init.Data.SInt.Lemmas
Int64.sub_self : ∀ (a : Int64), a - a = 0
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : Z₁₂ ⟶ X₁} →
                          {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : Z₂₃ ⟶ X₂} →
                                {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : Z₁₃ ⟶ X₁} →
                                      {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          (m₁ : Z₁₂ ⟶ Z₁₃) →
                                            (m₃ : Z₁₃ ⟶ Z₂₃) →
                                              CategoryTheory.CategoryStruct.comp m₁ v₁₃ = v₁₂ →
                                                CategoryTheory.CategoryStruct.comp w₁₂
                                                      ((CategoryTheory.shiftFunctor C 1).map m₁) =
                                                    CategoryTheory.CategoryStruct.comp u₂₃ w₁₃ →
                                                  CategoryTheory.CategoryStruct.comp w₁₃
                                                        ((CategoryTheory.shiftFunctor C 1).map m₃) =
                                                      w₂₃ →
                                                    CategoryTheory.CategoryStruct.comp m₃ v₂₃ =
                                                        CategoryTheory.CategoryStruct.comp v₁₃ u₁₂ →
                                                      CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
                                                            (CategoryTheory.CategoryStruct.comp v₂₃ w₁₂) ∈
                                                          CategoryTheory.Pretriangulated.distinguishedTriangles →
                                                        CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Counters : Type
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity_eq_ker : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ}, rootsOfUnity k M = (powMonoidHom k).ker
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.emptyc_eq : ∀ {α : Type u} {β : α → Type v}, ∅ = ↑Std.DHashMap.Internal.Raw₀.emptyWithCapacity
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instToExprLinearCnstr : Lean.ToExpr Lean.Meta.Simp.Arith.Nat.LinearCnstr
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.toMatrix_sumInl : ∀ {n : Type u_1} (p : Type u_2) {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  (t : Matrix.TransvectionStruct n R),
  (Matrix.TransvectionStruct.sumInl p t).toMatrix = Matrix.fromBlocks t.toMatrix 0 0 1
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.continuous_comp : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] [LocallyCompactSpace B],
  Continuous fun f => f.2.comp f.1
-- Mathlib.Data.Finset.Dedup
Finset.val_le_iff_val_subset : ∀ {α : Type u_1} {a : Finset α} {b : Multiset α}, a.val ≤ b ↔ a.val ⊆ b
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.toListRev_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.iter.toListRev = s.toListRev
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.BuiltinPropagators.mk : Lean.Meta.Grind.PropagatorMap → Lean.Meta.Grind.PropagatorMap → Lean.Meta.Grind.BuiltinPropagators
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α}, Std.ExtDHashMap.Const.get! (m.erase k) k = default
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.dite_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {P : Prop}
  [inst_2 : Decidable P] {X Y : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (if h : P then f h else f' h) Z =
    if h : P then CategoryTheory.MonoidalCategoryStruct.whiskerRight (f h) Z
    else CategoryTheory.MonoidalCategoryStruct.whiskerRight (f' h) Z
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mem_single : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} {J' : BoxIntegral.Box ι} (hJ : J ≤ I)
  (h : x ∈ BoxIntegral.Box.Icc I), J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h ↔ J' = J
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.app.inj : ∀ {arr arr_1 : Array Mathlib.Tactic.ClickSuggestions.ApplyLemma},
  Mathlib.Tactic.ClickSuggestions.Candidates.app✝ arr = Mathlib.Tactic.ClickSuggestions.Candidates.app✝ arr_1 →
    arr = arr_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool}
  {k fallback : α},
  (Std.TreeMap.filter (fun k x => f k) t).getKeyD k fallback = (Option.filter f (t.getKey? k)).getD fallback