mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Induction principle for matrices based on transvections: if a property is true for all diagonal
matrices, all transvections, and is stable under product, then it is true for all matrices. This is
the useful way to say that matrices are generated by diagonal matrices and transvections.

We state a slightly more general version: to prove a property for a matrix `M`, it suffices to
assume that the diagonal matrices we consider have the same determinant as `M`. This is useful to
obtain similar principles for `SLₙ` or `GLₙ`.  -/
Matrix.diagonal_transvection_induction : ∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (P : Matrix n n 𝕜 → Prop)
  (M : Matrix n n 𝕜),
  (∀ (D : n → 𝕜), (Matrix.diagonal D).det = M.det → P (Matrix.diagonal D)) →
    (∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix) → (∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)) → P M
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_prod : ∀ {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [inst : CommMonoid β] {f : ι → α → β} (I : Finset ι),
  (UniformOnFun.ofFun 𝔖) (∏ i ∈ I, f i) = ∏ i ∈ I, (UniformOnFun.ofFun 𝔖) (f i)
-- Init.Data.List.Lemmas
List.flatten_replicate_singleton : ∀ {n : ℕ} {α : Type u_1} {a : α}, (List.replicate n [a]).flatten = List.replicate n a
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_fg : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Function.Injective ⇑(algebraMap R S) → ∀ (I : Ideal R), (IsLocalization.coeSubmodule S I).FG ↔ Submodule.FG I
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableInsertReplaceEdit : Hashable Lean.Lsp.InsertReplaceEdit
-- Mathlib.Algebra.Order.Field.Basic
Bound.one_lt_div_of_pos_of_lt : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α}, 0 < b → b < a → 1 < a / b
-- Mathlib.CategoryTheory.Opposites
/-- The natural isomorphism between functors `G.unop ≅ F.unop` induced by a natural isomorphism
between the original functors `F ≅ G`.  -/
CategoryTheory.NatIso.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} → (F ≅ G) → (G.unop ≅ F.unop)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.GradedNatTrans.mk.congr_simp : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D}
  (app app_1 : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X) (e_app : app = app_1)
  (naturality :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y))
            (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y))
          (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Init.Data.String.Slice
/-- Checks whether the slice \(`s`\) begins with the pattern \(`pat`\).

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.startsWith "red" = true`

* `"red green blue".toSlice.startsWith "green" = false`

* `"red green blue".toSlice.startsWith "" = true`

* `"red green blue".toSlice.startsWith 'r' = true`

* `"red green blue".toSlice.startsWith Char.isLower = true`
 -/
String.Slice.startsWith : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Bool
-- Lean.CoreM
Lean.mapCoreM : {m : Type → Type u_1} →
  [MonadControlT Lean.CoreM m] → [Monad m] → ({α : Type} → Lean.CoreM α → Lean.CoreM α) → {α : Type} → m α → m α
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.id_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (A : CategoryTheory.Endofunctor.Algebra F),
  CategoryTheory.Endofunctor.Algebra.Hom.id A = CategoryTheory.CategoryStruct.id A
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Given a diagram `{ Dᵢ }` of schemes and an open `U ⊆ Dᵢ`,
this is the diagram of `{ Dⱼᵢ⁻¹ U }_{j ≤ i}`.  -/
AlgebraicGeometry.opensDiagram : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) →
      (i : I) → (D.obj i).Opens → CategoryTheory.Functor (CategoryTheory.Over i) AlgebraicGeometry.Scheme
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.iteratedDeriv_charFun_zero : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ},
  MeasureTheory.MemLp id (↑n) μ → iteratedDeriv n (MeasureTheory.charFun μ) 0 = Complex.I ^ n * ↑(∫ (x : ℝ), x ^ n ∂μ)
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorFinHPowNatOfNat : ∀ {w : ℕ}, LawfulXor (Fin (2 ^ w))
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.App.mk.inj : ∀ {coe fn arg coe_1 fn_1 arg_1 : Lean.Expr},
  { coe := coe, fn := fn, arg := arg } = { coe := coe_1, fn := fn_1, arg := arg_1 } →
    coe = coe_1 ∧ fn = fn_1 ∧ arg = arg_1
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (n : ℤ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.num n with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.intCast n => h_2 n
    | Lean.Grind.CommRing.Expr.natCast n => h_3 n
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | x => h_5 x) =
    h_1 n
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.isLocalizedModule_of_isLocalizedModule : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  (p : Submonoid R) [IsLocalization p S] [IsLocalizedModule p (IsScalarTower.toAlgHom R A B).toLinearMap],
  IsLocalizedModule p (↑R (KaehlerDifferential.map R S A B))
-- Mathlib.GroupTheory.Congruence.Defs
/-- Multiplicative congruence relations preserve multiplication.  -/
Con.mul : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {w x y z : M}, c w x → c y z → c (w * y) (x * z)
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixedField_antitone : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  Antitone IntermediateField.fixedField
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.failed.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (error : Std.Http.Protocol.H1.Error),
  sizeOf (Std.Http.Protocol.H1.Reader.State.failed error) = 1 + sizeOf error
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- The leading exponent of a multiseries with non-empty basis. For `ms = []` it is `⊥`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → WithBot ℝ
-- Init.PropLemmas
if_true_left : ∀ {p q : Prop} [h : Decidable p], (if p then True else q) ↔ ¬p → q
-- Lean.MetavarContext
Lean.DependsOn.State.mk : Lean.ExprSet → Lean.MetavarContext → Lean.DependsOn.State
-- Mathlib.Data.Finset.CastCard
Finset.cast_card_sdiff : ∀ {α : Type u_1} {R : Type u_2} {s t : Finset α} [inst : DecidableEq α] [inst_1 : AddGroupWithOne R],
  s ⊆ t → ↑(t \ s).card = ↑t.card - ↑s.card
-- Aesop.Forward.LevelIndex
Aesop.instDecidableEqLevelIndex : DecidableEq Aesop.LevelIndex
-- Init.Data.List.Basic
List.beq_cons_cons : ∀ {α : Type u} [inst : BEq α] {a b : α} {as bs : List α}, (a :: as).beq (b :: bs) = (a == b && as.beq bs)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- `zeroLocus` and `vanishingIdeal` form a Galois connection.  -/
PrimeSpectrum.gc : ∀ (R : Type u) [inst : CommSemiring R],
  GaloisConnection (fun I => PrimeSpectrum.zeroLocus ↑I) fun t => PrimeSpectrum.vanishingIdeal t
-- Mathlib.SetTheory.Cardinal.Defs
/-- A cardinal lifted to a lower or equal universe equals itself.

Unfortunately, the simp lemma doesn't work.  -/
Cardinal.lift_id' : ∀ (a : Cardinal.{max u v}), Cardinal.lift.{u, max u v} a = a
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.norm : Bool → Bool → Lean.Meta.Grind.AttrKind
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiff.of_succ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞},
  ContMDiff I I' (n + 1) f → ContMDiff I I' n f
-- Batteries.Data.Array.Scan
Subarray.scanl.eq_1 : ∀ {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (as : Subarray α),
  Subarray.scanl f init as = Array.scanl f init as.array as.start as.stop
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_add_left' : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {a : α}, (fun x => -a + x) '' t = (fun x => a + x) ⁻¹' t
-- Mathlib.Data.Fin.Embedding
/-- `Fin.succ` as an `Embedding`  -/
Fin.succEmb : (n : ℕ) → Fin n ↪ Fin (n + 1)
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Server.getIOState! : String → Dynamic → (stateType : Type) → [TypeName stateType] → IO stateType
-- Init.Data.List.Lemmas
List.contains_flatMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {l : List α} {f : α → List β} {x : β},
  (List.flatMap f l).contains x = l.any fun a => (f a).contains x
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicFrontier_subset_frontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, intrinsicFrontier 𝕜 s ⊆ frontier s
-- Mathlib.Data.List.Basic
List.instInsertOfDecidableEq_mathlib : {α : Type u} → [DecidableEq α] → Insert α (List α)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : DecidableEq α] (a : α) (x : G),
  AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq a x =
    AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq._aux_1 a x
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C}
  [inst_1 : CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) {Z : C} {f : (i : ι) → X i ⟶ Z}
  [inst_2 : CategoryTheory.Limits.HasPullback (f i) (f j)]
  (hc hc_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk Z f)),
  hc = hc_1 →
    CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit hij hc =
      CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit hij hc_1
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_inv_homologyπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv
      (((HomologicalComplex.single C c j).obj A).homologyπ j) =
    (HomologicalComplex.singleObjHomologySelfIso c j A).inv
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.mk.injEq : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  (tiles tiles_1 : ιₚ → DiscreteTiling.Prototile G X), ({ tiles := tiles } = { tiles := tiles_1 }) = (tiles = tiles_1)
-- Init.Data.List.Sublist
List.IsPrefix.map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) ⦃l₁ l₂ : List α⦄, l₁ <+: l₂ → List.map f l₁ <+: List.map f l₂
-- Mathlib.Data.Ordering.Lemmas
Ordering.dthen_eq_then : ∀ (o₁ o₂ : Ordering), (o₁.dthen fun x => o₂) = o₁.then o₂
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.cover_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {U : C}
  {S : CategoryTheory.Sieve (G.obj U)}, S ∈ K (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J U
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α} {v fallback : β},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
          (k, v) ∈ l →
            Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k' fallback = v
-- Init.Data.Fin.Lemmas
Fin.castLE.congr_simp : ∀ {n m : ℕ} (h : n ≤ m) (i i_1 : Fin n), i = i_1 → Fin.castLE h i = Fin.castLE h i_1
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_sub_smul : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E] (f : k → E) {a b : k},
  a ≠ b → slope (fun x => (x - a) • f x) a b = f b
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverUnit_map_left : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : C} (f : X ⟶ Y), ((CategoryTheory.toOverUnit C).map f).left = f
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.instIsLocallyFiniteMeasureMeasure : ∀ {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
  [inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)]
  (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ), MeasureTheory.IsLocallyFiniteMeasure ω.measure
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.eventually_atTop_prod_self : ∀ {α : Type u_3} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {p : α × α → Prop},
  (∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ a, ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryLT? k = t₂.getEntryLT? k
-- Lean.DocString.Parser
/-- Parses a code block. The resulting string literal has already had the fences' leading indentation
stripped.
 -/
Lean.Doc.Parser.codeBlock : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findM?.match_1.splitter : {α : Type} →
  (motive : List α → Sort u_1) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.lift_toCoprod_inr_eq_inr_mk : ∀ {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)),
  (FreeGroup.lift (PresentedGroup.toCoprod rels₁ rels₂)).comp (FreeGroup.map Sum.inr) =
    Monoid.Coprod.inr.comp (PresentedGroup.mk rels₂)
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.mk.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (toCoalgHom toCoalgHom_1 : A →ₗc[R] B) (e_toCoalgHom : toCoalgHom = toCoalgHom_1) (map_one' : toCoalgHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y),
  { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' } =
    { toCoalgHom := toCoalgHom_1, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_ofNatIsoLeft_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : F ⊣ H) (iso : F ≅ G) {X : C} {Y : D}
  (f : G.obj X ⟶ Y),
  ((adj.ofNatIsoLeft iso).homEquiv X Y) f = (adj.homEquiv X Y) (CategoryTheory.CategoryStruct.comp (iso.hom.app X) f)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.one_def : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X], 1 = DilationEquiv.refl X
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balance.eq_1 : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α),
  l.balance x r =
    Ordnode.casesOn (id l)
      (Ordnode.casesOn (id r) (Ordnode.singleton x) fun rs rl rx rr =>
        Ordnode.casesOn (id rl)
          (Ordnode.casesOn (motive := fun t => id rr = t → Ordnode α) (id rr) (fun h => Ordnode.node 2 Ordnode.nil x r)
            (fun size l x_1 r h => Ordnode.node 3 (Ordnode.singleton x) rx rr) ⋯)
          fun rls rll rlx rlr =>
          Ordnode.casesOn (id rr) (Ordnode.node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx)) fun rrs l x_1 r =>
            if rls < Ordnode.ratio * rrs then Ordnode.node (rs + 1) (Ordnode.node (rls + 1) Ordnode.nil x rl) rx rr
            else
              Ordnode.node (rs + 1) (Ordnode.node (rll.size + 1) Ordnode.nil x rll) rlx
                (Ordnode.node (rlr.size + rrs + 1) rlr rx rr))
      fun ls ll lx lr =>
      Ordnode.casesOn (id r)
        (Ordnode.casesOn (id ll)
          (Ordnode.casesOn lr (Ordnode.node 2 l x Ordnode.nil) fun size l lrx r =>
            Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x))
          fun lls l x_1 r =>
          Ordnode.casesOn (id lr) (Ordnode.node 3 ll lx (Ordnode.singleton x)) fun lrs lrl lrx lrr =>
            if lrs < Ordnode.ratio * lls then Ordnode.node (ls + 1) ll lx (Ordnode.node (lrs + 1) lr x Ordnode.nil)
            else
              Ordnode.node (ls + 1) (Ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx
                (Ordnode.node (lrr.size + 1) lrr x Ordnode.nil))
        fun rs rl rx rr =>
        if Ordnode.delta * ls < rs then
          Ordnode.casesOn (id rl) Ordnode.nil fun rls rll rlx rlr =>
            Ordnode.casesOn (id rr) Ordnode.nil fun rrs l_1 x_1 r =>
              if rls < Ordnode.ratio * rrs then Ordnode.node (ls + rs + 1) (Ordnode.node (ls + rls + 1) l x rl) rx rr
              else
                Ordnode.node (ls + rs + 1) (Ordnode.node (ls + rll.size + 1) l x rll) rlx
                  (Ordnode.node (rlr.size + rrs + 1) rlr rx rr)
        else
          if Ordnode.delta * rs < ls then
            Ordnode.casesOn (id ll) Ordnode.nil fun lls l x_1 r_1 =>
              Ordnode.casesOn (id lr) Ordnode.nil fun lrs lrl lrx lrr =>
                if lrs < Ordnode.ratio * lls then Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (lrs + rs + 1) lr x r)
                else
                  Ordnode.node (ls + rs + 1) (Ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx
                    (Ordnode.node (lrr.size + rs + 1) lrr x r)
          else Ordnode.node (ls + rs + 1) l x r
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h) =
    CategoryTheory.CategoryStruct.comp (X.δ f₂ f₃ n₀ n₁ hn₁) h
-- Lean.Server.References
Lean.Server.References.ParentDecl.mk.sizeOf_spec : ∀ (name : String) (range selectionRange : Lean.Lsp.Range),
  sizeOf { name := name, range := range, selectionRange := selectionRange } =
    1 + sizeOf name + sizeOf range + sizeOf selectionRange
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- A function `f : M → Icc x y` is smooth iff its composition with the inclusion
into `ℝ` is smooth.  -/
contMDiff_iff_comp_subtypeVal_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {x y : ℝ}
  [h : Fact (x < y)] {n : WithTop ℕ∞} {f : M → ↑(Set.Icc x y)},
  ContMDiff I (modelWithCornersEuclideanHalfSpace 1) n f ↔
    Continuous f ∧ ContMDiff I (modelWithCornersSelf ℝ ℝ) n ((fun z => ↑z) ∘ f)
-- Mathlib.Dynamics.BirkhoffSum.Basic
map_birkhoffSum : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {F : Type u_3} {N : Type u_4} [inst_1 : AddCommMonoid N]
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) (x : α),
  g' (birkhoffSum f g n x) = birkhoffSum f (⇑g' ∘ g) n x
-- Std.Data.HashMap.Raw
/-- Transforms the hash map into an array of mappings in some order.  -/
Std.HashMap.Raw.toArray : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → Array (α × β)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange], P.RespectsIso
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.InnerFibration.mk : ∀ {X Y : SSet} {q : X ⟶ Y}, SSet.innerFibrations q → SSet.InnerFibration q
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Two lifts of the same morphism are homotopic.  -/
CategoryTheory.ProjectiveResolution.liftHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (f : Y ⟶ Z) →
          {P : CategoryTheory.ProjectiveResolution Y} →
            {Q : CategoryTheory.ProjectiveResolution Z} →
              (g h : P.complex ⟶ Q.complex) →
                CategoryTheory.CategoryStruct.comp g Q.π =
                    CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) →
                  CategoryTheory.CategoryStruct.comp h Q.π =
                      CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) →
                    Homotopy g h
-- Mathlib.CategoryTheory.Galois.Basic
/-- If `X : ι → C` is a finite family of objects with non-empty fiber, then
also `∏ᶜ X` has non-empty fiber.  -/
CategoryTheory.PreGaloisCategory.nonempty_fiber_pi_of_nonempty_of_finite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {ι : Type u_1}
  [inst_3 : Finite ι] (X : ι → C) [∀ (i : ι), Nonempty (F.obj (X i)).obj], Nonempty (F.obj (∏ᶜ X)).obj
-- Mathlib.Tactic.TFAE
/-- A `tfae_have` type specification, e.g. `1 ↔ 3` The numbers refer to the proposition at the
corresponding position in the `TFAE` goal (starting at 1).  -/
Mathlib.Tactic.TFAE.Parser.tfaeType : Lean.Parser.Parser