mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteLatticeIntervals
/-- Complete lattice structure on `Set.Icc`  -/
Set.Icc.completeLattice : {α : Type u_2} → [inst : ConditionallyCompleteLattice α] → {a b : α} → [Fact (a ≤ b)] → CompleteLattice ↑(Set.Icc a b)
-- Init.Data.Array.Lemmas
Array.findSome?_toList : ∀ {α : Type u_1} {β : Type u_2} {p : α → Option β} {xs : Array α}, List.findSome? p xs.toList = Array.findSome? p xs
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsRestriction.loopless : ∀ {α : Type u_1} {M N : Matroid α} [M.Loopless], N.IsRestriction M → N.Loopless
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.id.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift : Mathlib.Tactic.BicategoryLike.IsoLift) (f : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.id e isoLift f) = 1 + sizeOf e + sizeOf isoLift + sizeOf f
-- Mathlib.Topology.Algebra.Indicator
continuous_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : One β], (∀ a ∈ frontier s, f a = 1) → ContinuousOn f (closure s) → Continuous (s.mulIndicator f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_alter_of_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ (f (t.get? k)).isSome = true)
-- Mathlib.Tactic.Measurability
/-- The `measurability` attribute used to tag measurability statements for the `measurability` tactic.

Note that `measurability` uses `fun_prop` for solving measurability of functions, so statements
about `Measurable`, `AEMeasurable`, `StronglyMeasurable` and `AEStronglyMeasurable` should be tagged
with `fun_prop` rather that `measurability`. The `measurability` attribute is equivalent to
`fun_prop` in these cases for backward compatibility with the earlier implementation.
 -/
measurability : Lean.ParserDescr
-- Mathlib.Order.Hom.WithTopBot
/-- Embedding into `WithBot α`.  -/
Function.Embedding.coeWithBot : {α : Type u_1} → α ↪ WithBot α
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the formal power series `X` is `1`.  -/
PowerSeries.order_X : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], PowerSeries.X.order = 1
-- Init.Data.Int.Order
Int.mul_lt_mul : ∀ {a b c d : ℤ}, a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.openCell_subset_of_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∈ E.I n → Topology.RelCWComplex.openCell n i ⊆ ↑E
-- Mathlib.CategoryTheory.Subobject.Basic
/-- This states that `pullbackπ f y` indeed forms a pullback square (see `Subobject.pullbackπ`).  -/
CategoryTheory.Subobject.isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y) (y : CategoryTheory.Subobject Y),
  CategoryTheory.IsPullback (CategoryTheory.Subobject.pullbackπ f y) ((CategoryTheory.Subobject.pullback f).obj y).arrow
    y.arrow f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictDerivAt.csin : ∀ {f : ℂ → ℂ} {f' x : ℂ},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') x
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.completeLattice : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] →
                {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → CompleteLattice (HomogeneousIdeal 𝒜)
-- Init.Data.Iterators.Basic
/-- Every iterator with state `α` in monad `m` has exactly one plausible step.
 -/
Std.LawfulDeterministicIterator.isPlausibleStep_eq_eq : ∀ {β α : Type w} {m : Type w → Type w'} {inst : Std.Iterator α m β} [self : Std.LawfulDeterministicIterator α m]
  (it : Std.IterM m β), ∃ step, it.IsPlausibleStep = fun x => x = step
-- Init.Data.Bool
Bool.eq_iff_iff : ∀ {a b : Bool}, a = b ↔ (a = true ↔ b = true)
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for completely multiplicative functions.

If `f : ℕ →*₀ F`, where `F` is a complete normed field and `‖f ·‖` is summable, then
`∏' p : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n`.  -/
EulerProduct.eulerProduct_completely_multiplicative_tprod : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →*₀ F},
  (Summable fun x => ‖f x‖) → ∏' (p : Nat.Primes), (1 - f ↑p)⁻¹ = ∑' (n : ℕ), f n
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instHashablePoly_lean : Hashable Int.Internal.Linear.Poly
-- Mathlib.Topology.Algebra.ConstMulAction
IsOpen.smul₀ : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α}, IsOpen s → c ≠ 0 → IsOpen (c • s)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.subset_adjoin_of_subset_right : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) {T : Set E},
  T ⊆ S → T ⊆ ↑(IntermediateField.adjoin F S)
-- Mathlib.Dynamics.Transitive
IsOpen.dense_iUnion_preimage_vadd : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [h : AddAction.IsTopologicallyTransitive M α] {U : Set α},
  IsOpen U → U.Nonempty → Dense (⋃ m, (fun x => m +ᵥ x) ⁻¹' U)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Constant size closed neighborhoods of the diagonal form a basis
of the uniformity filter.  -/
Metric.uniformity_basis_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun x => 0 < x) fun ε => {p | dist p.1 p.2 ≤ ε}
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.ι_mapBifunctorDesc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] {A : D} {j : J}
  (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)) (i₁ : I₁) (i₂ : I₂)
  (h : c₁.π c₂ c (i₁, i₂) = j),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (HomologicalComplex.mapBifunctorDesc f) =
    f i₁ i₂ h
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.instMul : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Mul ↑(Set.Ioo 0 1)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Quotient.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂),
  CategoryTheory.Quotient.lift r F H = CategoryTheory.Quotient.lift r F_1 ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- The first part of the factorization of an immersion `f : X ⟶ Y` to a closed immersion
`f.liftCoborder : X ⟶ f.coborderRange` and a dominant open immersion `f.coborderRange.ι`.
 -/
AlgebraicGeometry.Scheme.Hom.liftCoborder : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → [inst : AlgebraicGeometry.IsImmersion f] → X ⟶ ↑(AlgebraicGeometry.Scheme.Hom.coborderRange f)
-- Init.Omega.Constraint
/-- Multiply by `-1` if the leading coefficient is negative, otherwise return `none`.  -/
Lean.Omega.positivize? : Lean.Omega.Constraint × Lean.Omega.Coeffs → Option (Lean.Omega.Constraint × Lean.Omega.Coeffs)
-- Mathlib.Analysis.Convex.Between
Sbtw.not_swap_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y z : P},
  Sbtw R x y z → ¬Wbtw R x z y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_none : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, a ∉ t → t.get? a = none
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {ι : Type u_6} [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {M : Matrix ι ι R₁} (b : Module.Basis ι R₁ M₁),
  (Matrix.toBilin' M).Nondegenerate ↔ ((Matrix.toBilin b) M).Nondegenerate
-- Batteries.Lean.Expr
/-- Turns an expression that is a constructor of `Int` applied to a natural number literal
into an integer.  -/
Lean.Expr.intLit! : Lean.Expr → ℤ
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- A subgroup `K` includes `closure k` if and only if it includes `k`.  -/
Subgroup.closure_le : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {k : Set G}, Subgroup.closure k ≤ K ↔ k ⊆ ↑K
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_map_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c}
  (f : X ⟶ Y), ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).map f).right = f.left.right
-- Init.Data.String.Basic
String.Pos.isUTF8FirstByte_byte : ∀ {s : String} {pos : s.Pos} {h : pos ≠ s.endPos}, (pos.byte h).IsUTF8FirstByte
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_compLeft`. -/
BilinForm.toMatrix_compLeft : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁),
  (LinearMap.BilinForm.toMatrix b) (B.compLeft f) =
    ((LinearMap.toMatrix b b) f).transpose * (LinearMap.BilinForm.toMatrix b) B
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.α_ofIterM : ∀ {m : Type u_1 → Type u_2} {β α : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β},
  (Std.BundledIterM.ofIterM it).α = α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂)[k]? = t₂[k]?
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_inter' : ∀ {𝕜 : 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'] {f : M → M'} {x : M} {s t : Set M},
  t ∈ nhdsWithin x s → (MDiffAt[s ∩ t] f x ↔ MDiffAt[s] f x)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instSubtractionCommMonoid : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → SubtractionCommMonoid (E →ₛₗ.[σ] F)
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply : ∀ (R : Type u_5) [inst : Semiring R] {η : Type u_7} [inst_1 : Fintype η] {M : Type u_9} {ιs : η → Type u_10}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (f : (j : η) → ιs j →₀ M) (ji : (j : η) × ιs j),
  ((Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f) ji = (f ji.fst) ji.snd
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.volume_fundamentalDomain : ∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] (b : Module.Basis ι ℝ (ι → ℝ)),
  MeasureTheory.volume (ZSpan.fundamentalDomain b) = ENNReal.ofReal |(Matrix.of ⇑b).det|
-- Mathlib.Analysis.Analytic.IsolatedZeros
AnalyticOnNhd.eqOn_or_eventually_ne_of_preconnected : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜},
  AnalyticOnNhd 𝕜 f U →
    AnalyticOnNhd 𝕜 g U → IsPreconnected U → Set.EqOn f g U ∨ ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ g x
-- Aesop.Util.Basic
Aesop.SimpTheorems.simpEntries : Lean.Meta.SimpTheorems → Array Lean.Meta.SimpEntry
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_eq_self_iff_neg_le : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Submodule R M},
  -S = S ↔ -S ≤ S
-- Mathlib.Topology.Instances.Nat
Nat.instMetricSpace : MetricSpace ℕ
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the full range.
 -/
Std.Rii.size : {α : Type u} → Std.Rii α → [Std.PRange.Least? α] → [Std.Rxi.HasSize α] → ℕ
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_list_prod : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (L : List (Polynomial R)),
  0 ∉ L → L.prod.roots = (↑L).bind Polynomial.roots
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyLE_of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (p q : ℤ), p ≤ q → ∀ [K.IsStrictlyLE p], K.IsStrictlyLE q
-- Init.Data.UInt.Bitwise
instAssociativeUInt16HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- The quotient map from finite elements on the field to the associated residue field.  -/
ArchimedeanClass.FiniteResidueField.mk : {K : Type u_1} →
  [inst : LinearOrder K] →
    [inst_1 : Field K] →
      [inst_2 : IsOrderedRing K] → ArchimedeanClass.FiniteElement K →+*o ArchimedeanClass.FiniteResidueField K
-- Mathlib.Combinatorics.Hall.Finite
/-- Second case of the inductive step: assuming that
`∃ (s : Finset ι), s ≠ univ → #s = #(s.biUnion t)`
and that the statement of **Hall's Marriage Theorem** is true for all
`ι'` of cardinality ≤ `n`, then it is true for `ι` of cardinality `n + 1`.
 -/
HallMarriageTheorem.hall_hard_inductive_step_B : ∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] {t : ι → Finset α} [inst_1 : Fintype ι] {n : ℕ},
  Fintype.card ι = n + 1 →
    (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) →
      (∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
          Fintype.card ι' ≤ n →
            (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x) →
        ∀ (s : Finset ι),
          s.Nonempty → s ≠ Finset.univ → s.card = (s.biUnion t).card → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.rec.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β),
  MvQPF.Fix.rec g = Quot.lift (MvQPF.recF g) ⋯
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.eq_zero_of_forall_dual_eq_zero : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] {x : V},
  (∀ (f : StrongDual R V), f x = 0) → x = 0
-- Mathlib.Data.List.Flatten
/-- See also `getLast_getLast_eq_getLast_flatten`, which switches around the proof obligations.  -/
List.getLast_flatten_eq_getLast_getLast : ∀ {α : Type u_1} {l : List (List α)} (hl : l.flatten ≠ []) (hl' : l.getLast ⋯ ≠ []),
  l.flatten.getLast hl = (l.getLast ⋯).getLast hl'
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.List.TProd.mk.match_1.eq_1 : ∀ {ι : Type u_1} (motive : List ι → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (i : ι) → (is : List ι) → motive (i :: is)),
  (match [] with
    | [] => h_1 ()
    | i :: is => h_2 i is) =
    h_1 ()
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.reciprocalFactors.eq_def : ∀ (n : ℕ),
  DihedralGroup.reciprocalFactors n =
    if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else
        if Even n then 3 :: DihedralGroup.reciprocalFactors (n / 2)
        else n % 4 * n :: DihedralGroup.reciprocalFactors (n / 4 + 1)
-- Mathlib.Order.Fin.Tuple
Fin.preimage_insertNth_Icc_of_mem : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i}
  {q₁ q₂ : (j : Fin (n + 1)) → α j},
  x ∈ Set.Icc (q₁ i) (q₂ i) →
    i.insertNth x ⁻¹' Set.Icc q₁ q₂ = Set.Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.lie_toKer_apply : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L) (x : M) (y : E.L),
  ⁅y, ↑(E.toKer x)⁆ = ⁅y, E.incl x⁆
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.neg_toFun : ∀ (E : Type u_6) [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E] (a : E),
  (ContinuousAddMonoidHom.neg E) a = -a
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.mkFreshId : Lean.Meta.AbstractMVars.M Lean.Name
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The underlying modification of lax transformations.  -/
CategoryTheory.Lax.LaxTrans.Hom.as : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Lax.LaxTrans.Hom η θ → CategoryTheory.Lax.LaxTrans.Modification η θ
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The compatibility isomorphisms of the total complex with the shifts
in both variables "commute" only up to a sign `(x * y).negOnePow`.  -/
HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ)
  [inst_2 : K.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)}
  (h :
    (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj
        ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) h) =
    CategoryTheory.CategoryStruct.comp
      ((x * y).negOnePow •
        CategoryTheory.CategoryStruct.comp
          (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).hom.app K)
            (ComplexShape.up ℤ))
          (CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom
            (CategoryTheory.CategoryStruct.comp
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom)
              ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ))))))
      h
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for LMFDB identifiers: it accepts lower case words with `.` in between.
The words can also contain underscores and digits.  -/
Mathlib.CrossRef.lmfdbIdParser : Lean.Parser.Parser
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.instCovariantClassHSMulLe : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R],
  CovariantClass M (Ideal R) HSMul.hSMul LE.le
-- Mathlib.Topology.NhdsSet
IsOpen.mem_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → (s ∈ nhdsSet t ↔ t ⊆ s)
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.implicitFunction_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  φ.implicitFunction = Function.curry ↑(HasStrictFDerivAt.toOpenPartialHomeomorph φ.prodFun ⋯).symm
-- Mathlib.Algebra.Algebra.Operations
Submodule.prod_span_singleton : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {ι : Type u_1}
  (s : Finset ι) (x : ι → A), ∏ i ∈ s, R ∙ x i = R ∙ ∏ i ∈ s, x i
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.intercalateString.eq_1 : ∀ {α β : Type} [inst : Std.Iterator α Id β] [inst_1 : ToString β] (s : String.Slice) (it : Std.Iter β),
  Std.Iter.intercalateString s it =
    (Std.Iter.fold
          (fun x x_1 =>
            match x, x_1 with
            | none, sl => some sl
            | some str, sl => some (str ++ s ++ sl))
          none (Std.Iter.map toString it)).getD
      ""
-- Lean.Data.Lsp.Internal
/-- Converts a set of `DeclarationRanges` to a `DeclInfo`.  -/
Lean.Lsp.DeclInfo.ofDeclarationRanges : Lean.DeclarationRanges → Lean.Lsp.DeclInfo
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.expandNestedActionsAux : Lean.Name → Bool → Bool → Lean.Syntax → StateT (Array Lean.DoElem) Lean.Elab.Do.DoElabM Lean.Syntax
-- Init.Data.String.Basic
/-- Turns a valid position on the string `s` into a valid position on the slice `s.toSlice`.  -/
String.Pos.toSlice : {s : String} → s.Pos → s.toSlice.Pos
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
CategoryTheory.Precoverage.SubsheafClosure.below.amalgamate : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))}
  {motive : (Z : C) → (a : F.obj (Opposite.op Z)) → K.SubsheafClosure 𝒮 Z a → Prop} {Z : C}
  {R : CategoryTheory.Presieve Z} (hR : R ∈ K.coverings Z) {y : CategoryTheory.Presieve.FamilyOfElements F R}
  (hy : y.Compatible) (hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z) (hr : R r), K.SubsheafClosure 𝒮 W (y r hr))
  {t : F.obj (Opposite.op Z)} (ht : y.IsAmalgamation t),
  (∀ ⦃W : C⦄ (r : W ⟶ Z) (hr : R r), CategoryTheory.Precoverage.SubsheafClosure.below ⋯) →
    (∀ ⦃W : C⦄ (r : W ⟶ Z) (hr : R r), motive W (y r hr) ⋯) → CategoryTheory.Precoverage.SubsheafClosure.below ⋯
-- Batteries.Data.Fin.Lemmas
Fin.sum_succ : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α] (x : Fin (n + 1) → α),
  Fin.sum x = x 0 + Fin.sum fun x_1 => x x_1.succ