mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The short complex which expresses `X.cycles` as the kernel of `X.δ`.  -/
CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (i ⟶ j) →
                (j ⟶ k) →
                  (n₀ n₁ : ℤ) →
                    autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles._auto_1 →
                      CategoryTheory.ShortComplex C
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.sub_comp : ∀ {M : Type u_2} {N : Type u_3} {G : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommGroup G] (f g : N →+ G) (h : M →+ N), (f - g).comp h = f.comp h - g.comp h
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `QuotientAddGroup.quotientQuotientEquivQuotient`.  -/
QuotientAddGroup.quotientQuotientIsometryEquivQuotient : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {S T : AddSubgroup M} → S ≤ T → (M ⧸ S) ⧸ AddSubgroup.map (QuotientAddGroup.mk' S) T ≃ᵢ M ⧸ T
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.integral_pullback_invFun_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [BorelSpace A]
  (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [inst_11 : NormedSpace ℝ E]
  (f : CompactlySupportedContinuousMap B E) (b : B),
  ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_le_size_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m.size ≤ (m.erase k).size + 1
-- Init.Data.Vector.Lemmas
Vector.reverse_push : ∀ {α : Type u_1} {n : ℕ} {as : Vector α n} {a : α}, (as.push a).reverse = Vector.cast ⋯ (#v[a] ++ as.reverse)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.majorized_tail_toFun_head : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  List.length m = List.length basis_tl →
    Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) →
      Tactic.ComputeAsymptotics.Majorized (m.toFun basis_tl) basis_hd 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMon_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : CategoryTheory.Mon C} (ψ : X ⟶ Y) (x : Cᵒᵖ),
  (CategoryTheory.yonedaMon.map ψ).app x = MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom ψ.hom (Opposite.unop x))
-- Init.Data.Vector.Lemmas
Vector.getElem_append_right : ∀ {α : Type u_1} {n m i : ℕ} {xs : Vector α n} {ys : Vector α m} (h : i < n + m) (hi : n ≤ i), (xs ++ ys)[i] = ys[i - n]
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.hasLineDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E}, HasLineDerivAt 𝕜 f f' x v → ∀ (s : Set E), HasLineDerivWithinAt 𝕜 f f' s x v
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.hom_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} {φ₁ φ₂ : R ⟶ R'}, φ₁ = φ₂ ↔ φ₁.f = φ₂.f
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.conjTranspose_invOf : ∀ {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α] [inst_3 : StarRing α]
  (A : Matrix n n α) [inst_4 : Invertible A] [inst_5 : Invertible A.conjTranspose],
  (⅟A).conjTranspose = ⅟A.conjTranspose
-- Mathlib.Topology.EMetricSpace.Defs
/-- Auxiliary function to replace the topology on an emetric space with
a topology which is equal to the original one, but maybe not defeq.
This is useful if one wants to construct an emetric space with a
specified topology. See Note [forgetful inheritance] explaining why having definitionally
the right topology is often important.
See note [reducible non-instances].
 -/
EMetricSpace.replaceTopology : {γ : Type u_2} →
  [T : TopologicalSpace γ] →
    (m : EMetricSpace γ) → T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace → EMetricSpace γ
-- Mathlib.Order.Heyting.Boundary
/-- The boundary of an element of a co-Heyting algebra is the intersection of its Heyting negation
with itself. Note that this is always `⊥` for a Boolean algebra.  -/
Coheyting.boundary : {α : Type u_1} → [CoheytingAlgebra α] → α → α
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.eq_of_coeff_eq : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} [Finite ι] (hs : IsLocalFrameOn I F n s u),
  x ∈ u → ∀ {t t' : (x : M) → V x}, (∀ (i : ι), (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)) → t x = t' x
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.options? : Lean.Lsp.CreateFile → Option Lean.Lsp.CreateFile.Options
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.dpostDefault : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.DSimproc
-- Init.Data.String.FindPos
/-- Obtains the largest valid position that is strictly less than the given byte position.
 -/
String.posLT : (s : String) → (offset : String.Pos.Raw) → 0 < offset → s.Pos
-- Mathlib.Algebra.Category.Grp.Zero
CommGrpCat.instHasZeroObject : CategoryTheory.Limits.HasZeroObject CommGrpCat
-- Init.Data.String.Basic
String.Pos.Raw.utf8PrevAux.eq_def : ∀ (x : List Char) (x_1 x_2 : String.Pos.Raw),
  String.Pos.Raw.utf8PrevAux x x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, p => { byteIdx := p.byteIdx - 1 }
    | c :: cs, i, p =>
      have i' := i + c;
      if p ≤ i' then i else String.Pos.Raw.utf8PrevAux cs i' p
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- The equivalence `(X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)` given by `h : F.FullyFaithful`.  -/
CategoryTheory.Functor.FullyFaithful.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → F.FullyFaithful → {X Y : C} → (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.helper₄ : ∀ {w₀ w' : ℕ} (s : ℕ) (c : BitVec w₀) (v : BitVec w') (w : ℕ),
  BitVec.setWidth (w' + w) (c >>> s) &&& BitVec.setWidth (w' + w) (BitVec.allOnes w) ||| v ++ 0#w =
    v ++ BitVec.extractLsb' s w c
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.rank_self : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R], Module.rank R R = 1
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.ψ₁.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.Localization.Construction.ψ₁ W f =
    (CategoryTheory.Paths.of (CategoryTheory.Localization.Construction.LocQuiver W)).map (Sum.inl f)
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_inf : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L), ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_5 : ∀ (q : Turing.PartrecToTM2.Λ'), Turing.PartrecToTM2.trStmts₁ q.copy = insert q.copy (Turing.PartrecToTM2.trStmts₁ q)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The relation between TM2 configurations and TM1 configurations of the TM2 emulator.  -/
Turing.TM2to1.TrCfg : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} → Turing.TM2.Cfg Γ Λ σ → Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ → Prop
-- Mathlib.Logic.Unique
Unique.subsingleton_unique'_iff : ∀ {α : Sort u_1} {h₁ h₂ : Unique α}, h₁ = h₂ ↔ True
-- Mathlib.Topology.Homotopy.Basic
/-- Given `HomotopyRel f₀ f₁ S` and `HomotopyRel f₁ f₂ S`, we can define a `HomotopyRel f₀ f₂ S`
by putting the first homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
 -/
ContinuousMap.HomotopyRel.trans : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f₀ f₁ f₂ : C(X, Y)} → {S : Set X} → f₀.HomotopyRel f₁ S → f₁.HomotopyRel f₂ S → f₀.HomotopyRel f₂ S
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.go : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} → (k : K) → Turing.TM2to1.StAct K Γ σ k → Turing.TM2.Stmt Γ Λ σ → Turing.TM2to1.Λ' K Γ Λ σ
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_zero : ∀ {α : Type u_1}, Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.map_onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {M : Type u_1} [inst : L.Structure M]
  [inst_1 : L'.Structure M] [ϕ.IsExpansionOn M] {n : ℕ} (R : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_one_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [CanonicallyOrderedMul α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  HasProd f 1 ↔ ∀ (x : ι), f x = 1
-- Init.Data.SInt.Lemmas
ISize.neg_add : ∀ {a b : ISize}, -(a + b) = -a - b
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toLinearMap_injective : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S}
  {σ' : S →+* R} [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ],
  Function.Injective LinearEquiv.toLinearMap
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_congr : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  X =ᵐ[μ] Y → ProbabilityTheory.evariance X μ = ProbabilityTheory.evariance Y μ
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.untop.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : WithTop α) → x ≠ ⊤ → Sort u_2) (x : α) (x_1 : ↑x ≠ ⊤)
  (h_1 : (x : α) → (x_2 : ↑x ≠ ⊤) → motive (some x) x_2),
  (match some x, x_1 with
    | some x, x_2 => h_1 x x_2) =
    h_1 x x_1
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A locally uniform limit of continuous functions is continuous.  -/
TendstoLocallyUniformly.continuous : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι}, TendstoLocallyUniformly F f p → (∃ᶠ (n : ι) in p, Continuous (F n)) → Continuous f
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.SMulMemClass.coe_subtype : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] (S' : A), ⇑(SubMulAction.SMulMemClass.subtype S') = Subtype.val
-- Mathlib.Data.Int.Bitwise
Int.bodd_neg : ∀ (n : ℤ), (-n).bodd = n.bodd
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- The category of commutative algebras over a commutative ring `R` is the same as commutative
rings under `R`.  -/
commAlgCatEquivUnder : (R : CommRingCat) → CommAlgCat ↑R ≌ CategoryTheory.Under R
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
/-- Conditional expectation of the indicator of a measurable set with finite measure, in L2.  -/
MeasureTheory.condExpIndSMul : {α : Type u_1} →
  {G : Type u_5} →
    [inst : NormedAddCommGroup G] →
      {m m0 : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} →
          {s : Set α} → [NormedSpace ℝ G] → m ≤ m0 → MeasurableSet s → μ s ≠ ⊤ → G → ↥(MeasureTheory.Lp G 2 μ)
-- Mathlib.Order.ModularLattice
IsModularLattice.exists_inf_eq_and_codisjoint : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a b : α} [inst_2 : BoundedOrder α] [ComplementedLattice α],
  a ≤ b → ∃ b', b ⊓ b' = a ∧ Codisjoint b b'
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.isConnected_iff_final_of_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : Type w} [Unique T]
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)), CategoryTheory.IsConnected C ↔ F.Final
-- Mathlib.NumberTheory.NumberField.Cyclotomic.PID
/-- If `IsCyclotomicExtension {5} ℚ K` then `𝓞 K` is a principal ideal domain.  -/
IsCyclotomicExtension.Rat.five_pid : ∀ (K : Type u) [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {5} ℚ K],
  IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_sumPiEquivProdPi_symm : ∀ {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [inst : (i : δ ⊕ δ') → MeasurableSpace (α i)],
  ⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Summable.tsum_ofReal_lt_top : ∀ {α : Type u_1} {f : α → ℝ}, Summable f → ∑' (i : α), ENNReal.ofReal (f i) < ⊤
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.Array.mapM'.go : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      [Monad m] →
        (α → m β) → (as : Array α) → (i : ℕ) → { bs // bs.size = i } → i ≤ as.size → m { bs // bs.size = as.size }
-- Std.Data.ExtTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.ExtTreeMap.entryAtIdxD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → ℕ → α × β → α × β
-- Std.Data.ExtHashMap.Basic
/-- The notation `m[a]` or `m[a]'h` is preferred over calling this function directly.

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
`a ∈ m`.
 -/
Std.ExtHashMap.get : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [inst : EquivBEq α] → [inst_1 : LawfulHashable α] → (m : Std.ExtHashMap α β) → (a : α) → a ∈ m → β
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.pointReflection_self : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (x : P₁), (ContinuousAffineEquiv.pointReflection k x) x = x
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.State.mk.sizeOf_spec : ∀ (atoms : Std.HashMap Lean.Expr ℕ), sizeOf { atoms := atoms } = 1 + sizeOf atoms
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.setOfIdeal_eq_compl_singleton : ∀ {X : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X]
  (I : Ideal C(X, 𝕜)) [hI : I.IsMaximal], ∃ x, ContinuousMap.setOfIdeal I = {x}ᶜ
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_of_injOn : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (e : ι → κ),
  Set.InjOn e ↑s →
    Set.MapsTo e ↑s ↑t → (∀ i ∈ t, i ∉ e '' ↑s → g i = 0) → (∀ i ∈ s, f i = g (e i)) → ∑ i ∈ s, f i = ∑ j ∈ t, g j
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.darts_subset : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  p₂.IsSubwalk p₁ → p₂.darts ⊆ p₁.darts
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsMonHom.one_hom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.MonObj M} {inst_3 : CategoryTheory.MonObj N} (f : M ⟶ N) [self : CategoryTheory.IsMonHom f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ⊗ θ` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalHorizontalCompAux : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          Mathlib.Tactic.BicategoryLike.HorizontalComp →
            Mathlib.Tactic.BicategoryLike.HorizontalComp →
              Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Aesop.Tree.TreeM
Aesop.TreeM.Context.mk.inj : ∀ {currentIteration : Aesop.Iteration} {ruleSet : Aesop.LocalRuleSet} {currentIteration_1 : Aesop.Iteration}
  {ruleSet_1 : Aesop.LocalRuleSet},
  { currentIteration := currentIteration, ruleSet := ruleSet } =
      { currentIteration := currentIteration_1, ruleSet := ruleSet_1 } →
    currentIteration = currentIteration_1 ∧ ruleSet = ruleSet_1
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] [inst_5 : SizeOf ι] (val : ι → S) (σ' : S → MvPolynomial ι R)
  (aeval_val_σ' : ∀ (s : S), (MvPolynomial.aeval val) (σ' s) = s) (algebra : Algebra (MvPolynomial ι R) S)
  (algebraMap_eq :
    autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val))
      Algebra.Generators.algebraMap_eq._autoParam),
  sizeOf { val := val, σ' := σ', aeval_val_σ' := aeval_val_σ', algebra := algebra, algebraMap_eq := algebraMap_eq } =
    1 + sizeOf algebra + sizeOf algebraMap_eq
-- Init.Data.Int.Gcd
Int.lcm_eq_natAbs_left_iff_dvd : ∀ {a b : ℤ}, a.lcm b = a.natAbs ↔ b ∣ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey? k' = some k
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_comp_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], MvPowerSeries.constantCoeff.comp MvPowerSeries.C = RingHom.id R
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) (l : ℕ),
  (l = 0 → False) →
    CategoryTheory.Functor.OfSequence.map x_1 0 l.succ = fun x_2 =>
      CategoryTheory.CategoryStruct.comp (x_1 0) (CategoryTheory.Functor.OfSequence.map (fun n => x_1 (n + 1)) 0 l ⋯)
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLift_id : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L],
  galLift K L L (AlgHom.id A B) = AlgHom.id K L
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], ∅.minKey? = none
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.coeff_mul_of_add_lexOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ ψ : MvPowerSeries σ R} {p q : σ →₀ ℕ},
  φ.lexOrder = ↑(toLex p) →
    ψ.lexOrder = ↑(toLex q) →
      (MvPowerSeries.coeff (p + q)) (φ * ψ) = (MvPowerSeries.coeff p) φ * (MvPowerSeries.coeff q) ψ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.fst_mem_support_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {t u v w : V} (p : G.Walk v w), s(t, u) ∈ p.edges → t ∈ p.support
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.homCategory_id_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (Γ : F ⟶ G) (a : B),
  (CategoryTheory.CategoryStruct.id Γ).as.app a = CategoryTheory.CategoryStruct.id (Γ.app a)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- A finite coproduct in the category of a `SemilatticeSup` with `OrderBot` is the same as the
supremum.
 -/
CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {ι : Type u} [inst_2 : Fintype ι] (f : ι → α),
  ∐ f = Finset.univ.sup f
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_isBase_iff : ∀ {α : Type u_1} {E B : Set α}, (Matroid.freeOn E).IsBase B ↔ B = E
-- Mathlib.Analysis.CStarAlgebra.Fuglede
/-- A characterization of normal elements in a C⋆-algebra in terms of exponentials.  -/
isStarNormal_iff_forall_exp_mul_exp_mem_unitary : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A},
  IsStarNormal a ↔ ∀ (x : ℝ), NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) ∈ unitary A
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.eq_1 : ∀ (q k : ℕ), LucasLehmer.norm_num_ext.sModNatTR q k = LucasLehmer.norm_num_ext.sModNatTR.go✝ q k (4 % q)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.yonedaEquiv_δ_comp : ∀ {X : SSet} {n : ℕ} (g : SSet.stdSimplex.obj { len := n + 1 } ⟶ X) (i : Fin (n + 2)),
  SSet.yonedaEquiv (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) g) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) (SSet.yonedaEquiv g)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- there are unique morphisms to the object  -/
CategoryTheory.Limits.IsZero.unique_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → ∀ (Y : C), Nonempty (Unique (X ⟶ Y))
-- Mathlib.Data.EReal.Inv
EReal.div_self : ∀ {a : EReal}, a ≠ ⊥ → a ≠ ⊤ → a ≠ 0 → a / a = 1
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_map : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (s : Subfield K) (f : K →+* L),
  ↑(Subfield.map f s) = ⇑f '' ↑s