mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.take_of_take : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n k : ℕ} {p : G.Walk u v}, (p.take k).IsPath → n ≤ k → (p.take n).IsPath
-- Mathlib.Data.Rel
SetRel.inv_inv : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.inv.inv = R
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_injective : ∀ {n : ℕ}, Function.Injective SSet.stdSimplex.objMk₁
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisionAt.mk : ∀ {A : Type u_1} [inst : CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A},
  r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat →
    f = g * q + ↑r → f.IsWeierstrassDivisionAt g q r I
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instPow.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β], Lex.instPow = inst
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.natAbs_norm_mod_lt : ∀ (x : GaussianInt) {y : GaussianInt}, y ≠ 0 → (Zsqrtd.norm (x % y)).natAbs < (Zsqrtd.norm y).natAbs
-- Mathlib.Topology.Constructions
ContinuousAt.restrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
  {t : Set Y} (h1 : Set.MapsTo f s t) {x : ↑s}, ContinuousAt f ↑x → ContinuousAt (Set.MapsTo.restrict f s t h1) x
-- Mathlib.Algebra.Group.Conj
AddConjClasses.instInhabited.eq_1 : ∀ {α : Type u} [inst : AddMonoid α], AddConjClasses.instInhabited = { default := ⟦0⟧ }
-- Mathlib.Logic.Equiv.Multiset
decodeMultiset.eq_1 : ∀ {α : Type u_1} [inst : Encodable α] (n : ℕ), decodeMultiset n = Multiset.ofList <$> Encodable.decode n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂)[k]? = none
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.get! a = m_1.get! a_1
-- Mathlib.RingTheory.Congruence.Basic
RingCon.toCon_top : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R], ⊤.toCon = ⊤
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mem_closure : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : Set α} {x : α}, x ∈ TopologicalSpace.Closeds.closure s ↔ x ∈ closure s
-- Batteries.Lean.AttributeExtra
/-- Applies attribute `attr` to declaration `decl`, given a value for the parameter.  -/
Lean.ParametricAttributeExtra.setParam : {α : Type} → Lean.ParametricAttributeExtra α → Lean.Environment → Lean.Name → α → Except String Lean.Environment
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.map.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (p p_1 : CategoryTheory.Presieve.FamilyOfElements P R),
  p = p_1 →
    ∀ (φ φ_1 : P ⟶ Q), φ = φ_1 → ∀ ⦃Y : C⦄ (f f_1 : Y ⟶ X) (e_f : f = f_1) (a : R f), p.map φ f a = p_1.map φ_1 f_1 ⋯
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.eq_mul_of_ne_all : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G] {x y z : G}, x ≠ 1 → y ≠ 1 → x ≠ y → z ≠ 1 → z ≠ x → z ≠ y → z = x * y
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.map_residue : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] (f : R →+* S) [inst_4 : IsLocalHom f] (r : R),
  (IsLocalRing.ResidueField.map f) ((IsLocalRing.residue R) r) = (IsLocalRing.residue S) (f r)
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State : Type
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.quot_add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (x y : CommRingCat.Colimits.Prequotient F),
  Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) (x.add y) =
    (have this := Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x;
      this) +
      have this := Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) y;
      this
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_le_pow_iff_norm_lt_pow_add_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℤ), ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.below.const : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Sorted → Prop}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion []),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.below ⋯
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.subtype_apply : ∀ {M : Type u_4} [inst : AddZeroClass M] {s : AddSubmonoid M} (x : ↥s), s.subtype x = ↑x
-- Init.Data.Int.Order
Int.sub_le_sub_right : ∀ {a b : ℤ}, a ≤ b → ∀ (c : ℤ), a - c ≤ b - c
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.associator_naturality : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C}
  [inst_3 : X₁.HasTensor X₂] [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_5 : X₂.HasTensor X₃] [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_7 : Y₁.HasTensor Y₂] [inst_8 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃]
  [inst_9 : Y₂.HasTensor Y₃] [inst_10 : Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)]
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) [inst_11 : X₁.HasGoodTensor₁₂Tensor X₂ X₃]
  [inst_12 : X₁.HasGoodTensorTensor₂₃ X₂ X₃] [inst_13 : Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃]
  [inst_14 : Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃)
      (CategoryTheory.GradedObject.Monoidal.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom
      (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃))
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_of_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : ↥M},
  ↑a₂ * b₁ = ↑b₂ * a₁ → IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- This is another convenient method to verify that a fork is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.Cofork.IsColimit.mk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        (t : CategoryTheory.Limits.Cofork f g) →
          ((s : CategoryTheory.Limits.Cofork f g) →
              { l //
                CategoryTheory.CategoryStruct.comp t.π l = s.π ∧
                  ∀ {m : t.pt ⟶ s.pt}, CategoryTheory.CategoryStruct.comp t.π m = s.π → m = l }) →
            CategoryTheory.Limits.IsColimit t
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderivWithin.fst : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f₂ s x →
      fderivWithin 𝕜 (fun x => (f₂ x).1) s x = ContinuousLinearMap.fst 𝕜 F G ∘SL fderivWithin 𝕜 f₂ s x
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.quotientEquivOfIsTopCompl_symm_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q)
  (y : ↥q), (p.quotientEquivOfIsTopCompl q h).symm y = p.mkQ ↑y
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.isPullback_χ_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G)
  [CategoryTheory.Mono m],
  CategoryTheory.IsPullback m
    ((CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from F)
    (CategoryTheory.Presheaf.χ m) (CategoryTheory.Presheaf.truth C)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_sub : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Sub β],
  MeasureTheory.stoppedProcess (u - v) τ = MeasureTheory.stoppedProcess u τ - MeasureTheory.stoppedProcess v τ
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.quot_mk_assoc : ∀ {α : Type u} [inst : Add α] (x y z : α),
  Quot.mk (AddMagma.AssocRel α) (x + y + z) = Quot.mk (AddMagma.AssocRel α) (x + (y + z))
-- Init.SimpLemmas
and_iff_left_of_imp : ∀ {a b : Prop}, (a → b) → (a ∧ b ↔ a)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  (CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight X).inv.app Y = (β_ X Y).inv
-- Mathlib.FieldTheory.Finiteness
/-- A module over a division ring is Noetherian if and only if
its dimension (as a cardinal) is strictly less than the first infinite cardinal `ℵ₀`.
 -/
IsNoetherian.iff_rank_lt_aleph0 : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  IsNoetherian K V ↔ Module.rank K V < Cardinal.aleph0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictMonoOn.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, StrictMonoOn f s → StrictAntiOn (fun x => -f x) s
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.coe_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOne P] (g : N →* P)
  (f : M →* N), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℕ},
  ↑n ≠ 0 → (W.preΨ' n).natDegree = (n ^ 2 - if Even n then 4 else 1) / 2
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.Stable.bounded_difference : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F F' : I.Filtration M},
  F.Stable → F'.Stable → F.N 0 = F'.N 0 → ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
-- Batteries.Data.Fin.Lemmas
Fin.eq_none_of_findSome?_eq_none : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, Fin.findSome? f = none → ∀ (i : Fin n), f i = none
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.instNormedSpaceComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              (h : Manifold.IsImmersionAt I J n f x) → NormedSpace 𝕜 h.complement
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- Coefficients of a multivariate power series are uniformly continuous  -/
MvPowerSeries.WithPiTopology.uniformContinuous_coeff : ∀ {σ : Type u_1} (R : Type u_2) [inst : UniformSpace R] [inst_1 : Semiring R] (d : σ →₀ ℕ),
  UniformContinuous fun f => (MvPowerSeries.coeff d) f
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The basic open set `D₊(f)` associated to `f : A`.  -/
AlgebraicGeometry.Proj.basicOpen : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] → (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → A → (AlgebraicGeometry.Proj 𝒜).Opens
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_zero : ∀ {α : Type u_1}, FreeAddMonoid.length 0 = 0
-- Mathlib.Data.Fin.Tuple.Basic
/-- Concatenating the first element of a tuple with its tail gives back the original tuple  -/
Fin.cons_self_tail : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (q : (i : Fin (n + 1)) → α i), Fin.cons (q 0) (Fin.tail q) = q
-- Lean.Meta.Tactic.Grind.Types
/-- If `cheapCases` is `true`, `grind` only applies `cases` to types that contain
at most one minor premise.
Recall that `grind` applies `cases` when introducing types tagged with `[grind cases eager]`,
and at `Split.lean`
Remark: We add this option to implement the `lookahead` feature, we don't want to create several subgoals
when performing lookahead.
 -/
Lean.Meta.Grind.Context.cheapCases : Lean.Meta.Grind.Context → Bool
-- Mathlib.Data.List.Sort
List.orderedInsert_nil : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a : α), List.orderedInsert r a [] = [a]
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map₂_map_left_comm`.  -/
Option.map_map₂_distrib_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
  {α' : Type u_5} {g : γ → δ} {f' : α' → β → δ} {g' : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' (g' a) b) → Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g' a) b
-- Mathlib.Control.Functor
Functor.Comp.comp_map : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Functor F] [inst_1 : Functor G] [LawfulFunctor F]
  [LawfulFunctor G] {α β γ : Type v} (g' : α → β) (h : β → γ) (x : Functor.Comp F G α),
  Functor.Comp.map (h ∘ g') x = Functor.Comp.map h (Functor.Comp.map g' x)
-- Mathlib.Algebra.Algebra.Basic
algebraMap.coe_eq_zero_iff : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  (a : R), ↑a = 0 ↔ a = 0
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hom_comp : ∀ {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T),
  Semigrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Semigrp.Hom.hom g).comp (Semigrp.Hom.hom f)
-- Mathlib.Order.Bounds.Basic
IsLUB.exists_between : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a b : α}, IsLUB s a → b < a → ∃ c ∈ s, b < c ∧ c ≤ a
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationParams.mk.injEq : ∀ (expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx) (name : Lean.Name)
  (expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx) (name_1 : Lean.Name),
  ({ expr := expr, name := name } = { expr := expr_1, name := name_1 }) = (expr = expr_1 ∧ name = name_1)
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_unop : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ), P.unop.op = P
-- Mathlib.Algebra.Homology.LocalCohomology
/-- Casting from the full subcategory of ideals with radical containing `J` to the full
subcategory of ideals with radical containing `K`.  -/
localCohomology.SelfLERadical.cast : {R : Type u} →
  [inst : CommRing R] →
    {J K : Ideal R} →
      J.radical = K.radical → CategoryTheory.Functor (localCohomology.SelfLERadical J) (localCohomology.SelfLERadical K)
-- Mathlib.Data.EReal.Operations
EReal.bot_mul_of_neg : ∀ {x : EReal}, x < 0 → ⊥ * x = ⊤
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShapeSymmetrySymmetry.mk : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₂ c₁ c₁₂]
  [inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂] [inst_3 : TotalComplexShapeSymmetry c₂ c₁ c₁₂],
  (∀ (i₁ : I₁) (i₂ : I₂), c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂) → TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂
-- Lean.Parser.Extension
Lean.Parser.withSetOptionValue : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.mk.sizeOf_spec : ∀ {α : Type u_1} {s : Set α} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (s a)] (toFun : ℕ → Set α)
  (finite' : ∀ (n : ℕ), Finite ↑(toFun n)) (subset_succ' : ∀ (n : ℕ), toFun n ⊆ toFun (n + 1))
  (iUnion_eq' : ⋃ n, toFun n = s),
  sizeOf { toFun := toFun, finite' := finite', subset_succ' := subset_succ', iUnion_eq' := iUnion_eq' } =
    1 + sizeOf iUnion_eq'
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ind₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}
  (p : CategoryTheory.Subobject X → CategoryTheory.Subobject X → Prop),
  (∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g],
      p (CategoryTheory.Subobject.mk f) (CategoryTheory.Subobject.mk g)) →
    ∀ (P Q : CategoryTheory.Subobject X), p P Q
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_subset_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∪ t ⊆ u → s ⊆ u
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.IsSolvable.commutator_lt_of_ne_bot`. -/
IsSolvable.commutator_lt_of_ne_bot : ∀ {G : Type u_1} [inst : Group G] [Group.IsSolvable G] {H : Subgroup G}, H ≠ ⊥ → ⁅H, H⁆ < H
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblY_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 →
    P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
      P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3 → W'.dblY P = W'.dblU P ^ 3
-- Init.Data.Rat.Lemmas
Rat.zpow_neg : ∀ (q : ℚ) (n : ℤ), q ^ (-n) = (q ^ n)⁻¹
-- Mathlib.RingTheory.MvPolynomial.Groebner
/-- Division by a family of multivariate polynomials
whose leading coefficients are invertible with respect to a monomial order  -/
MonomialOrder.div : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {ι : Type u_3} {b : ι → MvPolynomial σ R},
  (∀ (i : ι), IsUnit (m.leadingCoeff (b i))) →
    ∀ (f : MvPolynomial σ R),
      ∃ g r,
        f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The pushforward functor is right adjoint to the pullback functor  -/
CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {I J : C} →
      (f : I ⟶ J) →
        {inst_1 : CategoryTheory.ChosenPullbacksAlong f} →
          [self : CategoryTheory.ExponentiableMorphism f] →
            CategoryTheory.ChosenPullbacksAlong.pullback f ⊣ CategoryTheory.ExponentiableMorphism.pushforward f
-- Std.Data.DTreeMap.Internal.Queries
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.DTreeMap.Internal.Impl.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.MappingConeCompHomotopyEquiv.hom.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CochainComplex.MappingConeCompHomotopyEquiv.hom f g =
    CochainComplex.mappingCone.lift (CochainComplex.mappingConeCompTriangle f g).mor₁
      (CochainComplex.mappingCone.descCocycle g
        (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr f)) 0
        CochainComplex.MappingConeCompHomotopyEquiv.hom._proof_6 ⋯)
      (CochainComplex.mappingCone.descCochain g 0
        (CochainComplex.HomComplex.Cochain.ofHom
          (CochainComplex.mappingCone.inr (CategoryTheory.CategoryStruct.comp f g)))
        CochainComplex.MappingConeCompHomotopyEquiv.hom._proof_7)
      ⋯
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [PartialEquivBEq α] [inst_3 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α}
  {h' : k ∈ Std.DTreeMap.Raw.Const.insertMany t l},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.insertMany t l) k h' =
    match w :
      List.findSomeRev?
        (fun x =>
          match x with
          | (a, b) => if cmp a k = Ordering.eq then some b else none)
        l with
    | some v => v
    | none => Std.DTreeMap.Raw.Const.get t k ⋯
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderHomLex.eq_1 : ∀ (Γ : Type u_1) (R : Type u_2) [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R],
  HahnSeries.finiteArchimedeanClassOrderHomLex Γ R =
    FiniteArchimedeanClass.liftOrderHom
      (fun x =>
        match x with
        | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))
      ⋯
-- Init.NotationExtra
Lean.explicitBinders : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_XIsoBiprod_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij)
      (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).hom =
    CategoryTheory.Limits.biprod.inl
-- Mathlib.GroupTheory.Perm.Centralizer
/-- The range of `Equiv.Perm.OnCycleFactors.toPermHom`.

The equality is proved by `Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom'`.  -/
Equiv.Perm.OnCycleFactors.range_toPermHom' : {α : Type u_1} →
  [inst : DecidableEq α] → [inst_1 : Fintype α] → (g : Equiv.Perm α) → Subgroup (Equiv.Perm ↥g.cycleFactorsFinset)