mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Defs
/-- Left-biased version of `List.map₂`. `map₂Left' f as bs` applies `f` to each
pair of elements `aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, `f` is
applied to `none` for the remaining `aᵢ`. Returns the results of the `f`
applications and the remaining `bs`.

```
map₂Left' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])

map₂Left' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
```
 -/
List.map₂Left' : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → List γ × List β
-- Lean.Meta.Tactic.Grind.Action
/-- Helper action that checks whether the resulting tactic script produced by its continuation
can close the original goal.
If `warnOnly = true`, just generates a warning message instead of an error
 -/
Lean.Meta.Grind.Action.checkTactic : Bool → Lean.Meta.Grind.Action
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_add : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ ν : MeasureTheory.Measure (α × β)}, (μ + ν).fst = μ.fst + ν.fst
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
CategoryTheory.CommGrpObj.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {X : C} →
          [toGrpObj : CategoryTheory.GrpObj X] →
            [toIsCommMonObj : CategoryTheory.IsCommMonObj X] → CategoryTheory.CommGrpObj X
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects colimits of shape `Jᵒᵖ`, then `F : C ⥤ Dᵒᵖ` reflects limits
of shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F.leftOp], CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.mul_le_of_le_mul_inv : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < c → a ≤ b * c⁻¹ → a * c ≤ b
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂IsoClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₂], P.isoClosure.IsTriangulatedClosed₂
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_mono_set : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A B : Set X} {ε : NNReal},
  A ⊆ B → Metric.externalCoveringNumber ε A ≤ Metric.externalCoveringNumber ε B
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
differentiable_sigmoid : Differentiable ℝ Real.sigmoid
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.augmentOfIsTerminal_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T) (x : SimplexCategoryᵒᵖ),
  (X.augmentOfIsTerminal hT).hom.app x = hT.from (X.obj x)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.mk : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} →
        {r : I₁ × I₂ × I₃ → J} →
          (I₁₂ : Type u_11) →
            (p : I₁ × I₂ → I₁₂) →
              (q : I₁₂ × I₃ → J) →
                (∀ (i : I₁ × I₂ × I₃), q (p (i.1, i.2.1), i.2.2) = r i) →
                  CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r
-- Mathlib.Computability.PartrecCode
/-- Helper lemma for the evaluation of `prec` in the recursive case.  -/
Nat.Partrec.Code.eval_prec_succ : ∀ (cf cg : Nat.Partrec.Code) (a k : ℕ),
  (cf.prec cg).eval (Nat.pair a k.succ) = do
    let ih ← (cf.prec cg).eval (Nat.pair a k)
    cg.eval (Nat.pair a (Nat.pair k ih))
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₂.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f''),
  Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 =
    ⟨0,
      ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P Homotopy.mkInductiveAux₂._proof_1).hom zero,
        ⋯⟩⟩
-- Mathlib.Algebra.Group.End
AddAut.add_apply : ∀ (M : Type u_2) [inst : Add M] (e₁ e₂ : AddAut M) (m : M), (e₁ + e₂) m = e₁ (e₂ m)
-- Init.Data.List.Erase
List.getLast_erase_mem : ∀ {α : Type u_1} [inst : BEq α] (xs : List α) (a : α) (h : xs.erase a ≠ []), (xs.erase a).getLast h ∈ xs
-- Mathlib.Data.List.MinMax
List.argmin_concat : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] (f : α → β) (a : α) (l : List α),
  List.argmin f (l ++ [a]) = Option.casesOn (List.argmin f l) (some a) fun c => if f a < f c then some a else some c
-- Lean.Level
Lean.LMVarIdMap : Type → Type
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.star_mem_nonZeroDivisors : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {z : QuadraticAlgebra R a b},
  z ∈ nonZeroDivisors (QuadraticAlgebra R a b) → star z ∈ nonZeroDivisors (QuadraticAlgebra R a b)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_lt_twoPow_of_le : ∀ {m n : ℕ}, m ≤ n → ∀ {x : BitVec m}, x.toNat < 2 ^ n
-- Lean.Elab.DefView
Lean.Elab.BodyProcessedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (state : Lean.Elab.Term.SavedState) (value : Lean.Expr)
  (moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) (toSnapshot_1 : Lean.Language.Snapshot)
  (state_1 : Lean.Elab.Term.SavedState) (value_1 : Lean.Expr)
  (moreSnaps_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  ({ toSnapshot := toSnapshot, state := state, value := value, moreSnaps := moreSnaps } =
      { toSnapshot := toSnapshot_1, state := state_1, value := value_1, moreSnaps := moreSnaps_1 }) =
    (toSnapshot = toSnapshot_1 ∧ state = state_1 ∧ value = value_1 ∧ moreSnaps = moreSnaps_1)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- A class registering that either `α` is countable or `β` is a countably generated
measurable space.  -/
MeasurableSpace.CountableOrCountablyGenerated : Type u_5 → (β : Type u_6) → [MeasurableSpace β] → Prop
-- Init.Data.SInt.Lemmas
Int32.le_toInt : ∀ (x : Int32), -2 ^ 31 ≤ x.toInt
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are subalgebras in a domain `S` over `R`, and if they are
linearly disjoint, then `A ⊗[R] B` is also a domain.  -/
Subalgebra.LinearDisjoint.isDomain : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S}, A.LinearDisjoint B → ∀ [IsDomain S], IsDomain (TensorProduct R ↥A ↥B)
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.iIndepFun.integral_prod_eq_prod_integral : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3}
  [inst_1 : Fintype ι] {X : ι → Ω → 𝕜},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (X i) μ) → ∫ (x : Ω), (∏ i, X i) x ∂μ = ∏ i, ∫ (x : Ω), X i x ∂μ
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.forM.eq_1 : ∀ {α : Type u} {β : α → Type v} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → m PUnit.{w + 1})
  (b : Std.DHashMap.Raw α β), Std.DHashMap.Raw.forM f b = Array.forM (Std.DHashMap.Internal.AssocList.forM f) b.buckets
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.projection_equiv_zero : ∀ {K : Type u_1} {V : Type u_2} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T : Submodule K V} [IsNoetherian K ↥S] (hST : IsCompl S T), S.projection T hST ≈ 0
-- Mathlib.Analysis.BoundedVariation
/-- A real Lipschitz function into a finite-dimensional real vector space is differentiable
almost everywhere. For the general Rademacher theorem assuming
that the source space is finite dimensional, see `LipschitzWith.ae_differentiableAt`.  -/
LipschitzWith.ae_differentiableAt_real : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal}
  {f : ℝ → V}, LipschitzWith C f → ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ),
  HasSumLocallyUniformly (fun l z => if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) (L.derivWeierstrassPExcept l₀)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k k' : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueD k' (Std.Internal.List.Const.modifyKey k f l) fallback =
      if (k == k') = true then (Option.map f (Std.Internal.List.getValue? k l)).getD fallback
      else Std.Internal.List.getValueD k' l fallback
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- If `M ≤ N` are submonoids of `R`, then the natural map `M⁻¹S →+* N⁻¹S` commutes with the
localization maps  -/
IsLocalization.localization_isScalarTower_of_submonoid_le : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (M N : Submonoid R) (h : M ≤ N) [inst_5 : IsLocalization M S]
  [inst_6 : IsLocalization N T], IsScalarTower R S T
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_one : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R), Polynomial.dickson k a 1 = Polynomial.X
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f g : CategoryTheory.Subobject A), CategoryTheory.IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- The homset equivalence which helps show that `L` is a left adjoint.  -/
CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv : {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] →
            {U : CategoryTheory.Functor A B} →
              {F : CategoryTheory.Functor B A} →
                (L : CategoryTheory.Functor C B) →
                  (U' : CategoryTheory.Functor A C) →
                    (adj₁ : F ⊣ U) →
                      (adj₂ : L.comp F ⊣ U') →
                        [inst_3 : CategoryTheory.Limits.HasCoreflexiveEqualizers C] →
                          ((X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) →
                            (Y : C) →
                              (X : B) →
                                (Y ⟶ CategoryTheory.LiftRightAdjoint.constructRightAdjointObj L U' adj₁ adj₂ X) ≃
                                  (L.obj Y ⟶ X)
-- Mathlib.FieldTheory.SeparableDegree
/-- If `K / E / F` is an extension tower such that `E / F` is separable,
`x : K` is separable over `E`, then it's also separable over `F`.  -/
IsSeparable.of_algebra_isSeparable_of_isSeparable : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] {x : K},
  IsSeparable E x → IsSeparable F x
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.Const.eq_of_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : LawfulBEq α] [inst_1 : BEq β] [LawfulBEq β]
  (m₁ m₂ : Std.ExtDHashMap α fun x => β), Std.ExtDHashMap.Const.beq m₁ m₂ = true → m₁ = m₂
-- Mathlib.Data.Finset.Sups
Finset.sups_eq_self : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s : Finset α}, s ⊻ s = s ↔ SupClosed ↑s
-- Mathlib.Algebra.Module.Defs
/-- A variant of `Module.ext` that's convenient for term-mode.  -/
Module.ext' : ∀ {R : Type u_5} [inst : Semiring R] {M : Type u_6} [inst_1 : AddCommMonoid M] (P Q : Module R M),
  (∀ (r : R) (m : M), r • m = r • m) → P = Q
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instLinearOrderedAddCommGroupWithTop : {R : Type u_1} →
  [inst : LinearOrder R] →
    [inst_1 : Field R] → [inst_2 : IsOrderedRing R] → LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.eq_of_mul_eq_zero : ∀ {m n : ℕ}, m.Coprime n → m * n = 0 → m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.mul_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β]
  [ContinuousMul β],
  Asymptotics.SuperpolynomialDecay l k f → ∀ (c : β), Asymptotics.SuperpolynomialDecay l k fun n => f n * c
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_mul_mk'_eq_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x y : ↥M),
  IsLocalization.mk' S (↑x) y * IsLocalization.mk' S (↑y) x = 1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.sup_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousSup β] (f g : CompactlySupportedContinuousMap α β) (a : α),
  (f ⊔ g) a = f a ⊔ g a
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.smul_iSup : ∀ {α : Type u_1} {R : Type u_3} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] {ι : Sort u_4}
  (f : ι → MeasureTheory.OuterMeasure α) (c : R), c • ⨆ i, f i = ⨆ i, c • f i
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.w' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y Z : C} {f : X ⟶ Z} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z)
  [inst_2 : F.Full] [F.Faithful],
  CategoryTheory.CategoryStruct.comp (hf.fst' (F.map g)) f = CategoryTheory.CategoryStruct.comp (hf.snd (F.map g)) g
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.esymm_mul_psum_to_weight : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] (k : ℕ),
  ∑ a ∈ Finset.HasAntidiagonal.antidiagonal k with a.1 < k,
      (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2 =
    ∑ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k with t.1.card < k, MvPolynomial.NewtonIdentities.weight✝ σ R k t
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addSemigroup : {α : Type u} → [Semigroup α] → AddSemigroup (Additive α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.keys → k ∈ t
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.eq_def : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn assignments cOpt =
    match cOpt with
    | none => assignments
    | some c =>
      match c.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment
      | some (l, false) => assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point}
  [inst_1 : SizeOf C] (hom : Φ₂.fiber ⟶ Φ₁.fiber), sizeOf { hom := hom } = 1 + sizeOf hom
-- Init.Data.BitVec.Lemmas
BitVec.replicate.eq_def : ∀ {w : ℕ} (x : ℕ) (x_1 : BitVec w),
  BitVec.replicate x x_1 =
    match x, x_1 with
    | 0, x => 0#0
    | n.succ, x => BitVec.cast ⋯ (x ++ BitVec.replicate n x)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_sUnion : ∀ {x y : ZFSet.{u}}, y ∈ x.sUnion ↔ ∃ z ∈ x, y ∈ z
-- Mathlib.Data.List.AList
_private.Mathlib.Data.List.AList.0.AList.insertRec.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : AList β → Sort u_3) →
      (x : AList β) →
        ((nodupKeys : [].NodupKeys) → motive { entries := [], nodupKeys := nodupKeys }) →
          ((c : Sigma β) →
              (l : List (Sigma β)) → (h : (c :: l).NodupKeys) → motive { entries := c :: l, nodupKeys := h }) →
            motive x
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".
 -/
CategoryTheory.Mon : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → Type (max u₁ v₁)
-- Mathlib.Analysis.Convex.Slope
/-- If `f : 𝕜 → 𝕜` is concave, then for any three points `x < y < z` the slope of the secant line of
`f` on `[x, y]` is greater than the slope of the secant line of `f` on `[y, z]`.  -/
ConcaveOn.slope_anti_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConcaveOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
-- Lean.Elab.Term.TermElabM
/-- Snapshot for incremental processing of current tactic, if any.

Invariant: if the bundle's `old?` is set, then the state *up to the start* of the tactic is
unchanged, i.e. reuse is possible.
 -/
Lean.Elab.Term.Context.tacSnap? : Lean.Elab.Term.Context → Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)
-- Mathlib.Analysis.Convex.Combination
/-- Two simplices glue nicely if the union of their vertices is affine independent.  -/
AffineIndependent.convexHull_inter : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {s t₁ t₂ : Finset E},
  AffineIndependent R Subtype.val →
    t₁ ⊆ s → t₂ ⊆ s → (convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.freeReflMap_naturality : ∀ {V : Type u_3} {W : Type u_4} [inst : CategoryTheory.ReflQuiver V] [inst_1 : CategoryTheory.ReflQuiver W]
  (F : V ⥤rq W),
  (CategoryTheory.Cat.FreeRefl.quotientFunctor V).comp (CategoryTheory.Cat.freeReflMap F) =
    (CategoryTheory.Cat.freeMap F.toPrefunctor).comp (CategoryTheory.Cat.FreeRefl.quotientFunctor W)
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- The `SmallCategoryOfSet` structure induced by a
`CoreSmallCategoryOfSet` structure.  -/
CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      CategoryTheory.CoreSmallCategoryOfSet Ω C → CategoryTheory.SmallCategoryOfSet Ω
-- Mathlib.GroupTheory.Divisible
AddCommGroup.smul_top_eq_top_of_divisibleBy_int : ∀ (A : Type u_1) [inst : AddCommGroup A] [DivisibleBy A ℤ] {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
-- Mathlib.CategoryTheory.Elementwise
CategoryTheory.Iso.hom_inv_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier X),
  (CategoryTheory.ConcreteCategory.hom self.inv) ((CategoryTheory.ConcreteCategory.hom self.hom) x) = x
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : AddMonoid.Coprod M N),
  AddMonoid.Coprod.snd ((AddMonoid.Coprod.swap M N) x) = AddMonoid.Coprod.fst x
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- This instance asserts that if `G` has a right-cancellative multiplication, a linear order, and
multiplication is strictly monotone w.r.t. the second argument, then `G` has `TwoUniqueProds`.  -/
TwoUniqueProds.of_covariant_right : ∀ {G : Type u} [inst : Mul G] [IsRightCancelMul G] [inst_2 : LinearOrder G] [MulLeftStrictMono G], TwoUniqueProds G
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.mul_def : ∀ {G : Type u_1} [inst : Add G] {a : G} (f g : AddConstMap G G a a), f * g = f.comp g
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: if a function `f` is continuous on a closed set `s` and it is
larger than a value in its image away from compact sets, then it has a minimum on this set.  -/
ContinuousOn.exists_isMinOn' : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] {s : Set β} {f : β → α},
  ContinuousOn f s →
    IsClosed s →
      ∀ {x₀ : β}, x₀ ∈ s → (∀ᶠ (x : β) in Filter.cocompact β ⊓ Filter.principal s, f x₀ ≤ f x) → ∃ x ∈ s, IsMinOn f s x
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.ne_zero_of_degree_gt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : WithBot ℕ}, n < p.degree → p ≠ 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_mapWithPostcondition : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [inst_8 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_10 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_12 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.IterM.mapWithPostcondition f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out).run
      g __do_lift acc
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_add : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f g : ↥(lp E p)),
  ↑(f + g) = ↑f + ↑g
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.NullMeasurableSet t μ → μ s ≠ ⊤ → μ t ≠ ⊤ → |μ.real s - μ.real t| ≤ μ.real (symmDiff s t)
-- Std.Time.Date.Unit.Week
/-- Converts an `Ordinal` to an `Offset`.
 -/
Std.Time.Week.OfYear.Ordinal.toOffset : Std.Time.Week.OfYear.Ordinal → Std.Time.Week.Offset