mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.exists_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0}
  (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ}
  {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0}
  (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)) (n m : ℤ)
  (hnm : autoParam (n + 1 = m) CochainComplex.Lifting.exists_hom._auto_1),
  ∃ φ,
    CategoryTheory.CategoryStruct.comp (π.f n) (CategoryTheory.CategoryStruct.comp φ (ι.f m)) =
      (↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.add k v p with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) =
    h_2 k v p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.keys_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Raw.map f t).keys = t.keys
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.sup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f g : α → β} [inst_1 : Zero β] [inst_2 : SemilatticeSup β] [ContinuousSup β],
  MeasureTheory.AEFinStronglyMeasurable f μ →
    MeasureTheory.AEFinStronglyMeasurable g μ → MeasureTheory.AEFinStronglyMeasurable (f ⊔ g) μ
-- Std.Time.Zoned.Database.TZdb
/-- A timezone ID such as `America/New_York`, looked up in the zoneinfo search paths.
 -/
Std.Time.Database.TZdb.TZSpec.zoneId : String → Std.Time.Database.TZdb.TZSpec
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.isInvertedBy_isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D), (CategoryTheory.MorphismProperty.isomorphisms C).IsInvertedBy F
-- Init.Data.List.Lemmas
List.set_append_right : ∀ {α : Type u_1} {s t : List α} (i : ℕ) (x : α), s.length ≤ i → (s ++ t).set i x = s ++ t.set (i - s.length) x
-- Init.Data.List.Control
List.idRun_findSomeM? : ∀ {α : Type u_1} {β : Type u_2} (f : α → Id (Option β)) (as : List α),
  (List.findSomeM? f as).run = List.findSome? (fun x => (f x).run) as
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_le_size_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.size ≤ (t.insert k v).size
-- Mathlib.Algebra.Group.Units.Hom
Units.map_id : ∀ (M : Type u) [inst : Monoid M], Units.map (MonoidHom.id M) = MonoidHom.id Mˣ
-- Mathlib.Tactic.CategoryTheory.IsoReassoc
/-- Simplify an expression using only the axioms of a groupoid.  -/
Mathlib.Tactic.Reassoc.categoryIsoSimp : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.map_injOn : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'],
  LinearIndepOn R v s → ∀ (f : M →ₗ[R] M'), Set.InjOn ⇑f ↑(Submodule.span R (v '' s)) → LinearIndepOn R (⇑f ∘ v) s
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_eq_Ico_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b = Set.Ico a b ↔ ¬a < b
-- Mathlib.Algebra.Group.EvenFunction
/-- If `f` and `g` are odd, then `f ∘ g` is odd.  -/
Function.Odd.comp_odd : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} [inst_1 : Neg β] [inst_2 : Neg γ] {f : β → γ},
  Function.Odd f → ∀ {g : α → β}, Function.Odd g → Function.Odd (f ∘ g)
-- Mathlib.GroupTheory.Sylow
Sylow.is_maximal' : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (self : Sylow p G) {Q : Subgroup G}, IsPGroup p ↥Q → ↑self ≤ Q → Q = ↑self
-- Mathlib.Order.CountableDenseLinearOrder
/-- Any two countable dense, nonempty linear orders without endpoints are order isomorphic. This is
also known as **Cantor's isomorphism theorem**.  -/
Order.iso_of_countable_dense : ∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrder α] [inst_1 : LinearOrder β] [Countable α] [DenselyOrdered α]
  [NoMinOrder α] [NoMaxOrder α] [Nonempty α] [Countable β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β]
  [Nonempty β], Nonempty (α ≃o β)
-- Mathlib.ModelTheory.Bundled
/-- Maps a bundled model along a bijection.  -/
FirstOrder.Language.Theory.ModelType.equivInduced : {L : FirstOrder.Language} → {T : L.Theory} → {M : T.ModelType} → {N : Type w'} → ↑M ≃ N → T.ModelType
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.subsemigroupMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (M' : AddSubsemigroup M),
  f.subsemigroupMap M' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_add' := ⋯ }
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.trans_apply : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Mul C] [inst_3 : Star A]
  [inst_4 : Star B] [inst_5 : Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) (x : A), (e₁.trans e₂) x = e₂ (e₁ x)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFractionRel.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ : W.RightFraction X Y},
  CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂ → CategoryTheory.MorphismProperty.LeftFractionRel z₁.op z₂.op
-- Mathlib.ModelTheory.LanguageMap
/-- The forward language homomorphism  -/
FirstOrder.Language.LEquiv.toLHom : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L ≃ᴸ L') → (L →ᴸ L')
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- The q-expansion coefficients of the normalised Eisenstein series `E k`: the constant term is
`1` and for `m ≥ 1` the `m`-th coefficient is `-(2k / B_k) * σ_{k-1}(m)` where `B_k` is the
`k`-th Bernoulli number.  -/
EisensteinSeries.E_qExpansion_coeff : ∀ {k : ℕ} (hk : 3 ≤ k),
  Even k →
    ∀ (m : ℕ),
      (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑(ModularForm.E hk)) =
        if m = 0 then 1 else -(2 * ↑k / ↑(bernoulli k)) * ↑((ArithmeticFunction.sigma (k - 1)) m)
-- Lean.Elab.Exception
Lean.Elab.throwUnsupportedSyntax : {m : Type u_1 → Type u_2} → {α : Type u_1} → [MonadExceptOf Lean.Exception m] → m α
-- Init.Data.List.TakeDrop
List.takeWhile_cons : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α},
  List.takeWhile p (a :: l) = if p a = true then a :: List.takeWhile p l else []
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_cons_iff : ∀ {xs : List ℕ} {m n a : ℕ}, (m<...n).toList = a :: xs ↔ m + 1 = a ∧ m + 1 < n ∧ ((m + 1)<...n).toList = xs
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.id_apply : ∀ {R : Type u} [inst : Ring R] (M : ModuleCat R) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.Hom.ext_iff : ∀ {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} {x_1 y_1 : x.Hom y},
  x_1 = y_1 ↔ x_1.fst = y_1.fst ∧ x_1.snd = y_1.snd
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x y : E),
  ‖((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k
-- Init.WFComputable
WellFounded.fixF_eq_fixFC : @WellFounded.fixF = @WellFounded.fixFC
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.comp_map : ∀ {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') (f : M ⟶ M') {M'' : PresheafOfModules R}
  {cM'' : CategoryTheory.Limits.Cocone M''.presheaf} (hcM'' : CategoryTheory.Limits.IsColimit cM'') (g : M' ⟶ M''),
  PresheafOfModules.ModuleColimit.map hcR hcM' hcM'' g ∘ₗ PresheafOfModules.ModuleColimit.map hcR hcM hcM' f =
    PresheafOfModules.ModuleColimit.map hcR hcM hcM'' (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.FieldTheory.CardinalEmb
/-- A basis of E/F indexed by the initial ordinal.  -/
Field.Emb.Cardinal.wellOrderedBasis : (F : Type u) →
  (E : Type v) →
    [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → Module.Basis (Module.rank F E).ord.ToType F E
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_apply_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] (g : E → ℂ) (f : TemperedDistribution E F) (f' : SchwartzMap E ℂ),
  ((TemperedDistribution.smulLeftCLM F g) f) f' = f ((SchwartzMap.smulLeftCLM ℂ g) f')
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.instWeaklyLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [WeaklyLocallyCompactSpace M], WeaklyLocallyCompactSpace Mᵃᵒᵖ
-- Mathlib.Data.Set.Function
Set.mapsTo_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : Set β), Set.MapsTo f ∅ t
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- `CRingHom a` is the constant SkewPolynomial `a`, as a ring homomorphism. This requires
`[MulSemiringAction (Multiplicative ℕ) R]`.  -/
SkewPolynomial.CRingHom : {R : Type u_1} → [inst : Semiring R] → [inst_1 : MulSemiringAction (Multiplicative ℕ) R] → R →+* SkewPolynomial R
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_iterate_pos_iff : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ}, 0 < n → (x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The categorical image of a morphism.  -/
CategoryTheory.Limits.image : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasImage f] → C
-- Mathlib.Topology.Inseparable
SeparationQuotient.isInducing_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsInducing SeparationQuotient.mk
-- Batteries.Classes.Order
/-- `LawfulLECmp cmp` asserts that `(cmp x y).isLE` and `x ≤ y` coincide.  -/
Std.LawfulLECmp : {α : Type u_1} → [LE α] → (α → α → Ordering) → Prop
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.eq : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) (a b : G),
  DoubleCoset.mk H K a = DoubleCoset.mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.cocones_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (X : C), F.cocones.obj X = (F ⟶ (CategoryTheory.Functor.const J).obj X)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.lazy.injEq : ∀ {α β : Type} (a a_1 : β), (Lean.Widget.StrictOrLazy.lazy a = Lean.Widget.StrictOrLazy.lazy a_1) = (a = a_1)
-- Init.Data.Option.Lemmas
Option.isNone_max : ∀ {α : Type u_1} [inst : Max α] {o o' : Option α}, (o ⊔ o').isNone = (o.isNone && o'.isNone)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.propagateDiseqOf.visitRhs : ℕ → Lean.Expr → Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Topology.EMetricSpace.Lipschitz
Set.MapsTo.lipschitzOnWith_iff_restrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β} {t : Set β} (h : Set.MapsTo f s t), LipschitzOnWith K f s ↔ LipschitzWith K (Set.MapsTo.restrict f s t h)
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.mk.inj : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} {inst : NontriviallyNormedField R}
  {inst_1 : (x : B) → AddCommMonoid (E x)} {inst_2 : (x : B) → Module R (E x)} {inst_3 : NormedAddCommGroup F}
  {inst_4 : NormedSpace R F} {inst_5 : TopologicalSpace B} {inst_6 : (x : B) → TopologicalSpace (E x)}
  {pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)}
  {pretrivialization_linear' : ∀ e ∈ pretrivializationAtlas, Bundle.Pretrivialization.IsLinear R e}
  {pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  {mem_base_pretrivializationAt : ∀ (x : B), x ∈ (pretrivializationAt x).baseSet}
  {pretrivialization_mem_atlas : ∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas}
  {exists_coordChange :
    ∀ e ∈ pretrivializationAtlas,
      ∀ e' ∈ pretrivializationAtlas,
        ∃ f,
          ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
            ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2}
  {totalSpaceMk_isInducing : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)}
  {pretrivializationAtlas_1 : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)}
  {pretrivialization_linear'_1 : ∀ e ∈ pretrivializationAtlas_1, Bundle.Pretrivialization.IsLinear R e}
  {pretrivializationAt_1 : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  {mem_base_pretrivializationAt_1 : ∀ (x : B), x ∈ (pretrivializationAt_1 x).baseSet}
  {pretrivialization_mem_atlas_1 : ∀ (x : B), pretrivializationAt_1 x ∈ pretrivializationAtlas_1}
  {exists_coordChange_1 :
    ∀ e ∈ pretrivializationAtlas_1,
      ∀ e' ∈ pretrivializationAtlas_1,
        ∃ f,
          ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
            ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2}
  {totalSpaceMk_isInducing_1 : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt_1 b) ∘ Bundle.TotalSpace.mk b)},
  { pretrivializationAtlas := pretrivializationAtlas, pretrivialization_linear' := pretrivialization_linear',
        pretrivializationAt := pretrivializationAt, mem_base_pretrivializationAt := mem_base_pretrivializationAt,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas, exists_coordChange := exists_coordChange,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing } =
      { pretrivializationAtlas := pretrivializationAtlas_1, pretrivialization_linear' := pretrivialization_linear'_1,
        pretrivializationAt := pretrivializationAt_1, mem_base_pretrivializationAt := mem_base_pretrivializationAt_1,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas_1, exists_coordChange := exists_coordChange_1,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing_1 } →
    pretrivializationAtlas = pretrivializationAtlas_1 ∧ pretrivializationAt = pretrivializationAt_1
-- Mathlib.RingTheory.Perfection
PreTilt.eq_1 : ∀ (O : Type u₂) [inst : CommRing O] (p : ℕ), PreTilt O p = Perfection (ModP O p) p
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.loop.eq_2 : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u} (f : (i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯)
  (m : ℕ) (h : m.succ ≤ n) (a : α (n - m.succ) ⋯),
  Nat.dfold.loop✝ n f m.succ h a = Nat.dfold.loop✝ n f m ⋯ (Nat.dfoldCast✝ α ⋯ (f (n - m.succ) ⋯ a))
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.immediate.injEq : ∀ (names names_1 : Array Lean.Name),
  (Aesop.Frontend.BuilderOption.immediate names = Aesop.Frontend.BuilderOption.immediate names_1) = (names = names_1)
-- Mathlib.Order.Filter.Extr
IsExtrOn.comp_mapsTo : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set δ} {g : δ → α}
  {b : δ}, IsExtrOn f s a → Set.MapsTo g t s → g b = a → IsExtrOn (f ∘ g) t b
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_eq : ∀ {w : ℕ} {x : BitVec w} {n : ℕ} (acc : ℕ), x.cpopNatRec n acc = x.cpopNatRec n 0 + acc
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X Y : P.FullSubcategory),
  (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.snd X.obj Y.obj
-- Std.Http.Protocol.H1
/-- Suppresses writing body bytes for the current outgoing message while keeping
header generation active. Used for responses that must not carry payload bytes.
 -/
Std.Http.Protocol.H1.Machine.suppressOutgoingBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → optParam Bool false → Std.Http.Protocol.H1.Machine dir
-- Init.Data.Array.Range
Array.snd_lt_add_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {k : ℕ} {xs : Array α}, x ∈ xs.zipIdx k → x.2 < k + xs.size
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.ι_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.ι.app CategoryTheory.Limits.WalkingSpan.left = c.inl
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instFunLike : {G : Type u_1} →
  {H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → FunLike (AddConstMap G H a b) G H
-- Std.Data.DTreeMap.Internal.WF.Defs
_private.Std.Data.DTreeMap.Internal.WF.Defs.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (b : β k) (h_1 : Unit → motive none)
  (h_2 : (b : β k) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Data.Sum.Basic
PSum.inl_injective : ∀ {α : Sort u_3} {β : Sort u_4}, Function.Injective PSum.inl
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.abs_sin_sub_sin_le : ∀ (x y : ℝ), |Real.sin x - Real.sin y| ≤ |x - y|
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Lemmas.0.Array.insertIdx!.eq_1 : ∀ {α : Type u} (as : Array α) (i : ℕ) (a : α),
  as.insertIdx! i a =
    if h : i ≤ as.size then as.insertIdx i a h
    else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.insertIdx!" 1924 7 "invalid index"
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Iic : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x : (i : ι) → α i),
  (Set.univ.pi fun i => Set.Iic (x i)) = Set.Iic x
-- Std.Data.ExtDHashMap.Basic
/-- Equivalent to (but potentially faster than) calling `Const.get?` followed by `insertIfNew`.

Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.
 -/
Std.ExtDHashMap.Const.getThenInsertIfNew? : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} →
        [EquivBEq α] →
          [LawfulHashable α] → (Std.ExtDHashMap α fun x => β) → α → β → Option β × Std.ExtDHashMap α fun x => β
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.mk.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (binderName : Lean.Name)
  (params : Array (Lean.Compiler.LCNF.Param pu)) (type : Lean.Expr) (value : Lean.Compiler.LCNF.Code pu),
  sizeOf (Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value) =
    1 + sizeOf fvarId + sizeOf binderName + sizeOf params + sizeOf type + sizeOf value
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLTD_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : α × β},
          Std.DTreeMap.Internal.Impl.Const.getEntryLTD k t₁ fallback =
            Std.DTreeMap.Internal.Impl.Const.getEntryLTD k t₂ fallback
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` and `N` are isomorphic as monoid objects, then `X ⟶ M` and `X ⟶ N` are isomorphic
monoids.  -/
CategoryTheory.Hom.mulEquivCongrRight : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M N : C} →
        [inst_2 : CategoryTheory.MonObj M] →
          [inst_3 : CategoryTheory.MonObj N] →
            (e : M ≅ N) → [CategoryTheory.IsMonHom e.hom] → (X : C) → (X ⟶ M) ≃* (X ⟶ N)
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- If `Subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`.  -/
Module.subsingletonEquiv : (R : Type u_4) →
  (M : Type u_5) →
    (ι : Type u_6) →
      [inst : Semiring R] → [Subsingleton R] → [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → M ≃ₗ[R] ι →₀ R
-- Mathlib.Combinatorics.HalesJewett
/-- A point in `ι → α` and a line in `ι' → α` determine a line in `ι ⊕ ι' → α`.  -/
Combinatorics.Line.vertical : {α : Type u_5} → {ι : Type u_6} → {ι' : Type u_7} → (ι → α) → Combinatorics.Line α ι' → Combinatorics.Line α (ι ⊕ ι')
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a}, m.WF → (Std.DHashMap.Raw.map f m).size = m.size
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers_isMulCommutative : ∀ {G : Type u_1} [inst : Group G] (g : G), IsMulCommutative ↥(Subgroup.zpowers g)
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Polynomial.degreeLTEquiv.eq_1 : ∀ (R : Type u) [inst : Semiring R] (n : ℕ),
  Polynomial.degreeLTEquiv R n =
    { toFun := fun p n_1 => (↑p).coeff ↑n_1, map_add' := ⋯, map_smul' := ⋯,
      invFun := fun f => ⟨∑ i, (Polynomial.monomial ↑i) (f i), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {s : Set M} {f : M → M'} {g : M → M''}, MDiff[s] f → MDiff[s] g → MDiff[s] fun x => (f x, g x)