mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtension_of_iso : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F' F'' : CategoryTheory.Functor D H} (e : F' ≅ F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') (α' : F ⟶ L.comp F''),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft e.hom) = α' →
    ∀ [F'.IsLeftKanExtension α], F''.IsLeftKanExtension α'
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pattern.Model.contains_eq_true_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [inst_4 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_6 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice},
  s.contains pat = true ↔ ∃ pos, String.Slice.Pattern.Model.MatchesAt pat pos
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y).obj (SSet.Truncated.HomotopyCategory.mk (x, y)) =
    (SSet.Truncated.HomotopyCategory.mk x, SSet.Truncated.HomotopyCategory.mk y)
-- Mathlib.Data.Num.Basic
Num.instLE : LE Num
-- Batteries.Recycling.RBTree.Lemmas
/-- A stronger version of `upperBound?_least` that holds when the cut is strict.  -/
RBTree.RBNode.Ordered.lt_upperBound? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} {x y : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.upperBound? cut t = some x → y ∈ t → (cmp y x = Ordering.lt ↔ cut y = Ordering.gt)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.pullbackSpecIso_hom_base : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (TensorProduct R S T)))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- Return the expression that we need to rewrite into to solving the goal with `rfl`.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.findRflTarget? : Lean.Expr →
  Lean.Expr →
    Mathlib.Tactic.ClickSuggestions.RwKind → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Option Lean.Expr)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ →
    s₂ ⊆ s₃ →
      μ.real (s₃ \ s₁) = 0 →
        autoParam (μ (s₃ \ s₁) ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_sdiff._auto_1 →
          μ.real s₁ = μ.real s₂
-- Mathlib.Algebra.Order.Floor.Div
CeilDiv.mk : {α : Type u_2} →
  {β : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : PartialOrder α] →
        [inst_2 : AddCommMonoid β] →
          [inst_3 : PartialOrder β] →
            [inst_4 : SMulZeroClass α β] →
              (ceilDiv : β → α → β) →
                (∀ ⦃a : α⦄, 0 < a → GaloisConnection (fun x => ceilDiv x a) fun x => a • x) →
                  (∀ ⦃a : α⦄, a ≤ 0 → ∀ (b : β), ceilDiv b a = 0) → (∀ (a : α), ceilDiv 0 a = 0) → CeilDiv α β
-- Mathlib.Analysis.Convex.Combination
mk_mem_convexHull_prod : ∀ {R : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] {s : Set E} [inst_5 : LinearOrder R] [IsStrictOrderedRing R] {t : Set F}
  {x : E} {y : F}, x ∈ (convexHull R) s → y ∈ (convexHull R) t → (x, y) ∈ (convexHull R) (s ×ˢ t)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The kernel of `A →ₐ[R₁] I.quotient` is `I`.  -/
Ideal.Quotient.mkₐ_ker : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] (I : Ideal A)
  [inst_3 : I.IsTwoSided], RingHom.ker ↑(Ideal.Quotient.mkₐ R₁ I) = I
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.reindex_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {J' : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [inst_3 : F.Final],
  (P.reindex F).diag = F.comp P.diag
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.rel_of_snd : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α₁ m] [inst_4 : Std.Iterators.Finite α₂ m]
  {it₂ it₂' : Std.IterM m β},
  it₂'.finitelyManySteps.Rel it₂.finitelyManySteps →
    Std.Iterators.Types.Append.Rel α₁ α₂ m β (Std.IterM.Intermediate.appendSnd α₁ it₂')
      (Std.IterM.Intermediate.appendSnd α₁ it₂)
-- Init.Data.BitVec.Bitblast
/-- The preliminary overflow flag is true for a certain `s` if and only if the conjunction returns true at
any `k` smaller than or equal to `s`.  -/
BitVec.resRec_true_iff : ∀ {w : ℕ} (x y : BitVec w) (s : ℕ) (hs : s < w) (hs' : 0 < s),
  x.resRec y s hs hs' = true ↔ ∃ k, ∃ (h : k ≤ s) (_ : 0 < k), x.aandRec y k ⋯ = true
-- Lean.Server.References
_private.Lean.Server.References.0.Lean.Server.combineIdents.findCanonicalRepresentative : Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent → Lean.Lsp.RefIdent → Lean.Lsp.RefIdent
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If three points are not collinear, the second and third are different.  -/
ne₂₃_of_not_collinear : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, ¬Collinear k {p₁, p₂, p₃} → p₂ ≠ p₃
-- Mathlib.CategoryTheory.Action.Continuous
Action.isContinuous_def : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  (X : Action V G),
  X.IsContinuous ↔
    Continuous fun p => (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ V TopCat).map (X.ρ p.1))) p.2
-- Init.Data.Nat.Lemmas
Nat.zero_eq_mul : ∀ {m n : ℕ}, 0 = m * n ↔ m = 0 ∨ n = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.instIsDenseCompOfIsEquivalence_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D C') [F.IsDense] [G.IsEquivalence], (F.comp G).IsDense
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instSub : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommGroup M] →
        [inst_1 : TopologicalSpace M] → [IsTopologicalAddGroup M] → Sub (MeasureTheory.VectorMeasure α M)
-- Mathlib.Algebra.Algebra.Basic
ULift.algebraMap_eq : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (algebraMap R (ULift.{u_4, u_2} A)) r = { down := (algebraMap R A) r }
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context.autoBoundImplicit : Lean.Elab.Term.Context → Bool
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedCosZeta.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedCosZeta a s = (HurwitzZeta.hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.CharP.Defs
CharP.ofNat_eq_zero' : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] (a : ℕ) [inst_2 : a.AtLeastTwo],
  p ∣ a → OfNat.ofNat a = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₁.getKey k ⋯
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mvPolynomialEquivMvPolynomial_apply : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [inst : CommSemiring R] [inst_1 : CommSemiring S₃]
  (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R)
  (hfgC : (f.comp g).comp MvPolynomial.C = MvPolynomial.C)
  (hfgX : ∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n)
  (hgfC : (g.comp f).comp MvPolynomial.C = MvPolynomial.C)
  (hgfX : ∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n) (a : MvPolynomial S₁ R),
  (MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) a = f a
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Adjunction.isCardinalAccessibleCategory : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (κ : Cardinal.{w})
  [inst_2 : Fact κ.IsRegular] [CategoryTheory.IsCardinalAccessibleCategory C κ] [G.IsCardinalAccessible κ] [G.Full]
  [G.Faithful], CategoryTheory.IsCardinalAccessibleCategory D κ
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommMonCat)
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj}
  {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt)
  (hs :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) =
        CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd))
  (ht :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 })
  (i : CategoryTheory.Limits.Fork s t) (x : J),
  (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).π.app x =
    CategoryTheory.CategoryStruct.comp i.ι (c₁.π.app { as := x })
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
invariantBasisNumber_iff_matrix : ∀ {R : Type u_1} [inst : Semiring R],
  InvariantBasisNumber R ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
-- Init.Data.Format.Instances
List.format : {α : Type u_1} → [Std.ToFormat α] → List α → Std.Format
-- Batteries.Data.MLList.Basic
/-- Return the first value on which a predicate returns true.  -/
MLList.first : {m : Type u_1 → Type u_1} → {α : Type u_1} → [AlternativeMonad m] → MLList m α → (α → Bool) → m α
-- Mathlib.CategoryTheory.Join.Basic
/-- Construct a natural transformation between functors out of a join from
the data of natural transformations between each side that are compatible with the
action on edge maps.  -/
CategoryTheory.Join.mkNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F F' : CategoryTheory.Functor (CategoryTheory.Join C D) E} →
              (αₗ : (CategoryTheory.Join.inclLeft C D).comp F ⟶ (CategoryTheory.Join.inclLeft C D).comp F') →
                (αᵣ : (CategoryTheory.Join.inclRight C D).comp F ⟶ (CategoryTheory.Join.inclRight C D).comp F') →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
                          ((CategoryTheory.Prod.snd C D).whiskerLeft αᵣ) =
                        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft αₗ)
                          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F'))
                      CategoryTheory.Join.mkNatTrans._auto_1 →
                    (F ⟶ F')
-- Mathlib.Logic.Denumerable
Denumerable.prod_nat_ofNat : Denumerable.ofNat (ℕ × ℕ) = Nat.unpair
-- Init.Data.SInt.Lemmas
Int32.add_comm : ∀ (a b : Int32), a + b = b + a
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i : ι),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.yoneda.map (AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i))
      (AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom =
    f i
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.ext : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] {f g : A →⋆ₐ[R] B},
  (∀ (x : A), f x = g x) → f = g
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapId'_eq_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (b : B), F.mapId' (CategoryTheory.CategoryStruct.id b) ⋯ = F.mapId b
-- Mathlib.Data.Ordmap.Invariants
Ordnode.length_toList' : ∀ {α : Type u_1} (t : Ordnode α), t.toList.length = t.realSize
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.transpose_mem_iff : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A.transpose ∈ Matrix.symplecticGroup l R ↔ A ∈ Matrix.symplecticGroup l R
-- Mathlib.MeasureTheory.Function.EssSup
essSup_const' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] [NeZero μ] (c : β), essSup (fun x => c) μ = c
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.addHom_ext_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_5} [inst_1 : AddMonoid M] {f g : SkewPolynomial R →+ M},
  f = g ↔ ∀ (n : ℕ) (a : R), f ((SkewPolynomial.monomial n) a) = g ((SkewPolynomial.monomial n) a)
-- Mathlib.Topology.Order.LeftRightNhds
/-- The filter of right neighborhoods has a basis of closed intervals.  -/
nhdsGE_basis_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α]
  [DenselyOrdered α] {a : α}, (nhdsWithin a (Set.Ici a)).HasBasis (fun x => a < x) (Set.Icc a)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (∀ (x : M), 0 ≤ (B x) x) →
    LinearMap.IsSymm B →
      ∀ {W : Submodule R M}, (LinearMap.domRestrict₁₂ B W W).Nondegenerate ↔ Disjoint W (LinearMap.ker B)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.isAdmissible_iff_isChain_and_le : ∀ {m : ℕ} {L : List ℕ},
  SimplexCategoryGenRel.IsAdmissible m L ↔
    List.IsChain (fun x1 x2 => x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α),
  Std.DHashMap.Internal.AssocList.erase a Std.DHashMap.Internal.AssocList.nil = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_eq_empty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {γ : α → Type u_3} {s : (a : α) → Finset (γ a)},
  Fintype.piFinset s = ∅ ↔ ∃ i, s i = ∅
-- Mathlib.Data.Int.CharZero
Int.cast_div_charZero : ∀ {k : Type u_3} [inst : DivisionRing k] [CharZero k] {m n : ℤ}, n ∣ m → ↑(m / n) = ↑m / ↑n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k k' : α} {fallback : β},
  (↑m).WF →
    ∀ {f : Option β → Option β},
      Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k' fallback =
        if (k == k') = true then (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback
        else Std.DHashMap.Internal.Raw₀.Const.getD m k' fallback
-- Mathlib.Topology.Algebra.Localization
/-- The ring topology on `Localization M` coinduced from the natural homomorphism sending `x : R`
to the equivalence class of `(x, 1)`.  -/
Localization.ringTopology : {R : Type u_1} → [inst : CommRing R] → [TopologicalSpace R] → {M : Submonoid R} → RingTopology (Localization M)
-- Init.Data.Fin.Lemmas
Fin.reverseInduction.go : {n : ℕ} →
  {motive : Fin (n + 1) → Sort u_1} →
    ((i : Fin n) → motive i.succ → motive i.castSucc) →
      (i : Fin (n + 1)) → (j : ℕ) → (h : j < n + 1) → ↑i ≤ j → motive ⟨j, h⟩ → motive i
-- Init.Data.Int.LemmasAux
Int.toNat_sub_max_self : ∀ (a : ℤ), (a - max a 0).toNat = 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.map_ι₀_mapHomologicalComplexObjIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (F : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel] {D : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_2, u_3} D] [inst_4 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)]
  [inst_7 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F))]
  [inst_8 :
    ∀ (i : ι),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i)
        (((H.mapHomologicalComplex c).obj F).X i)]
  [inst_9 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F))
        (-CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F)))]
  [inst_10 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.mapHomologicalComplex c).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F)))]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.cylinder.ι₀ F))
      (HomologicalComplex.cylinder.mapHomologicalComplexObjIso F H hc).hom =
    HomologicalComplex.cylinder.ι₀ ((H.mapHomologicalComplex c).obj F)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ofList_nil : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.DTreeMap.ofList [] cmp = ∅
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_pi_mulSingle : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : DecidableEq ι] [inst_1 : (a : ι) → CommMonoid (M a)] (a : ι)
  (f : (a : ι) → M a) (s : Finset ι), ∏ a' ∈ s, Pi.mulSingle a' (f a') a = if a ∈ s then f a else 1
-- Mathlib.Topology.Continuous
Equiv.continuous_symm_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y),
  Continuous ⇑e.symm ↔ IsOpenMap ⇑e
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.rightUnitor_inv_left_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.Limits.pullback.fst Y.hom (CategoryTheory.CategoryStruct.id X)) =
    CategoryTheory.CategoryStruct.id Y.left
-- Lean.Setup
Lean.ImportArtifacts.ofArrays.sizeOf_spec : ∀ (toArrays : Array (Array System.FilePath)), sizeOf { toArrays := toArrays } = 1 + sizeOf toArrays
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instZero : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [Zero G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] → Zero (ContMDiffMap I I' N G n)
-- Init.Data.Rat.Lemmas
Rat.lt_iff_le_and_not_ge : ∀ {a b : ℚ}, a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [Finite ι]
  {K : Type u_6} [inst_3 : Field K] [CharZero K] [inst_5 : Module K M] [inst_6 : Module K N] {P : RootPairing ι K M N}
  [P.IsRootSystem] [inst_8 : P.IsCrystallographic] (b : P.Base),
  ∃ d ∈ Submodule.span K (Set.range fun i j => ↑(P.pairingIn ℤ j ↑i)),
    (∀ (i : ι), d i ≠ 0) ∧ Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) d)
-- Std.Sat.AIG.CNF
/-- Add a `Decl.false` to a `Cache`.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.addFalse : {aig : Std.Sat.AIG ℕ} →
  {cnf : Std.Sat.CNF ℕ} →
    (cache : Std.Sat.AIG.toCNF.Cache✝ aig cnf) →
      (idx : ℕ) →
        (h : idx < aig.decls.size) →
          aig.decls[idx] = Std.Sat.AIG.Decl.false → { out // Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache out idx h }
-- Mathlib.Algebra.Tropical.Lattice
instConditionallyCompleteLatticeTropical : {R : Type u_1} → [ConditionallyCompleteLattice R] → ConditionallyCompleteLattice (Tropical R)