mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.of.eq_1 : ∀ (R : Type u) {X : Type v} [inst : CommRing R] (x : X),
  FreeLieAlgebra.of R x = Quot.mk (FreeLieAlgebra.Rel R X) (FreeNonUnitalNonAssocAlgebra.of R x)
-- Mathlib.Analysis.Seminorm
Seminorm.norm_sub_map_le_sub : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (x y : E), ‖p x - p y‖ ≤ p (x - y)
-- Mathlib.Data.Vector.Basic
List.Vector.get_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (v : List.Vector α n) (f : α → β) (i : Fin n),
  (List.Vector.map f v).get i = f (v.get i)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If `f` is multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate. Here, we give an auxiliary statement tailored for an inductive proof. Use instead
`map_sum_finset`.  -/
MultilinearMap.map_sum_finset_aux : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ι → Type u_1} (g : (i : ι) → α i → M₁ i)
  (A : (i : ι) → Finset (α i)) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] {n : ℕ},
  ∑ i, (A i).card = n → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ Fintype.piFinset A, f fun i => g i (r i)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsThetaTVS.symm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F},
  f =Θ[𝕜; l] g → g =Θ[𝕜; l] f
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- The span of all coefficients of `subProdXSubC f` as `f` ranges all polynomials in `k[X]`.  -/
AlgebraicClosure.spanCoeffs : (k : Type u) → [inst : Field k] → Ideal (MvPolynomial (AlgebraicClosure.Vars k) k)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_edgeSet : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet], Fintype.card ↑G.edgeSet = G.edgeFinset.card
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_lt_nsmul : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : PartialOrder R] [AddLeftStrictMono R] [Archimedean R] {a : R},
  0 < a → ∀ (b : R), ∃ n, b < n • a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.mergeSort_eq_mergeSortTR₂ : @List.mergeSort = @List.MergeSort.Internal.mergeSortTR₂
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x` has left cancellative
addition if `β` has left cancellative addition.  -/
FunLike.isLeftCancelAdd : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsLeftCancelAdd β] [IsAddApply F α β], IsLeftCancelAdd F
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ β) (h1 : Measurable ⇑e)
  (h2 : Measurable ⇑e.symm),
  { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm =
    { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedAltLHS.default : Lean.Meta.Match.AltLHS
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldRev.match_1.splitter : (motive :
    (n : ℕ) →
      {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldRev._auto_1 → Type u_1} →
        ((i : ℕ) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) → α n ⋯ → Sort u_2) →
  (n : ℕ) →
    {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldRev._auto_1 → Type u_1} →
      (f : (i : ℕ) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) →
        (init : α n ⋯) →
          ((α : (i : ℕ) → autoParam (i ≤ 0) Nat.dfoldRev._auto_1 → Type u_1) →
              (f : (i : ℕ) → (h : i < 0) → α (i + 1) ⋯ → α i ⋯) → (init : α 0 ⋯) → motive 0 f init) →
            ((n : ℕ) →
                (α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfoldRev._auto_1 → Type u_1) →
                  (f : (i : ℕ) → (h : i < n + 1) → α (i + 1) ⋯ → α i ⋯) → (init : α (n + 1) ⋯) → motive n.succ f init) →
              motive n f init
-- Mathlib.Algebra.Order.ZeroLEOne
/-- **Alias** of `zero_lt_one`.

---

See `zero_lt_one'` for a version with the type explicit.  -/
one_pos : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1], 0 < 1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Creates an E-matching theorem for a theorem with proof `proof`, `numParams` parameters, and the given set of patterns.
Pattern variables are represented using de Bruijn indices.
 -/
Lean.Meta.Grind.mkEMatchTheoremCore : Lean.Meta.Grind.Origin →
  Array Lean.Name →
    ℕ →
      Lean.Expr →
        List Lean.Expr →
          Lean.Meta.Grind.EMatchTheoremKind →
            optParam (List Lean.Meta.Grind.EMatchTheoremConstraint) [] →
              optParam Bool false → optParam Bool false → Lean.MetaM Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Algebra.Order.SuccPred
Order.IsPredPrelimit.lt_sub_natCast : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : AddCommGroupWithOne α] [PredSubOrder α],
  Order.IsPredPrelimit x → x < y → ∀ (n : ℕ), x < y - ↑n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)},
  m.WF → (k' ∈ m.alter k f ↔ if (k == k') = true then (f (m.get? k)).isSome = true else k' ∈ m)
-- Mathlib.Data.ZMod.QuotientGroup
/-- **Alias** of the reverse direction of `finite_zpowers`. -/
IsOfFinOrder.finite_zpowers : ∀ {α : Type u_3} [inst : Group α] {a : α}, IsOfFinOrder a → (↑(Subgroup.zpowers a)).Finite
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collectUsedPriorities : Lean.Meta.Grind.SymbolPriorities → Array Lean.Expr → Array ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_emod_self_left : ∀ (a b c : ℤ), (a * b - c) % a = -c % a
-- Mathlib.Combinatorics.Matroid.Sum
/-- The sum of an indexed collection of matroids, as a matroid on the sigma-type.  -/
Matroid.sigma : {ι : Type u_1} → {α : ι → Type u_2} → ((i : ι) → Matroid (α i)) → Matroid ((i : ι) × α i)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s₁ s₂ : Set α} {t : Set β}, (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
/-- The `R`-algebra homomorphism from $R[x_1,\dots,x_n]$ to the symmetric subalgebra of
$R[\{x_i \mid i ∈ σ\}]$ sending $x_i$ to the $i$-th elementary symmetric polynomial.  -/
MvPolynomial.esymmAlgHom : (σ : Type u_1) →
  (R : Type u_3) →
    (n : ℕ) →
      [inst : CommSemiring R] → [Fintype σ] → MvPolynomial (Fin n) R →ₐ[R] ↥(MvPolynomial.symmetricSubalgebra σ R)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_insert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ {a : α} {b : β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.insert a b)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.Data.Set.Card
Set.injOn_of_ncard_image_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β},
  (f '' s).ncard = s.ncard → autoParam s.Finite Set.injOn_of_ncard_image_eq._auto_1 → Set.InjOn f s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k : α} {v : β k}, (m.insert k v).getKey k ⋯ = k
-- Init.Data.String.Substring
/-- Folds a function over a substring from the left, accumulating a value starting with `init`. The
accumulated value is combined with each character in order, using `f`.
 -/
Substring.Raw.foldl : {α : Type u} → (α → Char → α) → α → Substring.Raw → α
-- Mathlib.GroupTheory.Index
Subgroup.finite_iff_finite_and_finiteIndex : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Finite G ↔ Finite ↥H ∧ H.FiniteIndex
-- Mathlib.Topology.Connected.Clopen
/-- A `PreconnectedSpace` version of `isPreconnected_of_forall_constant`  -/
preconnectedSpace_of_forall_constant : ∀ {α : Type u} [inst : TopologicalSpace α],
  (∀ (f : α → Bool), Continuous f → ∀ (x y : α), f x = f y) → PreconnectedSpace α
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.zero_eq_lift_iff : ∀ {a : Cardinal.{u}}, 0 = Cardinal.lift.{v, u} a ↔ 0 = a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      (List.map Prod.fst l).contains k = false → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.mk.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W}
  (toCommaMorphism toCommaMorphism_1 : CategoryTheory.CommaMorphism X.toComma Y.toComma)
  (e_toCommaMorphism : toCommaMorphism = toCommaMorphism_1) (prop_hom_left : Q toCommaMorphism.left)
  (prop_hom_right : W toCommaMorphism.right),
  { toCommaMorphism := toCommaMorphism, prop_hom_left := prop_hom_left, prop_hom_right := prop_hom_right } =
    { toCommaMorphism := toCommaMorphism_1, prop_hom_left := ⋯, prop_hom_right := ⋯ }
-- Mathlib.Order.Basic
/-- An order is dense if there is an element between any pair of distinct elements.  -/
DenselyOrdered.dense : ∀ {α : Type u_5} {inst : LT α} [self : DenselyOrdered α] (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2}
  [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C]
  (F : (i : α) → CategoryTheory.Functor (I i) C) [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasColimit (F i)]
  [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)] (k : (i : α) → I i) (s : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pointwiseProduct F) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)
        (CategoryTheory.Limits.Pi.π (fun s => CategoryTheory.Limits.colimit (F s)) s)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π ((CategoryTheory.Functor.pi F).obj k) s)
      (CategoryTheory.Limits.colimit.ι (F s) (k s))
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X_1 : K),
  (CategoryTheory.Limits.colimCompFlipIsoWhiskerColim.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X_1)).inv
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X.flip X_1).inv
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom ⋯
-- Mathlib.GroupTheory.GroupAction.Hom
instFunLikeMulActionHom : {M : Type u_2} →
  {N : Type u_3} →
    (φ : M → N) → (X : Type u_5) → [inst : SMul M X] → (Y : Type u_6) → [inst_1 : SMul N Y] → FunLike (X →ₑ[φ] Y) X Y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMon_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X Y : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N]
  (α : CategoryTheory.yonedaMonObj M ⟶ CategoryTheory.yonedaMonObj N) (f : X ⟶ Y) (g : Y ⟶ M) {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)
-- Mathlib.Topology.Sheaves.Skyscraper
germ_skyscraperPresheafStalkOfSpecializes_hom_assoc : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y) (U : TopologicalSpace.Opens ↑X) (hU : y ∈ U)
  {Z : C} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((skyscraperPresheaf p₀ A).germ U y hU)
      (CategoryTheory.CategoryStruct.comp (skyscraperPresheafStalkOfSpecializes p₀ A h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
not_isAddCyclic_prod_of_infinite_nontrivial : ∀ (M : Type u_4) (N : Type u_5) [inst : AddGroup M] [inst_1 : AddGroup N] [Infinite M] [Nontrivial N],
  ¬IsAddCyclic (M × N)
-- Init.Data.List.ToArray
List.finIdxOf?_toArray : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), l.toArray.finIdxOf? a = List.finIdxOf? a l
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {x : α}, x ∉ l → l.formPerm x = x
-- Mathlib.Order.Circular
btw_refl_left : ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), btw a a b
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.thm.inj : ∀ {a a_1 : Lean.Meta.SimpTheorem}, Lean.Meta.SimpEntry.thm a = Lean.Meta.SimpEntry.thm a_1 → a = a_1
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.upperHalfPlane_inter_integerComplement : {z | 0 < z.im} ∩ Complex.integerComplement = {z | 0 < z.im}
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.HashMap.ofList l).getD k' fallback = v
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax'_mapId_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] (a : B),
  ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapId a).inv = F.mapId a
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.F_nat_zero_zero_sub_le : ∀ {t : ℝ}, 0 < t → ‖HurwitzKernelBounds.F_nat 0 0 t - 1‖ ≤ Real.exp (-Real.pi * t) / (1 - Real.exp (-Real.pi * t))
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRat : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.assignments.size = n →
    ∀ (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
      (f.insertRatUnits units).1.clearRatUnits = f
-- Mathlib.Probability.Martingale.Convergence
/-- Part c of the **L¹ martingale convergence theorem**: Given an integrable function `g` which
is measurable with respect to `⨆ n, ℱ n` where `ℱ` is a filtration, the martingale defined by
`𝔼[g | ℱ n]` converges in L¹ to `g`.

This martingale also converges to `g` almost everywhere and this result is provided by
`MeasureTheory.Integrable.tendsto_ae_condExp`  -/
MeasureTheory.Integrable.tendsto_eLpNorm_condExp : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] {g : Ω → ℝ},
  MeasureTheory.Integrable g μ →
    MeasureTheory.StronglyMeasurable g →
      Filter.Tendsto (fun n => MeasureTheory.eLpNorm (μ[g | ↑ℱ n] - g) 1 μ) Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.ccos : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ}, Measurable f → Measurable fun x => Complex.cos (f x)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instIsVeryGoodSymmOfRespectsIsoFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [(HomotopicalAlgebra.fibrations C).RespectsIso] [inst_5 : CategoryTheory.Limits.HasBinaryProducts C] [P.IsVeryGood],
  P.symm.IsVeryGood
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_prod_nonempty_of_submultiplicative : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β), (∀ (a b : α), f (a * b) ≤ f a * f b) → ∀ (l : List α), l ≠ ∅ → f l.prod ≤ (List.map f l).prod
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.coe_copy : ∀ {M : Type u_4} {N : Type u_5} {x : MulOne M} {x_1 : MulOne N} (f : M →* N) (f' : M → N) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_FirstNonzeroIsNeg : ∀ {li : Tactic.ComputeAsymptotics.UnitMonomial}, li.FirstNonzeroIsPos → ¬li.FirstNonzeroIsNeg
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowingε₀_two : ONote.fastGrowingε₀ 2 = 2048
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_Prop : ∀ {M : Type u_4} [inst : CommMonoid M] (f : Prop → M), ∏ p, f p = f True * f False
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [hY : QuasiSeparatedSpace ↥Y] [AlgebraicGeometry.QuasiSeparated f],
  QuasiSeparatedSpace ↥X
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.closedCell_subset_skeleton`. -/
Topology.CWComplex.closedCell_subset_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
-- Mathlib.Data.NNReal.Defs
NNReal.mk_natCast : ∀ (n : ℕ), NNReal.mk ↑n ⋯ = ↑n
-- Mathlib.Tactic.NormNum.Prime
/-- Produce a proof that `n` is not prime from a factor `1 < d < n`. `en` should be the expression
that is the natural number literal `n`.  -/
Mathlib.Meta.NormNum.deriveNotPrime : ℕ → ℕ → (en : Q(ℕ)) → Q(¬Nat.Prime «$en»)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.eta_fin_three : ∀ {α : Type u} (A : Matrix (Fin 3) (Fin 3) α), A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2]
-- Mathlib.Order.Interval.Set.Fin
Fin.range_val : ∀ {n : ℕ}, Set.range Fin.val = Set.Iio n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_inter_le_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∩ t₂).size ≤ t₁.size
-- Lean.Meta.DiscrTree.Main
/-- Return true iff the argument should be treated as a "wildcard" by the discrimination tree.

- We ignore proofs because of proof irrelevance. It doesn't make sense to try to
  index their structure.

- We ignore instance implicit arguments (e.g., `[Add α]`) because they are "morally" canonical.
  Moreover, we may have many definitionally equal terms floating around.
  Example: `Ring.hasAdd Int Int.isRing` and `Int.hasAdd`.

- We considered ignoring implicit arguments (e.g., `{α : Type}`) since users don't "see" them,
  and may not even understand why some simplification rule is not firing.
  However, in type class resolution, we have instance such as `Decidable (@Eq Nat x y)`,
  where `Nat` is an implicit argument. Thus, we would add the path
  ```
  Decidable -> Eq -> * -> * -> * -> [Nat.decEq]
  ```
  to the discrimination tree IF we ignored the implicit `Nat` argument.
  This would be BAD since **ALL** decidable equality instances would be in the same path.
  So, we index implicit arguments if they are types.
  This setting seems sensible for simplification theorems such as:
  ```
  forall (x y : Unit), (@Eq Unit x y) = true
  ```
  If we ignore the implicit argument `Unit`, the `DiscrTree` will say it is a candidate
  simplification theorem for any equality in our goal.

Remark: if users have problems with the solution above, we may provide a `noIndexing` annotation,
and `ignoreArg` would return true for any term of the form `noIndexing t`.
 -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.ignoreArg : Lean.Expr → ℕ → Array Lean.Meta.ParamInfo → Lean.MetaM Bool
-- Std.Time.Date.Unit.Month
/-- Transforms `Month.Ordinal` into `Hour.Offset`.
 -/
Std.Time.Month.Ordinal.toHours : Bool → Std.Time.Month.Ordinal → Std.Time.Hour.Offset
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.homMk_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A B : CategoryTheory.Pretriangulated.Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂)
  (hom₃ : A.obj₃ ⟶ B.obj₃)
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
        CategoryTheory.CategoryStruct.comp hom₃ B.mor₃)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_5),
  (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₃ = hom₃
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₂.coe_mk : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : G × G → ↑A)
  (hf : f ∈ groupCohomology.coboundaries₂ A), ⇑⟨f, hf⟩ = f
-- Std.Time.DateTime.Timestamp
/-- Calculates the duration from the given `Timestamp` to the current time.
 -/
Std.Time.Timestamp.since : Std.Time.Timestamp → IO Std.Time.Duration
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_zpow : ∀ (x : ENNReal) (n : ℤ), x⁻¹ ^ n = (x ^ n)⁻¹