mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Hom.Monoid
strictMono_iff_map_neg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], StrictMono ⇑f ↔ ∀ a < 0, f a < 0
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.spanFinBasis.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  (x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)),
  Profinite.NobelingProof.spanFinBasis C s x = { toFun := fun y => if y = x then 1 else 0, isLocallyConstant := ⋯ }
-- Std.Async.Basic
/-- Runs two computations concurrently and returns the result of the one that finishes first.
The other result is lost and the other task is not cancelled, so the task will continue the execution
until the end.
 -/
Std.Async.BaseAsync.race : {α : Type} →
  [Inhabited α] →
    Std.Async.BaseAsync α → Std.Async.BaseAsync α → optParam Task.Priority Task.Priority.default → Std.Async.BaseAsync α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  {l : List (α × β)} {k : α} {v : β},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m ((k, v) :: l)) =
    ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany (m.insert k v) l)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- Compactness criterion: a closed set of compact metric spaces is compact if the spaces have
a uniformly bounded diameter, and for all `ε` the number of balls of radius `ε` required
to cover the spaces is uniformly bounded. This is an equivalence, but we only prove the
interesting direction that these conditions imply compactness.  -/
GromovHausdorff.totallyBounded : ∀ {t : Set GromovHausdorff.GHSpace} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ},
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ p ∈ t, Metric.diam Set.univ ≤ C) →
      (∀ p ∈ t, ∀ (n : ℕ), ∃ s, Cardinal.mk ↑s ≤ ↑(K n) ∧ Set.univ ⊆ ⋃ x ∈ s, Metric.ball x (u n)) → TotallyBounded t
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_map_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (c : CategoryTheory.Limits.Cone F) (α : F ⟶ G) {Z : C}
  (h : CategoryTheory.Limits.limit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap α) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.lift G ((CategoryTheory.Limits.Cone.postcompose α).obj c)) h
-- Mathlib.Analysis.Convex.BetweenList
List.exists_map_eq_of_sorted_iff_wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {l : List P},
  (∃ p₁ p₂ l', l'.SortedLE ∧ List.map (⇑(AffineMap.lineMap p₁ p₂)) l' = l) ↔ List.Wbtw R l
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.zero_apply : ∀ {V W : SemiNormedGrp} (x : V.carrier), (CategoryTheory.ConcreteCategory.hom 0) x = 0
-- Batteries.Data.UInt
UInt8.ext_iff : ∀ {x y : UInt8}, x = y ↔ x.toNat = y.toNat
-- Lean.Elab.Tactic.Grind.Basic
/-- Close the main goal using the given tactic. If it fails, log the error and `admit`  -/
Lean.Elab.Tactic.Grind.closeUsingOrAdmit : Lean.Elab.Tactic.Grind.GrindTacticM Unit → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.NumberTheory.LSeries.Basic
/-- An alternate spelling of `LSeries` as `∑' n, f n / n ^ s` for the case `f 0 = 0`.  -/
LSeries_def₀ : ∀ {f : ℕ → ℂ}, f 0 = 0 → ∀ (s : ℂ), LSeries f s = ∑' (n : ℕ), f n / ↑n ^ s
-- Init.Data.Rat.Lemmas
Rat.floor_add_le_floor_add_intCast : ∀ {x : ℚ} {y : ℤ}, x.floor + y ≤ (x + ↑y).floor
-- Mathlib.Order.Filter.Prod
Filter.Tendsto.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β}
  {c : Filter γ} {d : Filter δ},
  Filter.Tendsto f a c → Filter.Tendsto g b d → Filter.Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).isColimit =
    CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯
      (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) g) ⋯ ⋯
-- Std.Http.Data.Headers.Name
/-- The proof that it's a valid header name.
 -/
Std.Http.Header.Name.isValidHeaderValue : ∀ (self : Std.Http.Header.Name), Std.Http.Header.IsValidHeaderName self.value
-- Mathlib.Data.Int.ModEq
Int.modEq_add_modulus_mul_iff : ∀ {n a b c : ℤ}, a ≡ b + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.CategoryTheory.Galois.Basic
/-- The canonical action of `Aut F` on the fiber of each object.  -/
CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatObjFiniteObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → (X : C) → MulAction (CategoryTheory.Aut F) (F.obj X).obj
-- Mathlib.Algebra.Ring.Hom.Defs
RingHomClass.mk : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} [inst : NonAssocSemiring α]
  [inst_1 : NonAssocSemiring β] [inst_2 : FunLike F α β] [toMonoidHomClass : MonoidHomClass F α β]
  [toAddMonoidHomClass : AddMonoidHomClass F α β], RingHomClass F α β
-- Mathlib.Data.List.Rotate
List.length_cyclicPermutations_cons : ∀ {α : Type u} (x : α) (l : List α), (x :: l).cyclicPermutations.length = l.length + 1
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_zero_add_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd' C 0 a a ⋯).hom.app X =
    (CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
MvPolynomial.degLex_totalDegree_monotone : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R} [inst_1 : LinearOrder σ]
  [inst_2 : WellFoundedGT σ],
  MonomialOrder.degLex.toSyn (MonomialOrder.degLex.degree f) ≤
      MonomialOrder.degLex.toSyn (MonomialOrder.degLex.degree g) →
    f.totalDegree ≤ g.totalDegree
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- Every temperate growth measure defines a tempered distribution.  -/
MeasureTheory.Measure.toTemperedDistribution : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [inst_2 : MeasurableSpace E] →
        [BorelSpace E] →
          [SecondCountableTopology E] →
            (μ : autoParam (MeasureTheory.Measure E) _auto_26✝) → [hμ : μ.HasTemperateGrowth] → TemperedDistribution E ℂ
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X),
  P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)
-- Mathlib.LinearAlgebra.Pi
Submodule.coe_pi : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (I : Set ι) (p : (i : ι) → Submodule R (φ i)),
  ↑(Submodule.pi I p) = I.pi fun i => ↑(p i)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instNeg : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommGroup M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → Neg (MultilinearMap R M₁ M₂)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₂ : List ℕ → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.range_finite : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] {f : X → Y},
  IsLocallyConstant f → (Set.range f).Finite
-- Init.Data.ByteArray.Basic
ByteArray.usize.eq_1 : ∀ (a : ByteArray), a.usize = a.size.toUSize
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is convex on `S` and right-differentiable at `x ∈ S`, then the slope of any
secant line with left endpoint at `x` is bounded below by the right derivative of `f` at `x`.  -/
ConvexOn.le_slope_of_hasDerivWithinAt_Ioi : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Ioi x) x → f' ≤ slope f x y
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.epi_iff_range_eq_top : ∀ {A B : CommGrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ (CommGrpCat.Hom.hom f).range = ⊤
-- Mathlib.Analysis.Complex.Basic
RCLike.ofReal_eq_complex_ofReal : RCLike.ofReal = Complex.ofReal
-- Mathlib.Algebra.Ring.Parity
Nat.Odd.of_mul_right : ∀ {m n : ℕ}, Odd (m * n) → Odd n
-- Init.Data.Bool
Bool.toNat_true : true.toNat = 1
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_functor_map_op_inclRight : ∀ (C : Type u₁) {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {d d' : D} (f : d ⟶ d'),
  (CategoryTheory.Join.opEquiv C D).functor.map (Opposite.op ((CategoryTheory.Join.inclRight C D).map f)) =
    (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).map (Opposite.op f)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.fieldIdx.sizeOf_spec : ∀ (ref : Lean.Syntax) (i : ℕ) (levels : List Lean.Level),
  sizeOf (Lean.Elab.Term.LVal.fieldIdx ref i levels) = 1 + sizeOf ref + sizeOf i + sizeOf levels
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
SmoothBumpCovering.ind.congr_simp : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs fs_1 : SmoothBumpCovering ι I M s),
  fs = fs_1 → ∀ (x x_1 : M) (e_x : x = x_1) (hx : x ∈ s), fs.ind x hx = fs_1.ind x_1 ⋯
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.map_id' : ∀ {α : Type u_1} (l : List α), List.map (fun a => a) l = l
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (t.insertMany l).getKeyD k' fallback = k
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_singletonMonoidHom : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α], ⇑Finset.singletonMonoidHom = singleton
-- Lean.Meta.Basic
Lean.Meta.PostponedEntry.mk.inj : ∀ {ref : Lean.Syntax} {lhs rhs : Lean.Level} {ctx? : Option Lean.Meta.DefEqContext} {ref_1 : Lean.Syntax}
  {lhs_1 rhs_1 : Lean.Level} {ctx?_1 : Option Lean.Meta.DefEqContext},
  { ref := ref, lhs := lhs, rhs := rhs, ctx? := ctx? } = { ref := ref_1, lhs := lhs_1, rhs := rhs_1, ctx? := ctx?_1 } →
    ref = ref_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1 ∧ ctx? = ctx?_1
-- Lean.Declaration
Lean.InductiveType.mk.inj : ∀ {name : Lean.Name} {type : Lean.Expr} {ctors : List Lean.Constructor} {name_1 : Lean.Name} {type_1 : Lean.Expr}
  {ctors_1 : List Lean.Constructor},
  { name := name, type := type, ctors := ctors } = { name := name_1, type := type_1, ctors := ctors_1 } →
    name = name_1 ∧ type = type_1 ∧ ctors = ctors_1
-- Mathlib.Logic.Equiv.Multiset
/-- Outputs the list of differences of the input list, that is
`lower [a₁, a₂, ...] n = [a₁ - n, a₂ - a₁, ...]`  -/
Denumerable.lower : List ℕ → ℕ → List ℕ
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Transposing a matrix preserves the determinant.  -/
Matrix.det_transpose : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
  M.transpose.det = M.det
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_prodCongr : ∀ {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring R'] [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalNonAssocSemiring S']
  (f : R ≃+* R') (g : S ≃+* S'), ⇑(f.prodCongr g) = Prod.map ⇑f ⇑g
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.relabel : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n m : ℕ} {φ : L.BoundedFormula α m},
  φ.IsAtomic → ∀ (f : α → β ⊕ Fin n), (FirstOrder.Language.BoundedFormula.relabel f φ).IsAtomic
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.congr : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal} {Y : Ω → ℝ},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    X =ᵐ[ν.bind ⇑κ] Y → ProbabilityTheory.Kernel.HasSubgaussianMGF Y c κ ν
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_div : ∀ {K : Type u_1} [inst : RCLike K] (r s : ℝ), ↑(r / s) = ↑r / ↑s
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↥X),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)
-- Batteries.Data.List.Scan
List.getElem_flatten_aux₂ : ∀ {α : Type u_1} (L : List (List α)) (i : ℕ) (h : i < L.flatten.length),
  let j := List.findIdx (fun x => decide (x > i)) (List.map List.length L).partialSums - 1;
  have hj := ⋯;
  have k := i - (List.take j L).flatten.length;
  k < L[j].length
-- Mathlib.Order.Heyting.Hom
HeytingHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.Hom.Simps.hom.eq_1 : ∀ (X Y : AddCommMonCat) (f : X.Hom Y), AddCommMonCat.Hom.Simps.hom X Y f = f.hom
-- Mathlib.Order.Filter.Basic
Filter.frequently_imp_distrib_left : ∀ {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop}, (∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- See also `SkewPolynomial.sum_add'`.  -/
SkewPolynomial.sum_add : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (p : SkewPolynomial R) (f g : ℕ → R → S),
  (p.sum fun n x => f n x + g n x) = p.sum f + p.sum g
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.eq.sizeOf_spec : ∀ (solverId : ℕ) (lhs rhs : Lean.Expr) (rest : Lean.Meta.Grind.PendingSolverPropagationsData✝),
  sizeOf (Lean.Meta.Grind.PendingSolverPropagationsData.eq✝ solverId lhs rhs rest) =
    1 + sizeOf solverId + sizeOf lhs + sizeOf rhs + sizeOf rest
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_closure_of_isBounded : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], Bornology.IsBounded s → Bornology.IsBounded (closure s)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.toPresheaf_preservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.Limits.PreservesFiniteLimits (PresheafOfModules.toPresheaf R)
-- Mathlib.RingTheory.Nilpotent.Lemmas
Module.End.isNilpotent_restrict_of_le : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : Module.End R M} {p q : Submodule R M} {hp : Set.MapsTo ⇑f ↑p ↑p} {hq : Set.MapsTo ⇑f ↑q ↑q},
  p ≤ q → IsNilpotent (LinearMap.restrict f hq) → IsNilpotent (LinearMap.restrict f hp)
-- Init.Data.List.Sublist
List.drop_subset : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.drop i l ⊆ l
-- Init.Core
DoResultPR.pure.inj : ∀ {α β σ : Type u} {a : α} {a_1 : σ} {a_2 : α} {a_3 : σ},
  DoResultPR.pure a a_1 = DoResultPR.pure a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.of_isOpenCover : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U → ∀ [∀ (i : ι), PrespectralSpace ↥(U i)], PrespectralSpace X
-- Mathlib.Data.Set.Lattice
Set.Nonempty.of_sUnion : ∀ {α : Type u_1} {s : Set (Set α)}, (⋃₀ s).Nonempty → s.Nonempty
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivisionCommMonoid` if it admits an
injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `DivisionCommMonoid`.
See note [reducible non-instances].  -/
Function.Injective.divisionCommMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : DivisionCommMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → DivisionCommMonoid M₁
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote_mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α)
  (m₁ m₂ : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote ctx (m₁.mul m₂) =
    Lean.Grind.CommRing.Mon.denote ctx m₁ * Lean.Grind.CommRing.Mon.denote ctx m₂
-- Init.Data.Array.Zip
Array.unzip_zip_left : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β}, as.size ≤ bs.size → (as.zip bs).unzip.1 = as
-- Mathlib.Tactic.Linter.TextBased
/-- Creates `StyleError`s for bad usage of unicode characters.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicode : String → Array Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.subsingleton_or_norm_symm_pos : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂]
  (e : E ≃SL[σ₁₂] F), Subsingleton E ∨ 0 < ‖↑e.symm‖
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- Given `𝒰 i` covering `Y` and `𝒱 i j` covering `𝒰 i`, this is the open cover
`𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂` ranging over all `i`, `j₁`, `j₂`.
 -/
AlgebraicGeometry.Scheme.Pullback.diagonalCover : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (𝒰 : Y.OpenCover) →
      ((i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
          ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover) →
        (CategoryTheory.Limits.pullback.diagonalObj f).OpenCover
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.done.inj : ∀ {r r_1 : Lean.Meta.Simp.Result}, Lean.Meta.Simp.Step.done r = Lean.Meta.Simp.Step.done r_1 → r = r_1
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.nsmul_eq_mul : ∀ (n : ℕ) (a : Ordinal.{u_4}), n • a = a * ↑n
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_eq_measureReal_of_null_sdiff`. -/
MeasureTheory.measureReal_eq_measureReal_of_null_diff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s ⊆ t →
    μ.real (t \ s) = 0 →
      autoParam (μ (t \ s) ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_of_null_sdiff._auto_1 → μ.real s = μ.real t
-- Init.System.IO
/-- Returns the directory that the current executable is located in.
 -/
IO.appDir : IO System.FilePath
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_zero_add_string : ∀ (s : String), (0 + s).byteIdx = s.utf8ByteSize
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.inv_zero : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], 0⁻¹ = 0
-- Std.Time.Format.Modifier
Std.Time.instInhabitedZoneName : Inhabited Std.Time.ZoneName
-- Lean.Elab.App
/-- The type of the eliminator.  -/
Lean.Elab.Term.ElabElimInfo.elimType : Lean.Elab.Term.ElabElimInfo → Lean.Expr
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_sdiff_right_self`. -/
Set.diff_diff_right_self : ∀ {α : Type u_1} (s t : Set α), s \ (s \ t) = s ∩ t
-- Std.Http.Data.Headers
/-- Creates empty headers.
 -/
Std.Http.Headers.empty : Std.Http.Headers
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.var : Nat.Internal.Linear.Var → Nat.Internal.Linear.Expr
-- Mathlib.Topology.GDelta.Basic
/-- The union of finitely many Gδ sets is a Gδ set, bounded indexed union version.  -/
IsGδ.biUnion : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {s : Set ι},
  s.Finite → ∀ {f : ι → Set X}, (∀ i ∈ s, IsGδ (f i)) → IsGδ (⋃ i ∈ s, f i)
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from groups to types creates all limits.
 -/
GrpCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget GrpCat)
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The submonoid `M` of the monoid `M`.  -/
Submonoid.instTop : {M : Type u_1} → [inst : MulOneClass M] → Top (Submonoid M)
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSemisimple.booleanGenerators : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSemisimple R L], IsCompactlyGenerated.BooleanGenerators {I | IsAtom I}
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isPrimitiveRoot_iff : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ ξ : R},
  IsPrimitiveRoot ζ k → (IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvd_dvd : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Associated a b → a ∣ b ∧ b ∣ a
-- Mathlib.Data.Fintype.Pi
Finset.piFinset_filter_const : ∀ {α : Type u_1} {ι : Type u_3} [inst : DecidableEq (ι → α)] {s : Finset α} [inst_1 : DecidableEq ι]
  [inst_2 : Fintype ι], {f ∈ Fintype.piFinset fun x => s | ∃ a ∈ s, Function.const ι a = f} = s.piDiag ι
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_eq_getD_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α}, m.getD a fallback = (m.get? a).getD fallback
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Functor.instIsIsoId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C], (CategoryTheory.Functor.id C).IsIso
-- Mathlib.Topology.Constructions.SumProd
Continuous.comp₃ : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} {ε : Type u_3} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W]
  [inst_4 : TopologicalSpace ε] {g : X × Y × Z → ε},
  Continuous g →
    ∀ {e : W → X},
      Continuous e → ∀ {f : W → Y}, Continuous f → ∀ {k : W → Z}, Continuous k → Continuous fun w => g (e w, f w, k w)