mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The limit of the constant `⊤_ C` functor is `⊤_ C`.  -/
CategoryTheory.Limits.limitConstTerminal : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasTerminal C] →
          CategoryTheory.Limits.limit ((CategoryTheory.Functor.const J).obj (⊤_ C)) ≅ ⊤_ C
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- When `α` is a \*-(semi)ring, `Matrix.star` is also a \*-(semi)ring.  -/
Matrix.instStarRing : {n : Type u_3} →
  {α : Type v} → [inst : Fintype n] → [inst_1 : NonUnitalNonAssocSemiring α] → [StarRing α] → StarRing (Matrix n n α)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerSkip_flatMap_pure : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ it₁' : Std.Iter β},
  it₁.IsPlausibleStep (Std.IterStep.skip it₁') →
    (Std.Iter.flatMapAfter f it₁ none).IsPlausibleStep (Std.IterStep.skip (Std.Iter.flatMapAfter f it₁' none))
-- Init.MetaTypes
Lean.Meta.Simp.instInhabitedConfig.default : Lean.Meta.Simp.Config
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.constructors.inj : ∀ {constructorNames : Array Lean.Name} {md : Lean.Meta.TransparencyMode} {constructorNames_1 : Array Lean.Name}
  {md_1 : Lean.Meta.TransparencyMode},
  Aesop.RuleTacDescr.constructors constructorNames md = Aesop.RuleTacDescr.constructors constructorNames_1 md_1 →
    constructorNames = constructorNames_1 ∧ md = md_1
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Constructor for natural transformations between functors to the
category of triangles.  -/
CategoryTheory.Pretriangulated.Triangle.functorHomMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
          (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C)) →
            (hom₁ :
                A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₁) →
              (hom₂ :
                  A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ⟶
                    B.comp CategoryTheory.Pretriangulated.Triangle.π₂) →
                (hom₃ :
                    A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ⟶
                      B.comp CategoryTheory.Pretriangulated.Triangle.π₃) →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂)
                          hom₂ =
                        CategoryTheory.CategoryStruct.comp hom₁
                          (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
                      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_1 →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp
                            (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) hom₃ =
                          CategoryTheory.CategoryStruct.comp hom₂
                            (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
                        CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_3 →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp
                              (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
                              (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
                            CategoryTheory.CategoryStruct.comp hom₃
                              (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁))
                          CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_5 →
                        (A ⟶ B)
-- Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
/-- Shortcut instance for the fact that any nontrivial commutative ring satisfies
the strong rank condition.  -/
commRing_strongRankCondition : ∀ (R : Type u_1) [inst : CommRing R] [Nontrivial R], StrongRankCondition R
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.isRepresentable_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  {G : CategoryTheory.Functor Cᵒᵖ (Type v)} (i : F ≅ G) [F.IsRepresentable], G.IsRepresentable
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
cfc_mem : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [StarModule 𝕜 A] [inst_6 : ContinuousFunctionalCalculus 𝕜 A p]
  [IsTopologicalRing A] [ContinuousStar A] {𝕜' : Type u_3} {S : Type u_4} [inst_9 : Monoid 𝕜']
  [inst_10 : MulAction 𝕜' A] [inst_11 : SetLike S A] [SubringClass S A] [inst_13 : SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' A]
  [SMulMemClass S 𝕜' A] [StarMemClass S A] {s : S} [hs : IsClosed ↑s] (f : 𝕜 → 𝕜) {a : A}, a ∈ s → cfc f a ∈ s
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_one_div_one_add_sq : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  IntervalIntegrable (fun x => 1 / (1 + x ^ 2)) μ a b
-- Mathlib.Order.Filter.Basic
Filter.frequently_iSup : ∀ {α : Type u} {β : Type v} {p : α → Prop} {fs : β → Filter α},
  (∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.tendsto_card_div_pow₃ : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) [inst : Fintype ι],
  Bornology.IsBounded s →
    (∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) →
      ∀ᶠ (x : ℝ) in Filter.atTop,
        ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι ≤
          ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι
-- Mathlib.Data.Set.Finite.Lattice
Set.fintypeBiUnion' : {α : Type u} →
  [DecidableEq α] →
    {ι : Type u_1} → (s : Set ι) → [Fintype ↑s] → (t : ι → Set α) → [(i : ι) → Fintype ↑(t i)] → Fintype ↑(⋃ x ∈ s, t x)
-- Init.Data.Vector.Lemmas
Vector.foldl_flatMap : ∀ {α : Type u_1} {β : Type u_2} {m : ℕ} {γ : Type u_3} {n : ℕ} {f : α → Vector β m} {g : γ → β → γ} {xs : Vector α n}
  {init : γ}, Vector.foldl g init (xs.flatMap f) = Vector.foldl (fun acc x => Vector.foldl g acc (f x)) init xs
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_inv_leftUnitor : ∀ {R : Type u} [inst : CommRing R] {M : AlgCat R},
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv = ↑(Algebra.TensorProduct.lid R ↑M).symm
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (self : W₁.MapFactorizationData W₂ f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.p h) =
    CategoryTheory.CategoryStruct.comp f h
-- Init.Data.Vector.Lemmas
Vector.flatMap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {k n : ℕ} {f : α → β} {g : β → Vector γ k} {xs : Vector α n},
  (Vector.map f xs).flatMap g = xs.flatMap fun a => g (f a)
-- Init.Data.Array.MapIdx
Array.mapIdx_push : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Array α} {a : α},
  Array.mapIdx f (xs.push a) = (Array.mapIdx f xs).push (f xs.size a)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The canonical map `Y ⊞ Z ⟶ pushout f g` induces a cokernel cofork on the map
`X ⟶ Y ⊞ Z` induced by `f` and `-g`.  -/
CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushoutCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.Limits.HasPushouts C] →
        {X Y Z : C} →
          (f : X ⟶ Y) → (g : X ⟶ Z) → CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.biprod.lift f (-g))
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.clear.sizeOf_spec : ∀ (ref : Lean.Syntax), sizeOf (Lean.Elab.Tactic.RCases.RCasesPatt.clear ref) = 1 + sizeOf ref
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.iUnion : ∀ {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [inst : LE α] {f : ι → Set α},
  (∀ (i : ι), IsRelUpperSet (f i) P) → IsRelUpperSet (⋃ i, f i) P
-- Lean.Linter.UnusedVariables
/-- Reports unused variable warnings on each command. Use `linter.unusedVariables` to disable.  -/
Lean.Linter.UnusedVariables.unusedVariables : Lean.Linter
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.norm.go : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldl_one : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N), ((CliffordAlgebra.foldl Q f hf) n) 1 = n
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Read a vector of length `n` from the tape.  -/
Turing.TM1to1.readAux : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (n : ℕ) →
        (List.Vector Bool n → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) →
          Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.alter.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((y : α) → motive (some y)) → motive x
-- Mathlib.Data.Stream.Defs
/-- Prepend an element to a stream.  -/
Stream'.«term_::_» : Lean.TrailingParserDescr
-- Mathlib.Order.Bounds.Image
/-- **Alias** of `BddAbove.range_comp_left`. -/
BddAbove.range_comp : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {g : β → γ},
  BddAbove (Set.range f) → Monotone g → BddAbove (Set.range fun x => g (f x))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instOfIsClosedImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f], AlgebraicGeometry.IsImmersion f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_hom_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).iso.hom.app X_1 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj X_1))
      (CategoryTheory.CategoryStruct.comp (ψ.base.map (S.iso.hom.app X_1))
        ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G₁).hom.app (S.snd.obj X_1)))
-- Mathlib.Analysis.Complex.Hadamard
/-- Another technical lemma needed in the proof.  -/
_private.Mathlib.Analysis.Complex.Hadamard.0.Complex.HadamardThreeLines.bound_exp_eq : ∀ {l u : ℝ}, l < u → ∀ (z : ℂ), (z / (↑u - ↑l)).re - (↑l / (↑u - ↑l)).re = (z.re - l) / (u - l)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.finsetProd_singleton`. -/
Set.finset_prod_singleton : ∀ {M : Type u_5} {ι : Type u_6} [inst : CommMonoid M] (s : Finset ι) (I : ι → M), ∏ i ∈ s, {I i} = {∏ i ∈ s, I i}
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNewUnit.eq_1 : ∀ {α : Type u} [inst : BEq α] (l : List ((_ : α) × Unit)), Std.Internal.List.insertListIfNewUnit l [] = l
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeffAddEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (coeff : M →₀ R),
  AddMonoidAlgebra.coeffAddEquiv.symm coeff = AddMonoidAlgebra.ofCoeff coeff
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.mk : Lean.Name → Lean.Name → Array ℕ → ℕ → Lean.Meta.SimpCongrTheorem
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'}
  {c' : 𝕜'}, HasStrictDerivAt c c' x → HasStrictDerivAt f f' x → HasStrictDerivAt (c • f) (c x • f' + c' • f x) x
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'_undef : ∀ (z : ℂ) {τ : ℂ}, τ.im ≤ 0 → jacobiTheta₂' z τ = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Topology.IsEmbedding.measurableEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α]
  [mβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β] {f : α → β},
  Topology.IsEmbedding f → MeasurableSet (Set.range f) → MeasurableEmbedding f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `(M', f : M ⟶ M')` satisfies universal property of localized module, there is a canonical
map `LocalizedModule S M ⟶ M'`.
 -/
IsLocalizedModule.fromLocalizedModule : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M' : Type u_3} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M'] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M'] → (f : M →ₗ[R] M') → [IsLocalizedModule S f] → LocalizedModule S M →ₗ[R] M'
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.shift_comm : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {A : Type u_5}
  {inst_2 : AddMonoid A} {inst_3 : CategoryTheory.HasShift C A} {inst_4 : CategoryTheory.HasShift D A}
  {inst_5 : F₁.CommShift A} {inst_6 : F₂.CommShift A} [self : CategoryTheory.NatTrans.CommShift τ A] (a : A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₁ a).hom
      (CategoryTheory.Functor.whiskerRight τ (CategoryTheory.shiftFunctor D a)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).whiskerLeft τ)
      (CategoryTheory.Functor.commShiftIso F₂ a).hom
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.of_isIntegral : ∀ (R : Type u_1) [inst : CommRing R] (B : Type u_4) [inst_1 : CommRing B] [IsDomain B] [Nontrivial R]
  [inst_4 : Algebra R B] [Algebra.IsIntegral R B] [Ring.DimensionLEOne R], Ring.DimensionLEOne B
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functorialityEquivalence_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  (CategoryTheory.Limits.Cocone.functorialityEquivalence F e).counitIso =
    CategoryTheory.NatIso.ofComponents' (fun c => CategoryTheory.Limits.Cocone.extInv (e.counitIso.app c.pt) ⋯) ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The image of an additive monoid object under a lax monoidal functor is an additive
monoid object. -/
CategoryTheory.Functor.addMonObjObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.LaxMonoidal] → (X : C) → [CategoryTheory.AddMonObj X] → CategoryTheory.AddMonObj (F.obj X)
-- Mathlib.Algebra.Lie.Abelian
LieAlgebra.self_module_ker_eq_center : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieModule.ker R L L = LieAlgebra.center R L
-- Init.Core
NonScalar.mk.inj : ∀ {val val_1 : ℕ}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁)
  {Z : CategoryTheory.Functor C₃ C₃} (h : CategoryTheory.Functor.id C₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((G.obj (Opposite.op Y₁)).whiskerLeft (F.map f))
      (CategoryTheory.CategoryStruct.comp (adj₂.adj Y₁).counit h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (G.map f.op) (F.obj X₁))
      (CategoryTheory.CategoryStruct.comp (adj₂.adj X₁).counit h)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.ContinuousLinearMap.adjointAux.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E], ContinuousLinearMap.adjointAux✝ = ContinuousLinearMap.adjointAux✝
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_3 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is a more convenient formulation to show that a `PullbackCone` constructed using
`PullbackCone.mk` is a limit cone.
 -/
CategoryTheory.Limits.PullbackCone.IsLimit.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {W : C} →
            {fst : W ⟶ X} →
              {snd : W ⟶ Y} →
                (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g) →
                  (lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ W) →
                    (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                        CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) →
                      (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                          CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) →
                        (∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt ⟶ W),
                            CategoryTheory.CategoryStruct.comp m fst = s.fst →
                              CategoryTheory.CategoryStruct.comp m snd = s.snd → m = lift s) →
                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd eq)
-- Mathlib.Algebra.GroupWithZero.Basic
GroupWithZero.mul_right_injective : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {x : G₀}, x ≠ 0 → Function.Injective fun y => x * y
-- Lean.Meta.LazyDiscrTree
/-- Returns `true` if `e` is one of the following
- `Nat.add _ k` where `isNumeral k`
- `Add.add Nat _ _ k` where `isNumeral k`
- `HAdd.hAdd _ Nat _ _ k` where `isNumeral k`
- `Nat.succ _`
This function assumes `e.isAppOf fName`
 -/
Lean.Meta.LazyDiscrTree.MatchClone.isNatOffset : Lean.Name → Lean.Expr → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.comp_id : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁ →qᵢ Q₂),
  f.comp (QuadraticMap.Isometry.id Q₁) = f
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.piLinearEquiv_apply : ∀ {ι : Type v} {M₁ : ι → Type w₁} {R' : Type u_1} {A : Type u_2} [inst : Semiring R'] [inst_1 : Semiring A]
  [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] [inst_3 : (i : ι) → TopologicalSpace (M₁ i)]
  [inst_4 : (i : ι) → Module A (M₁ i)] {ι' : Type u_3} {M' : ι' → Type u_4} [inst_5 : (i : ι') → AddCommMonoid (M' i)]
  [inst_6 : (i : ι') → TopologicalSpace (M' i)] [inst_7 : ∀ (i : ι'), ContinuousAdd (M' i)]
  [inst_8 : (i : ι') → Module R' (M' i)] [inst_9 : (i : ι') → Module A (M' i)]
  [inst_10 : ∀ (i : ι'), SMulCommClass A R' (M' i)] [inst_11 : ∀ (i : ι'), ContinuousConstSMul R' (M' i)]
  (a : (i : ι') → ContinuousMultilinearMap A M₁ (M' i)),
  ContinuousMultilinearMap.piLinearEquiv a = ContinuousMultilinearMap.pi a
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (G : CategoryTheory.Functor D H)
  {Z : CategoryTheory.Functor C H} (h : L.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft ((L.ranAdjunction H).unit.app G))
      (CategoryTheory.CategoryStruct.comp (L.ranCounit.app (L.comp G)) h) =
    h