mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.object.sizeOf_spec : sizeOf Lean.IR.IRType.object = 1
-- Mathlib.RingTheory.Etale.Field
Algebra.FormallyEtale.iff_isSeparable : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.EssFiniteType K L],
  Algebra.FormallyEtale K L ↔ Algebra.IsSeparable K L
-- Mathlib.Algebra.Algebra.Unitization
/-- The coercion from a non-unital `R`-algebra `A` to its unitization `Unitization R A`
realized as a non-unital algebra homomorphism.  -/
Unitization.inrNonUnitalAlgHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : NonUnitalSemiring A] → [inst_2 : Module R A] → A →ₙₐ[R] Unitization R A
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.mul_right : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {a b : FreeNonUnitalNonAssocAlgebra R X}
  (c : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (a * c) (b * c)
-- Mathlib.Data.Finset.Basic
Finset.erase_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → ((s.erase a).Nonempty ↔ s.Nontrivial)
-- Std.Time.Zoned.Database.Basic
/-- Converts a `TZif.TZifV1` structure to a `ZoneRules` structure.
 -/
Std.Time.TimeZone.convertTZifV1 : Std.Time.TimeZone.TZif.TZifV1 → String → Except String Std.Time.TimeZone.ZoneRules
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_stepk : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k₁ k : ℤ)
  (init p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.d_stepk_cert k₁ p₁ k₂ m₂ p₂ p = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p₁ →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 →
        ↑(k₁ * k) * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instInhabited.eq_1 : AddCommGrpCat.instInhabited = { default := AddCommGrpCat.of PUnit.{u_1 + 1} }
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).right = Y.right.right
-- Mathlib.RingTheory.Coalgebra.Basic
CommSemiring.counit_apply : ∀ (R : Type u) [inst : CommSemiring R] (r : R), CoalgebraStruct.counit r = r
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.empty.nonempty_equiv_iff : ∀ {M : Type w} {N : Type w'} [inst : FirstOrder.Language.empty.Structure M]
  [inst_1 : FirstOrder.Language.empty.Structure N],
  Nonempty (FirstOrder.Language.empty.Equiv M N) ↔
    Cardinal.lift.{w', w} (Cardinal.mk M) = Cardinal.lift.{w, w'} (Cardinal.mk N)
-- Mathlib.Data.Finset.Sups
Finset.infs_self_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s : Finset α}, s ⊼ s ⊆ s ↔ InfClosed ↑s
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
rootsOfUnityCircleEquiv_apply : ∀ (n : ℕ) [inst : NeZero n] (w : ↥(rootsOfUnity n Circle)), ↑↑((rootsOfUnityCircleEquiv n) w) = ↑↑↑w
-- Std.Time.Date.Unit.Day
Std.Time.Day.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Day.Ordinal
-- Lean.Parser.Attr
Lean.Parser.Attr.tactic_tag.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
/-- The collection of all single functors `C ⥤ HomotopyCategory C (ComplexShape.up ℤ)`
for `n : ℤ` along with their compatibilities with shifts.  -/
HomotopyCategory.singleFunctors : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasZeroObject C] →
        CategoryTheory.SingleFunctors C (HomotopyCategory C (ComplexShape.up ℤ)) ℤ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.tensorHom_inv_inv_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.GrpObj A],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.GrpObj.inv)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- A variant of `aesop_graph` which does not fail if it is unable to solve the goal.
Use this only for exploration! Nonterminal Aesop is even worse than nonterminal `simp`.
 -/
aesop_graph_nonterminal : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instAddMonoid.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  AddMonoidAlgebra.instAddMonoid =
    {
      add := fun a a_1 =>
        AddMonoidAlgebra.coeffEquiv.2 (AddMonoidAlgebra.coeffEquiv.toFun a + AddMonoidAlgebra.coeffEquiv.toFun a_1),
      add_assoc := ⋯, zero := AddMonoidAlgebra.coeffEquiv.2 0, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun a a_1 => AddMonoidAlgebra.coeffEquiv.2 (a • AddMonoidAlgebra.coeffEquiv.toFun a_1), nsmul_zero := ⋯,
      nsmul_succ := ⋯ }
-- Mathlib.Analysis.Normed.Module.RCLike.Real
range_nnnorm : ∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E], Set.range nnnorm = Set.univ
-- Plausible.DeriveArbitrary
/-- Creates the *body* of the generator that appears in the instance of the `ArbitraryFueled` typeclass  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkBody : Lean.Elab.Deriving.Header → Lean.InductiveVal → Lean.TSyntax `term → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Data.Matrix.Diagonal
Matrix.map_ofNat : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] [inst_2 : Zero β]
  {f : α → β},
  f 0 = 0 → ∀ (d : ℕ) [inst_3 : d.AtLeastTwo], (OfNat.ofNat d).map f = Matrix.diagonal fun x => f (OfNat.ofNat d)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity_nonneg : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β),
  0 ≤ Rel.edgeDensity r s t
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.restr_of_source_subset : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] {f : Equidecomp X G} {A : Set X}, f.source ⊆ A → f.restr A = f
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_symm_apply_coe : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S)
  (J : FractionalIdeal (nonZeroDivisors S) L),
  ↑((FractionalIdeal.ringEquivOfRingEquiv K L f).symm J) =
    Submodule.map ↑(IsFractionRing.semilinearEquivOfRingEquiv L K f.symm) ↑J
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Adding the angles between two vectors in each order results in 0.  -/
Orientation.oangle_add_oangle_rev : ∀ {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), o.oangle x y + o.oangle y x = 0
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_inf : ∀ {G : Type u_1} [inst : AddGroup G] (p p' : AddSubgroup G), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.Analysis.Normed.Field.Ultra
/-- This technical lemma is used in the proof of
`isUltrametricDist_of_forall_norm_natCast_le_one`.  -/
IsUltrametricDist.isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm : ∀ {R : Type u_1} [inst : NormedDivisionRing R],
  (∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)) → IsUltrametricDist R
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.tensorObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj G H).X = CategoryTheory.MonoidalCategoryStruct.tensorObj G.X H.X
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.algHom_ext_iff : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Ring A] [inst_2 : Algebra R A]
  {f g : QuadraticAlgebra R a b →ₐ[R] A}, f = g ↔ f QuadraticAlgebra.omega = g QuadraticAlgebra.omega
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.lift.eq_1 : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G],
  Algebra.GrothendieckAddGroup.lift =
    { toFun := fun f => (AddLocalization.addMonoidOf ⊤).lift ⋯,
      invFun := fun f => f.comp Algebra.GrothendieckAddGroup.of, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Combinatorics.Configuration
/-- If a nondegenerate configuration has a unique point on any two lines, then `|L| ≤ |P|`.  -/
Configuration.HasPoints.card_le : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [Configuration.HasPoints P L] [inst : Fintype P]
  [inst_1 : Fintype L], Fintype.card L ≤ Fintype.card P
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If a function is meromorphic in normal form on `U`, then it is meromorphic on
`U`.
 -/
MeromorphicNFOn.meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicNFOn f U → MeromorphicOn f U
-- Mathlib.Data.Set.Finite.Basic
Set.card_singleton : ∀ {α : Type u} (a : α), Fintype.card ↑{a} = 1
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallUnopOfOpposite_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ)
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P], CategoryTheory.ObjectProperty.Small.{w, v, u} P.unop
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_false_of_or_eq_false_right : ∀ {a b : Bool}, (a || b) = false → b = false
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewRawFact.mk.sizeOf_spec : ∀ (proof prop : Lean.Expr) (generation : ℕ) (splitSource : Lean.Meta.Grind.SplitSource)
  (ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource),
  sizeOf
      { proof := proof, prop := prop, generation := generation, splitSource := splitSource,
        ematchDiagSource := ematchDiagSource } =
    1 + sizeOf proof + sizeOf prop + sizeOf generation + sizeOf splitSource + sizeOf ematchDiagSource
-- Mathlib.Data.Fin.VecNotation
Matrix.vecCons_inj : ∀ {α : Type u} {n : ℕ} {x y : α} {u v : Fin n → α}, Matrix.vecCons x u = Matrix.vecCons y v ↔ x = y ∧ u = v
-- Init.Data.List.Basic
List.cons_append : ∀ {α : Type u} {a : α} {as bs : List α}, a :: as ++ bs = a :: (as ++ bs)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_zero : ∀ (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S], ↑R 0 = 0
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.toPiNatEquiv_apply_ofPiNat : ∀ {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) (ofPiNat : X),
  ((Metric.PiNatEmbed.toPiNatEquiv X Y f) ofPiNat).ofPiNat = ofPiNat
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_def' : ∀ {α : Type u_2} (M : Matroid α) (X : Set α),
  autoParam (X ⊆ M.E) Matroid.closure_def'._auto_1 → M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ⊆ F}
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.toIsApproximateUnit : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {l : Filter A},
  l.IsIncreasingApproximateUnit → l.IsApproximateUnit
-- Mathlib.Data.Int.Init
Int.eq_mul_div_of_mul_eq_mul_of_dvd_left : ∀ {a b c d : ℤ}, b ≠ 0 → b ∣ c → b * a = c * d → a = c / b * d
-- Mathlib.Probability.Distributions.Fernique
/-- Auxiliary lemma for `exists_integrable_exp_sq_of_map_rotation_eq_self`, in which we will replace
the assumption `IsProbabilityMeasure μ` by the weaker `IsFiniteMeasure μ`.  -/
ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∃ C, 0 < C ∧ MeasureTheory.Integrable (fun x => Real.exp (C * ‖x‖ ^ 2)) μ
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x y : MonoidAlgebra R M), (x + y).coeff = x.coeff + y.coeff
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection is involutive.  -/
Submodule.reflection_involutive : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], Function.Involutive ⇑K.reflection
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The "projection" morphism in the factorization given by
the small object argument.  -/
CategoryTheory.SmallObject.πObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              {X Y : C} → (f : X ⟶ Y) → CategoryTheory.SmallObject.obj I κ f ⟶ Y
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
/-- **Alias** of `NumberField.InfinitePlace.IsRamified.finrank_eq_two`.

---

If `w` is a ramified place over `v` then `w.Completion` has `v.Completion` dimension two.  -/
NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  NumberField.InfinitePlace.IsRamified K w → Module.finrank v.Completion w.Completion = 2
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.discreteTopology_of_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn f s → ∀ [DiscreteTopology ↑(f '' s)], DiscreteTopology ↑s
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.pIntegral_bernoulli_even_term : ∀ {k m p : ℕ},
  m < k →
    ∀ [inst : Fact (Nat.Prime p)],
      Bernoulli.pIntegral✝ p (bernoulli (2 * m) + Bernoulli.vonStaudtIndicator✝ (2 * m) p / ↑p) →
        Bernoulli.pIntegral✝ p (bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- A sigma-algebra $\mathcal{A}$ and a stochastic process $(X_s)_{s \in S}$ are independent if
for all $A \in \mathcal{A}$, for all $s_1, ..., s_p \in S$ and
for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_{s_1}, ..., X_{s_p})] =
P(A) P[f(X_{s_1}, ..., X_{s_p})].$$  -/
indep_comap_process_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P],
  m ≤ mΩ →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (A : Set Ω),
          MeasurableSet A →
            ∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ),
              ∫ (ω : Ω) in A, f fun x => X (↑x) ω ∂P = P.real A * ∫ (ω : Ω), f fun x => X (↑x) ω ∂P) →
        ProbabilityTheory.Indep m (MeasurableSpace.comap (fun ω s => X s ω) MeasurableSpace.pi) P
-- Init.Data.UInt.Lemmas
USize.pos_iff_ne_zero : ∀ {a : USize}, 0 < a ↔ a ≠ 0
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.pow_add : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] [inst_4 : BinomialRing R] {x : ↥(HahnSeries.orderTopSubOnePos Γ R)} {r s : R},
  x ^ (r + s) = x ^ r * x ^ s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_functor_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapIso i).functor.obj X).left = X.left
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.map_mk : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {L : Type u_3}
  {W : Type u_4} [inst_3 : DivisionRing L] [inst_4 : AddCommGroup W] [inst_5 : Module L W] {σ : K →+* L}
  (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (v : V) (hv : v ≠ 0),
  Projectivization.map f hf (Projectivization.mk K v hv) = Projectivization.mk L (f v) ⋯
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_comp_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M)
  (e : c.Embedding c') {Z : HomologicalComplex C c'} (h : M.extend e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.extendMap (CategoryTheory.CategoryStruct.comp φ φ') e) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.extendMap φ e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.extendMap φ' e) h)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.add_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Add β]
  [ContinuousAdd β], MeasureTheory.StronglyMeasurable f → ∀ (c : β), MeasureTheory.StronglyMeasurable fun x => f x + c
-- Mathlib.Algebra.Group.Action.Defs
/-- A scalar multiplication is cancellative if it is pointwise injective on the left and right.

A group action is cancellative in this sense if and only if it is **free**.
See `isCancelSMul_iff_eq_one_of_smul_eq` for a more familiar condition.  -/
IsCancelSMul : (G : Type u_9) → (P : Type u_10) → [SMul G P] → Prop
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_neg : ∀ (a b : ℤ), a.tdiv (-b) = -a.tdiv b
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.ext : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : CuspForm Γ k}, (∀ (x : UpperHalfPlane), f x = g x) → f = g
-- Init.Data.SInt.Lemmas
Int64.toBitVec_sub : ∀ {a b : Int64}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Lean.DocString.Types
Lean.Doc.DescItem.mk.injEq : ∀ {α : Type u} {β : Type v} (term : Array α) (desc : Array β) (term_1 : Array α) (desc_1 : Array β),
  ({ term := term, desc := desc } = { term := term_1, desc := desc_1 }) = (term = term_1 ∧ desc = desc_1)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedZoneName.default : Std.Time.ZoneName
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousVAdd.mk : ∀ {Γ : Type u_4} {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : VAdd Γ T],
  (∀ {K L : Set T}, IsCompact K → IsCompact L → {γ | ((fun x => γ +ᵥ x) '' K ∩ L).Nonempty}.Finite) →
    ProperlyDiscontinuousVAdd Γ T
-- Mathlib.Data.Set.MulAntidiagonal
Set.swap_mem_mulAntidiagonal : ∀ {α : Type u_1} [inst : CommMagma α] {s t : Set α} {a : α} {x : α × α},
  x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a
-- Mathlib.Order.Bounds.Basic
DirectedOn.minimal_iff_isLeast : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α},
  DirectedOn (fun x y => y ≤ x) s → (Minimal (fun x => x ∈ s) a ↔ IsLeast s a)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the identity.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityId : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr
-- Mathlib.Topology.Algebra.Module.TransferInstance
/-- Given a continuous multiplicative equivalence `e : α ≃ₜ* β`, if `β` is a topological group,
then so is `α`.  -/
ContinuousMulEquiv.isTopologicalGroup : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] [inst_1 : Group β] [IsTopologicalGroup β]
  [inst_3 : TopologicalSpace α] [inst_4 : Group α] (e : α ≃ₜ* β), IsTopologicalGroup α
-- Init.Data.String.Basic
String.Slice.offset_pos : ∀ {s : String.Slice} {off : String.Pos.Raw} {h : String.Pos.Raw.IsValidForSlice s off}, (s.pos off h).offset = off
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.localGeneratorsData_I : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_3 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (G : M.GeneratingSections), G.localGeneratorsData.I = C
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The inclusion map from the first component of the coproduct.  -/
CategoryTheory.Limits.coprod.inl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] → X ⟶ X ⨿ Y
-- Init.Coe
instCoeHTCT : {α : Sort u_1} → CoeHTCT α α
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_mul_cycle : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g h : M →ₗ[R] M), (LinearMap.trace R M) (f * g * h) = (LinearMap.trace R M) (h * f * g)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.even_ncard_supp_sdiff_rep : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V} (K : G.ConnectedComponent),
  SimpleGraph.ConnectedComponent.Represents s G.oddComponents → Even (K.supp \ s).ncard
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.exists_set : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  ∃ S, Nonempty (Module.Basis (↑S) R M)
-- Mathlib.Order.RelIso.Basic
RelIso.symm_comp_self : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), ⇑e.symm ∘ ⇑e = id
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.hasNoLoop_up' : ∀ {α : Type u_2} [inst : AddZeroClass α] [inst_1 : IsRightCancelAdd α] [IsLeftCancelAdd α] (a : α),
  a ≠ 0 → (ComplexShape.up' a).HasNoLoop
-- Mathlib.Order.Category.FinBddDistLat
/-- Construct a bundled `FinBddDistLat` from a `Fintype` `BoundedOrder` `DistribLattice`.  -/
FinBddDistLat.of : (α : Type u_1) → [inst : DistribLattice α] → [BoundedOrder α] → [Fintype α] → FinBddDistLat