mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.comp h i) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv h_1)
-- Mathlib.Data.Set.Lattice
Set.biUnion_univ_pi : ∀ {α : Type u_1} {π : α → Type u_12} {ι : α → Type u_13} (s : (a : α) → Set (ι a)) (t : (a : α) → ι a → Set (π a)),
  (⋃ x ∈ Set.univ.pi s, Set.univ.pi fun a => t a (x a)) = Set.univ.pi fun a => ⋃ j ∈ s a, t a j
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A₁ B₁] [inst_2 : CategoryTheory.Limits.HasBinaryProduct A₂ B₂]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.Limits.prod.map h k) =
    CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)
-- Mathlib.FieldTheory.Fixed
FixedPoints.linearIndependent_smul_of_linearIndependent : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] {s : Finset F},
  LinearIndepOn (↥(FixedPoints.subfield G F)) id ↑s → LinearIndepOn F ⇑(MulAction.toFun G F) ↑s
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The right commuting triangle of the factorization morphism.  -/
CategoryTheory.Factorisation.Hom.h_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  (self : d.Hom e), CategoryTheory.CategoryStruct.comp self.h e.π = d.π
-- Init.Data.Nat.Sqrt.Lemmas
_private.Init.Data.Nat.Sqrt.Lemmas.0.Nat.IsSqrt : ℕ → ℕ → Prop
-- Init.Data.Int.Order
Int.lt_add_one_of_le : ∀ {a b : ℤ}, a ≤ b → a < b + 1
-- Init.Data.Float.Float32
Float32.ofModel.injEq : ∀ (toModel toModel_1 : Float32.Model), ({ toModel := toModel } = { toModel := toModel_1 }) = (toModel = toModel_1)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- A variant of `Matrix.det_units_conj'`.  -/
Matrix.det_conj' : ∀ {m : Type u} {α : Type v} [inst : CommRing α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m α},
  IsUnit M → ∀ (N : Matrix m m α), (M⁻¹ * N * M).det = N.det
-- Lean.Meta.Tactic.SolveByElim
/-- `applyTactics lemmas goal` will return an iterator that applies the
lemmas to the goal `goal` and returns ones that succeed.

Providing this to the `backtracking` tactic,
we can perform backtracking search based on applying a list of lemmas.

``applyTactics (trace := `name)`` will construct trace nodes for ``name` indicating which
calls to `apply` succeeded or failed.
 -/
Lean.Meta.SolveByElim.applyTactics : optParam Lean.Meta.ApplyConfig { } →
  optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.default →
    List Lean.Expr → Lean.MVarId → Lean.MetaM (Lean.Meta.Iterator (List Lean.MVarId))
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D =
    Algebra.Presentation.naive (fun x => if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯
-- Mathlib.Data.Finset.Sigma
Finset.sigma_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Finset ι} {t₁ t₂ : (i : ι) → Finset (α i)},
  s₁ ⊆ s₂ → (∀ (i : ι), t₁ i ⊆ t₂ i) → s₁.sigma t₁ ⊆ s₂.sigma t₂
-- Init.Data.Repr
Decidable.repr : {p : Prop} → Decidable p → ℕ → Std.Format
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.add : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.Supermartingale g ℱ μ → MeasureTheory.Supermartingale (f + g) ℱ μ
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.Raw.minEntry? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Option ((a : α) × β a)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.prod_eq_mul_prod_compl : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (a : ι) (f : ι → M),
  ∏ i, f i = f a * ∏ i ∈ {a}ᶜ, f i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_eq_zero_iff_sin_eq : ∀ {x : ℝ}, Real.cos x = 0 ↔ Real.sin x = 1 ∨ Real.sin x = -1
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.Disjoint g → Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_none : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  a ∉ t → t.getKey? a = none
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_mul_iff_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b c : α},
  a * b < a * c ↔ b < c
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.div_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f g : α →ₘ[μ] γ), (f / g).toGerm = f.toGerm / g.toGerm
-- Mathlib.LinearAlgebra.Isomorphisms
/-- The **first isomorphism theorem for surjective linear maps**.  -/
LinearMap.quotKerEquivOfSurjective : {R : Type u_1} →
  {M : Type u_2} →
    {M₂ : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₂] → (f : M →ₗ[R] M₂) → Function.Surjective ⇑f → (M ⧸ f.ker) ≃ₗ[R] M₂
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RooSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxoIterator α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The inverse jacobian of a presentation in the smaller coefficient ring,
provided `P.HasCoeffs R₀`.  -/
Algebra.SubmersivePresentation.invJacobianOfHasCoeffs : {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] → [P.HasCoeffs R₀] → MvPolynomial ι R₀
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β}, t.isEmpty = true → (t.insertIfNew k v).minKey! = k
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.eq_1 : ∀ (x n : ℕ) (R : Type u_2), TruncatedWittVector x n R = (Fin n → R)
-- Init.Data.String.Slice
String.Slice.SplitIterator : {σ : String.Slice → Type} →
  {ρ : Type} → (pat : ρ) → String.Slice → [String.Slice.Pattern.ToForwardSearcher pat σ] → Type
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.instIsScalarTower_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : Algebra R S] [inst_5 : IsLocalHom (algebraMap R S)] {R₀ : Type u_4}
  [inst_6 : CommRing R₀] [inst_7 : Algebra R₀ R] [inst_8 : Algebra R₀ S] [IsScalarTower R₀ R S]
  [inst_10 : IsLocalRing R₀] [inst_11 : IsLocalHom (algebraMap R₀ R)] [inst_12 : IsLocalHom (algebraMap R₀ S)],
  IsScalarTower (IsLocalRing.ResidueField R₀) (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The median of a simplex is the line through a vertex and its corresponding
`faceOppositeCentroid`.
 -/
Affine.Simplex.median : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : DivisionRing k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex k P n → Fin (n + 1) → AffineSubspace k P
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_le_vsub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f₁ f₂ g : Filter β}, f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g
-- Mathlib.GroupTheory.Coprod.Basic
/-- Lift an additive monoid homomorphism `FreeAddMonoid (M ⊕ N) →+ P` satisfying
additional properties to `AddMonoid.Coprod M N →+ P`.

Compared to `AddMonoid.Coprod.lift`,
this definition allows a user to provide a custom computational behavior.
Also, it only needs `AddZeroClass` assumptions
while `AddMonoid.Coprod.lift` needs an `AddMonoid` structure.  -/
AddMonoid.Coprod.clift : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_5} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] →
          [inst_2 : AddZeroClass P] →
            (f : FreeAddMonoid (M ⊕ N) →+ P) →
              f (FreeAddMonoid.of (Sum.inl 0)) = 0 →
                f (FreeAddMonoid.of (Sum.inr 0)) = 0 →
                  (∀ (x y : M),
                      f (FreeAddMonoid.of (Sum.inl (x + y))) =
                        f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) →
                    (∀ (x y : N),
                        f (FreeAddMonoid.of (Sum.inr (x + y))) =
                          f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) →
                      AddMonoid.Coprod M N →+ P
-- Init.Control.Lawful.Instances
ReaderT.run_controlAt : ∀ {m : Type u → Type u_1} {ρ α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ),
  (controlAt m f).run ctx = f fun {β} x => x.run ctx
-- Mathlib.Order.Booleanisation
/-- The natural inclusion `a ↦ a` from a generalized Boolean algebra to its generated Boolean
algebra.  -/
Booleanisation.lift : {α : Type u_1} → α → Booleanisation α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) The glue data for `𝒪ₓ/I`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueData : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → AlgebraicGeometry.Scheme.GlueData
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- The underlying linear equiv of modules.  -/
AffineEquiv.linear : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → (P₁ ≃ᵃ[k] P₂) → V₁ ≃ₗ[k] V₂
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_sInf : ∀ {a : ENNReal} {s : Set ENNReal}, a + sInf s = ⨅ b ∈ s, a + b
-- Mathlib.Data.EReal.Basic
instAddCommMonoidWithOneEReal : AddCommMonoidWithOne EReal
-- Mathlib.Order.SuccPred.Basic
Order.succ_mono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α], Monotone Order.succ
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofFin : ∀ (n : Fin UInt64.size), (UInt64.ofFin n).toUInt8 = UInt8.ofNat ↑n
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.bitwise.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) →
      ((m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) →
        ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) →
          ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
-- Mathlib.Tactic.WithoutCDot
Lean.Elab.Term.withoutCDotImpl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.monodromy_ext_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x y : X}
  {γ γ' : Path.Homotopic.Quotient x y} (e : ↑(p ⁻¹' {x})),
  ⋯.monodromy γ e = ⋯.monodromy γ' e ↔ ⋯.monodromy γ = ⋯.monodromy γ'
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.mk.injEq : ∀ (goals : Array Aesop.Subgoal) (postState : Lean.Meta.SavedState) (scriptSteps? : Option (Array Aesop.Script.LazyStep))
  (successProbability? : Option Aesop.Percent) (goals_1 : Array Aesop.Subgoal) (postState_1 : Lean.Meta.SavedState)
  (scriptSteps?_1 : Option (Array Aesop.Script.LazyStep)) (successProbability?_1 : Option Aesop.Percent),
  ({ goals := goals, postState := postState, scriptSteps? := scriptSteps?,
        successProbability? := successProbability? } =
      { goals := goals_1, postState := postState_1, scriptSteps? := scriptSteps?_1,
        successProbability? := successProbability?_1 }) =
    (goals = goals_1 ∧
      postState = postState_1 ∧ scriptSteps? = scriptSteps?_1 ∧ successProbability? = successProbability?_1)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Embedding of a non-unital subalgebra into the non-unital algebra.  -/
NonUnitalSubalgebraClass.subtype : {S : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [inst_3 : SetLike S A] →
              [inst_4 : NonUnitalSubsemiringClass S A] → [hSR : SMulMemClass S R A] → (s : S) → ↥s →ₙₐ[R] A
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.rel_rfl : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (h : Equivalence (Lean.Grind.IntModule.OfNatModule.r α))
  (q : Lean.Grind.IntModule.OfNatModule.Q α), Lean.Grind.IntModule.OfNatModule.rel✝ h q q
-- Mathlib.Order.SemiconjSup
/-- If an order automorphism `fa` is semiconjugate to an order embedding `fb` by a function `g`
and `g'` is an order right adjoint of `g` (i.e. `g' y = sSup {x | f x ≤ y}`), then `fb` is
semiconjugate to `fa` by `g'`.

This is a version of Proposition 2.1 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et
cohomologie bornée][ghys87:groupes].  -/
Function.Semiconj.symm_adjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {fa : α ≃o α} {fb : β ↪o β} {g : α → β},
  Function.Semiconj g ⇑fa ⇑fb → ∀ {g' : β → α}, IsOrderRightAdjoint g g' → Function.Semiconj g' ⇑fb ⇑fa
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.braiding_neg_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C), (β_ G H).inv.hom.hom = (β_ G.X H.X).inv
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofInjective_symm_apply : ∀ {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₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] {h : Function.Injective ⇑f} (x : ↥f.range),
  f ((LinearEquiv.ofInjective f h).symm x) = ↑x
-- Mathlib.Data.NNReal.Basic
NNReal.iSup_mul : ∀ {ι : Sort u_3} (f : ι → NNReal) (a : NNReal), (⨆ i, f i) * a = ⨆ i, f i * a
-- Mathlib.Algebra.Group.Units.Defs
Units.inv_mul : ∀ {α : Type u} [inst : Monoid α] (a : αˣ), ↑a⁻¹ * ↑a = 1
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_comapₐ : ∀ {R : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  {I : Ideal C} (f : A →ₐ[R] B) (g : B →ₐ[R] C), Ideal.comap f (Ideal.comap g I) = Ideal.comap (g.comp f) I
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpaceable.parallelogram_identity : ∀ {E : Type u_2} {inst : NormedAddCommGroup E} [self : InnerProductSpaceable E] (x y : E),
  ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
-- Mathlib.Data.Num.Prime
/-- Auxiliary function for computing the smallest prime factor of a `PosNum`. Unlike
`Nat.minFacAux`, we use a natural number `fuel` variable that is set to an upper bound on the
number of iterations. It is initialized to the number `n` we are determining primality for. Even
though this is exponential in the input (since it is a `Nat`, not a `Num`), it will get lazily
evaluated during kernel reduction, so we will only require about `sqrt n` unfoldings, for the
`sqrt n` iterations of the loop.  -/
PosNum.minFacAux : PosNum → ℕ → PosNum → PosNum
-- Lean.Data.Lsp.CodeActions
/-- The code action kind is supported with the following value set.  -/
Lean.Lsp.CodeActionLiteralSupport.codeActionKind : Lean.Lsp.CodeActionLiteralSupport → Lean.Lsp.CodeActionLiteralSupportValueSet
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.f_ne_zero : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → f ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x x_1 : Cᵒᵖ) (x_2 : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x x_1 x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.unop x) (Opposite.unop x_1)
          (Opposite.unop x_2)).symm.op
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_castSucc_comp_δ_succ_of_lt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  j.castSucc < i →
    CategoryTheory.CategoryStruct.comp (self.h j.castSucc) (Y.δ i.succ) =
      CategoryTheory.CategoryStruct.comp (X.δ i) (self.h j)
-- Init.Data.Option.Lemmas
Option.guard_lt_some : ∀ {α : Type u_1} [inst : LT α], (∀ (x : α), ¬x < x) → ∀ {x : α} {p : α → Bool}, Option.guard p x < some x ↔ p x = false
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.emptyOn_closure_eq : ∀ {α : Type u_2} (X : Set α), (Matroid.emptyOn α).closure X = ∅
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.mul_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Mathlib.Topology.QuasiSeparated
NoetherianSpace.to_quasiSeparatedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α], QuasiSeparatedSpace α
-- Init.Data.List.MinMaxIdx
List.minIdxOn_eq_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : ℕ},
  List.minIdxOn f xs h = i ↔
    ∃ (h : i < xs.length), (∀ (j : ℕ) (x : j < xs.length), f xs[i] ≤ f xs[j]) ∧ ∀ (j : ℕ) (x : j < i), f xs[i] < f xs[j]
-- Init.Data.Array.Find
Array.findIdx_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, Array.findIdx p #[a] = if p a = true then 0 else 1
-- Init.WF
/-- If `Acc r x` holds and `y` is transitively related to `x`, then `Acc r y` holds, too.
 -/
Acc.inv_of_transGen : ∀ {α : Sort u_1} {r : α → α → Prop} {x y : α}, Acc r x → Relation.TransGen r y x → Acc r y
-- Mathlib.Probability.Process.Stopping
MeasureTheory.isStoppingTime_piecewise_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {𝒢 : MeasureTheory.Filtration ι m} {i j : ι}
  {s : Set Ω} [inst_1 : DecidablePred fun x => x ∈ s],
  i ≤ j → MeasurableSet s → MeasureTheory.IsStoppingTime 𝒢 (s.piecewise (fun x => ↑i) fun x => ↑j)
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_eq_one : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : CommMonoid M] (f : α → M),
  (∀ (a : α), f a = 1) → ∏ a, f a = 1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instIsTorsionFree : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) [Module.IsTorsionFree R A], Module.IsTorsionFree R ↥S
-- Mathlib.NumberTheory.LSeries.ZMod
_private.Mathlib.NumberTheory.LSeries.ZMod.0.ZMod.term𝕖 : Lean.ParserDescr
-- Mathlib.Order.Filter.Defs
/-- Infimum of a set of filters.
This definition is marked as irreducible
so that Lean doesn't try to unfold it when unifying expressions.  -/
Filter.sInf : {α : Type u_1} → Set (Filter α) → Filter α
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_zero : ∀ {R : Type u_1} {a b : R} [inst : Zero R], QuadraticAlgebra.im 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.isLittleO_pow_log_id_atTop : ∀ {n : ℕ}, (fun x => Real.log x ^ n) =o[Filter.atTop] id
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseUserInfo : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI.UserInfo
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` to the domain of a `LatticeHom`.  -/
LatticeHom.withBot' : {α : Type u_1} →
  {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → [OrderBot β] → LatticeHom α β → LatticeHom (WithBot α) β
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqResolvableCompletionItem.beq : Lean.Lsp.ResolvableCompletionItem → Lean.Lsp.ResolvableCompletionItem → Bool
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀],
  0 ≤ a → ∀ (n : ℕ), 0 ≤ a ^ n