mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.mk.injEq : ∀ {G : Type u_1} [inst : Group G] (toSubgroup : Subgroup G)
  (isNormal' : autoParam toSubgroup.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam)
  (isFiniteIndex' : autoParam toSubgroup.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam)
  (toSubgroup_1 : Subgroup G)
  (isNormal'_1 : autoParam toSubgroup_1.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam)
  (isFiniteIndex'_1 : autoParam toSubgroup_1.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam),
  ({ toSubgroup := toSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' } =
      { toSubgroup := toSubgroup_1, isNormal' := isNormal'_1, isFiniteIndex' := isFiniteIndex'_1 }) =
    (toSubgroup = toSubgroup_1)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso_hom_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.RightLift f g} (P : s.IsKan) (Q : t.IsKan), (P.uniqueUpToIso Q).hom.left = Q.desc s
-- Init.Data.UInt.Lemmas
USize.toBitVec_div : ∀ {a b : USize}, (a / b).toBitVec = a.toBitVec / b.toBitVec
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C],
  CategoryTheory.Limits.HasImages C
-- Mathlib.Data.Sym.Sym2
Sym2.Mem.other'.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] {a a_1 : α} (e_a : a = a_1) {z z_1 : Sym2 α} (e_z : z = z_1) (h : a ∈ z),
  Sym2.Mem.other' h = Sym2.Mem.other' ⋯
-- Mathlib.CategoryTheory.Opposites
/-- The natural isomorphism between opposite functors `G.op ≅ F.op` induced by a natural
isomorphism between the original functors `F ≅ G`.  -/
CategoryTheory.NatIso.op : {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.op ≅ F.op)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.size = t.size ↔
    ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), (f a (t.get a h)).isSome = true
-- Init.Core
inline.eq_1 : ∀ {α : Sort u} (a : α), inline a = a
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- An effective presentation of an object `X` with respect to a functor `F` is the data of an effective
epimorphism of the form `F.obj p ⟶ X`.
 -/
CategoryTheory.Functor.EffectivePresentation : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → D → Type (max u_1 v_2)
-- Init.Grind.AC
Lean.Grind.AC.Expr.brecOn.eq : ∀ {motive : Lean.Grind.AC.Expr → Sort u} (t : Lean.Grind.AC.Expr)
  (F_1 : (t : Lean.Grind.AC.Expr) → Lean.Grind.AC.Expr.below t → motive t),
  Lean.Grind.AC.Expr.brecOn t F_1 = F_1 t (Lean.Grind.AC.Expr.brecOn.go t F_1).2
-- Init.Meta.Defs
Lean.Syntax.decodeStrLitAux : String → String.Pos.Raw → String → Option String
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasFDerivAt_exp_smul_const_of_mem_ball' : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂]
  [inst_2 : NormedCommRing 𝕊] [inst_3 : NormedRing 𝔸] [inst_4 : NormedSpace 𝕂 𝕊] [inst_5 : NormedAlgebra 𝕂 𝔸]
  [inst_6 : Algebra 𝕊 𝔸] [inst_7 : ContinuousSMul 𝕊 𝔸] [inst_8 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasFDerivAt (fun u => NormedSpace.exp (u • x))
      ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp (t • x))) t
-- Init.Data.Range.Polymorphic.PRange
/-- A downward-unbounded range of elements of `α` with a closed upper bound.

`*...=b` is the range of all values less than or equal to `b : α`.
This is notation for `Ric.mk b`.
 -/
Std.Ric : Type u → Type u
-- Mathlib.Data.Finset.Card
/-- If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole.

See also `Set.exists_ne_map_eq_of_encard_lt_of_maps_to` and
`Set.exists_ne_map_eq_of_ncard_lt_of_maps_to`.  -/
Finset.exists_ne_map_eq_of_card_lt_of_maps_to : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β},
  t.card < s.card → ∀ {f : α → β}, Set.MapsTo f ↑s ↑t → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
-- Mathlib.Algebra.Homology.Homotopy
prevD_eq_zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (i : ι),
  ¬c.Rel (c.prev i) i → (prevD i) f = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- A 2-truncated simplicial set `S` has an underlying refl quiver with `S _⦋0⦌₂` as its underlying
type.  -/
SSet.OneTruncation₂ : SSet.Truncated 2 → Type u_1
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- `curry'` and `uncurry'` are inverse bijections.  -/
CategoryTheory.MonoidalClosed.uncurry'_curry' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] (f : X ⟶ Y),
  CategoryTheory.MonoidalClosed.uncurry' (CategoryTheory.MonoidalClosed.curry' f) = f
-- Batteries.Data.MLList.Basic
MLList.instEmptyCollection : {m : Type u_1 → Type u_1} → {α : Type u_1} → EmptyCollection (MLList m α)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.toInteger_isPrimitiveRoot : ∀ {K : Type u} [inst : Field K] {ζ : K} {k : ℕ} [inst_1 : NeZero k] (hζ : IsPrimitiveRoot ζ k),
  IsPrimitiveRoot hζ.toInteger k
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.normalizer.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (S : Set G),
  AddSubgroup.normalizer S =
    { carrier := {g | ∀ (n : G), n ∈ S ↔ g + n + -g ∈ S}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Eta-expanded form of `MeasureTheory.VectorMeasure.Integrable.sub` -/
MeasureTheory.VectorMeasure.Integrable.fun_sub : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → μ.Integrable g → μ.Integrable fun i => f i - g i
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_insertMany!_list : ∀ {α : Type u} {β : Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α] {l : List (α × β)}
  {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).toListModel.Perm
      (Std.Internal.List.insertListConst t.toListModel l)
-- Mathlib.Tactic.NormNum.Result
/-- A shortcut (non)instance for `AddMonoidWithOne α` from `Ring α` to shrink generated proofs.  -/
Mathlib.Meta.NormNum.instAddMonoidWithOne : {α : Type u} → [Ring α] → AddMonoidWithOne α
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_le_div : ∀ {n : ℕ}, 0 < n → ¬Nat.Prime n → n.minFac ≤ n / n.minFac
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.Hom.mk.inj : ∀ {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}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} {fst : x.fst ⟶ y.fst} {snd : x.snd ⟶ y.snd}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map fst) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map snd))
      CategoryTheory.Limits.CategoricalPullback.Hom.w._autoParam}
  {fst_1 : x.fst ⟶ y.fst} {snd_1 : x.snd ⟶ y.snd}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map fst_1) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map snd_1))
      CategoryTheory.Limits.CategoricalPullback.Hom.w._autoParam},
  { fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 } → fst = fst_1 ∧ snd = snd_1
-- Init.NotationExtra
unexpandMkArray2 : Lean.PrettyPrinter.Unexpander
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
/-- Close the goal of the form `η.hom = θ.hom`, where `η` and `θ` are 2-isomorphisms made up only of
associators, unitors, and identities.
```lean
example {B : Type} [Bicategory B] {a : B} :
  (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom := by
  bicategory_coherence
```
 -/
Mathlib.Tactic.Bicategory.pureCoherence : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_right_le_size_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₂.size ≤ (m₁.union! m₂).size
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.ext_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A},
  S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinCLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂} {f : ContDiffMapSupportedIn E F₁ n K},
  (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ) f =
    if MeasureTheory.IntegrableOn φ (↑K) μ then ∫ (x : E), (B (f x)) (φ x) ∂μ else 0
-- Mathlib.Data.Fintype.Option
instFiniteOption : ∀ {α : Type u_3} [Finite α], Finite (Option α)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_filterMap : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m] [LawfulMonad n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Std.IterM m β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b =>
          match f b with
          | some c => g d c
          | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.filterMap f it) ⦃Q⦄
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.fixingAddSubgroupInsertEquiv.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (a : α)
  (s : Set ↥(SubAddAction.ofStabilizer M a)),
  SubAddAction.fixingAddSubgroupInsertEquiv a s =
    { toFun := fun m => ⟨⟨↑m, ⋯⟩, ⋯⟩, invFun := fun m => ⟨↑↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Lean.Meta.Tactic.Grind.Proof
Lean.Meta.Grind.mkEqCongrSymmProof : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Guessing rule for the `bound` tactic: when trying to prove `x ^ y ≤ x ^ z`, we can either assume
`1 ≤ x` or `0 < x ≤ 1`.  -/
Real.rpow_le_rpow_of_exponent_le_or_ge : ∀ {x y z : ℝ}, 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y → x ^ y ≤ x ^ z
-- Mathlib.Algebra.Algebra.Tower
/-- Any `f : A ≃ₐ[R] B` is also an `S`-algebra isomorphism if the `R`-algebra structure on
`A` and `B` factors via a surjective ring homomorphism `R →+* S`.  -/
AlgEquiv.extendScalarsOfSurjective : {R : Type u} →
  {S : Type v} →
    {A : Type w} →
      {B : Type u₁} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Algebra S A] →
                    [inst_6 : Algebra S B] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [IsScalarTower R S A] →
                            [IsScalarTower R S B] → Function.Surjective ⇑(algebraMap R S) → (A ≃ₐ[R] B) ≃ A ≃ₐ[S] B
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
/-- Given `t : TStructure C` and a preadditive category `H`, this typeclass
contains the data of a fully faithful additive functor `H ⥤ C` which identifies
`H` to the full subcategory of `C` consisting of the objects satisfying
the property `t.heart`.  -/
CategoryTheory.Triangulated.TStructure.Heart : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} 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] →
              CategoryTheory.Triangulated.TStructure C →
                (H : Type u') →
                  [inst : CategoryTheory.Category.{v', u'} H] →
                    [CategoryTheory.Preadditive H] → Type (max (max (max u u') v) v')
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.isUniformEmbedding_coeFn : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)), IsUniformEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- A morphism property is multiplicative if it contains identities and is stable by
composition.  -/
CategoryTheory.MorphismProperty.IsMultiplicative : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_diff!_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁.diff! m₂).isEmpty = true
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instNonUnitalSeminormedCommRing : {α : Type u_2} → [NonUnitalSeminormedCommRing α] → NonUnitalSeminormedCommRing αᵐᵒᵖ
-- Batteries.Data.MLList.Basic
/-- Folds a binary function across a monadic lazy list, from an initial starting value.
This will run forever if the list is infinite.  -/
MLList.fold : {m : Type u_1 → Type u_1} → {β α : Type u_1} → [Monad m] → (β → α → β) → β → MLList m α → m β
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centerCongr_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : Type u_1} [inst_1 : NonUnitalNonAssocRing S] (e : R ≃+* S)
  (r : ↥(Subsemigroup.center R)), ↑((NonUnitalSubring.centerCongr e) r) = e ↑r
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instCoeAddSubgroup.eq_1 : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  ClosedAddSubgroup.instCoeAddSubgroup G = { coe := ClosedAddSubgroup.toAddSubgroup }
-- Mathlib.Data.List.AList
AList.extract.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
  AList.extract a s =
    match List.kextract a s.entries, ⋯ with
    | (b, l), h => (b, { entries := l, nodupKeys := h })
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- The ball package made of unit balls.  -/
Besicovitch.unitBallPackage : (α : Type u_1) → Besicovitch.BallPackage α α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.keys_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keys = t₂.keys
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.neg_iso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (e : X ≅ Y), (-e).inv = -e.inv
-- Batteries.Data.List.Basic
List.zipWithLeft.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List α) (x_1 : List β),
  List.zipWithLeft f x x_1 =
    match x, x_1 with
    | [], x => []
    | a :: as, [] => List.map (fun a => f a none) (a :: as)
    | a :: as, b :: bs => f a (some b) :: List.zipWithLeft f as bs
-- Init.Prelude
/-- The identity function. `id` takes an implicit argument `α : Sort u`
(a type in any universe), and an argument `a : α`, and returns `a`.

Although this may look like a useless function, one application of the identity
function is to explicitly put a type on an expression. If `e` has type `T`,
and `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and Lean
knows that this expression has type `T'` rather than `T`. This can make a
difference for typeclass inference, since `T` and `T'` may have different
typeclass instances on them. `show T' from e` is sugar for an `@id T' e`
expression.
 -/
id : {α : Sort u} → α → α
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a co-Heyting algebra
with possibly different definitional equalities.  -/
CoheytingAlgebra.copy : {α : Type u} →
  (c : CoheytingAlgebra α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (sdiff : α → α → α) →
                          sdiff = SDiff.sdiff → (hnot : α → α) → hnot = HNot.hnot → CoheytingAlgebra α
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {x y : S₁.HomotopyEquiv S₂},
  x = y ↔
    x.hom = y.hom ∧ x.inv = y.inv ∧ x.homotopyHomInvId ≍ y.homotopyHomInvId ∧ x.homotopyInvHomId ≍ y.homotopyInvHomId
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLE_symm_mk : ∀ {R : Type u} [inst : CommRing R] {I J : Ideal R} (x : R) (h : I ≤ J),
  (DoubleQuot.quotQuotEquivQuotOfLE h).symm ((Ideal.Quotient.mk J) x) = (DoubleQuot.quotQuotMk I J) x
-- Mathlib.Order.Interval.Set.Image
MonotoneOn.mapsTo_Iic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  MonotoneOn f (Set.Iic b) → Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If `f` is a monomorphism, the pushforward-pullback adjunction on sieves is coreflective.  -/
CategoryTheory.Sieve.galoisCoinsertionOfMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : Y ⟶ X) →
        [CategoryTheory.Mono f] →
          GaloisCoinsertion (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
-- Mathlib.Topology.CompactOpen
/-- The compact-open topology on the space of continuous maps `C(X, Y)`.  -/
ContinuousMap.compactOpen : {X : Type u_2} → {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → TopologicalSpace C(X, Y)
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_sq_add_sin_sq : ∀ (x : ℝ), Real.cos x ^ 2 + Real.sin x ^ 2 = 1
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.instHasRightResolutionsIdOfContainsIdentities : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁}
  [W₁.ContainsIdentities], (CategoryTheory.LocalizerMorphism.id W₁).HasRightResolutions
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.Spec.birdDet.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (A_2 : Matrix (Fin 0) (Fin 0) R), BirdDet.Spec.birdDet A_2 = 1
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.ofUniqueLift.eq_1 : ∀ {G : Type u} [inst : Group G] (X : Type u) (of : X → G)
  (h : ∀ {H : Type u} [inst_1 : Group H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a),
  FreeGroupBasis.ofUniqueLift X of h =
    FreeGroupBasis.ofLift X of
      (fun {H} [Group H] =>
        { toFun := fun f => Classical.choose ⋯, invFun := fun F => ⇑F ∘ of, left_inv := ⋯, right_inv := ⋯ })
      ⋯
-- Aesop.BaseM
/-- Stats collected during an Aesop call.  -/
Aesop.BaseM.State.stats : Aesop.BaseM.State → Aesop.Stats
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.cofibrations_over_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.cofibrations (CategoryTheory.Over S) = (HomotopicalAlgebra.cofibrations C).over
-- Batteries.Data.MLList.Basic
/-- Try to deconstruct a `MLList`, returning an optional pair `α × MLList m α`
representing the head and tail of the list if it is already evaluated, and `none` otherwise.  -/
MLList.uncons? : {m : Type u → Type u} → {α : Type u} → MLList m α → Option (Option (α × MLList m α))
-- Aesop.Rule.Forward
/-- A forward rule.  -/
Aesop.ForwardRule : Type
-- Mathlib.Order.KrullDimension
Order.krullDim_nonpos_iff_forall_isMax : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubDuration : HSub Std.Time.WallTime Std.Time.Duration Std.Time.WallTime
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ShiftTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α]
  (vec : aig.RefVec w) (distance : ℕ), sizeOf { vec := vec, distance := distance } = 1 + sizeOf vec + sizeOf distance
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- Over a ring `R` of characteristic zero, `fun n => cyclotomic n R` is injective.  -/
Polynomial.cyclotomic_injective : ∀ {R : Type u_1} [inst : CommRing R] [CharZero R], Function.Injective fun n => Polynomial.cyclotomic n R
-- Mathlib.Data.Finset.Basic
List.toFinset_union : ∀ {α : Type u_1} [inst : DecidableEq α] (l l' : List α), (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ}, (Std.HashSet.emptyWithCapacity c).contains a = false
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.trans : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
  f =Θ[l] g → g =Θ[l] k → f =Θ[l] k
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.instCoeSortType : CoeSort Bipointed (Type u_1)
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  [inst_1 : SizeOf C] {k k' : ℕ} (hk : k < n) (hk' : k' < n) (a : (X k hk).fst) (a_1 : (X k' hk').fst),
  sizeOf (CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max✝ hk hk' a a_1) =
    1 + sizeOf k + sizeOf k' + sizeOf hk + sizeOf hk' + sizeOf a + sizeOf a_1