mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step_cons_of_LE : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β} [inst : Ord α] {upper : α} {h : (compare k upper).isLE = true},
  { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }.step =
    Std.IterStep.yield { internalState := { iter := Std.DTreeMap.Internal.Zipper.prependMap t it, upper := upper } }
      ⟨k, v⟩
-- Std.Async.Process
/-- Number of major (hard) page faults (disk I/O required)
 -/
Std.IO.Process.ResourceUsageStats.majorPageFaults : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.LinearAlgebra.Complex.Module
IsSelfAdjoint.imaginaryPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : A}, IsSelfAdjoint x → imaginaryPart x = 0
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (f : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.push k f q) =
    {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.push f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
-- Mathlib.Data.ENat.Basic
ENat.natCast_lift : ∀ (x : ℕ∞) (h : x < ⊤), ↑(x.lift h) = x
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- A termination measure with extra fields for use within GuessLex  -/
Lean.Elab.WF.GuessLex.BasicMeasure : Type
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals : Lean.TSyntax `tactic → List Lean.MessageData → Mathlib.TacticAnalysis.TerminalReplacementOutcome✝
-- Init.Data.Vector.Count
Vector.countP_congr : ∀ {α : Type u_1} {p q : α → Bool} {n : ℕ} {xs : Vector α n},
  (∀ x ∈ xs, p x = true ↔ q x = true) → Vector.countP p xs = Vector.countP q xs
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.measure_smul_setAverage : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} (f : α → E) {s : Set α},
  μ s ≠ ⊤ → μ.real s • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).inv.app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncLEι a).app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) h_1
-- Mathlib.Algebra.Ring.Int.Parity
Int.Odd.of_mul_left : ∀ {m n : ℤ}, Odd (m * n) → Odd m
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_gcd_of_dvd_right : ∀ {m k : ℕ} (n : ℕ), m ∣ k → n.gcd m ∣ n.gcd k
-- Mathlib.RingTheory.Multiplicity
/-- **Alias** of the reverse direction of `FiniteMultiplicity.neg_iff`. -/
FiniteMultiplicity.neg : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, FiniteMultiplicity a b → FiniteMultiplicity a (-b)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.mk : Option Lean.Term →
  Option Aesop.PhaseName →
    Option Aesop.Frontend.Priority →
      Option Aesop.Frontend.DBuilderName →
        Aesop.RuleBuilderOptions → Aesop.Frontend.RuleSets → Aesop.Frontend.RuleConfig
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The inclusion functor from `X.AffineZariskiSite` to `X.Opens`.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Functor X.AffineZariskiSite X.Opens
-- Mathlib.Order.Fin.Basic
Fin.castOrderIso_symm_apply : ∀ {m n : ℕ} (eq : n = m) (i : Fin m), (RelIso.symm (Fin.castOrderIso eq)) i = Fin.cast ⋯ i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_inter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂
-- Mathlib.Order.Partition.Basic
Partition.notMem_of_bot : ∀ {α : Type u_1} [inst : CompleteLattice α] (P : Partition ⊥) (x : α), x ∉ P
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.ae_iff_prob_eq_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  {p : α → Prop}, Measurable p → ((∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} = 1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_add_add_comm'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M]
  {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.imageIsoRange_inv_image_ι : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).inv (CategoryTheory.Limits.image.ι f) =
    ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.IsProbabilityMeasure ν], (μ.prod ν).fst = μ
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_of_integrable_trim : ∀ {α : Type u_1} {m : MeasurableSpace α} {H : Type u_8} [inst : NormedAddCommGroup H] {m0 : MeasurableSpace α}
  {μ' : MeasureTheory.Measure α} {f : α → H} (hm : m ≤ m0),
  MeasureTheory.Integrable f (μ'.trim hm) → MeasureTheory.Integrable f μ'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β} {f : β → β},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.modify m k f) k fallback =
    (Option.map f (Std.ExtDHashMap.Const.get? m k)).getD fallback
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.forall_mk : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop}, (∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x
-- Mathlib.Tactic.DeriveTraversable
/-- `nestedTraverse f α (List (Array (List α)))` synthesizes the expression
`traverse (traverse (traverse f))`. `nestedTraverse` assumes that `α` appears in
`(List (Array (List α)))`  -/
Mathlib.Deriving.Traversable.nestedTraverse : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Std.Do.WP.Sound
/-- Pure-proposition soundness for `StateT.run`, generalizing `StateM.of_wp_run_eq`.  -/
Std.Do.StateT.of_wp_run : ∀ {m : Type u → Type u_1} {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m ps]
  [Std.Do.WPSound m ps] [inst_4 : MonadAttach m] [LawfulMonadAttach m] {α σ : Type u} {prog : StateT σ m α} {s : σ}
  {p : α × σ} (P : α × σ → Prop),
  MonadAttach.CanReturn (prog.run s) p →
    (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.noThrow fun a s' => ⌜P (a, s')⌝) s) → P p
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_zero : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), ↑0 = 0
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_iInf : ∀ {α : Type u_1} {ι : Sort u_3} {f : ι → Filter α}, (iInf f).smallSets = ⨅ i, (f i).smallSets
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM.State : Type
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- Supporting function for the `F⟮x₁,x₂,...,xₙ⟯` adjunction notation.  -/
_private.Mathlib.FieldTheory.IntermediateField.Adjoin.Defs.0.IntermediateField.mkInsertTerm : {m : Type → Type} → [Monad m] → [Lean.MonadQuotation m] → Lean.TSyntaxArray `term → m Lean.Term
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.lift_quotient_mk'_sigma_mk' : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {P : Type u₁} [inst_5 : L.Structure P]
  (g : (i : ι) → L.Embedding (G i) P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x)
  {i : ι} (x : G i),
  (FirstOrder.Language.DirectLimit.lift L ι G f g Hg) ⟦FirstOrder.Language.Structure.Sigma.mk f i x⟧ = (g i) x
-- Init.Data.Vector.Algebra
/-- Componentwise multiplication of vectors.  -/
Vector.mul : {α : Type u_1} → {n : ℕ} → [Mul α] → Vector α n → Vector α n → Vector α n
-- Init.Data.UInt.Bitwise
UInt8.xor_self : ∀ {a : UInt8}, a ^^^ a = 0
-- Mathlib.GroupTheory.Schreier
Subgroup.IsComplement.toRightFun.congr_simp : ∀ {G : Type u_1} [inst : Group G] {H H_1 : Subgroup G} (e_H : H = H_1) {T : Set G} (hT : Subgroup.IsComplement (↑H) T)
  (a a_1 : G), a = a_1 → hT.toRightFun a = ⋯.toRightFun a_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntryD_eq_getD_minEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β} {fallback : α × β},
  Std.DTreeMap.Internal.Impl.Const.minEntryD l fallback = (Std.DTreeMap.Internal.Impl.Const.minEntry? l).getD fallback
-- Mathlib.Data.Fintype.CardEmbedding
Fintype.card_embedding_eq_of_unique : ∀ {α : Type u_1} {β : Type u_2} [Unique α] [inst : Fintype β] [inst_1 : Fintype (α ↪ β)],
  Fintype.card (α ↪ β) = Fintype.card β
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemMul.eq_1 : ∀ {α : Type u_2} [inst : Monoid α] {s t : Set α} [inst_1 : Fintype α] [inst_2 : DecidableEq α]
  [inst_3 : DecidablePred fun x => x ∈ s] [inst_4 : DecidablePred fun x => x ∈ t] (x : α),
  Set.decidableMemMul x = decidable_of_iff (∃ x_1 ∈ s, ∃ y ∈ t, x_1 * y = x) ⋯
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the sequence of denominators is monotone, that is `Bₙ ≤ Bₙ₊₁`.  -/
GenContFract.of_den_mono : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K], (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1)
-- Mathlib.Order.Interval.Set.InitialSeg
/-- If `f : α <i β` is a principal segment, this is the induced order
isomorphism `α ≃o Iio f.top`.  -/
PrincipalSeg.orderIsoIio : {α : Type u_1} →
  {β : Type u_2} → [inst : PartialOrder α] → [inst_1 : PartialOrder β] → (f : α <i β) → α ≃o ↑(Set.Iio f.top)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivWithinAt.const_cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {s : Set E} {c : ℂ},
  HasFDerivWithinAt f f' s x →
    c ≠ 0 ∨ f x ≠ 0 → HasFDerivWithinAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') s x
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.GrothendieckTopology.W.whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.MonoidalClosed A]
  [∀ (F₁ F₂ : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂]
  [∀ (F₁ F₂ : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂]
  [CategoryTheory.BraidedCategory A] {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ A} {f : F₁ ⟶ F₂},
  J.W f → ∀ (G : CategoryTheory.Functor Cᵒᵖ A), J.W (CategoryTheory.MonoidalCategoryStruct.whiskerRight f G)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiRing_zero : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : Fintype ι], MultilinearMap.mkPiRing R ι 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.equivOfIso_symm_apply : ∀ {X Y : SSet} (e : X ≅ Y) (s : Y.S),
  (SSet.S.equivOfIso e).symm s =
    { dim := s.dim,
      simplex := (CategoryTheory.ConcreteCategory.hom (e.inv.app (Opposite.op { len := s.dim }))) s.simplex }
-- Mathlib.Algebra.Squarefree.Basic
IsRelPrime.of_squarefree_mul : ∀ {R : Type u_1} [inst : CommMonoid R] {m n : R}, Squarefree (m * n) → IsRelPrime m n
-- Mathlib.Order.Antichain
IsAntichain.image_iso_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β] {φ : α ≃o β},
  IsAntichain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s) ↔ IsAntichain (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Order.Bounded
Set.unbounded_gt_inter_not_gt : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeInf α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 > x2) (s ∩ {b | ¬a < b}) ↔ Set.Unbounded (fun x1 x2 => x1 > x2) s
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- `.star` is an expression that will not be explicitly indexed.  -/
Lean.Meta.RefinedDiscrTree.StackEntry.star : Lean.Meta.RefinedDiscrTree.StackEntry
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  CategoryTheory.ShortComplex.rightHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Let `E` and `F` be two topological vector spaces over a `NontriviallyNormedField`, and assume
that the topology of `F` is generated by some family of seminorms `q`. For a family `f` of linear
maps from `E` to `F`, the following are equivalent:
* `f` is equicontinuous at `0`.
* `f` is equicontinuous.
* `f` is uniformly equicontinuous.
* For each `q i`, the family of seminorms `k ↦ (q i) ∘ (f k)` is bounded by some continuous
  seminorm `p` on `E`.
* For each `q i`, the seminorm `⊔ k, (q i) ∘ (f k)` is well-defined and continuous.

In particular, if you can determine all continuous seminorms on `E`, that gives you a complete
characterization of equicontinuity for linear maps from `E` to `F`. For example `E` and `F` are
both normed spaces, you get `NormedSpace.equicontinuous_TFAE`.  -/
WithSeminorms.equicontinuous_TFAE : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] {κ : Type u_11} {q : SeminormFamily 𝕜₂ F ι'}
  [inst_7 : UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [hu : IsUniformAddGroup F],
  WithSeminorms q →
    ∀ [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F),
      [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f),
          UniformEquicontinuous (DFunLike.coe ∘ f), ∀ (i : ι'), ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
          ∀ (i : ι'), BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))].TFAE
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_link : ∀ {a b : ℕ} {self : Batteries.UnionFind} {x y : Fin self.size},
  self.parent ↑x = ↑x →
    ∀ (yroot : self.parent ↑y = ↑y),
      (self.link x y yroot).Equiv a b ↔
        self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instAddCommMonoidWithOne : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoidWithOne (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] → AddCommMonoidWithOne (PiTensorProduct R fun i => A i)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.map_inrX_mapHomologicalComplexObjXIso_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] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] (i : ι),
  CategoryTheory.CategoryStruct.comp (H.map (HomologicalComplex.homotopyCofiber.inrX φ i))
      (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H i).hom =
    HomologicalComplex.homotopyCofiber.inrX ((H.mapHomologicalComplex c).map φ) i
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily
distinct!), then the size of `t` divides the size of `s +ᵥ t`.  -/
Finset.card_dvd_card_vadd_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {t : Finset β}
  {s : Finset α}, ((fun x => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s +ᵥ t).card
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.range_mul : ∀ {ι : Type u_1} {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {f g : ι → M},
  BddBelow (Set.range f) → BddBelow (Set.range g) → BddBelow (Set.range fun i => f i * g i)
-- Mathlib.Logic.Equiv.Multiset
/-- Explicit encoding function for `Multiset α`  -/
encodeMultiset : {α : Type u_1} → [Encodable α] → Multiset α → ℕ
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.isComplex_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂), S₁.IsComplex → S₂.IsComplex
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddCommMonoidOfContinuousAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommMonoid β]
  [inst_3 : ContinuousAdd β],
  ContinuousMap.instAddCommMonoidOfContinuousAdd =
    { toAddMonoid := ContinuousMap.instAddMonoidOfContinuousAdd, add_comm := ⋯ }
-- Mathlib.Algebra.Homology.SingleHomology
ChainComplex.exactAt_succ_single_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℕ),
  HomologicalComplex.ExactAt ((ChainComplex.single₀ C).obj A) (n + 1)
-- Lean.Setup
Lean.instFromJsonModuleSetup.fromJson : Lean.Json → Except String Lean.ModuleSetup
-- Init.Data.String.Modify
/-- Given a valid position in a string, obtain the corresponding position after setting a character on
that string, provided that the position was before the changed position.  -/
String.Pos.toSetOfLE : {s : String} → (q p : s.Pos) → (c : Char) → (hp : p ≠ s.endPos) → q ≤ p → (p.set c hp).Pos
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The `Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat`
for commutative rings.  -/
Submodule.LinearDisjoint.rank_inf_le_one_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → Module.Flat R ↥M ∨ Module.Flat R ↥N → Module.rank R ↥(M ⊓ N) ≤ 1
-- Lean.Data.Json.FromToJson.Basic
Lean.Float.toJson : Float → Lean.Json
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The degree of a product of polynomials is at most the sum of the degrees,
where the degree of the zero polynomial is ⊥.
 -/
Polynomial.degree_multiset_prod_le : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
  t.prod.degree ≤ (Multiset.map Polynomial.degree t).sum
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.neg_def : ∀ (x : ℝ),
  Real.neg✝ x =
    match x with
    | { cauchy := a } => { cauchy := -a }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α]
  [beqOrd : Std.LawfulBEqOrd α] [Std.TransOrd α] {k : α},
  t.WF → t.keys.contains k = Std.DTreeMap.Internal.Impl.contains k t
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.exists_lt_add : ∀ {α : Sort u_1} [hα : Nonempty α] {o : Ordinal.{u_2}} {f : α → Ordinal.{u_2}},
  (∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i) →
    ∀ {b : Ordinal.{u_2}} ⦃a : Ordinal.{u_2}⦄, a < b + o → ∃ i, a < b + f i
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.comap_range_self : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.comap f f.range = ⊤
-- Lean.MetavarContext
Lean.MetavarContext.mkForall : Array Lean.Expr →
  Lean.Expr →
    optParam Bool false →
      optParam Bool true →
        optParam Bool true →
          optParam Lean.BinderInfo Lean.BinderInfo.implicit → Lean.MetavarContext.MkBindingM Lean.Expr
-- Std.Sync.Broadcast
/-- A channel that can create `Bounded.Receiver` and send messages.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded : Type → Type
-- Mathlib.LinearAlgebra.BilinearMap
IsBilinearMap.smul_right : ∀ {R : Type u_1} [inst : CommSemiring R] {E : Type u_2} [inst_1 : AddCommMonoid E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommMonoid F] [inst_4 : Module R F] {G : Type u_4} [inst_5 : AddCommMonoid G] [inst_6 : Module R G]
  {f : E → F → G}, IsBilinearMap R f → ∀ (c : R) (x : E) (y : F), f x (c • y) = c • f x y
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_rel₁ : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {v : α → M} {R : L.Relations 1}
  {t : L.Term α},
  (R.formula₁ t).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize v t]
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_eq_iInter_thickening'' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.cthickening δ E = ⋂ ε, ⋂ (_ : max 0 δ < ε), Metric.thickening ε E
-- Mathlib.ModelTheory.LanguageMap
/-- The inclusion of the left factor into the sum of two languages.  -/
FirstOrder.Language.LHom.sumInl : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → L →ᴸ L.sum L'
-- Mathlib.Data.Set.Card
Set.nonempty_inter_of_lt_ncard_add_ncard : ∀ {α : Type u_1} {s t : Set α} [Finite α], Nat.card α < s.ncard + t.ncard → (s ∩ t).Nonempty
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t) {Z : C} (h : r.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv
      (CategoryTheory.CategoryStruct.comp (P.desc r) h) =
    CategoryTheory.CategoryStruct.comp (Q.desc r) h