mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Language.Basic
Lean.Language.SnapshotTreeTransform.mk.injEq : ∀ (addTrailing addTrailing_1 : Substring.Raw),
  ({ addTrailing := addTrailing } = { addTrailing := addTrailing_1 }) = (addTrailing = addTrailing_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instDecidableEqCompletionItemTag : DecidableEq Lean.Lsp.CompletionItemTag
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ),
  H.unop = { carrier := AddOpposite.op ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.mk : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β},
  H.IsSubgraph G →
    (∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsLink e x y) → H.IsInducedSubgraph G
-- Mathlib.Data.Set.UnionLift
Set.iUnionLift.congr_simp : ∀ {α : Type u_1} {ι : Sort u_2} {β : Sort u_3} (S : ι → Set α) (f f_1 : (i : ι) → ↑(S i) → β) (e_f : f = f_1)
  (x : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) (T : Set α)
  (hT : T ⊆ Set.iUnion S) (x_1 x_2 : ↑T), x_1 = x_2 → Set.iUnionLift S f x T hT x_1 = Set.iUnionLift S f_1 ⋯ T hT x_2
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.isInvalidContinuationByte : UInt8 → Bool
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.liminf_eq_sSup_iUnion_iInter : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι}, v.HasBasis p s → Filter.liminf f v = sSup (⋃ j, ⋂ i, Set.Iic (f ↑i))
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : AddMonoid A] [inst_1 : GroupWithZero G₀] [inst_2 : DistribMulAction G₀ A]
  {S T : AddSubmonoid A} {a : G₀}, a ≠ 0 → (S ≤ a • T ↔ a⁻¹ • S ≤ T)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₀ : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X), data.toPreOneHypercover.I₀ = data.I₀
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ScopedEntries.mk : {β : Type} → Lean.SMap Lean.Name (Lean.PArray β) → Lean.ScopedEnvExtension.ScopedEntries β
-- Mathlib.Algebra.Group.End
Equiv.Perm.sigmaCongrRightHom_injective : ∀ {α : Type u_7} {β : α → Type u_8}, Function.Injective ⇑(Equiv.Perm.sigmaCongrRightHom β)
-- Init.Data.Fin.Basic
Fin.coe_neg : ∀ {n : ℕ} (a : Fin n), ↑(-a) = (n - ↑a) % n
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instMulActionWithZeroSubtypeMem : {K : Type u} →
  [inst : DivisionRing K] →
    {X : Type u_1} → [inst_1 : Zero X] → [MulActionWithZero K X] → (F : Subfield K) → MulActionWithZero (↥F) X
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_eq_top : ∀ {G : Type u_2} [inst : Group G] {S : Subgroup G}, S.op = ⊤ ↔ S = ⊤
-- Mathlib.Topology.Category.Compactum
_private.Mathlib.Topology.Category.Compactum.0.termβ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instVAddCommClassOfUniformContinuousConstVAdd : ∀ (M : Type v) (N : Type w) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X] [inst_2 : VAdd N X]
  [VAddCommClass M N X] [UniformContinuousConstVAdd M X] [UniformContinuousConstVAdd N X],
  VAddCommClass M N (UniformSpace.Completion X)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_inv`. -/
MonovaryOn.inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g s → MonovaryOn f⁻¹ g⁻¹ s
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_le_pow_iff_le_valuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]), x ≠ 0 → ∀ (n : ℕ), ‖x‖ ≤ ↑p ^ (-↑n) ↔ n ≤ x.valuation
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Ideal.under.eq_1 : ∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B),
  Ideal.under A P = Ideal.comap (algebraMap A B) P
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIco_zero_coe_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] {p : 𝕜}
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜}, x ∈ Set.Ico 0 p → AddCircle.liftIco p 0 f ↑x = f x
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelUnitBorel.instIsCondKernel : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [inst_2 : ProbabilityTheory.IsFiniteKernel κ],
  κ.IsCondKernel κ.condKernelUnitBorel
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Given a topological space `X : TopCat` and a type family `T : X → Type`,
a `P : LocalPredicate 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, and
* a proof that given some `f : Π x : U, T x`,
  if for every `x : U` we can find an open set `x ∈ V ≤ U`
  so that the restriction of `f` to `V` satisfies the predicate,
  then `f` itself satisfies the predicate.
 -/
TopCat.LocalPredicate : {X : TopCat} → (↑X → Type u_1) → Type (max u_1 u_2)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isEmbedding_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsEmbedding fun x => {x}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_Y : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R), W'.addXYZ P Q 1 = W'.addY P Q
-- Init.Prelude
/-- Creates a string that contains the characters in a list, in order.

Examples:
* `String.ofList ['L', '∃', '∀', 'N'] = "L∃∀N"`
* `String.ofList [] = ""`
* `String.ofList ['a', 'a', 'a'] = "aaa"`
 -/
String.ofList : List Char → String
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualQuotEquivDualAnnihilator_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (W : Submodule R M)
  (φ : Module.Dual R (M ⧸ W)) (x : M), (W.dualQuotEquivDualAnnihilator φ) x = φ (Submodule.Quotient.mk x)
-- Batteries.Lean.Position
/-- Yields the `Syntax.Range` for the declaration `decl` in the current file. If `decl` is not in
the current file, yields `none`.

By default, this provides the "selection range", which is usually the declaration's identifier or
e.g. the `instance` token for an unnamed instance. If `fullRange` is instead set to `true`, this
returns the full declaration range (which includes modifiers, such as the docstring).  -/
Lean.findDeclarationSyntaxRange? : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadLiftT BaseIO m] → [Lean.MonadFileMap m] → Lean.Name → optParam Bool false → m (Option Lean.Syntax.Range)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel_not : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α k),
  FirstOrder.Language.BoundedFormula.relabel g φ.not = (FirstOrder.Language.BoundedFormula.relabel g φ).not
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_diagonal : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : DecidableEq n] {f : X → n → R} {a : n → R},
  HasSum f a L → HasSum (fun x => Matrix.diagonal (f x)) (Matrix.diagonal a) L
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.whiskerRight_apply : ∀ {Y Z : TopCat} (f : Y ⟶ Z) (X : TopCat) (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)) p =
    ((CategoryTheory.ConcreteCategory.hom f) p.1, p.2)
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsAffineMap.add : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N] {f g : M → N} [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N],
  Convexity.IsAffineMap R f → Convexity.IsAffineMap R g → Convexity.IsAffineMap R (f + g)
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → ∀ {s : Set β}, μb s = 0 → μa (f ⁻¹' s) = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.hasLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] [Small.{v, u₂} J],
  CategoryTheory.Limits.HasLimitsOfShape J (PresheafOfModules R)
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.isHomeomorph_smul : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] {c : M}, IsUnit c → IsHomeomorph fun x => c • x
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_add : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → AddZeroClass (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)]
  [inst_4 : ∀ (i : ι), AddMemClass (S i) (G i)] (i : ι) (r s : G i),
  RestrictedProduct.single A i (r + s) = RestrictedProduct.single A i r + RestrictedProduct.single A i s
-- Mathlib.RingTheory.Binomial
Ring.multichoose_one_right' : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R),
  Ring.multichoose r 1 = r ^ 1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap_comp_descOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S S₁ : CategoryTheory.ShortComplex C} {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology] (φ : S₁ ⟶ S) [inst_3 : S₁.HasRightHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (S.descOpcycles k hk) =
    S₁.descOpcycles (CategoryTheory.CategoryStruct.comp φ.τ₂ k) ⋯
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.eq_of_length_le_one : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v}, p.length ≤ 1 → q.length ≤ 1 → p = q
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.argPartialEquiv_target : Circle.argPartialEquiv.target = Set.Ioc (-Real.pi) Real.pi
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_insert_of_ne : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v' v : α} [Std.TransCmp cmp] (t : RBTree.RBSet α cmp),
  cmp v' v ≠ Ordering.eq → (t.insert v).find? v' = t.find? v'
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_sq_sub_sinh_sq : ∀ (x : ℂ), Complex.cosh x ^ 2 - Complex.sinh x ^ 2 = 1
-- Mathlib.Topology.NhdsKer
mem_nhdsKer_iff_specializes : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {x : X}, x ∈ nhdsKer s ↔ ∃ y ∈ s, x ⤳ y
-- Mathlib.Algebra.Polynomial.Div
_private.Mathlib.Algebra.Polynomial.Div.0.Polynomial.divModByMonicAux.match_1.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (motive : Polynomial R → (x : Polynomial R) → x.Monic → Sort u_2) (p q : Polynomial R)
  (hq : q.Monic) (h_1 : (p q : Polynomial R) → (hq : q.Monic) → motive p q hq),
  (match p, q, hq with
    | p, q, hq => h_1 p q hq) =
    h_1 p q hq
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sub_mul_sub_pos_iff : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R]
  [AddLeftMono R] (x : R), a ≤ b → (0 < (x - a) * (x - b) ↔ x < a ∨ b < x)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : C)
  {x x_1 : C} (φ : x ⟶ x_1),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ C).obj X₁).obj X₂).map φ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ X₁ x).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ φ))
        (CategoryTheory.MonoidalCategoryStruct.associator X₂ X₁ x_1).inv)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- We can transport limits of shape `J` along an equivalence `J ≌ J'`.
 -/
CategoryTheory.Limits.hasLimitsOfShape_of_equivalence : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {J' : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} J'] (e : J ≌ J')
  [CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.HasLimitsOfShape J' C
-- Mathlib.Data.Set.Function
Function.invFunOn_injOn_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α), Set.InjOn (Function.invFunOn f s) (f '' s)
-- Mathlib.Data.List.MinMax
List.maximum_le_of_forall_le : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {b : WithBot α}, (∀ a ∈ l, ↑a ≤ b) → l.maximum ≤ b
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.inclusion_inclusion : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H K : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
  [inst_3 : Preorder S] [inst_4 : IsConcreteLE S G] {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : ↥H),
  (SubgroupClass.inclusion hKL) ((SubgroupClass.inclusion hHK) x) = (SubgroupClass.inclusion ⋯) x
-- Mathlib.RingTheory.Smooth.Locus
Algebra.basicOpen_subset_smoothLocus_iff_smooth : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A] {f : A},
  ↑(PrimeSpectrum.basicOpen f) ⊆ Algebra.smoothLocus R A ↔ Algebra.Smooth R (Localization.Away f)
-- Mathlib.Algebra.Lie.Basic
LieHom.lie_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (f : M →ₗ[R] N) (x : L) (m : M), ⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, m⁆
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.instNontrivialElemForall : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X] [IsOrderedRing S]
  [Nontrivial S] [Nontrivial X], Nontrivial ↑(stdSimplex S X)
-- Init.Data.Range.Polymorphic.Iterators
Std.Rci.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] {r : Std.Rci α} {a : α},
  (Std.Rci.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.intermediateFieldEquivSubgroup_symm_apply : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [inst_4 : IsGalois F E] (H : (Subgroup Gal(E/F))ᵒᵈ),
  IsGalois.intermediateFieldEquivSubgroup.symm H = IntermediateField.fixedField (OrderDual.ofDual H)
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalAddGroup.to_continuousSub : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G], ContinuousSub G
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.Literal.mk : (n : ℕ) → BitVec n → BitVec.Literal✝
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
_private.Mathlib.LinearAlgebra.RootSystem.Finite.G2.0.RootPairing.EmbeddedG2.isOrthogonal_short_and_long_aux : ∀ {a b c d e f a' b' c' d' e' f' : ℤ} {S : Set (ℤ × ℤ)},
  S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)} →
    (a, a') ∈ S →
      (b, b') ∈ S →
        (c, c') ∈ S →
          (d, d') ∈ S →
            (e, e') ∈ S →
              (f, f') ∈ S →
                c = a + 3 * b →
                  c' = a' + b' →
                    d = 2 * a + 3 * b →
                      d' = 2 * a' + b' →
                        e = a + b → e' = 3 * a' + b' → f = a + 2 * b → f' = 3 * a' + 2 * b' → a = 0 ∧ b = 0
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnInfo.mk : ℕ → ℕ → Lean.Meta.CoeFnType → Lean.Meta.CoeFnInfo
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} {x y : X.Hom Y}, x = y ↔ x.base = y.base ∧ x.c ≍ y.c
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_map : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (s : Subsemiring R) (g : S →+* T) (f : R →+* S),
  Subsemiring.map g (Subsemiring.map f s) = Subsemiring.map (g.comp f) s
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The forgetful functor from categories to quivers.  -/
CategoryTheory.ReflQuiv.forgetToQuiv : CategoryTheory.Functor CategoryTheory.ReflQuiv CategoryTheory.Quiv
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.isUniformAddGroup : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  IsUniformAddGroup (ContDiffMapSupportedIn E F n K)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite_point_eq_point_rev : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Affine.Simplex k P 1) (i : Fin 2) (n : Fin 1),
  (s.faceOpposite i).points n = s.points i.rev
-- Mathlib.Tactic.Ring.Common
/-- Negates a polynomial `va` to get another polynomial.

* `-0 = 0` (for `c` coefficient)
* `-(a₁ + a₂) = -a₁ + -a₂`
 -/
Mathlib.Tactic.Ring.Common.evalNeg : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          {a : Q(«$α»)} →
            (rα : Q(CommRing «$α»)) →
              Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(-«$a»))
-- Mathlib.Order.Cofinal
IsCofinal.image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  IsCofinal s → Monotone f → IsCofinal (Set.range f) → IsCofinal (f '' s)
-- Mathlib.Order.SupClosed
InfClosed.iInf_mem : ∀ {ι : Sort u_1} {α : Type u_3} [inst : CompleteLattice α] {f : ι → α} {s : Set α} [Finite ι],
  InfClosed s → ⊤ ∈ s → (∀ (i : ι), f i ∈ s) → ⨅ i, f i ∈ s
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_singleton : ∀ {M : Type u_3} [inst : CommMonoid M] (a : M), {a}.prod = a
-- Init.Data.List.Lemmas
List.filterMap.eq_def : ∀ {α : Type u} {β : Type v} (f : α → Option β) (x : List α),
  List.filterMap f x =
    match x with
    | [] => []
    | a :: as =>
      match f a with
      | none => List.filterMap f as
      | some b => b :: List.filterMap f as
-- Std.Data.HashSet.Lemmas
Std.HashSet.foldM_eq_foldlM_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {δ : Type v} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.HashSet.foldM (fun d a => f d a) init m = Array.foldlM f init m.toArray
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) (a : σ → σ)
  (q : Turing.TM2.Stmt Γ Λ σ), Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.load a q) = Turing.TM2.SupportsStmt S q
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $(X, Y)$ is Gaussian, then $X$ and $Y$ are independent if $\mathrm{Cov}(X, Y) = 0$.  -/
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P →
    ProbabilityTheory.covariance X Y P = 0 → ProbabilityTheory.IndepFun X Y P
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.support_add : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] [inst_1 : DecidableEq G] {p q : SkewMonoidAlgebra k G},
  (p + q).support ⊆ p.support ∪ q.support
-- Mathlib.Data.Num.ZNum
Num.mod.eq_2 : ∀ (x : Num), (x = Num.zero → False) → x.mod Num.zero = x
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.comp_continuous_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] {α : Type u_5} [inst_7 : TopologicalSpace α] (e : A ≃A[R] B) {f : α → A},
  Continuous (⇑e ∘ f) ↔ Continuous f
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- Given an orthonormal family, a second family of vectors is orthonormal if every vector equals
the corresponding vector in the original family or its negation.  -/
Orthonormal.orthonormal_of_forall_eq_or_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v w : ι → E}, Orthonormal 𝕜 v → (∀ (i : ι), w i = v i ∨ w i = -v i) → Orthonormal 𝕜 w
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingComp_map_incl_sup_of_codisjoint : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] {N₁ N₂ : LieSubmodule R L M},
  Codisjoint N₁ N₂ →
    LieSubmodule.map N₁.incl (LieModule.posFittingComp R L ↥N₁) ⊔
        LieSubmodule.map N₂.incl (LieModule.posFittingComp R L ↥N₂) =
      LieModule.posFittingComp R L M
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- The unit iso in the equivalence of sheaf categories.  -/
CategoryTheory.Equivalence.sheafCongr.unitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    CategoryTheory.Functor.id (CategoryTheory.Sheaf J A) ≅
                      (CategoryTheory.Equivalence.sheafCongr.functor J K e A).comp
                        (CategoryTheory.Equivalence.sheafCongr.inverse J K e A)
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.equivProjectivization_apply_coe : ∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : DecidableEq K] (t : K),
  (OnePoint.equivProjectivization K) ↑t = Projectivization.mk K ![t, 1] ⋯
-- Init.Data.Range.Polymorphic.SInt
Int16.lt.eq_1 : ∀ (a b : Int16), a.lt b = (a.toBitVec.slt b.toBitVec = true)