mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₀ F₁ F₂ : CategoryTheory.Functor C C} (α : F₀ ⟶ F₁)
  (β : F₁ ⟶ F₂) (X : CategoryTheory.Endofunctor.Coalgebra F₀),
  ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α β).hom.app X).f = CategoryTheory.CategoryStruct.id X.V
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.private : Lean.Elab.Visibility
-- Mathlib.Analysis.Normed.Group.Uniform
edist_add_add_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E),
  edist (a₁ + a₂) (b₁ + b₂) ≤ edist a₁ b₁ + edist a₂ b₂
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinite_iff_exist_lt_gt : ∀ {x : ℝ*}, ¬x.Infinite ↔ ∃ r s, ↑r < x ∧ x < ↑s
-- Mathlib.CategoryTheory.Shift.Opposite
/-- The natural isomorphism `NatTrans.OppositeShift.natIsoId C A` commutes with shifts.
 -/
CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A : Type u_3) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.OppositeShift.natIsoId C A).hom A
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.concreteCategory : {R : Type u} →
  [inst : CommRing R] → CategoryTheory.ConcreteCategory (HopfAlgCat R) fun x1 x2 => x1.carrier →ₐc[R] x2.carrier
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp},
  Std.TreeMap.empty.Equiv t ↔ t.isEmpty = true
-- Mathlib.LinearAlgebra.Matrix.Cartan
Matrix.IsSimplyLaced.eq_1 : ∀ {ι : Type u_1} (A : Matrix ι ι ℤ), A.IsSimplyLaced = Pairwise fun i j => A i j = 0 ∨ A i j = -1
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Equiv.cg_iff : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N]
  (f : L.Equiv M N), FirstOrder.Language.Structure.CG L M ↔ FirstOrder.Language.Structure.CG L N
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, (m.erase k)[a]? = if (k == a) = true then none else m[a]?
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_le_size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α}, m.size ≤ (m.insertMany l).size
-- Init.Data.Array.QSort.Basic
_private.Init.Data.Array.QSort.Basic.0.Array.qsort.match_8.eq_1 : ∀ {α : Type u_1} {n : ℕ} (lo hi : ℕ) (motive : { m // lo ≤ m ∧ m ≤ hi } × Vector α n → Sort u_2) (mid : ℕ)
  (hmid : lo ≤ mid ∧ mid ≤ hi) (as : Vector α n)
  (h_1 : (mid : ℕ) → (hmid : lo ≤ mid ∧ mid ≤ hi) → (as : Vector α n) → motive (⟨mid, hmid⟩, as)),
  (match (⟨mid, hmid⟩, as) with
    | (⟨mid, hmid⟩, as) => h_1 mid hmid as) =
    h_1 mid hmid as
-- Mathlib.Algebra.Module.Equiv.Basic
Units.symm_mulLeftLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a : Aˣ), ((Units.mulLeftLinearEquiv R A) a).symm = (Units.mulLeftLinearEquiv R A) a⁻¹
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwise_iUnion : ∀ {α : Type u_1} {κ : Sort u_4} {r : α → α → Prop} {f : κ → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) f → ((⋃ n, f n).Pairwise r ↔ ∀ (n : κ), (f n).Pairwise r)
-- Init.Data.Nat.Gcd
Nat.instIdempotentOpGcd : Std.IdempotentOp Nat.gcd
-- Mathlib.Topology.ContinuousOn
continuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.comp.mk_get : ∀ {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α : TypeVec.{u} m} (x : ↑(P.comp Q) α),
  MvPFunctor.comp.mk (MvPFunctor.comp.get x) = x
-- Mathlib.Order.Filter.Pointwise
Filter.zero_neBot : ∀ {α : Type u_2} [inst : Zero α], Filter.NeBot 0
-- Mathlib.Data.Matrix.Mul
/-- Associate the dot product of `mulVec` to the left.  -/
Matrix.dotProduct_mulVec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : NonUnitalSemiring R]
  (v : m → R) (A : Matrix m n R) (w : n → R), v ⬝ᵥ A.mulVec w = Matrix.vecMul v A ⬝ᵥ w
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.oddKernel_undef : ∀ (a : UnitAddCircle) {x : ℝ}, x ≤ 0 → HurwitzZeta.oddKernel a x = 0
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.StrictBackwardPattern.ne_endPos : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.BackwardPattern pat}
  [self : String.Slice.Pattern.StrictBackwardPattern pat] {s : String.Slice} (h : s.isEmpty = false) (q : s.Pos),
  String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty? pat s h = some q → q ≠ s.endPos
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
/-- Equivalence relation on iterators. Equivalent iterators behave the same as long as the
internal state of them is not directly inspected.

Two iterators (possibly of different types) are equivalent if they have the same
`Iterator.IsPlausibleStep` relation and their step functions are the same *up to equivalence of the
successor iterators*. This coinductive definition captures the idea that the only relevant feature
of an iterator is its step function. Other information retrievable from the iterator -- for example,
whether it is a list iterator or an array iterator -- is totally irrelevant for the equivalence
judgement.
 -/
Std.Iter.Equiv : {α₁ α₂ β : Type u_1} → [Std.Iterator α₁ Id β] → [Std.Iterator α₂ Id β] → Std.Iter β → Std.Iter β → Prop
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is upper semicontinuous at `x` if, for any `ε > 0`, for all `x'` close
enough to `x`, then `f x'` is at most `f x + ε`. We formulate this in a general preordered space,
using an arbitrary `y > f x` instead of `f x + ε`.  -/
UpperSemicontinuousAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → α → Prop
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_stepk_cert.eq_1 : ∀ (k₁ : ℤ) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.d_stepk_cert k₁ p₁ k₂ m₂ p₂ p =
    p.beq' ((Lean.Grind.CommRing.Poly.mulConst_k k₁ p₁).combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂))
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + t/n) ^ n` as `n → ∞` is `exp t` for `t : ℂ`.  -/
Complex.tendsto_one_add_div_pow_exp : ∀ (t : ℂ), Filter.Tendsto (fun n => (1 + t / ↑n) ^ n) Filter.atTop (nhds (Complex.exp t))
-- Lean.Meta.FunInfo
Lean.Meta.getFunInfoNArgs : Lean.Expr → ℕ → Lean.MetaM Lean.Meta.FunInfo
-- Mathlib.Order.SupClosed
infClosure_idem : ∀ {α : Type u_3} [inst : SemilatticeInf α] (s : Set α), infClosure (infClosure s) = infClosure s
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_eq_iInter_thickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ},
  0 ≤ δ → ∀ (E : Set α), Metric.cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), Metric.thickening ε E
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToFormatContext : Std.ToFormat Mathlib.Tactic.ITauto.Context
-- Mathlib.Order.LiminfLimsup
Filter.limsup_le_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.limsup_le_of_le._auto_1 →
    (∀ᶠ (n : β) in f, u n ≤ a) → Filter.limsup u f ≤ a
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_beq : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain c pos pos' ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAtChain (fun x => x == c) pos pos'
-- Mathlib.Data.Finset.Pi
Finset.restrict₂_comp_restrict₂ : ∀ {ι : Type u_2} {π : ι → Type u_3} {s t u : Finset ι} (hst : s ⊆ t) (htu : t ⊆ u),
  Finset.restrict₂ hst ∘ Finset.restrict₂ htu = Finset.restrict₂ ⋯
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_sup_of_normal_left : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  IsPGroup p ↥H → IsPGroup p ↥K → ∀ [H.Normal], IsPGroup p ↥(H ⊔ K)
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- The colimit type of a functor from a finite category to Types that only
involves finite objects is finite.  -/
CategoryTheory.Limits.FintypeCat.finite_colimitType : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (K : CategoryTheory.Functor J (Type u)) [∀ (j : J), Finite (K.obj j)], Finite K.ColimitType
-- Lean.Parser.Term
Lean.Parser.Term.haveI.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.mk : Lean.Syntax → Array Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Elab.Term.LetIdDeclView
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_def : ∀ {R : Type u_1} [inst : Semiring R] {s : Unit →₀ ℕ} {n : ℕ}, s () = n → PowerSeries.coeff n = MvPowerSeries.coeff s
-- Mathlib.Order.CompleteLattice.Basic
iSup_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {g : β → α} {f : ι → β},
  ⨆ b ∈ Set.range f, g b = ⨆ i, g (f i)
-- Mathlib.Data.Finset.NAry
Finset.image₂_inter_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β}
  [inst_1 : DecidableEq β],
  Function.Injective2 f → Finset.image₂ f s (t ∩ t') = Finset.image₂ f s t ∩ Finset.image₂ f s t'
-- Mathlib.RingTheory.FractionalIdeal.Basic
_private.Mathlib.RingTheory.FractionalIdeal.Basic.0.Nat.unaryCast.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Data.Finset.Pi
/-- The empty dependent product function, defined on the empty set. The assumption `a ∈ ∅` is never
satisfied.  -/
Finset.Pi.empty : {α : Type u_1} → (β : α → Sort u_2) → (a : α) → a ∈ ∅ → β a
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_centralizer_iff : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A} {z : A},
  z ∈ NonUnitalSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀] (i : σ),
  (MvPolynomial.map (algebraMap R₀ R)) (P.jacobianRelationsOfHasCoeffs R₀ i) = P.jacobianRelations i
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_eq_dist_iff_vsub_mem_span : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P), ((signedDist v) p) q = dist p q ↔ q -ᵥ p ∈ NNReal ∙ v
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_iInter_apply : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : CompleteLattice M] [inst_1 : One M] [Nonempty ι],
  ⊥ = 1 → ∀ (s : ι → Set α) (f : α → M) (x : α), (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x
-- Mathlib.Data.ENNReal.Basic
ENNReal.instInv : Inv ENNReal
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.bind₁_frobeniusPoly_wittPolynomial : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  (MvPolynomial.bind₁ (WittVector.frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.inv_eq' : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (hf : f v = 0) (hf' : autoParam ((-f) v = 0) LinearEquiv.transvection.inv_eq'._auto_1),
  (LinearEquiv.transvection hf)⁻¹ = LinearEquiv.transvection hf'
-- Mathlib.Algebra.Star.Basic
/-- A \*-additive monoid `R` is an additive monoid with an involutive `star` operation which
preserves addition.  -/
StarAddMonoid : (R : Type u) → [AddMonoid R] → Type u
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Any path to `a` gives `treeHom T a`, since paths in the tree are unique.  -/
IsFreeGroupoid.SpanningTree.treeHom_eq : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : G}
  (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a),
  IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T p
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_sub : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Sub Y] (f g : LocallyConstant X Y),
  ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Triangle.scalene_iff_dist_ne_and_dist_ne_and_dist_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {t : Affine.Triangle R P},
  Affine.Simplex.Scalene t ↔
    dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
      dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
        dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- A generalization of the **Matrix determinant lemma**  -/
Matrix.det_add_mul : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} (U : Matrix m n α) (V : Matrix n m α),
  IsUnit A.det → (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.comp_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (g : L.Hom N P) (f : L.Hom M N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.ext_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {x y : Monoid.CoprodI.Word M},
  x = y ↔ x.toList = y.toList
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.insertMany m l) k =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if (a == k) = true then some b else none)
              l).or
          (Std.DHashMap.Raw.Const.get? m k)
-- Mathlib.GroupTheory.OrderOfElement
multiplesEquivMultiples_apply : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [inst_1 : Finite G] {x y : G} (h : addOrderOf x = addOrderOf y) (n : ℕ),
  (multiplesEquivMultiples h) ⟨n • x, ⋯⟩ = ⟨n • y, ⋯⟩
-- Lean.Elab.ParseImportsFast
_private.Lean.Elab.ParseImportsFast.0.Lean.ParseImports.moduleIdent.parse : String → (Lean.Name → Lean.ParseImports.Parser) → Lean.Name → Lean.ParseImports.State → Lean.ParseImports.State
-- Std.Time.Time.Unit.Nanosecond
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Nanosecond.Offset.ofNat : ℕ → Std.Time.Nanosecond.Offset
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- The inverse map of a homeomorphism is a continuous function.  -/
ContinuousAlgEquiv.continuous_invFun : ∀ {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] (self : A ≃A[R] B), Continuous self.invFun
-- Batteries.Control.AlternativeMonad
failure_seqLeft : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Alternative m] [LawfulAlternative m] (x : m α),
  failure <* x = failure
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.id_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (V : CategoryTheory.Endofunctor.Coalgebra F),
  CategoryTheory.Endofunctor.Coalgebra.Hom.id V = CategoryTheory.CategoryStruct.id V
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_pos' : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {x : R}, 0 < Polynomial.rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.rightUnitor_hom_iso : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor x).hom.iso = CategoryTheory.Bicategory.rightUnitor x.of
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.clear : (Turing.PartrecToTM2.Γ' → Bool) → Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.Data.Set.Semiring
SetSemiring.down_up : ∀ {α : Type u_1} (s : Set α), SetSemiring.down (Set.up s) = s
-- Mathlib.Order.Category.PartOrd
PartOrd.dualEquiv_functor : PartOrd.dualEquiv.functor = PartOrd.dual
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Ref.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (gate : ℕ) (invert : Bool)
  (hgate : gate < aig.decls.size) (gate_1 : ℕ) (invert_1 : Bool) (hgate_1 : gate_1 < aig.decls.size),
  ({ gate := gate, invert := invert, hgate := hgate } = { gate := gate_1, invert := invert_1, hgate := hgate_1 }) =
    (gate = gate_1 ∧ invert = invert_1)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracket_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W V₁ : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt (T% V) x →
    MDiffAt (T% V₁) x →
      VectorField.mlieBracket I (V + V₁) W x = VectorField.mlieBracket I V W x + VectorField.mlieBracket I V₁ W x
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- A proof that each element of `parts` doesn't have a pair of adjacent vertices.  -/
SimpleGraph.Partition.independent : ∀ {V : Type u} {G : SimpleGraph V} (self : G.Partition), ∀ s ∈ self.parts, IsAntichain G.Adj s
-- Mathlib.Util.Tactic
/-- `modifyLocalDecl mvarId fvarId f` updates the local decl `fvarId` in the local
context of `mvarId` with `f`. `f` must leave the `fvarId` and `index` of the
`LocalDecl` unchanged. The type of the new `LocalDecl` must be defeq to the type
of the old `LocalDecl` (and the same applies to the value of the `LocalDecl`, if
any).

If `mvarId` does not refer to a declared metavariable or if `fvarId` does not
exist in the local context of `mvarId`, nothing happens.
 -/
Mathlib.Tactic.modifyLocalDecl : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → Lean.FVarId → (Lean.LocalDecl → Lean.LocalDecl) → m Unit
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instIntCast : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → IntCast (WithVal v)
-- Mathlib.Order.Filter.Map
Filter.comap_eq_bot_iff_compl_range : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, Filter.comap m f = ⊥ ↔ (Set.range m)ᶜ ∈ f
-- Mathlib.Computability.TuringMachine.Tape
/-- The `map` function on lists is well defined on `ListBlank`s provided that the map is
pointed.  -/
Turing.ListBlank.map : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    [inst : Inhabited Γ] → [inst_1 : Inhabited Γ'] → Turing.PointedMap Γ Γ' → Turing.ListBlank Γ → Turing.ListBlank Γ'
-- Mathlib.Logic.Equiv.Finset
_private.Mathlib.Logic.Equiv.Finset.0.Denumerable.lower'.match_1.eq_1 : ∀ (motive : List ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (m : ℕ) → (l : List ℕ) → (n : ℕ) → motive (m :: l) n),
  (match [], x with
    | [], x => h_1 x
    | m :: l, n => h_2 m l n) =
    h_1 x
-- Mathlib.Geometry.Convex.Cone.Basic
Convex.mem_toCone' : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s) {x : M},
  x ∈ Convex.toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s
-- Mathlib.CategoryTheory.Category.PartialFun
pointedToPartialFun_obj : ∀ (X : Pointed), pointedToPartialFun.obj X = PartialFun.of { x // x ≠ X.point }
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Summable.tendstoUniformlyOn_tsum_nat_log_one_add : ∀ {α : Type u_1} {K : Set α} {f : ℕ → α → ℂ} {u : ℕ → ℝ},
  Summable u →
    (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) →
      TendstoUniformlyOn (fun n x => ∑ m ∈ Finset.range n, Complex.log (1 + f m x))
        (fun x => ∑' (n : ℕ), Complex.log (1 + f n x)) Filter.atTop K
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.DHashMap.Const.unitOfList l).getKeyD k' fallback = k
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ihom_obj_ρ_def : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B : Rep.{u, u, v} k G),
  (A ⟹ B).ρ = (A.ihom.obj B).ρ
-- Init.Data.Array.Attach
Array.unattach_reverse : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }}, xs.reverse.unattach = xs.unattach.reverse
-- Mathlib.Data.Num.Bitwise
instDecidableEqSNum.decEq : (x x_1 : SNum) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.mk.inj : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {obj : C → D → Type w} {map : {X X' : C} → {Y Y' : D} → (X ⟶ X') → (Y ⟶ Y') → (obj X Y' ⟶ obj X' Y)}
  {map_id :
    autoParam
      (∀ (X : C) (Y : D),
        map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
          CategoryTheory.CategoryStruct.id (obj X Y))
      CategoryTheory.ProfunctorCore.map_id._autoParam}
  {map_comp :
    autoParam
      (∀ {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃),
        map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') =
          CategoryTheory.CategoryStruct.comp (map f g') (map f' g))
      CategoryTheory.ProfunctorCore.map_comp._autoParam}
  {obj_1 : C → D → Type w} {map_1 : {X X' : C} → {Y Y' : D} → (X ⟶ X') → (Y ⟶ Y') → (obj_1 X Y' ⟶ obj_1 X' Y)}
  {map_id_1 :
    autoParam
      (∀ (X : C) (Y : D),
        map_1 (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
          CategoryTheory.CategoryStruct.id (obj_1 X Y))
      CategoryTheory.ProfunctorCore.map_id._autoParam}
  {map_comp_1 :
    autoParam
      (∀ {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃),
        map_1 (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') =
          CategoryTheory.CategoryStruct.comp (map_1 f g') (map_1 f' g))
      CategoryTheory.ProfunctorCore.map_comp._autoParam},
  { obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map_comp := map_comp_1 } →
    obj = obj_1 ∧ map ≍ map_1