mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.SetLike.Basic
/-- A class to indicate that there is a canonical injection between `A` and `Set B`.

This has the effect of giving terms of `A` elements of type `B` (through a `Membership`
instance) and a compatible coercion to `Type*` as a subtype.

Note: if `SetLike.coe` is a projection, implementers should create a simp lemma such as
```
@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl
```
to normalize terms.

If you declare an unbundled subclass of `SetLike`, for example:
```
class MulMemClass (S : Type*) (M : Type*) [Mul M] [SetLike S M] where
  ...
```
Then you should *not* repeat the `outParam` declaration so `SetLike` will supply the value instead.
This ensures your subclass will not have issues with synthesis of the `[Mul M]` parameter starting
before the value of `M` is known.
 -/
SetLike : Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)
-- Aesop.Tree.Data
Aesop.MVarClusterUnsafe : Type
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.smallHomMap_mk : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {X Y : C₁}
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)] (f : X ⟶ Y),
  Φ.smallHomMap (CategoryTheory.Localization.SmallHom.mk W₁ f) =
    CategoryTheory.Localization.SmallHom.mk W₂ (Φ.functor.map f)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.invOn_arg_exp : Set.InvOn (Complex.arg ∘ Subtype.val) (⇑Circle.exp) (Set.Ioc (-Real.pi) Real.pi) Set.univ
-- Mathlib.Topology.Order
generateFrom_sUnion : ∀ {α : Type u} {S : Set (Set (Set α))}, TopologicalSpace.generateFrom (⋃₀ S) = ⨅ s ∈ S, TopologicalSpace.generateFrom s
-- Mathlib.Algebra.Group.End
Equiv.Perm.sumCongrHom_injective : ∀ {α : Type u_7} {β : Type u_8}, Function.Injective ⇑(Equiv.Perm.sumCongrHom α β)
-- Mathlib.Topology.Sion
/-- A minimax theorem without completeness, using `IsGLB` and `IsLUB`.  -/
Sion.minimax : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
          ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F],
            Convex ℝ Y →
              (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                  ∀ [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F],
                    Convex ℝ X →
                      ∀ (sup_y : E → β),
                        (∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)) →
                          ∀ (inf_sup : β),
                            IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup →
                              ∀ (inf_x : F → β),
                                (∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)) →
                                  ∀ (sup_inf : β), IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf → inf_sup = sup_inf
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.computeSemanticTokens : Lean.Server.FileWorker.EditableDocument →
  String.Pos.Raw →
    Option String.Pos.Raw → List Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM Lean.Lsp.SemanticTokens
-- Batteries.Data.List.Pairwise
List.pwFilter_eq_self : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {l : List α}, List.pwFilter R l = l ↔ List.Pairwise R l
-- Mathlib.Algebra.Order.Ring.Idempotent
instSemilatticeSupSubtypeProdAndEqHMulFstSndOfNatHAdd : {R : Type u_1} → [inst : CommSemiring R] → SemilatticeSup { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
-- Batteries.Recycling.RBTree.Lemmas
/-- A statement of the greatest-ness of the result of `lowerBound?`. If `x` is the return value of
`lowerBound?` and it is strictly less than the cut, then any other `y > x` in the tree is in fact
strictly greater than the cut (so there is no exact match, and nothing closer to the cut).
 -/
RBTree.RBNode.Ordered.lowerBound?_greatest : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} {x y : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.lowerBound? cut t = some x → y ∈ t → cmp x y = Ordering.lt → cut x = Ordering.gt → cut y = Ordering.lt
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_one_le_lift : ∀ {o : Ordinal.{u}}, Ordinal.omega 1 ≤ Ordinal.lift.{v, u} o ↔ Ordinal.omega 1 ≤ o
-- Mathlib.Data.Sigma.Interval
Sigma.card_Ico : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i),
  (Finset.Ico a b).card = if h : a.fst = b.fst then (Finset.Ico (h ▸ a.snd) b.snd).card else 0
-- Mathlib.Analysis.Calculus.Deriv.Slope
HasDerivAt.continuousAt_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : DecidableEq 𝕜] {f : 𝕜 → 𝕜} {c a : 𝕜},
  HasDerivAt f a c → ContinuousAt (Function.update (fun x => (f x - f c) / (x - c)) c a) c
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Two morphisms into a limit are equal if their compositions with
each cone morphism are equal.  -/
CategoryTheory.Limits.IsLimit.hom_ext : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C}
  {f f' : W ⟶ t.pt},
  (∀ (j : J), CategoryTheory.CategoryStruct.comp f (t.π.app j) = CategoryTheory.CategoryStruct.comp f' (t.π.app j)) →
    f = f'
-- Lean.Parser.Term
/-- `private_decl% e` elaborates `e` in a private context and wraps the result in a helper `def`.  -/
Lean.Parser.Term.privateDecl : Lean.Parser.Parser
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  (m.erase k).getD k fallback = fallback
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  b < a → Order.pred b < Order.pred a
-- Mathlib.Algebra.Group.Commute.Basic
Commute.inv_left_iff : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a⁻¹ b ↔ Commute a b
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.sup_nhds' : ∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Max L]
  [ContinuousSup L], Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (f ⊔ g) l (nhds (x ⊔ y))
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Ioi : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] {a : α}, frontier (Set.Ioi a) = {a}
-- Lean.Meta.Tactic.ElimInfo
/-- If `provesMotive := true`, then this alternative has `motive` as its conclusion.
Only for those alternatives the `induction` tactic should introduce reverted hypotheses.   -/
Lean.Meta.ElimAltInfo.provesMotive : Lean.Meta.ElimAltInfo → Bool
-- Mathlib.Order.SymmDiff
bihimp_assoc : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b c : α), bihimp (bihimp a b) c = bihimp a (bihimp b c)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The pullback cone built from the pullback projections is a pullback.  -/
CategoryTheory.Limits.pullbackIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPullback f g] →
            CategoryTheory.Limits.IsLimit
              (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.fst f g)
                (CategoryTheory.Limits.pullback.snd f g) ⋯)
-- Mathlib.Data.Multiset.Lattice
Multiset.nodup_sup_iff : ∀ {α : Type u_2} [inst : DecidableEq α] {m : Multiset (Multiset α)}, m.sup.Nodup ↔ ∀ a ∈ m, a.Nodup
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int8
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
ContinuousOn.integrableOn_compact : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {f : X → E}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [T2Space X],
  IsCompact K → ContinuousOn f K → MeasureTheory.IntegrableOn f K μ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.Model.0.Lean.Meta.Grind.Arith.Cutsat.isIntNatENode : Lean.Meta.Grind.ENode → Lean.MetaM Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shiftAddHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a : ℤ) (γ : CochainComplex.HomComplex.Cochain K L n),
  (CochainComplex.HomComplex.Cochain.shiftAddHom K L n a) γ = γ.shift a
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.prod_ne_zero : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀},
  0 ∉ s → s.prod ≠ 0
-- Mathlib.Analysis.Calculus.BumpFunction.Convolution
/-- If `φ` is a normed bump function, compute `φ ⋆ g`
if `g` is constant on `Metric.ball x₀ φ.rOut`.  -/
ContDiffBump.normed_convolution_eq_right : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace ℝ G]
  [CompleteSpace E'] {φ : ContDiffBump 0} [BorelSpace G] [inst_7 : FiniteDimensional ℝ G]
  [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {x₀ : G},
  (∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀) →
    MeasureTheory.convolution (φ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀ = g x₀
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.add_def : ∀ (x x_1 : ℝ),
  Real.add✝ x x_1 =
    match x, x_1 with
    | { cauchy := a }, { cauchy := b } => { cauchy := a + b }
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The non-zero elements of `M` are invariant under the action by the units of `R`.  -/
Units.nonZeroSubMul : (R : Type u_1) →
  (M : Type u_2) → [inst : Monoid R] → [inst_1 : AddCommMonoid M] → [inst_2 : DistribMulAction R M] → SubMulAction Rˣ M
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.direction_perpBisector : ∀ {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), (AffineSubspace.perpBisector p₁ p₂).direction = (ℝ ∙ (p₂ -ᵥ p₁))ᗮ
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsEquivalentIsBigO : {α : Type u_1} →
  {β : Type u_2} →
    {β₂ : Type u_3} →
      [inst : NormedAddCommGroup β] →
        [inst_1 : Norm β₂] →
          {l : Filter α} → Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsBigO l) (Asymptotics.IsBigO l)
-- Init.Data.Rat.Lemmas
Rat.le_iff : ∀ (a b : ℚ), a ≤ b ↔ a.num * ↑b.den ≤ b.num * ↑a.den
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.congr_arg : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (φ : A →ₐc[R] B) {x y : A}, x = y → φ x = φ y
-- Mathlib.Data.Finset.Sups
Finset.disjSups_disjSups_disjSups_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] (s t u v : Finset α),
  (s.disjSups t).disjSups (u.disjSups v) = (s.disjSups u).disjSups (t.disjSups v)
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.not_strictMono_of_isNoetherianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.IsNoetherianObject X]
  (f : ℕ → CategoryTheory.Subobject X), ¬StrictMono f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Order.InitialSeg
/-- Composition of a principal segment embedding with a relation isomorphism, as a principal segment
embedding  -/
PrincipalSeg.transRelIso : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → PrincipalSeg r s → s ≃r t → PrincipalSeg r t
-- Mathlib.Topology.Neighborhoods
mem_closure_of_tendsto : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} [b.NeBot],
  Filter.Tendsto f b (nhds x) → (∀ᶠ (x : α) in b, f x ∈ s) → x ∈ closure s
-- Mathlib.RingTheory.Polynomial.Quotient
Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R),
  I.polynomialQuotientEquivQuotientPolynomial.symm ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f) =
    Polynomial.map (Ideal.Quotient.mk I) f
-- Mathlib.GroupTheory.HNNExtension
/-- To avoid duplicating code, we define `toSubgroup A B u` and `toSubgroupEquiv u`
where `u : ℤˣ` is `1` or `-1`. `toSubgroup A B u` is `A` when `u = 1` and `B` when `u = -1`,
and `toSubgroupEquiv` is the group isomorphism from `toSubgroup A B u` to `toSubgroup A B (-u)`.
It is defined to be `φ` when `u = 1` and `φ⁻¹` when `u = -1`.  -/
HNNExtension.toSubgroupEquiv : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → ↥A ≃* ↥B → (u : ℤˣ) → ↥(HNNExtension.toSubgroup A B u) ≃* ↥(HNNExtension.toSubgroup A B (-u))
-- Lean.Data.PersistentArray
_private.Lean.Data.PersistentArray.0.Lean.PersistentArray.emptyArray : {α : Type u} → Array (Lean.PersistentArrayNode α)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.Nonempty.ciSup_mem_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] (f : ι → α) {s : Finset ι},
  s.Nonempty → ⨆ i ∈ s, f i ∈ Finset.image f s
-- Init.Data.String.Basic
String.slice_toSlice : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁.toSlice ≤ p₂.toSlice}, s.toSlice.slice p₁.toSlice p₂.toSlice h = s.slice p₁ p₂ h
-- Mathlib.Order.Filter.Subsingleton
Filter.subsingleton_iff_exists_singleton_mem : ∀ {α : Type u_1} {l : Filter α} [Nonempty α], l.Subsingleton ↔ ∃ a, {a} ∈ l
-- Lean.Meta.Tactic.Grind.Ctor
/-- Homogeneous case where constructor applications `a` and `b` have the same type `α`.  -/
_private.Lean.Meta.Tactic.Grind.Ctor.0.Lean.Meta.Grind.propagateCtorHomo : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.Distribution.Support
Distribution.mem_dsupport_iff : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} (x : α),
  x ∈ Distribution.dsupport f ↔ ∀ (s : Set α), Distribution.IsVanishingOn f sᶜ → IsClosed s → x ∈ s
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_mul_add_left : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [inst_4 : AddLeftCancelMonoid ι] [inst_5 : GradedRing 𝒜]
  (a : ↥(𝒜 i)) {b : A},
  ((DirectSum.decompose 𝒜) (↑a * b)) (i + j) = GradedMonoid.GMul.mul a (((DirectSum.decompose 𝒜) b) j)
-- Mathlib.Algebra.Group.Units.Hom
Units.coe_map_inv : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (u : Mˣ), ↑((Units.map f) u)⁻¹ = f ↑u⁻¹
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_surjective : Function.Surjective ⇑Cardinal.toNat
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.proj.injEq : ∀ (i : ℕ) (x : Lean.IR.VarId) (i_1 : ℕ) (x_1 : Lean.IR.VarId),
  (Lean.IR.Expr.proj i x = Lean.IR.Expr.proj i_1 x_1) = (i = i_1 ∧ x = x_1)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_H0Iso_hom_f_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(groupCohomology A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.shortComplexH0 B).f)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso B).hom)
        ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map f φ 0)) x)) =
    (Rep.Hom.hom φ).toLinearMap
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.shortComplexH0 A).f)
        ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso A).hom) x))
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.id_whiskerRight : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  (X Y : CategoryTheory.FreeMonoidalCategory C), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.rhs : {k : Lean.SyntaxNodeKinds} → Lean.Elab.Term.MatchAltView k → Lean.TSyntax k
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The quadratic character is `1` or `-1` on nonzero arguments.  -/
quadraticChar_eq_neg_one_iff_not_one : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
  a ≠ 0 → ((quadraticChar F) a = -1 ↔ ¬(quadraticChar F) a = 1)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_mul : ∀ (f g : CircleDeg1Lift), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- The `MulEquiv` between the double dual `(G →* Mˣ) →* Mˣ` of a finite commutative group `G`
and itself  where `M` is a commutative monoid with enough `n`th roots of unity, where `n` is
the exponent of `G`.
The image `g` of `η : (G →* Mˣ) →* Mˣ` is such that, for all `φ : G →* Mˣ`, we have `φ g = η g`,
see `CommGroup.apply_monoidHomMonoidHomEquiv`.
 -/
CommGroup.monoidHomMonoidHomEquiv : (G : Type u_1) →
  (M : Type u_2) →
    [inst : CommGroup G] →
      [Finite G] → [inst_2 : CommMonoid M] → [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] → ((G →* Mˣ) →* Mˣ) ≃* G
-- Mathlib.Algebra.Opposites
MulOpposite.op_add : ∀ {α : Type u_1} [inst : Add α] (x y : α), MulOpposite.op (x + y) = MulOpposite.op x + MulOpposite.op y
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {x y : FormalGroup R}, x = y ↔ x.toPowerSeries = y.toPowerSeries
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.instNontrivialOfNonempty : ∀ {α : Type u_1} [Nonempty α], Nontrivial (FreeGroup α)
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.inter : ∀ {α : Type u_1} {S : Set (Set α)} {s t : Set α},
  FiniteInter.finiteInterClosure S s → FiniteInter.finiteInterClosure S t → FiniteInter.finiteInterClosure S (s ∩ t)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_sub_left_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (y * z - x) y ↔ IsCoprime x y
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_apply_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : N),
  Monoid.Coprod.fst (Monoid.Coprod.inr x) = 1
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instPosSMulMono : ∀ {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [inst : Semiring α] [inst_1 : Preorder α]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] [inst_3 : (i : ι) → Preorder (β i)] [inst_4 : (i : ι) → Module α (β i)]
  [∀ (i : ι), PosSMulMono α (β i)], PosSMulMono α (Π₀ (i : ι), β i)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIco_eq_lift_Icc : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  {p a : 𝕜} [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)),
  AddCircle.liftIco p a f = Quot.lift ((Set.Icc a (a + p)).domRestrict f) ⋯ ∘ ⇑(AddCircle.equivIccQuot p a)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.val.inj : ∀ {a a_1 : Lean.Expr}, Lean.Meta.Match.Example.val a = Lean.Meta.Match.Example.val a_1 → a = a_1
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.neg_left : ∀ {R₁ : Type u_4} {M₁ : Type u_5} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁} (x y : M₁), (B₁ (-x)) y = -(B₁ x) y
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- A type synonym for `V`, when thought of as a quiver having only the arrows from
some `WideSubquiver`.  -/
WideSubquiver.toType : (V : Type u) → [inst : Quiver V] → WideSubquiver V → Type u
-- Mathlib.CategoryTheory.Galois.Basic
/-- `F` preserves pullbacks (G4).  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.PreGaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minEntry_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.minEntry he = t₂.minEntry ⋯
-- Mathlib.Control.Functor
Functor.Comp.lawfulFunctor : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Functor F] [inst_1 : Functor G] [LawfulFunctor F]
  [LawfulFunctor G], LawfulFunctor (Functor.Comp F G)
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.prod_compacts : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {f : α → TopologicalSpace.Compacts β} {g : α → TopologicalSpace.Compacts γ},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x ×ˢ g x
-- Mathlib.NumberTheory.SumTwoSquares
/-- If `-1` is a square modulo `n` and `m` divides `n`, then `-1` is also a square modulo `m`.  -/
ZMod.isSquare_neg_one_of_dvd : ∀ {m n : ℕ}, m ∣ n → IsSquare (-1) → IsSquare (-1)
-- Std.Time.Zoned.Database.TzIf
/-- The header information of the TZif file.
 -/
Std.Time.TimeZone.TZif.TZifV1.header : Std.Time.TimeZone.TZif.TZifV1 → Std.Time.TimeZone.TZif.Header
-- Init.Data.UInt.Lemmas
UInt64.div_one : ∀ {a : UInt64}, a / 1 = a
-- Mathlib.Order.Partition.Basic
/-- The part of a partition containing a given element. If the element is not in the
underlying set, this is empty.  -/
Partition.partOf : {α : Type u_1} → {u : Set α} → Partition u → α → Set α
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W W_1 : CategoryTheory.MorphismProperty C),
  W = W_1 →
    ∀ (J : Type w) [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J]
      {X Y : C} (f f_1 : X ⟶ Y), f = f_1 → W.TransfiniteCompositionOfShape J f = W_1.TransfiniteCompositionOfShape J f_1
-- Init.Data.UInt.Lemmas
UInt8.ofNat_size : UInt8.ofNat UInt8.size = 0
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limIsoFlipCompWhiskerLim_hom_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X_1 : K),
  (CategoryTheory.Limits.limIsoFlipCompWhiskerLim.hom.app X).app X_1 =
    (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X X_1).hom