mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between two vectors is zero if and only if the first vector is zero or
the second is a multiple of a `π / 2` rotation of that vector.  -/
Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, inner ℝ x y = 0 ↔ x = 0 ∨ ∃ r, r • (o.rotation ↑(Real.pi / 2)) x = y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.finite_range : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β), (Set.range ⇑f).Finite
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instInterOfBEqOfHashable : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Inter (Std.HashMap.Raw α β)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofNatIso_inr : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂) {F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} (e : F ≅ F'),
  (sq.ofNatIso e).inr = CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app Y₂) sq.inr
-- Mathlib.Analysis.SpecialFunctions.Sqrt
HasFDerivAt.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E},
  HasFDerivAt f f' x → f x ≠ 0 → HasFDerivAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') x
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.homDiagram_map : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat}
  (X Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) {X_1 Y_1 : J} (f : X_1 ⟶ Y_1),
  (CategoryTheory.Cat.HasLimits.homDiagram X Y).map f =
    TypeCat.ofHom fun g =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map g) (CategoryTheory.eqToHom ⋯))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C) (x : B), (F.mapIdIso x).inv = CategoryTheory.eqToHom ⋯
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
/-- If `f` maps `p ^ i` to `(f p) ^ i` for primes `p`, and `f`
is multiplicative on coprime elements, then `f` is multiplicative on all products of primes.  -/
UniqueFactorizationMonoid.multiplicative_prime_power : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3}
  [inst_2 : CommMonoidWithZero β] {f : α → β} (s : Finset α) (i j : α → ℕ),
  (∀ p ∈ s, Prime p) →
    (∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) →
      (∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) →
        (∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) →
          (∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y) →
            f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eraseKey_eq_iff_beq_minKey!_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.minKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey! l ↔
          (k == Std.Internal.List.minKey! l) = false)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.map_le : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} {U : Subalgebra R B},
  Subalgebra.map f S ≤ U ↔ S ≤ Subalgebra.comap f U
-- Mathlib.Data.List.Forall2
List.forall₂_refl : ∀ {α : Type u_1} {Rₐ : α → α → Prop} [Std.Refl Rₐ] (l : List α), List.Forall₂ Rₐ l l
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.mk : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α},
  (∀ I ∈ S, IsAtom I) →
    (∀ (s : Finset α) (a : α), ↑s ⊆ S → IsCompactElement a → a ≤ s.sup id → ∃ t ⊆ s, a = t.sup id) →
      IsCompactlyGenerated.BooleanGenerators S
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
CategoryTheory.Precoherent.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ {B₁ B₂ : C} (f : B₂ ⟶ B₁) (α : Type) [Finite α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁),
      CategoryTheory.EffectiveEpiFamily X₁ π₁ →
        ∃ β,
          ∃ (_ : Finite β),
            ∃ X₂ π₂,
              CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧
                ∃ i ι,
                  ∀ (b : β),
                    CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f) →
    CategoryTheory.Precoherent C
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support_neg : ∀ {X : Type u_1} (a : FreeAbelianGroup X), (-a).support = a.support
-- Mathlib.Data.Holor
HolorIndex.cast_type : ∀ {ds₁ ds₂ : List ℕ} (is : List ℕ) (eq : ds₁ = ds₂) (h : List.Forall₂ (fun x1 x2 => x1 < x2) is ds₁),
  ↑(cast ⋯ ⟨is, h⟩) = is
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
_private.Mathlib.LinearAlgebra.ExteriorPower.Basic.0.exteriorPower.presentation.relations.match_1.eq_3 : ∀ (R : Type u_1) (ι : Type u_2) (M : Type u_3) (motive : exteriorPower.presentation.Rels R ι M → Sort u_4) (m : ι → M)
  (i j : ι) (hm : m i = m j) (hij : i ≠ j)
  (h_1 : (m : ι → M) → (i : ι) → (x y : M) → motive (exteriorPower.presentation.Rels.add m i x y))
  (h_2 : (m : ι → M) → (i : ι) → (r : R) → (x : M) → motive (exteriorPower.presentation.Rels.smul m i r x))
  (h_3 :
    (m : ι → M) →
      (i j : ι) → (hm : m i = m j) → (hij : i ≠ j) → motive (exteriorPower.presentation.Rels.alt m i j hm hij)),
  (match exteriorPower.presentation.Rels.alt m i j hm hij with
    | exteriorPower.presentation.Rels.add m i x y => h_1 m i x y
    | exteriorPower.presentation.Rels.smul m i r x => h_2 m i r x
    | exteriorPower.presentation.Rels.alt m i j hm hij => h_3 m i j hm hij) =
    h_3 m i j hm hij
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalRing.toIsTopologicalSemiring : ∀ {R : Type u_1} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocRing R} [self : IsTopologicalRing R],
  IsTopologicalSemiring R
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.coeList : {α : Type u} → Coe (List α) (Stream'.WSeq α)
-- Init.Data.UInt.Lemmas
USize.toUInt8_add : ∀ (a b : USize), (a + b).toUInt8 = a.toUInt8 + b.toUInt8
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The top level program.  -/
Turing.TM1to1.tr : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      {n : ℕ} →
        (Γ → List.Vector Bool n) →
          (List.Vector Bool n → Γ) →
            (Λ → Turing.TM1.Stmt Γ Λ σ) → Turing.TM1to1.Λ' Γ Λ σ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
ZMod.instIsAddCyclic : ∀ (n : ℕ), IsAddCyclic (ZMod n)
-- Init.Omega.IntList
Lean.Omega.IntList.sdiv_nil : ∀ {g : ℤ}, Lean.Omega.IntList.sdiv [] g = []
-- Mathlib.Geometry.Euclidean.Incenter
/-- The excenter with signs determined by the given set of indices (for the empty set, this is
the incenter; for a singleton set, this is the excenter opposite a vertex).  This is only
meaningful if `s.ExcenterExists signs`; otherwise, it is some arbitrary point.  -/
Affine.Simplex.excenter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → P
-- Init.Data.Array.Lemmas
Array.foldr_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {init : β}, Array.foldr f init #[] = init
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasLaw.prodMk_of_hasCondDistrib : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {Q : MeasureTheory.Measure 𝓧},
  ProbabilityTheory.HasLaw X Q P →
    ProbabilityTheory.HasCondDistrib Y X κ P → ProbabilityTheory.HasLaw (fun ω => (X ω, Y ω)) (Q.compProd κ) P
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.add_le_add_iff_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α] [AddLeftMono α] {a b c : α},
  AddLECancellable a → (a + b ≤ a + c ↔ b ≤ c)
-- Lean.Meta.Match.Basic
_private.Lean.Meta.Match.Basic.0.Lean.Meta.Match.Pattern.toExpr.visit : Bool → Lean.Meta.Match.Pattern → Lean.MetaM Lean.Expr
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetInstance.mk.inj : ∀ {toWidgetInstance : Lean.Widget.WidgetInstance} {range? : Option Lean.Lsp.Range} {name? : Option String}
  {toWidgetInstance_1 : Lean.Widget.WidgetInstance} {range?_1 : Option Lean.Lsp.Range} {name?_1 : Option String},
  { toWidgetInstance := toWidgetInstance, range? := range?, name? := name? } =
      { toWidgetInstance := toWidgetInstance_1, range? := range?_1, name? := name?_1 } →
    toWidgetInstance = toWidgetInstance_1 ∧ range? = range?_1 ∧ name? = name?_1
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.body : Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.image_vertexSet : ∀ {α : Type u_1} {β : Type u_2} (H : Hypergraph α) (f : α → β), (H.image f).vertexSet = f '' H.vertexSet
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.descOpcycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1)
  (n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x x_1 : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ A)
  (e_x : x = x_1) (hx : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0),
  X.descOpcycles f g n₀ n₁ hn₁ x hx = X.descOpcycles f g n₀_1 n₁ ⋯ x_1 ⋯
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.r_trans : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {a b c : α × α},
  Lean.Grind.Ring.OfSemiring.r α a b → Lean.Grind.Ring.OfSemiring.r α b c → Lean.Grind.Ring.OfSemiring.r α a c
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
MeasureTheory.analyticSet_range_of_polishSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] [PolishSpace β] {f : β → α},
  Continuous f → MeasureTheory.AnalyticSet (Set.range f)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_nil_iff : ∀ {n : ℕ}, (*...n).toList = [] ↔ n = 0
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- An absolute left Kan lift is a Kan lift such that every 1-morphism commutes with it.  -/
CategoryTheory.Bicategory.LeftLift.IsAbsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.LeftLift f g → Type (max (max u v) w)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_balanceₘ : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.balanceₘ k v l r).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Construct a strong natural transformation from a lax natural transformation whose
naturality 2-morphism is an isomorphism.  -/
CategoryTheory.Lax.StrongTrans.mkOfLax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (η : CategoryTheory.Lax.LaxTrans F G) → η.StrongCore → CategoryTheory.Lax.StrongTrans F G
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesIsoSc'_hom_iCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (K.sc' i j k).iCycles = K.iCycles j
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?_eq_match.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
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.insert! k v t) = true
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNatCast.eq_1 : ∀ {R : Type u_1} [inst : NatCast R], MulOpposite.instNatCast = { natCast := fun n => MulOpposite.op ↑n }
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_eq_toReal_iff : ∀ (x y : ENNReal), x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0
-- Init.Data.BitVec.Lemmas
/-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
smaller than the bitwidth.  -/
BitVec.rotateRight_eq_rotateRightAux_of_lt : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, r < w → x.rotateRight r = x.rotateRightAux r
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(uliftYoneda.obj X).obj Y = ULift (unop Y ⟶ X)`.  -/
CategoryTheory.uliftYoneda_obj_obj_eq_hom' : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → Cᵒᵖ → Cᵒᵖ → Prop
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.rfl : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set α → Prop}, μ.InnerRegularWRT p p
-- Mathlib.Algebra.Order.Ring.Abs
abs_mul_self : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] (a : α), |a * a| = a * a
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (W : CategoryTheory.MorphismProperty C) {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂),
  W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The size of `s * s` is at least the size of `s`, version with left-cancellative multiplication.
See `card_le_card_mul_self'` for the version with right-cancellative multiplication.
 -/
Finset.card_le_card_mul_self : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [inst_2 : DecidableEq α] {s : Finset α}, s.card ≤ (s * s).card
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS_toPolyS : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α)
  (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Poly.denoteS ctx e.toPolyS = Lean.Grind.CommRing.Expr.denoteS ctx e
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.of_add : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (w z : P.ker.Cotangent),
  Algebra.Extension.Cotangent.of (w + z) = Algebra.Extension.Cotangent.of w + Algebra.Extension.Cotangent.of z
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.single_v_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ L.X q) (n p' q' : ℤ) (hpq' : p' + n = q'),
  p' ≠ p → (CochainComplex.HomComplex.Cochain.single f n).v p' q' hpq' = 0
-- Init.Data.Int.Gcd
Int.lcm_dvd : ∀ {a b : ℤ} {c : ℕ}, a ∣ ↑c → b ∣ ↑c → a.lcm b ∣ c
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {hom : X ⟶ Y} {inv : Y ⟶ X}
  {hom_inv_id :
    autoParam (CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Iso.hom_inv_id._autoParam}
  {inv_hom_id :
    autoParam (CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.Iso.inv_hom_id._autoParam}
  {hom_1 : X ⟶ Y} {inv_1 : Y ⟶ X}
  {hom_inv_id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 inv_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Iso.hom_inv_id._autoParam}
  {inv_hom_id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inv_1 hom_1 = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.Iso.inv_hom_id._autoParam},
  { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } =
      { hom := hom_1, inv := inv_1, hom_inv_id := hom_inv_id_1, inv_hom_id := inv_hom_id_1 } →
    hom = hom_1 ∧ inv = inv_1
-- Mathlib.Analysis.Normed.Lp.PiLp
_private.Mathlib.Analysis.Normed.Lp.PiLp.0.PiLp.lipschitzWith_ofLp_aux : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fact (1 ≤ p)] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
  [inst_2 : Fintype ι], LipschitzWith 1 WithLp.ofLp
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ofList_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {l : List ((a : α) × β a)},
  (Std.DTreeMap.ofList l cmp).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) ∅ l)
-- Mathlib.Data.Finset.NAry
Finset.sup_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
  (t : Finset β) [inst_1 : SemilatticeSup δ] [inst_2 : OrderBot δ] (g : γ → δ),
  (Finset.image₂ f s t).sup g = t.sup fun y => s.sup fun x => g (f x y)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.le_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : LE Y] [inst_2 : Zero Y]
  {D₁ D₂ : Function.locallyFinsuppWithin U Y}, D₁ ≤ D₂ ↔ ⇑D₁ ≤ ⇑D₂
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
AbsoluteValue.IsAdmissible.mk : {R : Type u_1} →
  [inst : EuclideanDomain R] →
    {abv : AbsoluteValue R ℤ} →
      abv.IsEuclidean →
        (card : ℝ → ℕ) →
          (∀ (n : ℕ) {ε : ℝ},
              0 < ε →
                ∀ {b : R},
                  b ≠ 0 →
                    ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε) →
            abv.IsAdmissible
-- Mathlib.Data.Num.ZNum
ZNum.zneg_neg : ∀ (n : PosNum), -ZNum.neg n = ZNum.pos n
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instTransOrdOfDay : Std.TransOrd Std.Time.Nanosecond.Ordinal.OfDay
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.obj_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n)
  (X : C), CategoryTheory.ComposableArrows.Precomp.obj F X 1 = F.obj' 0 ⋯
-- Init.Data.UInt.Lemmas
UInt8.add_mul : ∀ {a b c : UInt8}, (a + b) * c = a * c + b * c
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.mk.injEq : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (toDistribMulActionHom : A →ₑ+[φ] B)
  (map_mul' :
    ∀ (x y : A), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y)
  (toDistribMulActionHom_1 : A →ₑ+[φ] B)
  (map_mul'_1 :
    ∀ (x y : A),
      toDistribMulActionHom_1.toFun (x * y) = toDistribMulActionHom_1.toFun x * toDistribMulActionHom_1.toFun y),
  ({ toDistribMulActionHom := toDistribMulActionHom, map_mul' := map_mul' } =
      { toDistribMulActionHom := toDistribMulActionHom_1, map_mul' := map_mul'_1 }) =
    (toDistribMulActionHom = toDistribMulActionHom_1)
-- Std.Do.Triple.SpecLemmas
/-- An invariant for a `repeatM` loop, given as a `PostCond` over the `α ⊕ β` cursor:
`.inl a` is the `continue` case at `a`; `.inr b` is the `break` case with result `b`.
 -/
Std.Do.WhileInvariant : Type u → Type u → Std.Do.PostShape → Type u
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.query : LeanSearchClient.SearchServer → String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult)
-- Mathlib.CategoryTheory.Action.Monoidal
Action.leftRegularTensorIso_inv_hom : ∀ (G : Type u) [inst : Group G] (X : Action (Type u) G),
  (Action.leftRegularTensorIso G X).inv.hom =
    { toFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
          invFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯,
          right_inv := ⋯ }.toIso.inv
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.ColimitType.AddGroupWithOne : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → AddGroupWithOne (RingCat.Colimits.ColimitType F)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.mk_singleton : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {x : α},
  { carrier := {x}, isIrreducible' := ⋯, isClosed' := ⋯ } = {x}
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.instIsSplitMonoInl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f], CategoryTheory.IsSplitMono (CategoryTheory.Limits.pushout.inl f f)
-- Mathlib.Order.Ideal
/-- A specific witness of `I.directed` when `P` has joins.  -/
Order.Ideal.sup_mem : ∀ {P : Type u_1} [inst : SemilatticeSup P] {x y : P} {s : Order.Ideal P}, x ∈ s → y ∈ s → x ⊔ y ∈ s
-- Mathlib.FieldTheory.AlgebraicClosure
/-- An element is contained in the algebraic closure of `F` in `E` if and only if
it is an algebraic element.  -/
mem_algebraicClosure_iff : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ algebraicClosure F E ↔ IsAlgebraic F x
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.injectiveDimension_le_injectiveDimension_of_isLocalizedModule : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (S : Submonoid R) (M : ModuleCat R),
  CategoryTheory.injectiveDimension (M.localizedModule S) ≤ CategoryTheory.injectiveDimension M
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_neg_distrib : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module ℚ≥0 M] (s : Finset ι) (f : ι → M),
  (s.expect fun i => -f i) = -s.expect fun i => f i
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.wrepr.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n},
  MvQPF.wrepr = MvQPF.recF ((MvQPF.P F).wMk' ∘ MvQPF.repr)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrTheoremCacheKey.mk : Lean.Expr → ℕ → Lean.Meta.Grind.CongrTheoremCacheKey
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Complex.exp` is complex analytic.  -/
analyticOn_cexp : AnalyticOn ℂ Complex.exp Set.univ
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.congr_simp : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A A_1 : IntermediateField F E),
  A = A_1 →
    ∀ (L : Type w) [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
      A.LinearDisjoint L = A_1.LinearDisjoint L
-- Mathlib.Data.Finset.Dedup
Finset.val_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s.val.toFinset = s