mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OrderOfElement
/-- If each prime factor of
`addOrderOf x` has higher multiplicity in `addOrderOf y`, and `x` commutes with `y`,
then `x + y` has the same order as `y`.  -/
AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
  AddCommute x y →
    IsOfFinAddOrder y →
      (∀ (p : ℕ), Nat.Prime p → p ∣ addOrderOf x → p * addOrderOf x ∣ addOrderOf y) → addOrderOf (x + y) = addOrderOf y
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- If `P` and `Q` are stable under cobase change and pushouts along `f` exist for morphisms in `P`,
this is the functor `P.Under Q X ⥤ P.Under Q Y` given by cobase change along `f`.  -/
CategoryTheory.MorphismProperty.Under.pushout : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P Q : CategoryTheory.MorphismProperty T) →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          (f : X ⟶ Y) →
            [P.HasPushoutsAlong f] →
              [P.IsStableUnderCobaseChangeAlong f] →
                [Q.IsStableUnderCobaseChange] → CategoryTheory.Functor (P.Under Q X) (P.Under Q Y)
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.geo_series : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] [Archimedean α] [Nontrivial β] (x : β),
  abv x < 1 → IsCauSeq abv fun n => ∑ m ∈ Finset.range n, x ^ m
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
/-- `TensorProduct.map` for `QuadraticForm.Isometry`s  -/
QuadraticMap.Isometry.tmul : {R : Type uR} →
  {M₁ : Type uM₁} →
    {M₂ : Type uM₂} →
      {M₃ : Type uM₃} →
        {M₄ : Type uM₄} →
          [inst : CommRing R] →
            [inst_1 : AddCommGroup M₁] →
              [inst_2 : AddCommGroup M₂] →
                [inst_3 : AddCommGroup M₃] →
                  [inst_4 : AddCommGroup M₄] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module R M₄] →
                            [inst_9 : Invertible 2] →
                              {Q₁ : QuadraticForm R M₁} →
                                {Q₂ : QuadraticForm R M₂} →
                                  {Q₃ : QuadraticForm R M₃} →
                                    {Q₄ : QuadraticForm R M₄} → (Q₁ →qᵢ Q₂) → (Q₃ →qᵢ Q₄) → Q₁.tmul Q₃ →qᵢ Q₂.tmul Q₄
-- Mathlib.Analysis.Convex.Deriv
/-- Reformulation of `ConvexOn.le_slope_of_hasDerivWithinAt` using `derivWithin`.  -/
ConvexOn.derivWithin_le_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S x → derivWithin f S x ≤ slope f x y
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is `r`-Hölder over a bounded space, then it is also `s`-Hölder when `s ≤ r`.  -/
HolderWith.of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C D s : NNReal}, (∀ (x y : X), edist x y ≤ ↑D) → HolderWith C r f → s ≤ r → HolderWith (C * D ^ (↑r - ↑s)) s f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple
of a rotation of another by `π / 2`, version subtracting vectors.  -/
Orientation.oangle_sub_left_smul_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V},
  x ≠ 0 → ∀ (r : ℝ), o.oangle (x - r • (o.rotation ↑(Real.pi / 2)) x) x = ↑(Real.arctan r)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.importEnv?.unsafe_impl_2 : Lean.Environment → Option Lean.Environment
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (W : CategoryTheory.MorphismProperty C) →
                [inst_6 : W.HasLeftCalculusOfFractions] →
                  [inst_7 : W.IsCompatibleWithTriangulation] →
                    [inst_8 : W.HasLocalization] → CategoryTheory.Pretriangulated W.Localization'
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain : {R : Type u_1} →
  [inst : CommRing R] →
    {L : Type u_2} →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → FunLike (↥(LieModule.Cohomology.twoCochain R L M)) L (L →ₗ[R] M)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.Approx.P_mk : ∀ {F : PFunctor.{uA, uB}} (x : ↑F F.M), PFunctor.Approx.AllAgree (PFunctor.M.Approx.sMk x)
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.dense_iff : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {s : Set X}, Dense s ↔ ∀ (x : X), f x ∈ closure (f '' s)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_iUnion_iff_of_countable : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {ι : Sort u_1} {f : ι → Set α} [Countable ι],
  Order.cof α ≠ Cardinal.aleph0 → (IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i))
-- Lean.Meta.DiscrTree.Main
/-- Return `true` if `fn` is a "bad" key. That is, `pushArgs` would add `Key.other` or `Key.star`.
We use this function when processing "root terms, and will avoid unfolding terms.
Note that without this trick the pattern `List.map f ∘ List.map g` would be mapped into the key `Key.other`
since the function composition `∘` would be unfolded and we would get `fun x => List.map g (List.map f x)`
 -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.isBadKey : Lean.Expr → Bool
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The unique maximal ideal of the localization at `I.primeCompl` lies over the ideal `I`.  -/
Localization.AtPrime.under_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime],
  Ideal.under R (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_sub : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R) (n : ℕ), (p - q).coeff n = p.coeff n - q.coeff n
-- Mathlib.Algebra.CharP.Defs
/-- Any power of the exponential characteristic is positive.  -/
expChar_pow_pos : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (q : ℕ) [ExpChar R q] (n : ℕ), 0 < q ^ n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
/-- **Alias** of `cfc_mem_elemental`. -/
cfc_apply_mem_elemental : ∀ {𝕜 : 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] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A] [inst_8 : ContinuousStar A] (f : 𝕜 → 𝕜)
  (a : A), cfc f a ∈ StarAlgebra.elemental 𝕜 a
-- Mathlib.Topology.WithTopology
WithTopology.instSubsingleton : ∀ {X : Type u_1} (t : TopologicalSpace X) [Subsingleton X], Subsingleton (WithTopology X t)
-- Init.Data.Slice.Basic
/-- Wrapper structure for slice types that makes generic slice functions available via dot notation.
The implementation of the functions depends on the type `γ` of the internal representation.

Usually, if `γ` is the internal representation of a slice of some type `α`, then `Slice γ` can be
used directly, but one usually creates an abbreviation `AlphaSlice := Slice γ` and provides
`Self (Slice γ) AlphaSlice` and `Sliceable shape α AlphaSlice` instances. Then `AlphaSlice` can
be worked with without ever thinking of `Slice` and it is possible to extend the API with
`α`/`γ`-specific functions.
 -/
Std.Slice : Type u → Type u
-- Mathlib.Algebra.Order.Sum
Sum.nonneg_elim_iff : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [inst : LE β] [inst_1 : Zero β] {v₁ : α₁ → β} {v₂ : α₂ → β},
  0 ≤ Sum.elim v₁ v₂ ↔ 0 ≤ v₁ ∧ 0 ≤ v₂
-- Mathlib.Data.Sum.Order
OrderIso.sumDualDistrib_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (a : α),
  (OrderIso.sumDualDistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inl (OrderDual.toDual a)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.div_sUnion : ∀ {α : Type u_2} [inst : Div α] (s : Set α) (T : Set (Set α)), s / ⋃₀ T = ⋃ t ∈ T, s / t
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
Submodule.coe_subtypeₗᵢ : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {R' : Type u_11} [inst_1 : Ring R'] [inst_2 : Module R' E]
  (p : Submodule R' E), ⇑p.subtypeₗᵢ = ⇑p.subtype
-- Mathlib.Order.Bounds.Image
/-- A monotone map sends a least element of a set to a least element of its image.  -/
MonotoneOn.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  MonotoneOn f t → IsLeast t a → IsLeast (f '' t) (f a)
-- Init.Data.Array.InsertIdx
Array.mem_insertIdx : ∀ {α : Type u} {a : α} {i : ℕ} {b : α} {xs : Array α} {h : i ≤ xs.size}, a ∈ xs.insertIdx i b h ↔ a = b ∨ a ∈ xs
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (x v_1 : V) (r : G.Adj v v_1) (p : G.Walk v_1 w)
  (x_1 : x ∈ (SimpleGraph.Walk.cons r p).support),
  (SimpleGraph.Walk.cons r p).takeUntil x x_1 =
    if hx : v = x then hx ▸ SimpleGraph.Walk.nil else SimpleGraph.Walk.cons r (p.takeUntil x ⋯)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (f g : M ⟶ N), f.hom = g.hom → f = g
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.Exact.exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (self : S.Exact) (i : ℕ)
  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.Exact._auto_1), (S.sc ⋯ i hi).Exact
-- Aesop.Rule
Aesop.SafeRuleInfo.mk.sizeOf_spec : ∀ (penalty : ℤ) (safety : Aesop.Safety),
  sizeOf { penalty := penalty, safety := safety } = 1 + sizeOf penalty + sizeOf safety
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_bmod_self_left : ∀ (a : ℕ) (b c : ℤ), (↑a * b - c).bmod a = (-c).bmod a
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pullback.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ φ_1 : A →* B}
  (e_φ : φ = φ_1) {ψ ψ_1 : B →* C} (e_ψ : ψ = ψ_1) (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A]
  [inst_7 : IsTopologicalGroup B] [inst_8 : NormedAddCommGroup E] (f f_1 : CompactlySupportedContinuousMap B E),
  f = f_1 → ∀ (b b_1 : B), b = b_1 → H.pullback f b = ⋯.pullback f_1 b_1
-- Init.Data.Int.Linear
Int.Internal.Linear.cdiv.eq_1 : ∀ (a b : ℤ), Int.Internal.Linear.cdiv a b = -(-a / b)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).getKey? k = if t₂.contains k = true then none else t₁.getKey? k
-- Init.Data.List.MapIdx
List.mem_mapFinIdx : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : (i : ℕ) → α → i < l.length → β},
  b ∈ l.mapFinIdx f ↔ ∃ i, ∃ (h : i < l.length), f i l[i] h = b
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.id_hom_hom_hom_apply : ∀ (X : LightDiagram) (a : ↑X.toProfinite.toTop), (TopCat.Hom.hom (CategoryTheory.CategoryStruct.id X).hom.hom) a = a
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating the second vector by `θ` adds `θ` to the angle between two vectors.  -/
Orientation.oangle_rotation_right : ∀ {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},
  x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle x ((o.rotation θ) y) = o.oangle x y + θ
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence_eq_prefixFunction : ∀ {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size} {guess : ℕ} {hg : guess < stackPos},
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst ≤ guess + 1 →
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat guess stackPos →
      String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat stackPos hst guess hg =
        String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsFiniteKernel.restrict : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (hs : MeasurableSet s),
  ProbabilityTheory.IsFiniteKernel (κ.restrict hs)
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_range_toEnd_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.IsNilpotent (↥(LieModule.toEnd R L M).range) M ↔ LieModule.IsNilpotent L M
-- Mathlib.Data.Nat.Init
Nat.AtLeastTwo.neZero_sub_one : ∀ (n : ℕ) [n.AtLeastTwo], NeZero (n - 1)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.StrictPseudofunctor.mapAdjunction_unit : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {a b : B}
  {f : a ⟶ b} {g : b ⟶ a} (F : CategoryTheory.StrictPseudofunctor B C) (adj : CategoryTheory.Bicategory.Adjunction f g),
  (F.mapAdjunction adj).unit =
    CategoryTheory.CategoryStruct.comp (F.mapId a).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ adj.unit) (F.mapComp f g).hom)
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- An element of the character space, as a continuous linear map.  -/
WeakDual.CharacterSpace.toCLM : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : NonUnitalNonAssocSemiring A] →
              [inst_5 : TopologicalSpace A] → [inst_6 : Module 𝕜 A] → ↑(WeakDual.characterSpace 𝕜 A) → A →L[𝕜] 𝕜
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.scopeName : Aesop.CoreRuleBuilderOutput → Aesop.ScopeName
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.insertSmallerList : {α : Type u} → {β : α → Type v} → [BEq α] → List ((a : α) × β a) → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.exists_finsupp_nat_of_fin_fun_injective : ∀ {R : Type u_1} {P : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {n : ℕ}
  {f : (Fin (n + 1) → P) →ₗ[R] Fin n → P}, Function.Injective ⇑f → ∃ g, Function.Injective ⇑g
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrLeft'_apply : ∀ {ι : Type u_7} {ι' : Type u_8} (R : ι → Type u_9) (e : ι ≃ ι') [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)]
  (f : (a : ι) → R a) (x : ι'), (RingEquiv.piCongrLeft' R e) f x = f (e.symm x)
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `Config` which allows a class of goals to be returned as subgoals.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.accept : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } →
  (Lean.MVarId → Lean.MetaM Bool) → Lean.Meta.SolveByElim.SolveByElimConfig
-- Init.Data.Array.Find
Array.find?_eq_some_iff_getElem : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {b : α},
  Array.find? p xs = some b ↔
    p b = true ∧ ∃ i, ∃ (h : i < xs.size), xs[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p xs[j]) = true
-- Mathlib.Analysis.Complex.Trigonometric
Complex.enorm_exp_I_mul_ofReal : ∀ (x : ℝ), ‖Complex.exp (Complex.I * ↑x)‖ₑ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mkIso.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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}
  [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'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left left_1 : ψ.left ≅ ψ'.left) (e_left : left = left_1)
  (right right_1 : ψ.right ≅ ψ'.right) (e_right : right = right_1) (base base_1 : ψ.base ≅ ψ'.base)
  (e_base : base = base_1)
  (left_coherence :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
        (CategoryTheory.Functor.whiskerRight left.hom F') =
      CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
        (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
  (right_coherence :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
        (CategoryTheory.Functor.whiskerRight right.hom G') =
      CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
        (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom),
  CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence =
    CategoryTheory.Limits.CatCospanTransform.mkIso left_1 right_1 base_1 ⋯ ⋯
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerDone_flatMapM_pure : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α Id β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β}
  {it₂ : Std.IterM m γ},
  it₂.IsPlausibleStep Std.IterStep.done →
    (Std.Iter.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (Std.IterStep.skip (Std.Iter.flatMapAfterM f it₁ none))
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.comp_ofId : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (f : 𝒜 →ₐᵍ[R] ℬ), (↑f).comp (Algebra.ofId R A) = Algebra.ofId R B
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- For any path `p` from `x₀` to `x₁`, we have a homotopy from `(Path.refl x₀).trans p` to `p`.  -/
Path.Homotopy.reflTrans : {X : Type u_1} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → (p : Path x₀ x₁) → ((Path.refl x₀).trans p).Homotopy p
-- Lean.Data.Lsp.Communication
_private.Lean.Data.Lsp.Communication.0.Lean.IO.FS.Stream.parseHeaderField : String → Option (String × String)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conjRingEquiv_apply_apply : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {M₁ : Type u_13} {M₂ : Type u_14} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M₁] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂]
  (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₁ →ₗ[R₁] M₁) (x : M₂), (e.conjRingEquiv f) x = e (f (e.symm x))
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_inv : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (a : Quaternion R),
  Quaternion.normSq a⁻¹ = (Quaternion.normSq a)⁻¹
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
/-- If the Frobenius map is surjective on `R/pR`, then the Fontaine's θ map is surjective.  -/
surjective_fontaineTheta : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) R],
  Function.Surjective ⇑(frobenius (ModP R p) p) → Function.Surjective ⇑(WittVector.fontaineTheta R p)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_eq_getD_get? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, m.getD a fallback = (m.get? a).getD fallback
-- Init.Control.Basic
/-- Lifts an action from the inner monad `m` to the outer monad `n`. The inner monad has access to a
reverse lifting operator that can run an `n` action, returning a value and state together.
 -/
MonadControl.liftWith : {m : semiOutParam (Type u → Type v)} →
  {n : Type u → Type w} →
    [self : MonadControl m n] → {α : Type u} → (({β : Type u} → n β → m (MonadControl.stM m n β)) → m α) → n α
-- Lean.Meta.Tactic.ElimInfo
/-- Eliminators/recursors may have implicit targets. For builtin recursors, all indices are implicit targets.
Given an eliminator and the sequence of explicit targets, this methods returns a new sequence containing
implicit and explicit targets.
 -/
Lean.Meta.addImplicitTargets : Lean.Meta.ElimInfo → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ u₁₂_1 : X₁ ⟶ X₂} (e_u₁₂ : u₁₂ = u₁₂_1) {u₂₃ u₂₃_1 : X₂ ⟶ X₃} (e_u₂₃ : u₂₃ = u₂₃_1)
  {u₁₃ u₁₃_1 : X₁ ⟶ X₃} (e_u₁₃ : u₁₃ = u₁₃_1) (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
  {v₁₂ v₁₂_1 : X₂ ⟶ Z₁₂} (e_v₁₂ : v₁₂ = v₁₂_1) {w₁₂ w₁₂_1 : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (e_w₁₂ : w₁₂ = w₁₂_1)
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ v₂₃_1 : X₃ ⟶ Z₂₃} (e_v₂₃ : v₂₃ = v₂₃_1) {w₂₃ w₂₃_1 : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  (e_w₂₃ : w₂₃ = w₂₃_1)
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ v₁₃_1 : X₃ ⟶ Z₁₃} (e_v₁₃ : v₁₃ = v₁₃_1) {w₁₃ w₁₃_1 : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (e_w₁₃ : w₁₃ = w₁₃_1)
  (h₁₃ :
    CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ = CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯
-- Init.Control.Lawful.Instances
ReaderT.run_bind : ∀ {m : Type u_1 → Type u_2} {ρ α β : Type u_1} [inst : Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ),
  (x >>= f).run ctx = do
    let a ← x.run ctx
    (f a).run ctx