mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.reachable_of_mem_supp : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V}, u ∈ C.supp → v ∈ C.supp → G.Reachable u v
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f₁ f₂ : E →L[𝕜] F),
  ContinuousLinearMap.rTensor G (f₁ + f₂) = ContinuousLinearMap.rTensor G f₁ + ContinuousLinearMap.rTensor G f₂
-- Mathlib.Data.List.Sigma
List.kerase_keys_subset : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)), (List.kerase a l).keys ⊆ l.keys
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.LaxTrans.Modification η θ},
  x.app = y.app → x = y
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- **Alias** of `MeasureTheory.setToFun_finsetSum'`. -/
MeasureTheory.setToFun_finset_sum' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (s : Finset ι)
  {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) →
    MeasureTheory.setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (f i)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- Two `ConvexCone`s are equal if they have the same elements.  -/
ConvexCone.ext : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C₁ C₂ : ConvexCone R M}, (∀ (x : M), x ∈ C₁ ↔ x ∈ C₂) → C₁ = C₂
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The homotopy equivalence from a short complex to itself that is induced
by the identity.  -/
CategoryTheory.ShortComplex.HomotopyEquiv.refl : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (S : CategoryTheory.ShortComplex C) → S.HomotopyEquiv S
-- Mathlib.Data.String.Basic
String.lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList < s₂.toList
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (m : Submodule R M) (n : Submodule R N) (x : M) (y : N),
  (TensorProduct.quotientTensorQuotientEquiv m n) (Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y) =
    Submodule.Quotient.mk (x ⊗ₜ[R] y)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.nhds : ∀ (a : ℝ), intervalIntegral.FTCFilter a (nhds a) (nhds a)
-- Init.Prelude
/-- A non-identifier atomic component of syntax.

All of the following are atoms:
 * keywords, such as `def`, `fun`, and `inductive`
 * literals, such as numeric or string literals
 * punctuation and delimiters, such as `(`, `)`, and `=>`.

Identifiers are represented by the `Lean.Syntax.ident` constructor. Atoms also correspond to
quoted strings inside `syntax` declarations.
 -/
Lean.Syntax.atom : Lean.SourceInfo → String → Lean.Syntax
-- Mathlib.Order.Filter.Basic
Filter.sets_subset_sets : ∀ {α : Type u} {f g : Filter α}, f.sets ⊆ g.sets ↔ g ≤ f
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_bot : ∀ {R : Type u_2} [inst : NonAssocSemiring R], ⊥.op = ⊥
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_add_of_forall_lt : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b c : α},
  (∀ a' > a, ∀ b' > b, c ≤ a' + b') → c ≤ a + b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.getKey_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂),
  m₁.getKey k hk = m₂.getKey k ⋯
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- An auxiliary lemma en route to `RootPairing.Base.lie_e_f_ne`.  -/
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations.0.RootPairing.GeckConstruction.lie_e_f_ne_aux₀ : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  {i j : ↥b.support} (k : ↥b.support) (l : ι),
  ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.f j⁆ (Sum.inl k) (Sum.inr l) = 0
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) (ι : C → Type (max u v))
  (t : (X : C) → ι X → F.obj (Opposite.op X)) (x : C) (i : ι x),
  CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t
      (CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ x i) =
    some (t x i)
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.exists_le_prime_notMem_of_isIdempotentElem : ∀ {α : Type u} [inst : CommSemiring α] (I : Ideal α) (a : α),
  IsIdempotentElem a → a ∉ I → ∃ p, p.IsPrime ∧ I ≤ p ∧ a ∉ p
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_one_one : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {m : Type u_10} {n : Type u_11} [inst : Zero α] [inst_1 : Zero β]
  [inst_2 : Zero γ] [inst_3 : One α] [inst_4 : One β] [inst_5 : One γ] [inst_6 : DecidableEq m] [inst_7 : DecidableEq n]
  (f : α → β → γ), (∀ (b : β), f 0 b = 0) → (∀ (a : α), f a 0 = 0) → f 1 1 = 1 → Matrix.kroneckerMap f 1 1 = 1
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.trans_symm_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S')
  {E'' : Type u_5} [inst_4 : Group E''] {S'' : GroupExtension N E'' G} (equiv' : S'.Equiv S'') (a : E''),
  (equiv.trans equiv').symm a = equiv.symm (equiv'.symm a)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.coeff : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Var → ℤ
-- Mathlib.Algebra.Order.Archimedean.Class
/-- A closed ball defined by `ArchimedeanClass.addSubgroup` of `UpperSet.Ici c`.  -/
ArchimedeanClass.closedBallAddSubgroup : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → ArchimedeanClass M → AddSubgroup M
-- Std.Async.ContextAsync
/-- Runs two computations concurrently and returns both results. Each computation runs in its own child context;
if either fails or is cancelled, both are cancelled immediately and the exception is propagated.
 -/
Std.Async.ContextAsync.concurrently : {α β : Type} →
  Std.Async.ContextAsync α →
    Std.Async.ContextAsync β → optParam Task.Priority Task.Priority.default → Std.Async.ContextAsync (α × β)
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.cancel_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : C(β, γ)} {g₁ g₂ : C(α, β)},
  Function.Injective ⇑f → (f.comp g₁ = f.comp g₂ ↔ g₁ = g₂)
-- Mathlib.RingTheory.Etale.Field
Algebra.FormallyEtale.of_isSeparable : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L],
  Algebra.FormallyEtale K L
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.sub_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  AntivaryOn f g₁ s → MonovaryOn f g₂ s → AntivaryOn f (g₁ - g₂) s
-- Mathlib.Order.Heyting.Hom
CoheytingHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
  [inst_2 : CoheytingAlgebra γ] [inst_3 : CoheytingAlgebra δ] (f : CoheytingHom γ δ) (g : CoheytingHom β γ)
  (h : CoheytingHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Init.Data.Nat.MinMax
Nat.instCommutativeMax : Std.Commutative max
-- Mathlib.GroupTheory.Finiteness
Group.fg_of_surjective : ∀ {G : Type u_3} [inst : Group G] {G' : Type u_5} [inst_1 : Group G'] [hG : Group.FG G] {f : G →* G'},
  Function.Surjective ⇑f → Group.FG G'
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The underlying abelian presheaf of an `𝒪ₓ`-module.  -/
AlgebraicGeometry.Scheme.Modules.presheaf : {X : AlgebraicGeometry.Scheme} → X.Modules → TopCat.Presheaf Ab ↑X.toPresheafedSpace
-- Mathlib.Logic.Function.Basic
eq_rec_on_bijective : ∀ {α : Sort u_1} {C : α → Sort u_3} {a a' : α} (h : a = a'), Function.Bijective fun x => h ▸ x
-- Mathlib.Data.DFinsupp.Multiset
/-- `Multiset.toDFinsupp` as an `AddEquiv`.  -/
Multiset.equivDFinsupp : {α : Type u_1} → [DecidableEq α] → Multiset α ≃+ Π₀ (x : α), ℕ
-- Mathlib.LinearAlgebra.Span.Basic
/-- A version of `Submodule.span_le_restrictScalars` with coercions.  -/
Submodule.span_subset_span : ∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [IsScalarTower R S M],
  ↑(Submodule.span R s) ⊆ ↑(Submodule.span S s)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_snoc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (x : M) (f : Fin n → M), ∏ i, Fin.snoc f x i = (∏ i, f i) * x
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.le_of_succ?_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.succ? a = some b → Std.PRange.UpwardEnumerable.LE a b
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_subset_smul_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A B : Set β} {a : α}, a • A ⊆ a • B ↔ A ⊆ B
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.coe_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : α), ↑(a * b) = ↑a * ↑b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size =
    if k ∈ t ∧ (f (t.get? k)).isNone = true then t.size - 1
    else if k ∉ t ∧ (f (t.get? k)).isSome = true then t.size + 1 else t.size
-- Mathlib.Geometry.Manifold.IsManifold.Basic
PartialEquiv.Continuous.invFun : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (e : PartialEquiv α β),
  Continuous ↑e.symm → Continuous e.invFun
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.instSigmaFiniteAddHaar : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (b : Module.Basis ι ℝ E), MeasureTheory.SigmaFinite b.addHaar
-- Aesop.RuleTac.Basic
Aesop.instInhabitedRuleTacInput : Inhabited Aesop.RuleTacInput
-- Lean.Environment
/-- The trust level used by the kernel. For example,
the kernel assumes imported constants are type correct when the trust level is greater than zero.
 -/
Lean.EnvironmentHeader.trustLevel : Lean.EnvironmentHeader → UInt32
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Construct a `Type v`-enriched category from an honest category.
 -/
CategoryTheory.enrichedCategoryTypeOfCategory : (C : Type u₁) → [𝒞 : CategoryTheory.Category.{v, u₁} C] → CategoryTheory.EnrichedCategory (Type v) C
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ X₂ Y₂ : Cᴹᵒᵖ} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).unmop =
    CategoryTheory.MonoidalCategoryStruct.tensorHom g.unmop f.unmop
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_succ_le_succ_sqrt : ∀ (n : ℕ), n.succ.sqrt ≤ n.sqrt.succ
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Auxiliary simp lemma for the `coherence` tactic:
this moves brackets to the left in order to expose a maximal prefix
built out of unitors and associators.
 -/
Mathlib.Tactic.Coherence.assoc_liftHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} [inst_1 : Mathlib.Tactic.Coherence.LiftObj W]
  [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] [inst_3 : Mathlib.Tactic.Coherence.LiftObj Y] (f : W ⟶ X) (g : X ⟶ Y)
  (h : Y ⟶ Z) [Mathlib.Tactic.Coherence.LiftHom f] [Mathlib.Tactic.Coherence.LiftHom g],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h
-- Mathlib.Algebra.Module.Lattice
/-- Any lattice has `R`-rank equal to the `K`-rank of `V`.  -/
Submodule.IsLattice.rank' : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module K V] [inst_5 : Module R V] [inst_6 : IsScalarTower R K V] [IsDomain R]
  [IsPrincipalIdealRing R] [IsFractionRing R K] (M : Submodule R V) [Submodule.IsLattice K M],
  Module.rank R ↥M = Module.rank K V
-- Aesop.Rule.Name
Aesop.PhaseName.unsafe : Aesop.PhaseName
-- Std.Data.DHashMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.Const.alter : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} → (Std.DHashMap α fun x => β) → α → (Option β → Option β) → Std.DHashMap α fun x => β
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.continuousOn_iteratedFDerivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} {m : ℕ},
  ContDiffOn 𝕜 n f s → ↑m ≤ n → UniqueDiffOn 𝕜 s → ContinuousOn (iteratedFDerivWithin 𝕜 m f s) s
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] {P : Ideal R} [inst_4 : P.IsPrime] [inst_5 : Algebra S T] [inst_6 : Algebra R T]
  [inst_7 : IsScalarTower R S T],
  IsScalarTower S (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
    (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))
-- Lean.Data.Json.Elab
/-- Json syntactic category  -/
Lean.Parser.Category.json : Lean.Parser.Category
-- Mathlib.Order.Heyting.Regular
Heyting.IsRegular.eq_1 : ∀ {α : Type u_1} [inst : Compl α] (a : α), Heyting.IsRegular a = (aᶜᶜ = a)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_snd_eq_p₂_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] {Z : C} (h : A₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃))
      (CategoryTheory.CategoryStruct.comp (hf₁.snd f₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃) h
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_cons_iff : ∀ {xs : List ℕ} {n a : ℕ}, (*...=n).toList = a :: xs ↔ 0 = a ∧ (1...=n).toList = xs
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullback_map_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] {A B : P.Over Q Y} (g : A ⟶ B),
  ((CategoryTheory.MorphismProperty.Over.pullback P Q f).map g).left =
    CategoryTheory.Limits.pullback.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom f) g.left)
      (CategoryTheory.Limits.pullback.snd A.hom f) ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.map_baseChange : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange A).map ↑f = W'.baseChange B
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Reindexing a matrix preserves row-stochasticity.  -/
Matrix.reindex_mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {m : Type u_3} [inst_5 : Fintype m] [inst_6 : DecidableEq m]
  {M : Matrix n n R} {e₁ e₂ : n ≃ m}, M ∈ Matrix.rowStochastic R n → (Matrix.reindex e₁ e₂) M ∈ Matrix.rowStochastic R m
-- Init.Prelude
/-- `` `name `` is the node kind of name literals like `` `foo ``.  -/
Lean.nameLitKind : Lean.SyntaxNodeKind
-- Init.Prelude
/-- A success value of type `α` and a new state `σ`.  -/
EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.atomic.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toArray_insert_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α} {v : β},
  (t.insert k v).toArray.Perm ((Array.filter (fun x => decide ¬(k == x.1) = true) t.toArray).push (k, v))
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- If a colimit is nonempty, also its index category is nonempty.  -/
CategoryTheory.Limits.Types.nonempty_of_nonempty_colimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimit F], Nonempty (CategoryTheory.Limits.colimit F) → Nonempty J
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.localPreimage.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f f_1 : F ⟶ G) (e_f : f = f_1)
  {U : Cᵒᵖ} (s s_1 : CategoryTheory.ToType (G.obj U)) (e_s : s = s_1) {V : C} (g g_1 : V ⟶ Opposite.unop U)
  (e_g : g = g_1) (hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g),
  CategoryTheory.Presheaf.localPreimage f s g hg = CategoryTheory.Presheaf.localPreimage f_1 s_1 g_1 ⋯
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instInhabitedOrdinal : Inhabited Std.Time.Millisecond.Ordinal
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.toCompletion_surjective : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  Function.Surjective NumberField.InfinitePlace.Completion.toCompletion
-- Init.Prelude
/-- `a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. -/
HAdd.hAdd : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAdd α β γ] → α → β → γ
-- Mathlib.Computability.DFA
DFA.acceptsFrom.eq_1 : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ), M.acceptsFrom s = {x | M.evalFrom s x ∈ M.accept}
-- Init.Data.Array.Lemmas
Array.forall_mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {P : β → Prop},
  (∀ i ∈ Array.map f xs, P i) ↔ ∀ j ∈ xs, P (f j)
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.ofSeparation.eq_1 : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 1),
  NormedCommGroup.ofSeparation h =
    { toNorm := inst.toNorm, toCommGroup := inst.toCommGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (i₂₃ : ι₂₃) (j : ι₄)
  (h₂₃ : c₂.π c₃ c₂₃ (i₂, i₃) = i₂₃), ⋯
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An `n`-Freiman homomorphism preserves products of `n` elements.  -/
IsMulFreimanIso.map_prod_eq_map_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  IsMulFreimanIso n A B f →
    ∀ ⦃s t : Multiset α⦄,
      (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
        (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
          s.card = n → t.card = n → ((Multiset.map f s).prod = (Multiset.map f t).prod ↔ s.prod = t.prod)
-- Init.Tactics
Lean.Parser.Tactic.ImpossibleConfig.mk : Bool → Lean.Parser.Tactic.ImpossibleConfig