mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
ModuleCat.shortComplexOfConj_exact : ∀ {R : Type u} [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type v}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Type v} [inst_5 : AddCommGroup L] [inst_6 : Module R L]
  {M' : Type u_1} {N' : Type u_2} {L' : Type u_3} [inst_7 : AddCommGroup M'] [inst_8 : AddCommGroup N']
  [inst_9 : AddCommGroup L'] [inst_10 : Module R M'] [inst_11 : Module R N'] [inst_12 : Module R L'] (eM : M ≃ₗ[R] M')
  (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L') (exact : Function.Exact ⇑f ⇑g),
  (ModuleCat.shortComplexOfConj eM eN eL f g ⋯).Exact
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.toLinearExpr : Lean.Expr → Lean.MetaM (Lean.Meta.Simp.Arith.Nat.LinearExpr × Array Lean.Expr)
-- Mathlib.RingTheory.Localization.Away.AdjoinRoot
IsLocalization.adjoin_inv : ∀ {R : Type u_1} [inst : CommRing R] (r : R), IsLocalization.Away r (AdjoinRoot (Polynomial.C r * Polynomial.X - 1))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.baseChange_polynomialY : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange B).polynomialY = (MvPolynomial.map ↑f) (W'.baseChange A).polynomialY
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lintNamed : Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Iio_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Iio b
-- Init.Data.SInt.Lemmas
Int64.toISize_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toISize = OfNat.ofNat n
-- Mathlib.Order.Filter.Extr
isExtrFilter_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter (⇑OrderDual.toDual ∘ f) l a ↔ IsExtrFilter f l a
-- Init.Data.SInt.Lemmas
Int32.one_mul : ∀ (a : Int32), 1 * a = a
-- Mathlib.Algebra.Group.Hom.Basic
AddHom.instAdd.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : AddCommSemigroup N],
  AddHom.instAdd = { add := fun f g => { toFun := fun m => f m + g m, map_add' := ⋯ } }
-- Init.Data.Float.Model.Float32
Float32.Model.instMax : Max Float32.Model
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isMaximal : ∀ (R : Type u_1) [inst : CommSemiring R] [Ring.KrullDimLE 0 R], minimalPrimes R = {I | I.IsMaximal}
-- Init.Data.Nat.Lemmas
Nat.div_ne_zero_iff_of_dvd : ∀ {b a : ℕ}, b ∣ a → (a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0)
-- Lean.Widget.InteractiveGoal
Lean.Widget.instEmptyCollectionInteractiveGoals : EmptyCollection Lean.Widget.InteractiveGoals
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.div_comp : ∀ {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 : CategoryTheory.Functor C E) [F.Faithful]
  (G : CategoryTheory.Functor D E) [inst_4 : G.Faithful] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X)
  (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f),
  (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).comp G = F
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.obj_surjective_of_im_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj),
  CategoryTheory.Subgroupoid.im φ hφ = ⊤ → Function.Surjective φ.obj
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.x_sub_y_dvd_pow : ∀ {a : ℕ} (a1 : 1 < a) (y n : ℕ), 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ Pell.yz a1 n * (↑a - ↑y) + ↑(y ^ n) - Pell.xz a1 n
-- Mathlib.Data.List.Chain
List.IsChain.backwards_cons_induction : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α),
  List.IsChain r (a :: l) → (a :: l).getLast ⋯ = b → (∀ ⦃x y : α⦄, r x y → p y → p x) → p b → ∀ i ∈ a :: l, p i
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.trustOfNat : Lean.Option Bool
-- Init.Data.Range.Polymorphic.Basic
Std.Ric.le_upper_of_mem : ∀ {α : Type u} {r : Std.Ric α} {a : α} [inst : LE α] [LT α], a ∈ r → a ≤ r.upper
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Methods.toMethodsRef.unsafe_impl_2 : Lean.Meta.Grind.Methods → Lean.Meta.Grind.MethodsRef
-- Mathlib.Topology.SeparatedMap
IsSeparatedMap.pullback : ∀ {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace A] {f : X → Y},
  IsSeparatedMap f → ∀ (g : A → Y), IsSeparatedMap Function.Pullback.snd
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), p.comp q = Polynomial.eval₂ Polynomial.C q p
-- Init.Data.SInt.Lemmas
Int8.toInt.eq_1 : ∀ (i : Int8), i.toInt = i.toBitVec.toInt
-- Mathlib.Algebra.Order.Archimedean.Hom
OrderRingHom.apply_eq_self : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α →+*o α)
  (x : α), f x = x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomology_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {A : C} (f₁ f₂ : A ⟶ S.rightHomology),
  CategoryTheory.CategoryStruct.comp f₁ S.rightHomologyι = CategoryTheory.CategoryStruct.comp f₂ S.rightHomologyι →
    f₁ = f₂
-- Mathlib.Topology.Defs.Sequences
seqCompactSpace_iff : ∀ (X : Type u_1) [inst : TopologicalSpace X], SeqCompactSpace X ↔ IsSeqCompact Set.univ
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.evaluationPreservesLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesLimitsOfSize.{v₂, v, max u₁ v, v, max (max (max u u₁) (v + 1)) v₁, max u (v + 1)}
    (SheafOfModules.evaluation R X)
-- Mathlib.Order.RelIso.Basic
RelIso.emptySumLex_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsEmpty α] (a : α ⊕ β),
  (RelIso.emptySumLex r s) a = (Equiv.sumEmpty β α) a.swap
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedMessageDirection : Inhabited Lean.JsonRpc.MessageDirection
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.div_conj_eq_sub_one : ∀ {p q : ℝ}, p.HolderConjugate q → p / q = p - 1
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_dvd_of_le_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (C : IntermediateField F E), A ≤ B → B.relrank C ∣ A.relrank C
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Two affine maps from a Pi-type of modules `(i : ι) → φv i` are equal if they are equal in their
operation on `Pi.single` and `ι` is nonempty.  Analogous to `LinearMap.pi_ext`. See also
`pi_ext_zero`, which instead of `Nonempty ι` requires agreement at 0.  -/
AffineMap.pi_ext_nonempty : ∀ {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V2] [inst_2 : AddTorsor V2 P2]
  [inst_3 : Module k V2] {ι : Type u_9} {φv : ι → Type u_10} [inst_4 : (i : ι) → AddCommGroup (φv i)]
  [inst_5 : (i : ι) → Module k (φv i)] [Finite ι] [inst_7 : DecidableEq ι] {f g : ((i : ι) → φv i) →ᵃ[k] P2}
  [Nonempty ι], (∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)) → f = g
-- Mathlib.Data.Nat.Factors
Nat.dvd_of_mem_primeFactorsList : ∀ {n p : ℕ}, p ∈ n.primeFactorsList → p ∣ n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.equiv_of_beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  [inst_3 : BEq β] [LawfulBEq β], m₁.WF → m₂.WF → Std.DHashMap.Raw.Const.beq m₁ m₂ = true → m₁.Equiv m₂
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
MeasurableEquiv.prodCongr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSpace δ] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ),
  ab.prodCongr cd = { toEquiv := ab.prodCongr cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.IsStrictSegal.mk : ∀ {X : SSet}, (∀ (n : ℕ), Function.Bijective (X.spine n)) → X.IsStrictSegal
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Map which produces an `n + 1`-simplex from a `1`-simplex and an `n`-simplex when
the target vertex of the `1`-simplex equals the zeroth simplex of the `n`-simplex.  -/
SSet.StrictSegalCore.concat : {X : SSet} →
  {n : ℕ} →
    X.StrictSegalCore n →
      (x : X.obj (Opposite.op { len := 1 })) →
        (s : X.obj (Opposite.op { len := n })) →
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
              (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s →
            X.obj (Opposite.op { len := n + 1 })
-- Init.Data.Order.PackageFactories
Std.LinearPreorderPackage.le_total : ∀ {α : Type u} [self : Std.LinearPreorderPackage α] (a b : α), a ≤ b ∨ b ≤ a
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The difference `log (1+z) - z` is bounded by `‖z‖^2/(2*(1-‖z‖))` when `‖z‖ < 1`.  -/
Complex.norm_log_one_add_sub_self_le : ∀ {z : ℂ}, ‖z‖ < 1 → ‖Complex.log (1 + z) - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_neg_right : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute a ↑u → AddCommute a ↑(-u)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.Const.alter.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option ((_ : α) × β) → Sort u_3) (fst : α) (v' : β) (h_1 : Unit → motive none)
  (h_2 : (fst : α) → (v' : β) → motive (some ⟨fst, v'⟩)),
  (match some ⟨fst, v'⟩ with
    | none => h_1 ()
    | some ⟨fst, v'⟩ => h_2 fst v') =
    h_2 fst v'
-- Aesop.Nanos
Aesop.Nanos.instDecidableRelLt : DecidableRel fun x1 x2 => x1 < x2
-- Mathlib.Tactic.Linter.UnusedTactic
/-- Search for tactic executions in the info tree and remove the syntax of the tactics that
changed something.  -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.eraseUsedTactics : Std.HashSet Lean.SyntaxNodeKind → Lean.PersistentArray Lean.Elab.InfoTree → Mathlib.Linter.UnusedTactic.M✝ Unit
-- Mathlib.Topology.Bornology.Constructions
Bornology.IsBounded.snd_of_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set α} {t : Set β},
  Bornology.IsBounded (s ×ˢ t) → s.Nonempty → Bornology.IsBounded t
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_inv_right`. -/
Antivary.of_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Antivary f g⁻¹ → Monovary f g
-- Mathlib.Topology.Constructions
continuous_sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, Continuous (Sigma.mk i)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_ofFractionRing_algebraMap : ∀ {L : Type u_2} {R : Type u_3} [inst : Field L] [inst_1 : CommRing R] (φ : Polynomial R →+* L)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : Polynomial R),
  (RatFunc.liftRingHom φ hφ) { toFractionRing := (algebraMap (Polynomial R) (FractionRing (Polynomial R))) x } = φ x
-- Mathlib.Data.Finset.Card
List.card_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.toFinset.card = l.dedup.length
-- Std.Http.Data.Method
Std.Http.Method.rebind.sizeOf_spec : sizeOf Std.Http.Method.rebind = 1
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instNumberField : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Field R] (v : Valuation R Γ₀)
  [NumberField R], NumberField (WithVal v)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.eq_one_of_isUnit : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → IsUnit p → p = 1
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsEmbedding g → Topology.IsEmbedding f → Topology.IsEmbedding (g ∘ f)
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- Open subsets of strongly locally contractible spaces are strongly locally contractible.  -/
IsOpen.stronglyLocallyContractibleSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [StronglyLocallyContractibleSpace X] {U : Set X},
  IsOpen U → StronglyLocallyContractibleSpace ↑U
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- If `M, M'` are `R`-modules, then any `R`-linear map `g : M ⟶ M'` induces an `S`-linear map
`(S →ₗ[R] M) ⟶ (S →ₗ[R] M')` defined by `h ↦ g ∘ h`  -/
ModuleCat.CoextendScalars.map' : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          {M M' : ModuleCat R} → (M ⟶ M') → (ModuleCat.CoextendScalars.obj' f M ⟶ ModuleCat.CoextendScalars.obj' f M')
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_star_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) _auto_374✝ → cfc (fun x => star x) a = star a
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lt_one_iff_zero : ∀ {a : Ordinal.{u_1}}, a < 1 ↔ a = 0
-- Mathlib.Algebra.GroupWithZero.Action.End
/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.

See also `Function.Surjective.mulActionLeft` and `Function.Surjective.moduleLeft`.
 -/
Function.Surjective.distribMulActionLeft : {R : Type u_6} →
  {S : Type u_7} →
    {M : Type u_8} →
      [inst : Monoid R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : DistribMulAction R M] →
            [inst_3 : Monoid S] →
              [inst_4 : SMul S M] →
                (f : R →* S) → Function.Surjective ⇑f → (∀ (c : R) (x : M), f c • x = c • x) → DistribMulAction S M
-- Mathlib.Order.WithBot
WithTop.toDual_symm : ∀ {α : Type u_1}, WithTop.toDual.symm = WithBot.ofDual
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.mk.sizeOf_spec : ∀ {V : Type u_1} [inst : SizeOf V] (Adj : V → V → Prop), sizeOf { Adj := Adj } = 1
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLE.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero β] [inst_6 : Zero γ] [SMulPosReflectLE α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → f 0 = 0 → SMulPosReflectLE α β
-- Mathlib.Order.RelClasses
/-- Set notation form of `Eq.trans_lt` -/
Eq.trans_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [inst : LT α], a = b → b ⊂ c → a ⊂ c
-- Mathlib.Combinatorics.Enumerative.Schroder
/-- The small Schröder number is equal to : `largeSchroder n = 2 * smallSchroder (n + 1), n ≥ 1`  -/
Nat.smallSchroder : ℕ → ℕ
-- Std.Data.DTreeMap.Basic
/-- Returns `true` if the tree map contains no mappings.  -/
Std.DTreeMap.isEmpty : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Bool
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftUnitor_isEquivalence : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.prod.leftUnitor C).IsEquivalence
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_one : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜],
  (DirectSum.decompose 𝒜) 1 = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, t.WF → (Std.TreeMap.Raw.map f t).contains k = t.contains k
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.ext'_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F},
  f = g ↔
    ∃ (hs₀ : f.s₀ = g.s₀) (_ :
      ∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯)) (hs₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)),
      ∀ (i j : E.I₀) (k : E.I₁ i j),
        f.h₁ k =
          CategoryTheory.CategoryStruct.comp (g.h₁ k)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv
              (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvd_iff_dvd_left : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, Associated a b → (a ∣ c ↔ b ∣ c)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_of_le_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α}, x ≤ a → Set.projIcc a b h x = ⟨a, ⋯⟩
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- A choice of which discrimination trees to build.  -/
Mathlib.Tactic.ClickSuggestions.Choice : Type
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasStrictFDerivAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (x : E), HasStrictFDerivAt 0 0 x
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntry?_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.getEntry? a = Std.Internal.List.getEntry? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Init.Data.Format.Basic
/-- Creates a format `l ++ f ++ r` with a flattening group, nesting the contents by the length of `l`.

The group's `FlattenBehavior` is `allOrNone`; for `fill` use `Std.Format.bracketFill`.
 -/
Std.Format.bracket : String → Std.Format → String → Std.Format
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- **Alias** of `linearIndependent_finCons`. -/
linearIndependent_fin_cons : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V} {n : ℕ}
  {v : Fin n → V}, LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The equivalence class of a projective point representative on a Weierstrass curve.  -/
WeierstrassCurve.Projective.PointClass : (R : Type r) → [CommRing R] → Type r
-- Mathlib.Algebra.GroupWithZero.Defs
eq_zero_or_one_of_sq_eq_self : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] [IsRightCancelMulZero M₀] {x : M₀}, x ^ 2 = x → x = 0 ∨ x = 1
-- Std.Time.Zoned.Database.TZdb
/-- Retrieves the timezone rules for the local timezone, re-reading the `TZ` and `TZDIR`
environment variables on each call so that runtime changes are reflected immediately.
 -/
Std.Time.Database.TZdb.getLocalZoneRules : Std.Time.Database.TZdb → IO Std.Time.TimeZone.ZoneRules
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.add_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s : Set G},
  IsOpen s → ∀ (t : Set G), s + closure t = s + t
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_pow : ∀ {x : ℝ} (n : ℕ), Irrational (x ^ n) → Irrational x
-- Mathlib.Data.Finset.MulAntidiagonal
Set.IsWF.min_add : ∀ {α : Type u_1} {s t : Set α} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty), ⋯.min ⋯ = hs.min hsn + ht.min htn
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_replicateCol : ∀ {n : Type u_4} {α : Type u_5} {ι : Type u_7} [inst : Fintype n] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : n → α), ‖Matrix.replicateCol ι v‖ = ‖WithLp.toLp 2 v‖
-- Mathlib.Algebra.Order.SuccPred
Order.not_isSuccLimit_add_one : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α) [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] [NoMaxOrder α],
  ¬Order.IsSuccLimit (a + 1)
-- Mathlib.RingTheory.Complex
Algebra.leftMulMatrix_complex : ∀ (z : ℂ), (Algebra.leftMulMatrix Complex.basisOneI) z = !![z.re, -z.im; z.im, z.re]
-- Init.Data.UInt.Basic
/-- The power operation, raising a 16-bit unsigned integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
UInt16.pow : UInt16 → ℕ → UInt16
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mult_isComplex : ∀ {K : Type u_1} [inst : Field K] (w : { w // w.IsComplex }), (↑w).mult = 2
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  m.toList.contains k = m.contains k
-- Mathlib.Algebra.Group.Action.Defs
Function.Surjective.smulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul N α] [inst_2 : SMul M β]
  [inst_3 : SMul N β] [SMulCommClass M N α] {f : α → β},
  Function.Surjective f →
    (∀ (c : M) (x : α), f (c • x) = c • f x) → (∀ (c : N) (x : α), f (c • x) = c • f x) → SMulCommClass M N β
-- Init.Data.String.Basic
String.Pos.Raw.isValidUTF8_extract_iff : ∀ {s : String} (p₁ p₂ : String.Pos.Raw),
  p₁ ≤ p₂ →
    p₂ ≤ s.rawEndPos →
      ((s.toByteArray.extract p₁.byteIdx p₂.byteIdx).IsValidUTF8 ↔
        p₁ = p₂ ∨ String.Pos.Raw.IsValid s p₁ ∧ String.Pos.Raw.IsValid s p₂)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_self_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {H : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {x y : H},
  ↑(extChartAt I x) y = ↑I y
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.zero_mem_measurableLE : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  0 ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- The sum over primes `k ≤ p ≤ 4^(π(k-1)+1)` over `1/p` (as a real number) is at least `1/2`.  -/
one_half_le_sum_primes_ge_one_div : ∀ (k : ℕ), 1 / 2 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
/-- There are 3 kinds of casting functions for a definition `foo := body`:
1. Equality: `foo = body`
2. Unfolding: `foo → body`
3. Refolding: `body → foo`
 -/
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind : Type
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.continuousWithinAt_log_of_re_neg_of_im_zero : ∀ {z : ℂ}, z.re < 0 → z.im = 0 → ContinuousWithinAt Complex.log {z | 0 ≤ z.im} z