mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow'_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier (CategoryTheory.Limits.kernel f)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobjectIso f).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) x
-- Mathlib.Algebra.Group.Center
/-- The centralizer of the product of non-empty sets is equal to the product of the centralizers.  -/
Set.centralizer_prod : ∀ {M : Type u_1} [inst : Mul M] {N : Type u_2} [inst_1 : Mul N] {S : Set M} {T : Set N},
  S.Nonempty → T.Nonempty → (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer
-- Init.Data.List.Impl
/-- Auxiliary for `flatMap`: `flatMap.go f as = acc.toList ++ bind f as`  -/
_private.Init.Data.List.Impl.0.List.flatMapTR.go : {α : Type u_1} → {β : Type u_2} → (α → List β) → List α → Array β → List β
-- Mathlib.GroupTheory.Torsion
CommGroup.isMulTorsionFree_iff_torsion_eq_bot : ∀ {G : Type u_1} [inst : CommGroup G], IsMulTorsionFree G ↔ CommGroup.torsion G = ⊥
-- Std.Data.Internal.List.Associative
Std.Internal.List.alterKey_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
  {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → (Std.Internal.List.alterKey a f l).Perm (Std.Internal.List.alterKey a f l')
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTriv_continuousLinearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) {i : ι}
  {b : B},
  b ∈ (Z.localTriv i).baseSet →
    Bundle.Trivialization.continuousLinearMapAt R (Z.localTriv i) b = Z.coordChange (Z.indexAt b) i b
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.toLinearEquiv_prodEquivOfIsTopCompl : ∀ {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),
  ↑(p.prodEquivOfIsTopCompl q h) = p.prodEquivOfIsCompl q ⋯
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.processNewFactsImpl : Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_iSup_comap_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f →
    ∀ {ι : Sort u_9} (S : ι → Submodule R₂ M₂), Submodule.map f (⨆ i, Submodule.comap f (S i)) = iSup S
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.zero_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : Zero β], 0 x = 0
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- Pythagorean theorem, if-and-only-if vector angle form.  -/
InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi / 2
-- Mathlib.Order.Filter.Map
Filter.seq_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Filter α) (g : Filter (α → β)) (h : Filter (β → γ)),
  h.seq (g.seq x) = ((Filter.map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.root_eq_neg_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j : ι},
  P.root i = -P.root j ↔ i = (P.reflectionPerm j) j
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_mul_left_add_right : ∀ (m n k : ℕ), m.Coprime (m * k + n) ↔ m.Coprime n
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.carrier_eq_coe : ∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), U.carrier = ↑U
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
PowerBasis.ofAdjoinEqTop'_gen : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x) (hx' : R[x] = ⊤), (PowerBasis.ofAdjoinEqTop' hx hx').gen = x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_map_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} (e : ι ≃ κ),
  (Finset.map e.toEmbedding s).sum (f ∘ ⇑e.symm) = s.sum f
-- Batteries.Recycling.RBTree.Basic
/-- Recolor the root of the tree to `red` if possible.  -/
RBTree.RBNode.setRed : {α : Type u_1} → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.le_preAleph_ord : ∀ (c : Cardinal.{u_1}), c ≤ Cardinal.preAleph c.ord
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.equiv_def₃ : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f g : CauSeq β abv},
  f ≈ g → ∀ {ε : α}, 0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑g j) < ε
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableWithinAt.add` -/
DifferentiableWithinAt.fun_add : ∀ {𝕜 : 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] {f g : E → F}
  {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 g s x → DifferentiableWithinAt 𝕜 (fun i => f i + g i) s x
-- Mathlib.LinearAlgebra.Span.Basic
/-- A version of `Submodule.span_eq` for when the span is by a smaller ring.  -/
Submodule.span_coe_eq_restrictScalars : ∀ {R : Type u_1} {M : Type u_4} {S : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M) [inst_3 : Semiring S] [inst_4 : SMul S R] [inst_5 : Module S M] [inst_6 : IsScalarTower S R M],
  Submodule.span S ↑p = Submodule.restrictScalars S p
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractLeft_algebraMap_mul : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (r : R) (b : CliffordAlgebra Q),
  (CliffordAlgebra.contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) =
    (algebraMap R (CliffordAlgebra Q)) r * (CliffordAlgebra.contractLeft d) b
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.rhs : Lean.Meta.Grind.AC.DiseqCnstr → Lean.Grind.AC.Seq
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- Given a `n`-simplex of `X` that is constant on the boundary, this
is the corresponding `n`-simplex of `X.op`.  -/
SSet.PtSimplex.op : {X : SSet} →
  {n : ℕ} → {x : X.obj (Opposite.op { len := 0 })} → X.PtSimplex n x → X.op.PtSimplex n (SSet.opObjEquiv.symm x)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.ExtHashSet.ofList l).getD k fallback = fallback
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_nat_pos_inv_mul_lt : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ 0 → ∃ n > 0, (↑n)⁻¹ * a < b
-- Mathlib.Combinatorics.SetFamily.FourFunctions
le_collapse_of_insert_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset α → β} {s t : Finset α},
  a ∉ s → 0 ≤ f → t = insert a s → t ∈ 𝒜 → f t ≤ collapse✝ 𝒜 a f s
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Auxiliary definition for `equivalenceModuleMonoidAlgebra`.  -/
Rep.unitIso : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (V : Rep.{w, u, v} k G) → V ≅ (Rep.toModuleMonoidAlgebra.comp Rep.ofModuleMonoidAlgebra).obj V
-- Mathlib.RingTheory.Adjoin.Basic
Subalgebra.restrictScalars.congr_simp : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  (U U_1 : Subalgebra S A), U = U_1 → Subalgebra.restrictScalars R U = Subalgebra.restrictScalars R U_1
-- Mathlib.Probability.Distributions.Binomial
/-- The binomial probability distribution with parameter `p`.  -/
ProbabilityTheory.binomial : ℕ → ↑unitInterval → MeasureTheory.Measure ℕ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom.inj : ∀ {α α_1 : Mathlib.Tactic.BicategoryLike.StructuralAtom},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α = Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α_1 →
    α = α_1
-- Lean.Data.Json.Basic
Lean.Json.str : String → Lean.Json
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.square_commutes : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ Sum.inl =
    ⇑(CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom (Profinite.NobelingProof.πs C o))) ∘
      Profinite.NobelingProof.GoodProducts.eval
        (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An independent set in the complement graph is a clique and vice versa.  -/
SimpleGraph.isIndepSet_compl : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, Gᶜ.IsIndepSet s ↔ G.IsClique s
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- `3α + 2β` is long.  -/
RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_longRoot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.EmbeddedG2] (B : P.InvariantForm),
  (B.form (RootPairing.EmbeddedG2.threeShortAddTwoLongRoot P)) (RootPairing.EmbeddedG2.threeShortAddTwoLongRoot P) =
    (B.form (RootPairing.EmbeddedG2.longRoot P)) (RootPairing.EmbeddedG2.longRoot P)
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.coeHom.eq_1 : ∀ (M : Type u) [inst : AddMonoid M], AddUnits.coeHom M = { toFun := AddUnits.val, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Order.Compact
ContinuousOn.image_uIcc : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] [DenselyOrdered α] [inst_5 : ConditionallyCompleteLinearOrder β]
  [OrderTopology β] {f : α → β} {a b : α},
  ContinuousOn f (Set.uIcc a b) → f '' Set.uIcc a b = Set.uIcc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
-- Mathlib.Data.Sum.Interval
Sum.Iio_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] (b : β), Finset.Iio (Sum.inr b) = Finset.map Function.Embedding.inr (Finset.Iio b)
-- Init.Data.Option.Attach
Option.toList_attachWith : ∀ {α : Type u_1} {p : α → Prop} {o : Option α} {h : ∀ (x : α), o = some x → p x},
  (o.attachWith p h).toList = List.map (fun x => ⟨↑x, ⋯⟩) o.toList.attach
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.toEquiv_symm_apply : ∀ {X Y : Type u} (i : X ≅ Y) (a : Y), i.toEquiv.symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.instEpiσ₀Iter : ∀ (i : ℕ) {n m : ℕ} (hi : n + i = m), CategoryTheory.Epi (SimplexCategory.σ₀Iter i hi)
-- Mathlib.Logic.Relation
/-- **Alias** of `refl`. -/
Std.Refl.reflexive : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α), r a a
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If ∠BCD = π, then ∠ABC = ∠ABD.  -/
EuclideanGeometry.angle_eq_angle_of_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ : P) {p₂ p₃ p₄ : P},
  EuclideanGeometry.angle p₂ p₃ p₄ = Real.pi → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p₄
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.forget_obj : ∀ (C : CategoryTheory.Cat), CategoryTheory.Quiv.forget.obj C = CategoryTheory.Quiv.of ↑C
-- Init.Data.List.Basic
List.Lex.below.cons : ∀ {α : Type u} {r : α → α → Prop} {motive : (as bs : List α) → List.Lex r as bs → Prop} {a : α} {l₁ l₂ : List α}
  (h : List.Lex r l₁ l₂), List.Lex.below h → motive l₁ l₂ h → List.Lex.below ⋯
-- Mathlib.Data.List.TakeDrop
List.cons_get_drop_succ : ∀ {α : Type u} {l : List α} {n : Fin l.length}, l.get n :: List.drop (↑n + 1) l = List.drop (↑n) l
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofSetSetoid.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] (s s_1 : Setoid α),
  s = s_1 →
    ∀ (x : Finset α) {inst_1 : DecidableRel ⇑s} [inst_2 : DecidableRel ⇑s_1],
      Finpartition.ofSetSetoid s x = Finpartition.ofSetSetoid s_1 x
-- Init.Data.Array.Lemmas
/-- Variant of `all_reverse` with a side condition for the `stop` argument.  -/
Array.all_reverse' : ∀ {α : Type u_1} {stop : ℕ} {f : α → Bool} {xs : Array α}, stop = xs.size → xs.reverse.all f 0 stop = xs.all f
-- Mathlib.RingTheory.DedekindDomain.Different
pow_sub_one_dvd_differentIdeal : ∀ (A : Type u_1) {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B]
  [inst_7 : Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal]
  (P : Ideal B) (e : ℕ), p ≠ ⊥ → P ^ e ∣ Ideal.map (algebraMap A B) p → P ^ (e - 1) ∣ differentIdeal A B
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.comul_comp_inl : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B],
  CoalgebraStruct.comul ∘ₗ LinearMap.inl R A B =
    TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B) ∘ₗ CoalgebraStruct.comul
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_map_of_eq : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (i : U = V) (s : Set ↑(X.presheaf.obj (Opposite.op V))),
  X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.eqToHom i).op)) '' s) = X.zeroLocus s
-- Mathlib.Algebra.Order.Group.Lattice
sub_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a b c : α),
  c - a ⊔ b = (c - a) ⊓ (c - b)
-- Mathlib.NumberTheory.Niven
/-- `2 cos(q * π)` for `q : ℚ` is integral over `ℤ`, using the real `cos` function.  -/
Real.isIntegral_two_mul_cos_rat_mul_pi : ∀ (q : ℚ), IsIntegral ℤ (2 * Real.cos (↑q * Real.pi))
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_7 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.existsInv with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_7 ()
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The presieve of `S` that is generated by the morphisms `f i : X i ⟶ S`.  -/
CategoryTheory.PreZeroHypercover.presieve₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {S : C} → CategoryTheory.PreZeroHypercover S → CategoryTheory.Presieve S
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_inv_right₀`. -/
Antivary.inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, StrongLT 0 g → Antivary f g → Monovary f g⁻¹
-- Mathlib.Algebra.Ring.Invertible
invOf_add_invOf : ∀ {R : Type u_1} [inst : Semiring R] (a b : R) [inst_1 : Invertible a] [inst_2 : Invertible b],
  ⅟a + ⅟b = ⅟a * (a + b) * ⅟b
-- Mathlib.Topology.Algebra.Star
starContinuousMap_apply : ∀ {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [inst_2 : ContinuousStar R] (a : R),
  starContinuousMap a = star a
-- Mathlib.Logic.Equiv.Finset
Encodable.sortedUniv_toFinset : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Encodable α] [inst_2 : DecidableEq α],
  (Encodable.sortedUniv α).toFinset = Finset.univ
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_iff_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] {x₁ x₂ : R} {y₁ y₂ : ↥M},
  IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ (algebraMap R S) (↑y₂ * x₁) = (algebraMap R S) (↑y₁ * x₂)
-- Mathlib.Algebra.Category.Ring.Basic
/-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.  -/
CommSemiRingCat.forget_obj_eq_coe : CommSemiRingCat → CommSemiRingCat → Prop
-- Mathlib.Data.List.MinMax
List.minimum_eq_coe_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {m : α}, l.minimum = ↑m ↔ m ∈ l ∧ ∀ a ∈ l, m ≤ a
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_div_closedBall : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E),
  {x} / Metric.closedBall y δ = Metric.closedBall (x / y) δ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.eraseKey.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k k_1 : α) (v : β k_1) (l : List ((a : α) × β a)),
  Std.Internal.List.eraseKey k (⟨k_1, v⟩ :: l) = bif k_1 == k then l else ⟨k_1, v⟩ :: Std.Internal.List.eraseKey k l
-- Aesop.Tree.Data
Aesop.Rapp.instNonempty : Nonempty Aesop.Rapp
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- A set `s` is von Neumann bounded if every neighborhood of 0 absorbs `s`.  -/
Bornology.IsVonNBounded : (𝕜 : Type u_1) → {E : Type u_3} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → [Zero E] → [TopologicalSpace E] → Set E → Prop
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_def : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α},
  s.sup f = (Multiset.map f s.val).sup
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.id_eq_path_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : FundamentalGroupoid X),
  CategoryTheory.CategoryStruct.id x = ⟦Path.refl x.as⟧
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- A morphism property is `StableUnderInverse` if the inverse of a morphism satisfying
the property still falls in the class.  -/
CategoryTheory.MorphismProperty.StableUnderInverse : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_iff_lt_one_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulRightStrictMono α] [MulRightReflectLT α] {a : α} (b : α),
  a * b < b ↔ a < 1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.eq_2 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option β')} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (out' : β') (h' : (f out).Property (some out'))
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨some out', h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_2 out' h'
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The minimum degree of all vertices (and `0` if there are no vertices).
The key properties of this are given in `exists_minimal_degree_vertex`, `minDegree_le_degree`
and `le_minDegree_of_forall_le_degree`.  -/
SimpleGraph.minDegree : {V : Type u_1} → (G : SimpleGraph V) → [Fintype V] → [DecidableRel G.Adj] → ℕ
-- Mathlib.GroupTheory.NoncommCoprod
/-- Coproduct of two `AddHom`s with the same codomain with `AddCommute` assumption:
`f.noncommCoprod g _ (p : M × N) = f p.1 + g p.2`.
(For the commutative case, use `AddHom.coprod`)  -/
AddHom.noncommCoprod : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : Add M] →
        [inst_1 : Add N] →
          [inst_2 : AddSemigroup P] →
            (f : M →ₙ+ P) → (g : N →ₙ+ P) → (∀ (m : M) (n : N), AddCommute (f m) (g n)) → M × N →ₙ+ P
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
/-- Given a right inverse `f₂ : M₂ →L[R] M₁` to `f₁ : M₁ →L[R] M₂`,
`projKerOfRightInverse f₁ f₂ h` is the projection `M₁ →L[R] LinearMap.ker f₁` along
`LinearMap.range f₂`.  -/
ContinuousLinearMap.projKerOfRightInverse : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Ring R₁] →
      [inst_1 : Ring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [RingHomInvPair σ₁₂ σ₂₁] →
              {M₁ : Type u_4} →
                {M₂ : Type u_5} →
                  [inst_3 : TopologicalSpace M₁] →
                    [inst_4 : AddCommGroup M₁] →
                      [inst_5 : Module R₁ M₁] →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommGroup M₂] →
                            [inst_8 : Module R₂ M₂] →
                              [IsTopologicalAddGroup M₁] →
                                (f₁ : M₁ →SL[σ₁₂] M₂) →
                                  (f₂ : M₂ →SL[σ₂₁] M₁) → Function.RightInverse ⇑f₂ ⇑f₁ → M₁ →L[R₁] ↥(↑f₁).ker
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.toComposableArrows_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {X Y : Fin (1 + 1 + 1)} (g : X ⟶ Y),
  S.toComposableArrows.map g =
    CategoryTheory.ComposableArrows.Precomp.map (CategoryTheory.ComposableArrows.mk₁ S.g) S.f X Y ⋯
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_list_sum : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] (l : List (Matrix n n R)),
  l.sum.trace = (List.map Matrix.trace l).sum
-- Init.Data.SInt.Lemmas
Int8.pow_zero : ∀ (x : Int8), x ^ 0 = 1
-- Init.Data.SInt.Bitwise
instIdempotentOpISizeHAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2