mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom
        (CategoryTheory.Bicategory.whiskerLeft (η.app a)
          (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g).hom h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (η.app c)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom
          h)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c))
              h).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (F.map f)
              (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g))
                  h).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerRight
                  (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerRight
                    (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight
                      (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h)
                    (CategoryTheory.Bicategory.associator (η.app a)
                        (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom)))))))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.π_comp_eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.Limits.Pi.π f j'
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the maximum element of the map, or panics if the map is empty.  -/
RBTree.RBMap.max! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → [Inhabited β] → RBTree.RBMap α β cmp → α × β
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.indepFun_congr`. -/
ProbabilityTheory.Kernel.IndepFun.congr : ∀ {α : Type u_1} {Ω : Type u_2} {γ : Type u_6} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_10} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.IndepFun f g κ μ → ProbabilityTheory.Kernel.IndepFun f g η μ
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.e_lie_u : ∀ {ι : 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.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] (i j : ↥b.support),
  ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.u j⁆ =
    |b.cartanMatrix i j| • RootPairing.GeckConstruction.v b ↑i
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.card_le_card_biUnion_add_card_fiber : ∀ {ι : Type u_1} {α : Type u_2} [inst : DecidableEq α] {s : Finset ι} {f : ι → Finset α},
  (↑s).PairwiseDisjoint f → s.card ≤ (s.biUnion f).card + {i ∈ s | f i = ∅}.card
-- Mathlib.Data.List.MinMax
/-- If `a ≤ x` for some `x` in the list `l`, and `b : α`, then `a ≤ l.foldr max b`.  -/
List.le_max_of_le' : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a x : α} (b : α), x ∈ l → a ≤ x → a ≤ List.foldr max b l
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_iInf : ∀ {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α}, MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.incl_apply : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] (s : AddSubgroup V) (self : ↥s),
  (NormedAddGroupHom.incl s) self = ↑self
-- Mathlib.Analysis.Calculus.Deriv.Abs
deriv_abs_neg : ∀ {x : ℝ}, x < 0 → deriv (fun x => |x|) x = -1
-- Mathlib.Algebra.Group.Commute.Defs
Commute.eq_1 : ∀ {S : Type u_3} [inst : Mul S] (a b : S), Commute a b = SemiconjBy a b b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_add_one : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : Option β → Option β},
      m.contains k = false →
        (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome = true →
          (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size = (↑m).size + 1
-- Aesop.Tree.TreeM
Aesop.Tree.mk : Aesop.MVarClusterRef → Lean.Meta.SavedState → ℕ → ℕ → Aesop.GoalId → Aesop.RappId → Std.HashSet Lean.MVarId → Aesop.Tree
-- Lean.Meta.Sym.SymM
/-- Returns `true` if `e` is the internalized `Bool.false` expression.   -/
Lean.Meta.Sym.isBoolFalseExpr : Lean.Expr → Lean.Meta.Sym.SymM Bool
-- Mathlib.Algebra.GCDMonoid.Basic
instAssociativeGcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α], Std.Associative gcd
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.prod.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : A →ₜ+ B) (g : A →ₜ+ C),
  f.prod g = { toAddMonoidHom := f.prod g.toAddMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Range
/-- This is the restriction of `f` as a function taking values in `valueGroup₀ f`.  -/
MonoidWithZeroHom.ValueGroup₀.restrict₀ : {A : Type u_1} →
  {B : Type u_2} → [inst : MonoidWithZero A] → [inst_1 : GroupWithZero B] → (f : A →*₀ B) → A →*₀ f.ValueGroup₀
-- Mathlib.Analysis.Convex.StrictConvexSpace
StrictConvexSpace.of_pairwise_sphere_norm_ne_two : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  ((Metric.sphere 0 1).Pairwise fun x y => ‖x + y‖ ≠ 2) → StrictConvexSpace ℝ E
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Init.ShareCommon
ShareCommonM : ShareCommon.StateFactory → Type u_1 → Type u_1
-- Mathlib.Tactic.Basic
/-- This tactic clears all auxiliary declarations from the context.  -/
Mathlib.Tactic.clearAuxDecl : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (Std.Internal.List.insertEntryIfNew k v l) = true →
    (k == a) = false → Std.Internal.List.containsKey a l = true
-- Std.Data.Iterators.Producers.Monadic.Empty
Std.Iterators.Types.Empty.mk.sizeOf_spec : ∀ {m : Type w → Type w'} {β : Type w} [inst : (a : Type w) → SizeOf (m a)] [inst_1 : SizeOf β], sizeOf { } = 1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Result.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {E : Q(«$α») → Type u_1} {e : Q(«$α»)} [inst : (a : Q(«$α»)) → SizeOf (E a)]
  (expr : Q(«$α»)) (val : E expr) (proof : Q(«$e» = «$expr»)),
  sizeOf { expr := expr, val := val, proof := proof } = 1 + sizeOf expr + sizeOf val + sizeOf proof
-- Mathlib.ModelTheory.LanguageMap
/-- The map between two sum-languages induced by maps on the two factors.  -/
FirstOrder.Language.LHom.sumMap : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    (L →ᴸ L') → {L₁ : FirstOrder.Language} → {L₂ : FirstOrder.Language} → (L₁ →ᴸ L₂) → (L.sum L₁ →ᴸ L'.sum L₂)
-- Mathlib.Data.Finset.Sym
Finset.sym_mono : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⊆ t → ∀ (n : ℕ), s.sym n ⊆ t.sym n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.termZ_1 : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.coe_symm : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ), ⇑φ.toLinearEquiv.symm = ⇑φ.symm
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {mT : MeasurableSpace T} {κ : ProbabilityTheory.Kernel X Y} {X' : Type u_5}
  {mX' : MeasurableSpace X'} {η : ProbabilityTheory.Kernel X' Z} [ProbabilityTheory.IsSFiniteKernel η]
  {ξ : ProbabilityTheory.Kernel Z T} [ProbabilityTheory.IsSFiniteKernel ξ],
  (ξ.parallelComp ProbabilityTheory.Kernel.id).comp (η.parallelComp κ) = (ξ.comp η).parallelComp κ
-- Std.Do.WP.SimpLemmas
Except.tryCatch.eq_1 : ∀ {ε : Type u} {α : Type u_1} (handle : ε → Except ε α) (a : α), (Except.ok a).tryCatch handle = Except.ok a
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- **Alias** of `AddSubgroup.normalizer`.

---

The `normalizer` of `S` is the subgroup of `G` whose elements satisfy `g + S - g = S`.
When `S` is a subgroup, this is the largest subgroup of `G` inside which `S` is normal.  -/
AddSubgroup.setNormalizer : {G : Type u_1} → [inst : AddGroup G] → Set G → AddSubgroup G
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map, and
`j : M →+ M'` is an injective monoid homomorphism, such that the scalar multiplications on `M` and
`M'` are compatible, then the rank of `M / R` is smaller than or equal to the rank of `M' / R'`.
As a special case, taking `R = R'` it is `LinearMap.lift_rank_le_of_injective`.  -/
lift_rank_le_of_surjective_injective : ∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] (i : R → R')
  (j : M →+ M'),
  Function.Surjective i →
    Function.Injective ⇑j →
      (∀ (r : R) (m : M), j (r • m) = i r • j m) →
        Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The boundary of a fundamental domain, those
points of the domain that also lie in a nontrivial translate.  -/
MeasureTheory.addFundamentalFrontier : (G : Type u_1) → {α : Type u_3} → [inst : AddGroup G] → [AddAction G α] → Set α → Set α
-- Mathlib.CategoryTheory.MorphismProperty.Quotient
/-- Let `W : MorphismProperty C` and `homRel : HomRel C`. We say that `W` induces
a class of morphisms on the quotient category by `homRel` if `homRel` is stable under
pre- and postcomposition and if `W f ↔ W g` whenever `homRel f g` hold.  -/
CategoryTheory.MorphismProperty.HasQuotient : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C →
      (homRel : HomRel C) →
        [CategoryTheory.HomRel.IsStableUnderPrecomp homRel] →
          [CategoryTheory.HomRel.IsStableUnderPostcomp homRel] → Prop
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1_add : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (x y : G),
  MeasureTheory.condExpIndL1 hm μ s (x + y) = MeasureTheory.condExpIndL1 hm μ s x + MeasureTheory.condExpIndL1 hm μ s y
-- Batteries.Data.DList.Basic
/-- Concatenates a list of difference lists to form a single difference list. Similar to
`List.join`.  -/
Batteries.DList.join : {α : Type u_1} → List (Batteries.DList α) → Batteries.DList α
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- The map from Lie derivations to linear endomorphisms is injective.  -/
LieDerivation.toLinearMapLieHom_injective : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  Function.Injective ⇑(LieDerivation.toLinearMapLieHom R L)
-- Std.Http.Data.URI.Basic
/-- Returns a new URI with the fragment replaced.
 -/
Std.Http.URI.withFragment : Std.Http.URI → Option String → Std.Http.URI
-- Mathlib.Analysis.Complex.Arg
Complex.norm_sub_eq : ∀ {x y : ℂ}, x.arg = y.arg → ‖x - y‖ = ‖‖x‖ - ‖y‖‖
-- Mathlib.RingTheory.Artinian.Module
isArtinianRing_rangeS : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S) [IsArtinianRing R],
  IsArtinianRing ↥f.rangeS
-- Init.Data.List.Find
List.finIdxOf?_eq_pmap_idxOf? : ∀ {α : Type u_1} {l : List α} {a : α} [inst : BEq α] [inst_1 : LawfulBEq α],
  List.finIdxOf? a l = Option.pmap (fun i h => ⟨i, ⋯⟩) (List.idxOf? a l) ⋯
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.isometry_real_vadd : ∀ (a : ℝ), Isometry fun x => a +ᵥ x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_opcyclesMap' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.p (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) =
    CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p
-- Mathlib.Algebra.Group.Submonoid.Units
IsUnit.coe : ∀ {M : Type u_1} [inst : Monoid M] {S : Type u_2} [inst_1 : SetLike S M] [inst_2 : SubmonoidClass S M] {N : S} {a : ↥N},
  IsUnit a → IsUnit ↑a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_val_eq_bitblast : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache =
    Std.Tactic.BVDecide.BVExpr.bitblast aig { val := expr, cache := cache }
-- Init.Data.Option.Lemmas
Option.isSome_of_isSome_filter : ∀ {α : Type u_1} (p : α → Bool) (o : Option α), (Option.filter p o).isSome = true → o.isSome = true
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mem_localTriv_source : ∀ {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 : ι)
  (p : Z.TotalSpace), p ∈ (Z.localTriv i).source ↔ p.proj ∈ Z.baseSet i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_erase_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey? = t.maxKey? ↔
    ∀ {km : α}, t.maxKey? = some km → ¬compare k km = Ordering.eq
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- **Alias** of `IsLocalization.AtPrime.under_maximalIdeal_pow`. -/
IsLocalization.AtPrime.comap_maximalIdeal_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Ideal R) [inst_1 : p.IsPrime] (Rₚ : Type u_4) [inst_2 : CommSemiring Rₚ]
  [inst_3 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] [p.IsMaximal] (n : ℕ),
  Ideal.under R (IsLocalRing.maximalIdeal Rₚ ^ n) = p ^ n
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv (s.π.app j) =
    CategoryTheory.CategoryStruct.comp (t.π.app j) (w.inv.app j)
-- Mathlib.SetTheory.ZFC.Basic
/-- A simpler constructor for `ZFSet.Definable₂`.  -/
ZFSet.Definable₂.mk : {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} →
  (out : PSet.{u} → PSet.{u} → PSet.{u}) → (∀ (x y : PSet.{u}), ⟦out x y⟧ = f ⟦x⟧ ⟦y⟧) → ZFSet.Definable₂ f
-- Init.Data.Array.Extract
Array.takeWhile_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {as : Array α},
  Array.takeWhile p (Array.filterMap f as) = Array.filterMap f (Array.takeWhile (fun a => Option.all p (f a)) as)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.normalizedFactorsEquivSpanNormalizedFactors`.

---

The bijection between the (normalized) prime factors of `r` and the (normalized) prime factors
of `span {r}`  -/
normalizedFactorsEquivSpanNormalizedFactors : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [inst_2 : IsPrincipalIdealRing R] →
        [inst_3 : NormalizationMonoid R] →
          {r : R} →
            r ≠ 0 →
              ↑{d | d ∈ UniqueFactorizationMonoid.normalizedFactors r} ≃
                ↑{I | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}
-- Mathlib.CategoryTheory.Products.Basic
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F.obj a`.  -/
CategoryTheory.whiskeringLeft_comp_evaluation : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (a : A),
  ((CategoryTheory.Functor.whiskeringLeft A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) =
    (CategoryTheory.evaluation B C).obj (F.obj a)
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.errorMsg : Lean.Parser.ParserCacheEntry → Option Lean.Parser.Error
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.dropEndWhile_prop_eq_dropEndWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.dropEndWhile p = s.dropEndWhile fun x => decide (p x)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.CacheHit.mk.inj : ∀ {α : Type} {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} {idx : ℕ} {hbound : idx < decls.size}
  {hvalid : decls[idx] = decl} {idx_1 : ℕ} {hbound_1 : idx_1 < decls.size} {hvalid_1 : decls[idx_1] = decl},
  { idx := idx, hbound := hbound, hvalid := hvalid } = { idx := idx_1, hbound := hbound_1, hvalid := hvalid_1 } →
    idx = idx_1
-- Mathlib.Order.Filter.IsBounded
Antitone.isCoboundedUnder_ge_of_isCobounded : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Antitone f →
    ∀ [F.NeBot], Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) F → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) F f
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Two simplices are equal if they have the same points.  -/
Affine.Simplex.ext : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} {s1 s2 : Affine.Simplex k P n},
  (∀ (i : Fin (n + 1)), s1.points i = s2.points i) → s1 = s2
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁')
  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j),
  c₁.prev i₁' = i₁ →
    CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h)
        (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') =
      c₁.ε₁ c₂ c (i₁, i₂) •
        CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂))
          (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂))
            (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))
-- Mathlib.LinearAlgebra.LinearPMap
/-- The (semi)linear map itself.  -/
LinearPMap.toFun : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_3} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_4} →
                  [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → (self : E →ₛₗ.[σ] F) → ↥self.domain →ₛₗ[σ] F
-- Mathlib.Data.Set.Image
Set.range_inter_ssubset_iff_preimage_ssubset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s s' : Set β}, Set.range f ∩ s ⊂ Set.range f ∩ s' ↔ f ⁻¹' s ⊂ f ⁻¹' s'
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.one_right : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, FiniteMultiplicity a 1 → multiplicity a 1 = 0
-- Mathlib.Topology.Defs.Basic
/-- The preimage of an open set under a continuous function is an open set. Use `IsOpen.preimage`
instead.  -/
Continuous.isOpen_preimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.toAddSubgroup_injective : ∀ {R : Type u} [inst : NonAssocRing R], Function.Injective Subring.toAddSubgroup
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Any topology coinduced by a locally path-connected topology is locally path-connected.  -/
LocallyPathConnectedSpace.coinduced : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {Y : Type u_4} (f : X → Y),
  LocallyPathConnectedSpace Y