mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Homotopy.Basic
/-- Casting a `ContinuousMap.Homotopy f₀ f₁` to a `ContinuousMap.Homotopy g₀ g₁` where `f₀ = g₀`
and `f₁ = g₁`.
 -/
ContinuousMap.Homotopy.cast : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ g₀ g₁ : C(X, Y)} → f₀.Homotopy f₁ → f₀ = g₀ → f₁ = g₁ → g₀.Homotopy g₁
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- `rpow` version of `Finset.prod_pow`.  -/
Real.finsetProd_rpow : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ℝ), (∀ i ∈ s, 0 ≤ f i) → ∀ (r : ℝ), ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
-- Init.Data.Rat.Lemmas
Rat.mul_lt_mul_right : ∀ {a b c : ℚ}, 0 < c → (a * c < b * c ↔ a < b)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map.of : ∀ {α : Type u} {β : Type v} {f : α → β} {x : α}, (FreeAddGroup.map f) (FreeAddGroup.of x) = FreeAddGroup.of (f x)
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.prod_parallelepiped : ∀ {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Fintype ι] [inst_1 : Fintype ι']
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace ℝ F]
  (v : Module.Basis ι ℝ E) (w : Module.Basis ι' ℝ F), (v.prod w).parallelepiped = v.parallelepiped ×ˢ w.parallelepiped
-- Mathlib.Tactic.FunProp.FunctionData
/-- Is `f` an identity function?  -/
Mathlib.Meta.FunProp.FunctionData.isIdentityFun : Mathlib.Meta.FunProp.FunctionData → Bool
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_pos_of_integrable_nonneg_nonzero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α] [μ.IsOpenPosMeasure]
  {f : α → ℝ} {x : α}, Continuous f → MeasureTheory.Integrable f μ → 0 ≤ f → f x ≠ 0 → 0 < ∫ (x : α), f x ∂μ
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
/-- A colimit multicofork attached to a `MulticoequalizerDiagram`
structure in the complete lattice of subcomplexes of a simplicial set.
In this variant, we assume that the index type `ι` has a linear order. This allows
to consider only the "relations" given by tuples `(i, j)` such that `i < j`.  -/
SSet.Subcomplex.MulticoequalizerDiagram.isColimit' : {X : SSet} →
  {A : X.Subcomplex} →
    {ι : Type u_1} →
      {U : ι → X.Subcomplex} →
        {V : ι → ι → X.Subcomplex} →
          (h : A.MulticoequalizerDiagram U V) →
            [inst : LinearOrder ι] →
              CategoryTheory.Limits.IsColimit
                ((CompleteLattice.MulticoequalizerDiagram.multicofork h).toLinearOrder.map
                  SSet.Subcomplex.toSSetFunctor)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cosh_antiperiodic : Function.Antiperiodic Complex.cosh (↑Real.pi * Complex.I)
-- Mathlib.Combinatorics.Graph.Basic
Graph.Compatible.rfl : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.Compatible G
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (h₁ h₂ : CategoryTheory.MonObj X), CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul → h₁ = h₂
-- Mathlib.Data.List.Sort
List.SortedLT.getElem_le_getElem_iff : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α],
  l.SortedLT → ∀ {i j : ℕ} {hi : i < l.length} {hj : j < l.length}, l[i] ≤ l[j] ↔ i ≤ j
-- Mathlib.Algebra.GroupWithZero.Defs
/-- If `α` has no zero divisors, then the product of two elements is nonzero iff both of them
are nonzero.  -/
mul_ne_zero_iff : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_pow : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (x : ℤ) (k : ℕ), ↑(x ^ k) = ↑x ^ k
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_pairwise_disjoint : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  (↑f.cycleFactorsFinset).Pairwise Equiv.Perm.Disjoint
-- Mathlib.Data.Quot
Quot.out_eq : ∀ {α : Sort u_1} {r : α → α → Prop} (q : Quot r), Quot.mk r q.out = q
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.getKey a ⋯
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.distinguished_cocone_triangle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  ∃ Z g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
-- Mathlib.Order.Nucleus
Nucleus.idempotent : ∀ {X : Type u_1} [inst : SemilatticeInf X] {n : Nucleus X} (x : X), n (n x) = n x
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_iff_dvd_of_dvd_sub : ∀ {a b c : ℤ}, a ∣ b - c → (a ∣ b ↔ a ∣ c)
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.
 -/
Std.DTreeMap.Internal.Impl.mergeWith : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        ((a : α) → β a → β a → β a) →
          (t₁ : Std.DTreeMap.Internal.Impl α β) →
            Std.DTreeMap.Internal.Impl α β → t₁.Balanced → Std.DTreeMap.Internal.Impl.BalancedTree α β
-- Init.System.IO
IO.Prim.setAccessRights : System.FilePath → UInt32 → IO Unit
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.coe_restrictScalarsL : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type u_3}
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜 F]
  {𝕜' : Type u_4} [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F] {𝕜'' : Type u_5}
  [inst_15 : Ring 𝕜''] [inst_16 : Module 𝕜'' F] [inst_17 : ContinuousConstSMul 𝕜'' F] [inst_18 : SMulCommClass 𝕜 𝕜'' F]
  [inst_19 : SMulCommClass 𝕜' 𝕜'' F],
  ↑(ContinuousLinearMap.restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalarsₗ 𝕜 E F 𝕜' 𝕜''
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset`.

---

The category of `κ`-filtered partially ordered types,
with morphisms given by order embeddings.  -/
CategoryTheory.CardinalFilteredPoset : (κ : Cardinal.{u}) → [Fact κ.IsRegular] → Type (u + 1)
-- Init.Data.Array.MinMax
_private.Init.Data.Array.MinMax.0.Array.min?.eq_1 : ∀ {α : Type u_1} [inst : Min α] (arr : Array α), arr.min? = if h : arr ≠ #[] then some (arr.min h) else none
-- Mathlib.Algebra.CharP.Defs
charP_iff : ∀ (R : Type u_2) [inst : AddMonoidWithOne R] (p : outParam ℕ), CharP R p ↔ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.vecMulVec_update : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Mul α] (u : m → α) (v : n → α) (j : n)
  (a : α), Matrix.vecMulVec u (Function.update v j a) = (Matrix.vecMulVec u v).updateCol j (MulOpposite.op a • u)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasAbsLeftKanExtension.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [toHasLeftKanExtension : CategoryTheory.Bicategory.HasLeftKanExtension f g],
  (∀ {x : B} (h : c ⟶ x), CategoryTheory.Bicategory.Lan.CommuteWith f g h) →
    CategoryTheory.Bicategory.HasAbsLeftKanExtension f g
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyIrreducible f],
  IrreducibleSpace ↥(AlgebraicGeometry.Scheme.Hom.fiber f s)
-- Mathlib.Analysis.Calculus.VectorField
/-- The differentiation operator along `[W, V]`
is the commutator of the differentiation operators along `W` and `V`.  -/
VectorField.fderiv_apply_lieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {V W : E → E}
  {x : E} {f : E → F} {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n f x →
    minSmoothness 𝕜 2 ≤ n →
      DifferentiableAt 𝕜 W x →
        DifferentiableAt 𝕜 V x →
          (fderiv 𝕜 f x) (VectorField.lieBracket 𝕜 V W x) =
            (fderiv 𝕜 (fun x => (fderiv 𝕜 f x) (W x)) x) (V x) - (fderiv 𝕜 (fun x => (fderiv 𝕜 f x) (V x)) x) (W x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_le_pow_iff_left : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b : M}
  {n : ℕ}, n ≠ 0 → (a ^ n ≤ b ^ n ↔ a ≤ b)
-- Mathlib.Order.DirectedInverseSystem
DirectedSystem.mk : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {f : ⦃i j : ι⦄ → i ≤ j → F i → F j},
  (∀ ⦃i : ι⦄ (x : F i), f ⋯ x = x) →
    (∀ ⦃k j i : ι⦄ (hij : i ≤ j) (hjk : j ≤ k) (x : F i), f hjk (f hij x) = f ⋯ x) → DirectedSystem F f
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.findExistsOneDivLT.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (i : Set α),
  MeasureTheory.SignedMeasure.findExistsOneDivLT✝ s i =
    if hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i then Nat.find ⋯ else 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
secondCountableTopologyEither_of_right : ∀ (α : Type u_6) (β : Type u_7) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [SecondCountableTopology β],
  SecondCountableTopologyEither α β
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} {l : B ⟶ X}
  {fac_left :
    autoParam (CategoryTheory.CategoryStruct.comp i l = f) CategoryTheory.CommSq.LiftStruct.fac_left._autoParam}
  {fac_right :
    autoParam (CategoryTheory.CategoryStruct.comp l p = g) CategoryTheory.CommSq.LiftStruct.fac_right._autoParam}
  {l_1 : B ⟶ X}
  {fac_left_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i l_1 = f) CategoryTheory.CommSq.LiftStruct.fac_left._autoParam}
  {fac_right_1 :
    autoParam (CategoryTheory.CategoryStruct.comp l_1 p = g) CategoryTheory.CommSq.LiftStruct.fac_right._autoParam},
  { l := l, fac_left := fac_left, fac_right := fac_right } =
      { l := l_1, fac_left := fac_left_1, fac_right := fac_right_1 } →
    l = l_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_of_contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.ExtTreeMap.map f t).contains k = true → t.contains k = true
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The truth morphism of the subobject classifier  -/
CategoryTheory.Subobject.Classifier.truth : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (self : CategoryTheory.Subobject.Classifier C) → self.Ω₀ ⟶ self.Ω
-- Std.Data.HashSet.Basic
Std.HashSet.instUnion : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Union (Std.HashSet α)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- `Integrable f μ` means that `f` is measurable and that the integral `∫⁻ a, ‖f a‖ ∂μ` is finite.
`Integrable f` means `Integrable f volume`.  -/
MeasureTheory.Integrable : {ε : Type u_5} →
  [inst : TopologicalSpace ε] →
    [ContinuousENorm ε] →
      {α : Type u_8} →
        {x : MeasurableSpace α} → (α → ε) → autoParam (MeasureTheory.Measure α) MeasureTheory.Integrable._auto_1 → Prop
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.instDecidableRelSameCycle : {α : Type u_2} → [DecidableEq α] → [Fintype α] → (f : Equiv.Perm α) → DecidableRel f.SameCycle
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.instHasZeroMorphisms : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.ShortComplex C)
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Push.of_reverse : ∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} (σ : V → V') [inst_1 : Quiver.HasInvolutiveReverse V] (X Y : V)
  (f : X ⟶ Y), Quiver.reverse ((Quiver.Push.of σ).map f) = (Quiver.Push.of σ).map (Quiver.reverse f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β}
  {h : k' ∈ Std.DHashMap.Const.alter m k f},
  (Std.DHashMap.Const.alter m k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Data.Finset.Sym
/-- **Alias** of the reverse direction of `Finset.sym2_nonempty`. -/
Finset.Nonempty.sym2 : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s.sym2.Nonempty
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.comp_apply : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {A : Type u_4} [inst_3 : AddMonoid A] [inst_4 : DistribMulAction M A] {B : Type u_5}
  [inst_5 : AddMonoid B] [inst_6 : DistribMulAction N B] {C : Type u_7} [inst_7 : AddMonoid C]
  [inst_8 : DistribMulAction P C] (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [inst_9 : φ.CompTriple ψ χ] (x : A),
  (g.comp f) x = g (f x)
-- Mathlib.Tactic.FieldSimp
/-- `field_simp` normalizes expressions in (semi-)fields (i.e., does not require additive inverses)
by rewriting them to a common denominator, i.e. to reduce them to expressions of the form `n / d`
where neither `n` nor `d` contains any division symbol. The `field_simp` tactic will also clear
denominators in field *(in)equalities*, by cross-multiplying.

A very common pattern is `field_simp; ring` (clear denominators, then the resulting goal is
solvable by the axioms of a commutative ring). The finishing tactic `field` is a shorthand for this
pattern.

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging
fails. These denominators are made out of denominators appearing in the input expression,
by repeatedly taking products or divisors. The default discharger can be non-universal, i.e. can be
specific to the field at hand (order properties, explicit `≠ 0` hypotheses, `CharZero` if that is
known, etc). See `field_simp_discharge` for full details of the default discharger algorithm.

* `field_simp at l1 l2 ...` can be used to normalize at the given locations.
* `field_simp (disch := tac)` uses the tactic sequence `tac` to discharge nonzeroness/positivity
  proofs.
* `field_simp [t₁, ..., tₙ]` provides terms `t₁`, ..., `tₙ` to the discharger for
  nonzeroness/positivity proofs.

Examples:
```
-- `x / (1 - y) / (1 + y / (1 - y))` is reduced to `x / (1 - y + y)`
example (x y z : ℚ) (hy : 1 - y ≠ 0) :
    ⌊x / (1 - y) / (1 + y / (1 - y))⌋ < 3 := by
  field_simp
  -- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
  sorry

-- `field_simp` will clear the `x` denominators in the following equation
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  field_simp
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
  sorry
```
 -/
Mathlib.Tactic.FieldSimp.fieldSimp : Lean.ParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forM_eq_forM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}}, forM t f = t.toList.forM f
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.ext_iff : ∀ {ι : Type u_1} {x y : ComplexShape ι}, x = y ↔ x.Rel = y.Rel
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).right.left.as = PUnit.unit
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.drop_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {Y X :
    CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C)
      (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))}
  (f : Y ⟶ X), CategoryTheory.CosimplicialObject.Augmented.drop.map f = f.right
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.consRecOn_cons : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  {motive : HNNExtension.NormalWord d → Sort u_4} (g : G) (u : ℤˣ) (w : HNNExtension.NormalWord d)
  (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u')
  (ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g))
  (cons :
    (g : G) →
      (u : ℤˣ) →
        (w : HNNExtension.NormalWord d) →
          (h1 : w.head ∈ d.set u) →
            (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
              motive w → motive (HNNExtension.NormalWord.cons g u w h1 h2)),
  HNNExtension.NormalWord.consRecOn (HNNExtension.NormalWord.cons g u w h1 h2) ofGroup cons =
    cons g u w h1 h2 (HNNExtension.NormalWord.consRecOn w ofGroup cons)
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrange_eq_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), MonoidHom.mrange f = Submonoid.map f ⊤
-- Lean.Compiler.LCNF.Basic
/-- Low-level update `FunDecl` function. It does not update the local context.
Consider using `FunDecl.update : LetDecl → Expr → Array Param → Code → CompilerM FunDecl` if you want the local context
to be updated.
 -/
Lean.Compiler.LCNF.FunDecl.updateCore : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.FunDecl pu →
    Lean.Expr → Array (Lean.Compiler.LCNF.Param pu) → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.FunDecl pu
-- Mathlib.LinearAlgebra.SesquilinearForm.Star
LinearMap.isPosSemidef_iff_posSemidef_toMatrix : ∀ {M : Type u_2} {n : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {R : Type u_4}
  [inst_3 : CommRing R] [inst_4 : StarRing R] [inst_5 : PartialOrder R] [inst_6 : Module R M] {B : M →ₗ⋆[R] M →ₗ[R] R}
  (b : Module.Basis n R M), B.IsPosSemidef ↔ ((LinearMap.toMatrix₂ b b) B).PosSemidef
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- A morphism in `SimplexCategory` with domain `⦋0⦌`, `⦋1⦌`, or `⦋2⦌` defines an object in the
comma category `StructuredArrow (op ⦋n⦌) (Truncated.inclusion (n := 2)).op`.  -/
SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ : {i n : ℕ} →
  ({ len := i } ⟶ { len := n }) →
    autoParam (i ≤ 2) SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂._auto_1 →
      CategoryTheory.StructuredArrow (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_le_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), ↑N ≤ ↑N' ↔ N ≤ N'
-- Init.Data.String.Search
String.posOfAux : String → Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Data.PNat.Basic
PNat.recOn_one : ∀ {p : ℕ+ → Sort u_1} (one : p 1) (succ : (n : ℕ+) → p n → p (n + 1)), PNat.recOn 1 one succ = one
-- Init.Prelude
/-- Implementation of `getMethods`.  -/
Lean.Macro.getMethodsImp : Lean.MacroM Lean.Macro.Methods
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.nsmul_neg : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] {n : ℕ} {x : M}, 0 < n → x < 0 → n • x < 0
-- Mathlib.Data.Tree.Basic
BinaryTree.comp_map : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β) (g : β → γ) (t : BinaryTree α),
  BinaryTree.map (g ∘ f) t = BinaryTree.map g (BinaryTree.map f t)
-- Mathlib.Data.Matrix.Basic
Matrix.transposeAddEquiv_apply : ∀ (m : Type u_2) (n : Type u_3) (α : Type u_11) [inst : Add α] (M : Matrix m n α),
  (Matrix.transposeAddEquiv m n α) M = M.transpose
-- Init.Data.Array.Zip
Array.getElem?_zipWith_eq_some : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β} {z : γ} {i : ℕ},
  (Array.zipWith f as bs)[i]? = some z ↔ ∃ x y, as[i]? = some x ∧ bs[i]? = some y ∧ f x y = z
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `x` is a letter and `w` is a word such that `x + w` reduces to the empty word, then `w`
reduces to `-x`.  -/
FreeAddGroup.Red.cons_nil_iff_singleton : ∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool},
  FreeAddGroup.Red ((x, b) :: L) [] ↔ FreeAddGroup.Red L [(x, !b)]
-- Plausible.Testable
_private.Plausible.Testable.0.Plausible.instEvalExprConfiguration : Lean.Elab.ConfigEval.EvalExpr Plausible.Configuration
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → s ∈ nhds x → HasFDerivAt f f' x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.homEquiv_naturality_left_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf}
  (hcM' : CategoryTheory.Limits.IsColimit cM') {N : ModuleCat ↑cR.pt} (f : M ⟶ M')
  (g : M' ⟶ (PresheafOfModules.constFunctor cR).obj N),
  (PresheafOfModules.ModuleColimit.homEquiv hcR hcM).symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (PresheafOfModules.ModuleColimit.map hcR hcM hcM' f))
      ((PresheafOfModules.ModuleColimit.homEquiv hcR hcM').symm g)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If a point is in the affine span of a set, adding it to that set does not change the affine
span.  -/
affineSpan_insert_eq_affineSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p : P} {ps : Set P}, p ∈ affineSpan k ps → affineSpan k (insert p ps) = affineSpan k ps
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₂ → Std.DHashMap.Const.getD (m₁.union m₂) k fallback = Std.DHashMap.Const.getD m₁ k fallback