mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_app_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) {Z_1 : CommRingCat}
  (h :
    X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.CategoryStruct.comp f g) U) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U)
        (AlgebraicGeometry.Scheme.Hom.app f ((TopologicalSpace.Opens.map g.base).obj U)))
      h
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset`. -/
Set.diff_subset : ∀ {α : Type u_1} {s t : Set α}, s \ t ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
/-- If `R` is a ring object, then `Hom(-, R)` is a presheaf of rings.  -/
CategoryTheory.yonedaRingObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (R : C) → [CategoryTheory.RingObj R] → CategoryTheory.Functor Cᵒᵖ RingCat
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiableAt_const_add_iff`. -/
DifferentiableAt.const_add : ∀ {𝕜 : 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} (c : F), DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun y => c + f y) x
-- Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
/-- **Poisson limit Theorem**: If `n * p n → r` as `n → ∞`. Then
`(n.choose k) * (p n)^k * (1 - p n)^(n - k) → exp (-r) * r^k / k!`.
 -/
ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop : ∀ {p : ℕ → ℝ} {r : ℝ} (k : ℕ),
  Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r) →
    Filter.Tendsto (fun n => ↑(n.choose k) * p n ^ k * (1 - p n) ^ (n - k)) Filter.atTop
      (nhds (Real.exp (-r) * r ^ k / ↑k.factorial))
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The category of profinite additive groups. A term of this type consists of a profinite
set with a topological additive group structure.
 -/
ProfiniteAddGrp : Type (u + 1)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mem_mk_iff' : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L] (p : Submodule A L)
  (h : ∀ {a b : L}, a ∈ p.carrier → b ∈ p.carrier → ⁅a, b⁆ ∈ p.carrier) {x : L},
  x ∈ { toSubmodule := p, lie_mem' := h } ↔ x ∈ p
-- Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
/-- A map between two inner product spaces is a conformal map if and only if it preserves inner
products up to a scalar factor, i.e., there exists a positive `c : ℝ` such that
`⟪f u, f v⟫ = c * ⟪u, v⟫` for all `u`, `v`.  -/
isConformalMap_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] (f : E →L[ℝ] F),
  IsConformalMap f ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner ℝ (f u) (f v) = c * inner ℝ u v
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The canonical morphism of sheafed spaces from `X` to the spectrum of its global sections.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace : (X : AlgebraicGeometry.LocallyRingedSpace) →
  X.toSheafedSpace ⟶
    AlgebraicGeometry.Spec.toSheafedSpace.obj (Opposite.op (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis.eq_1 : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate)
  (b : Module.Basis ι K V), B.dualBasis hB b = b.dualBasis.map (B.toDual hB).symm
-- Mathlib.GroupTheory.Index
AddSubgroup.inf_eq_bot_of_coprime : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, (Nat.card ↥H).Coprime (Nat.card ↥K) → H ⊓ K = ⊥
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim.injEq : ∀ (c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.sum_dite_eq`.  -/
Fintype.sum_dite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  (f : (j : ι) → i = j → M), (∑ j, if h : i = j then f j h else 0) = f i ⋯
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_transpose_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂)
  (j : n), ((LinearMap.toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered semifield with the order topology, if `f` tends to `Filter.atTop` and `g`
tends to a positive constant `C` then `f * g` tends to `Filter.atTop`.  -/
Filter.Tendsto.atTop_mul_pos : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  0 < C →
    Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Lean.Attributes
Lean.attributeImplBuilderTableRef : IO.Ref Lean.AttributeImplBuilderTable
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The range of an injective group homomorphism is isomorphic to its domain.  -/
MonoidHom.ofInjective : {G : Type u_1} →
  [inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → {f : G →* N} → Function.Injective ⇑f → G ≃* ↥f.range
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDeriv_smul_le : ∀ {𝕜 : 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] {𝕜' : Type u_2}
  [inst_5 : NormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F]
  {f : E → 𝕜'} {g : E → F} {N : WithTop ℕ∞},
  ContDiff 𝕜 N f →
    ContDiff 𝕜 N g →
      ∀ (x : E) {n : ℕ},
        ↑n ≤ N →
          ‖iteratedFDeriv 𝕜 n (fun y => f y • g y) x‖ ≤
            ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
-- Mathlib.Analysis.Convex.Segment
vadd_segment : ∀ (𝕜 : Type u_1) {E : Type u_2} {G : Type u_4} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup G] [inst_5 : Module 𝕜 E] [inst_6 : AddTorsor G E]
  [VAddCommClass G E E] (a : G) (b c : E), a +ᵥ segment 𝕜 b c = segment 𝕜 (a +ᵥ b) (a +ᵥ c)
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- Definition of a fibered category.

See SGA 1 VI.6.1.  -/
CategoryTheory.Functor.IsFibered : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] → CategoryTheory.Functor 𝒳 𝒮 → Prop
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_zero : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [Nonempty ι], f 0 = 0
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_map : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) [inst_1 : CommSemiring S]
  (f : R →+* S), ((MvPolynomial.map f) p).vars ⊆ p.vars
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
instSMulCommClassSubtypeMemSubalgebraIntegralClosure : ∀ {G : Type u_1} {R : Type u_2} {K : Type u_3} [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G K] [inst_5 : SMulCommClass G R K],
  SMulCommClass G R ↥(integralClosure R K)
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedHomogeneousComponent_mul_of_le_weightedOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {w : σ → ℕ} {f g : MvPowerSeries σ R} {p q : ℕ},
  ↑p ≤ MvPowerSeries.weightedOrder w f →
    ↑q ≤ MvPowerSeries.weightedOrder w g →
      (MvPowerSeries.weightedHomogeneousComponent w (p + q)) (f * g) =
        (MvPowerSeries.weightedHomogeneousComponent w p) f * (MvPowerSeries.weightedHomogeneousComponent w q) g
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.append.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b c : RBTree.RBNode α) (y : α) (d : RBTree.RBNode α) (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x)
  (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_3 a x b c y d
-- Aesop.Script.CtorNames
Aesop.CtorNames.toRCasesPat : Aesop.CtorNames → Lean.TSyntax `rcasesPat
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.continuousOn_symm : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj),
  ContinuousOn (fun z => ⟨z.1, e.symm z.1 z.2⟩) (e.baseSet ×ˢ Set.univ)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainOfBialgHom_mapDomainBialgHom : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H] (f : G →+ H), AddMonoidAlgebra.mapDomainOfBialgHom (AddMonoidAlgebra.mapDomainBialgHom R f) = f
-- Mathlib.RingTheory.IsTensorProduct
TensorProduct.isTensorProduct : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_4) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Type u_8)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N], IsTensorProduct (TensorProduct.mk R M N)
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.Tendsto.add_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {α : Type u_2} {f : α → M}
  {x : Filter α} {a : M} (b : M), Filter.Tendsto f x (nhds a) → Filter.Tendsto (fun x => f x + b) x (nhds (a + b))
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_lt_sqrt_iff_of_pos : ∀ {x y : ℝ}, 0 < y → (√x < √y ↔ x < y)
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instAddHom : {M N : AddCommGrpCat} → Add (M ⟶ N)
-- Init.Data.List.Basic
List.replicate.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : α),
  List.replicate x x_1 =
    match x, x_1 with
    | 0, x => []
    | n.succ, a => a :: List.replicate n a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapCLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ}
  (f : ContDiffMapSupportedIn E F n K),
  ⇑((ContDiffMapSupportedIn.structureMapCLM 𝕜 n i) f) = if ↑i ≤ n then iteratedFDeriv ℝ i ⇑f else 0
-- Mathlib.Algebra.Order.Module.Equiv
symm_ofLexLinearEquiv : ∀ (α : Type u_1) (β : Type u_2) [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β],
  (ofLexLinearEquiv α β).symm = toLexLinearEquiv α β
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.PlausibleStep.done : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep Std.IterStep.done → Std.Iterators.Types.Take.PlausibleStep it Std.IterStep.done
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.MonObj.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (one one_1 : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) (e_one : one = one_1)
  (mul mul_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X) (e_mul : mul = mul_1)
  (one_mul :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one X) mul =
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
  (mul_one :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X one) mul =
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
  (mul_assoc :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X) mul =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul) mul)),
  { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc } =
    { one := one_1, mul := mul_1, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.MeasureTheory.OuterMeasure.Induced
_private.Mathlib.MeasureTheory.OuterMeasure.Induced.0.Option.elim'.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_1.eq_2 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x₁ x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq)
  (h_1 : (x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂))
  (h_2 :
    (x₁ x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂))
  (h_4 :
    (x₁ : Lean.Grind.AC.Var) →
      (s₁ : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) →
          (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂)),
  (match Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s with
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ => h_1 x₁ x₂
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => h_2 x₁ x s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => h_3 x s x₂
    | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ => h_4 x₁ s₁ x₂ s₂) =
    h_2 x₁ x s
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsIsoSchemeCoprodSpec : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S], CategoryTheory.IsIso (AlgebraicGeometry.coprodSpec R S)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformContinuous_map : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous (UniformSpace.Completion.map f)
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Given a topological space `X : TopCat` and a type family `T : X → Type`,
a `P : PrelocalPredicate T` consists of:
* a family of predicates `P.pred`, one for each `U : Opens X`, of the form `(Π x : U, T x) → Prop`
* a proof that if `f : Π x : V, T x` satisfies the predicate on `V : Opens X`, then
  the restriction of `f` to any open subset `U` also satisfies the predicate.
 -/
TopCat.PrelocalPredicate : {X : TopCat} → (↑X → Type u_1) → Type (max u_1 u_2)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonCommand : Lean.FromJson Lean.Lsp.Command
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof : Type
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.colimit.toOver_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J),
  (CategoryTheory.Limits.colimit.toOver F).ι.app j = CategoryTheory.Over.homMk (CategoryTheory.Limits.colimit.ι F j) ⋯
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- `HasExactColimitsOfShape` can be "pushed forward" along final functors  -/
CategoryTheory.hasExactColimitsOfShape_of_final : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] {J : Type u_1}
  {J' : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} J] [inst_3 : CategoryTheory.Category.{v_2, u_2} J']
  (F : CategoryTheory.Functor J J') [F.Final] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J' C]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C],
  CategoryTheory.HasExactColimitsOfShape J' C
-- Mathlib.Order.Filter.Basic
/-- If `f : ι → Filter α` is directed, `ι` is not empty, and `∀ i, f i ≠ ⊥`, then `iInf f ≠ ⊥`.
See also `iInf_neBot_of_directed` for a version assuming `Nonempty α` instead of `Nonempty ι`.  -/
Filter.iInf_neBot_of_directed' : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι],
  Directed (fun x1 x2 => x1 ≥ x2) f → (∀ (i : ι), (f i).NeBot) → (iInf f).NeBot
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- A typeclass for `SMul` structures which can be moved through a `LinearMap`.
This typeclass is generated automatically from an `IsScalarTower` instance, but exists so that
we can also add an instance for `AddCommGroup.toIntModule`, allowing `z •` to be moved even if
`S` does not support negation.
 -/
LinearMap.CompatibleSMul : (M : Type u_8) →
  (M₂ : Type u_10) →
    [inst : AddCommMonoid M] →
      [inst_1 : AddCommMonoid M₂] →
        (R : Type u_14) →
          (S : Type u_15) → [inst_2 : Semiring S] → [SMul R M] → [Module S M] → [SMul R M₂] → [Module S M₂] → Prop
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average.eq_1 : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) (f : α → E), MeasureTheory.average μ f = ∫ (x : α), f x ∂(μ Set.univ)⁻¹ • μ
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map.id : ∀ {α : Type u} (x : FreeAddGroup α), (FreeAddGroup.map id) x = x
-- Init.Data.String.PosRaw
String.Pos.Raw.byteDistance_eq : ∀ {lo hi : String.Pos.Raw}, lo.byteDistance hi = hi.byteIdx - lo.byteIdx
-- Mathlib.Order.Monotone.Basic
monotoneOn_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The identity equivalence of an affine subspace equal to `⊤` to the whole space.  -/
AffineIsometryEquiv.ofTop : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : PseudoMetricSpace P] →
              [inst_4 : NormedAddTorsor V P] →
                (s₁ : AffineSubspace 𝕜 P) → [inst_5 : Nonempty ↥s₁] → s₁ = ⊤ → ↥s₁ ≃ᵃⁱ[𝕜] P
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- The non-negative norm of the tensor product of a scalar linear map and of an element of a normed
space is the product of the non-negative norms.  -/
ContinuousLinearMap.nnnorm_smulRight_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E)
  (f : Fₗ), ‖ContinuousLinearMap.smulRight c f‖₊ = ‖c‖₊ * ‖f‖₊
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_nonzero_iff : ∀ {xs : List ℕ} {y : ℕ}, y ≠ 0 → (Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs = y ↔ y ∈ xs ∧ ∀ x ∈ xs, y ≤ x ∨ x = 0)
-- Mathlib.Combinatorics.Graph.Simple
Graph.loopless_iff : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β), G.Loopless ↔ ∀ (e : β) (x : α), ¬G.IsLoopAt e x
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.ComonToMonOpOp_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Comon C), (CategoryTheory.Comon.ComonToMonOpOp C).obj A = Opposite.op A.ComonToMonOpOpObj
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.ker_subtype : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subtype.ker = ⊥
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.ExtHashMap.ofList l).getKey? k = none
-- Mathlib.Order.Sublattice
Sublattice.coe_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice β) (f : LatticeHom α β),
  ↑(Sublattice.comap f L) = ⇑f ⁻¹' ↑L
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closure of a set equals the intersection of its (open) thickenings of positive radii.  -/
Metric.closure_eq_iInter_thickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α), closure E = ⋂ δ, ⋂ (_ : 0 < δ), Metric.thickening δ E
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unop_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.unop.X₁ = Opposite.unop S.X₃
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
/-- If scalar multiplication by elements of `α` sends `(0 : β)` to zero,
then the same is true for `(0 : Set β)`.  -/
Set.smulZeroClassSet : {α : Type u_1} → {β : Type u_2} → [inst : Zero β] → [SMulZeroClass α β] → SMulZeroClass α (Set β)
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.category.sizeOf_spec : ∀ (cat : Lean.Name), sizeOf (Lean.Parser.ParserResolution.category cat) = 1 + sizeOf cat