mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If you add multiples of previous columns to the next columns, the determinant doesn't change.  -/
Matrix.det_eq_of_forall_col_eq_smul_add_pred : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R} (c : Fin n → R),
  (∀ (i : Fin (n + 1)), A i 0 = B i 0) →
    (∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc) → A.det = B.det
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceE_g : ∀ {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]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_3),
  (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g =
    CategoryTheory.Limits.biprod.lift ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃))
      (X.δ f₁ f₂₃ n₁ n₂ ⋯)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldr_eq_foldr_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : α → β → δ → δ}
  {init : δ}, Std.TreeMap.Raw.foldr f init t = Array.foldr (fun a b => f a.1 a.2 b) init t.toArray
-- Mathlib.Topology.Sequences
/-- A set is sequentially closed if it is closed.  -/
IsClosed.isSeqClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → IsSeqClosed s
-- Mathlib.Data.Set.Insert
Set.uniqueSingleton : {α : Type u_1} → (a : α) → Unique ↑{a}
-- Mathlib.Order.Interval.Set.Image
StrictAnti.mapsTo_Ico : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAnti f → Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → Y.Opens),
  iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_def : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G), ‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i, ‖m i‖}
-- Init.Data.SInt.Bitwise
Int16.toInt8_xor : ∀ (a b : Int16), (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Any object `J : CardinalDirectedPoset κ` is a colimit
of its subsets that are of cardinality `< κ` and have a terminal object.  -/
CategoryTheory.CardinalDirectedPoset.isColimitCocone : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] → (J : CategoryTheory.CardinalDirectedPoset κ) → CategoryTheory.Limits.IsColimit J.cocone
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.liftHomology_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : A ⟶ S.opcycles)
  (hk : CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0) {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.liftHomology k hk) (CategoryTheory.CategoryStruct.comp S.homologyι h) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.Algebra.Group.Prod
Prod.instAddCommSemigroup : {G : Type u_1} → {H : Type u_2} → [AddCommSemigroup G] → [AddCommSemigroup H] → AddCommSemigroup (G × H)
-- Mathlib.Computability.DFA
DFA.mk : {α : Type u} → {σ : Type v} → (σ → α → σ) → σ → Set σ → DFA α σ
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles in a vector space are translation invariant.  -/
EuclideanGeometry.angle_const_add : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v v₁ v₂ v₃ : V),
  EuclideanGeometry.angle (v + v₁) (v + v₂) (v + v₃) = EuclideanGeometry.angle v₁ v₂ v₃
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (e : C ≌ D),
  (CategoryTheory.Equivalence.symmEquivFunctor C D).obj e = Opposite.op e.symm
-- Std.Http.Data.Status
/-- Proof that the code does not clash with any named `Status` constructor.
 -/
Std.Http.CustomStatus.validUnknown : ∀ (self : Std.Http.CustomStatus), ¬Std.Http.isKnownStatusCode self.code = true
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier integral converts right-translation into scalar multiplication by a phase factor.  -/
VectorFourier.fourierIntegral_comp_add_right : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] [MeasurableAdd V] (e : AddChar 𝕜 Circle)
  (μ : MeasureTheory.Measure V) [μ.IsAddRightInvariant] (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (v₀ : V),
  VectorFourier.fourierIntegral e μ L (f ∘ fun v => v + v₀) = fun w =>
    e ((L v₀) w) • VectorFourier.fourierIntegral e μ L f w
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableOn.clm_apply : ∀ {𝕜 : 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_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M}, MDiff[s] g → MDiff[s] f → MDiff[s] fun x => (g x) (f x)
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.exists_quasiIso_injective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C] (K : CochainComplex.Plus C) (n : ℤ) [K.obj.IsStrictlyGE n],
  ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), ∃ i, CochainComplex.Plus.quasiIso C i
-- Mathlib.Data.Nat.BinaryRec
/-- A recursion principle for `bit` representations of natural numbers.
For a predicate `motive : Nat → Sort u`, if instances can be
constructed for natural numbers of the form `bit b n`,
they can be constructed for all natural numbers.  -/
Nat.binaryRec : {motive : ℕ → Sort u} → motive 0 → ((b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)) → (n : ℕ) → motive n
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPurePure_1 : ∀ (φ : Prop), Std.Do.SPred.Tactic.IsPure ⌜φ⌝ φ
-- Mathlib.Order.Hom.CompleteLattice
/-- Composition of `FrameHom`s as a `FrameHom`.  -/
FrameHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : CompleteLattice α] →
        [inst_1 : CompleteLattice β] → [inst_2 : CompleteLattice γ] → FrameHom β γ → FrameHom α β → FrameHom α γ
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.instNonemptyOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty],
  P.op.Nonempty
-- Mathlib.ModelTheory.Encoding
/-- Encodes a term as a list of variables and function symbols.  -/
FirstOrder.Language.Term.listEncode : {L : FirstOrder.Language} → {α : Type u'} → L.Term α → List (α ⊕ (i : ℕ) × L.Functions i)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom`  -/
AddMonoidAlgebra.liftNCAlgHom : {R : Type u_1} →
  {A : Type u_4} →
    {B : Type u_5} →
      {M : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddMonoid M] →
            [inst_2 : Semiring A] →
              [inst_3 : Algebra R A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] →
                    (f : A →ₐ[R] B) →
                      (g : Multiplicative M →* B) →
                        (∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)) → AddMonoidAlgebra A M →ₐ[R] B
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.coe_top : ∀ {M : Type u_1} [inst : Add M], ↑⊤ = Set.univ
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_eq_empty_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R}, x.support = ∅ ↔ x = 0
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.SymmGen.of_le`. -/
LE.le.symmGen : ∀ {α : Type u_7} [inst : LE α] {a b : α}, a ≤ b → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.overObj_iff : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] {W : CategoryTheory.MorphismProperty T} {X : T}
  (Y : CategoryTheory.Over X), W.overObj Y ↔ W Y.hom
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.isBasis_inter_ground : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → M.IsBasis I (X ∩ M.E)
-- Mathlib.Algebra.Star.TransferInstance
/-- Transfer `InvolutiveStar` across an `Equiv`. See note [reducible non-instances].  -/
Equiv.involutiveStar : {R : Type u_1} → {S : Type u_2} → R ≃ S → [InvolutiveStar S] → InvolutiveStar R
-- Batteries.Lean.PersistentHashSet
Lean.PersistentHashSet.instForInOfMonad_batteries : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → {m : Type u_2 → Type u_3} → [Monad m] → ForIn m (Lean.PersistentHashSet α) α
-- Mathlib.Algebra.Lie.Weights.Basic
/-- If `M` is a representation of a Lie algebra `L` and `χ : L → R` is a family of scalars,
then `weightSpace M χ` is the intersection of the `χ x`-eigenspaces
of the action of `x` on `M` as `x` ranges over `L`.  -/
LieModule.weightSpace : {R : Type u_2} →
  {L : Type u_3} →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → (L → R) → LieSubmodule R L M
-- Mathlib.Order.Sublattice
Sublattice.map_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {f : LatticeHom α β},
  Monotone (Sublattice.map f)
-- Mathlib.Algebra.Star.Module
/-- Note that this lemma holds for an arbitrary `ℚ≥0`-action, rather than merely one coming from a
`DivisionSemiring`. We keep both the `nnqsmul` and `nnrat_smul` naming conventions for
discoverability. See `star_nnrat_smul`.  -/
star_nnqsmul : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : StarAddMonoid R] [inst_2 : Module ℚ≥0 R] (q : ℚ≥0) (x : R),
  star (q • x) = q • star x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'},
      List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
        ⟨k, v⟩ ∈ l → (t.insertMany l).getD k' fallback = cast ⋯ v
-- Init.Data.Vector.Basic
/-- Returns `true` with the monad if `p` returns `true` for any element of the vector.  -/
Vector.anyM : {m : Type → Type u_1} → {α : Type u_2} → {n : ℕ} → [Monad m] → (α → m Bool) → Vector α n → m Bool
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_nil : ∀ {m n : ℤ}, n < m → (m...=n).toList = []
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.instBEqExprVisited : BEq Lean.Meta.Canonicalizer.ExprVisited
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ext : ∀ {α : Type u_1} {x y : Matroid α}, x.E = y.E → x.IsBase = y.IsBase → x.Indep = y.Indep → x = y
-- Mathlib.Util.AtomM
/-- The context (read-only state) of the `AtomM` monad.  -/
Mathlib.Tactic.AtomM.Context : Type
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.lsmul_apply_apply : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [inst_4 : Module S M] (s : S) (x : RestrictScalars R S M),
  ((RestrictScalars.lsmul R S M) s) x = (RestrictScalars.addEquiv R S M).symm (s • (RestrictScalars.addEquiv R S M) x)
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.addLeftMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)], AddLeftMono (Colex (Π₀ (i : ι), α i))
-- Init.Data.Array.Lemmas
Array.getElem_of_append : ∀ {α : Type u_1} {a : α} {i : ℕ} {xs ys zs : Array α} (eq : xs = ys.push a ++ zs) (h : ys.size = i), xs[i] = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.mono_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C},
  sq.IsPullback → ∀ [CategoryTheory.Mono sq.f₂₄], CategoryTheory.Mono sq.f₁₃
-- Init.PropLemmas
Bool.ite_else_true : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then x else true) = true ↔ ¬p ∨ x = true
-- Mathlib.Data.Sigma.Basic
PSigma.decidableEq : {α : Sort u_1} → {β : α → Sort u_2} → [h₁ : DecidableEq α] → [h₂ : (a : α) → DecidableEq (β a)] → DecidableEq (PSigma β)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
LinearOrderedCommGroupWithZero.zpow_neg' : ∀ {α : Type u_3} [self : LinearOrderedCommGroupWithZero α] (n : ℕ) (a : α), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Std.Time.Zoned.ZoneRules
/-- Returns the transition time as a `Timestamp`.
 -/
Std.Time.TimeZone.Transition.timestamp : Std.Time.TimeZone.Transition → Std.Time.Timestamp
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instSecondCountableTopology : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X] [SecondCountableTopology X],
  SecondCountableTopology (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).pt = F.obj (Opposite.op (iSup U))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map from the short complex
`(G × G × G →₀ A) --d₃₂--> (G × G →₀ A) --d₂₁--> (G →₀ A)` to
`(H × H × H →₀ B) --d₃₂--> (H × H →₀ B) --d₂₁--> (H →₀ B)`.  -/
groupHomology.mapShortComplexH2 : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} →
            (f : G →* H) → (A ⟶ Rep.res f B) → (groupHomology.shortComplexH2 A ⟶ groupHomology.shortComplexH2 B)
-- Mathlib.Algebra.Lie.Submodule
/-- A morphism of Lie modules `f : M → N` whose values lie in a Lie submodule `P ⊆ N` can be
restricted to a morphism of Lie modules `M → P`.  -/
LieModuleHom.codRestrict : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup N] →
                    [inst_6 : Module R N] →
                      [inst_7 : LieRingModule L N] →
                        (P : LieSubmodule R L N) → (f : M →ₗ⁅R,L⁆ N) → (∀ (m : M), f m ∈ P) → M →ₗ⁅R,L⁆ ↥P
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.sieve₁'_refineOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  [inst_1 : E.HasPullbacks]
  (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀),
  (E.refineOneHypercover F).sieve₁' i j = (F i j).sieve₀
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Context.mk.injEq : ∀ (ctx : Lean.Meta.Simp.Context) (simp : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result)
  (ctx_1 : Lean.Meta.Simp.Context) (simp_1 : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result),
  ({ ctx := ctx, simp := simp } = { ctx := ctx_1, simp := simp_1 }) = (ctx = ctx_1 ∧ simp = simp_1)
-- Mathlib.SetTheory.Cardinal.Defs
/-- A cardinal lifted to the same universe equals itself.  -/
Cardinal.lift_id : ∀ (a : Cardinal.{u}), Cardinal.lift.{u, u} a = a
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.match_1.eq_1 : ∀ (motive : Lean.Grind.IntInterval → Lean.Grind.IntInterval → Sort u_1) (a a_1 b b_1 : ℤ)
  (h_1 : (a a_2 b b_2 : ℤ) → motive (Lean.Grind.IntInterval.co a a_2) (Lean.Grind.IntInterval.co b b_2))
  (h_2 : (a b : ℤ) → motive (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b))
  (h_3 : (a b : ℤ) → motive (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii)
  (h_5 : (x x_1 : Lean.Grind.IntInterval) → motive x x_1),
  (match Lean.Grind.IntInterval.co a a_1, Lean.Grind.IntInterval.co b b_1 with
    | Lean.Grind.IntInterval.co a a_2, Lean.Grind.IntInterval.co b b_2 => h_1 a a_2 b b_2
    | Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b => h_2 a b
    | Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b => h_3 a b
    | Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii => h_4 ()
    | x, x_1 => h_5 x x_1) =
    h_1 a a_1 b b_1
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of a tuple of elements of `K`.  -/
Height.logHeight : {K : Type u_1} → [inst : Field K] → [Height.AdmissibleAbsValues K] → {ι : Type u_2} → (ι → K) → ℝ
-- Init.Data.Nat.Basic
Nat.add_le_add_left : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), k + n ≤ k + m
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidate.mk : Lean.Elab.Structural.IndGroupInst → Array Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.RecArgCandidate
-- Mathlib.Algebra.Algebra.Unitization
/-- **Alias** of the forward direction of `Unitization.isSelfAdjoint_inr`. -/
IsSelfAdjoint.of_inr : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarAddMonoid R] [inst_2 : Star A] {a : A},
  IsSelfAdjoint ↑a → IsSelfAdjoint a
-- Mathlib.Data.Rel
SetRel.comp_subset_self : ∀ {α : Type u_1} {R : SetRel α α} [R.IsTrans], R.comp R ⊆ R
-- Mathlib.Analysis.LocallyConvex.Polar
/-- The map `B.polar : Set E → Set F` forms an order-reversing Galois connection with
`B.flip.polar : Set F → Set E`. We use `OrderDual.toDual` and `OrderDual.ofDual` to express
that `polar` is order-reversing.  -/
LinearMap.polar_gc : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜),
  GaloisConnection (⇑OrderDual.toDual ∘ B.polar) (B.flip.polar ∘ ⇑OrderDual.ofDual)
-- Mathlib.Algebra.Group.Units.Defs
Units.val_injective : ∀ {α : Type u} [inst : Monoid α], Function.Injective Units.val
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.mk.sizeOf_spec : ∀ (graph : Array (Array (Option (Array (Option ℕ))))) (revDeps : Array (Array (Array ℕ))),
  sizeOf { graph := graph, revDeps := revDeps } = 1 + sizeOf graph + sizeOf revDeps
-- Mathlib.Algebra.Group.Units.Defs
Units.instMulOneClass.eq_1 : ∀ {α : Type u} [inst : Monoid α],
  Units.instMulOneClass = { toOne := Units.instOne, toMul := Units.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_one : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.inv.app CategoryTheory.Limits.WalkingParallelPair.one =
  CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingParallelPair.one
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
IsMIntegralCurveOn.comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ},
  IsMIntegralCurveOn γ v s → ∀ (dt : ℝ), IsMIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s}
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.eq_iff_eq : ∀ {K : Type u_1} [inst : Field K] (x : K) (r : ℝ),
  (∀ (w : NumberField.InfinitePlace K), w x = r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ = r
-- Mathlib.Algebra.Module.Torsion.Basic
/-- See also `iSupIndep.linearIndependent` which provides the same conclusion
but requires the stronger hypothesis `Module.IsTorsionFree R M`.  -/
Ideal.iSupIndep.linearIndependent' : ∀ {ι : Type u_3} {R : Type u_4} {M : Type u_5} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M],
  (iSupIndep fun i => R ∙ v i) → (∀ (i : ι), Ideal.torsionOf R M (v i) = ⊥) → LinearIndependent R v
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_surjective`. -/
Submodule.linearProjOfIsCompl_surjective : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), Function.Surjective ⇑(p.projectionOnto q h)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Misc
/-- Let `M` be a `(n+1) × n` matrix whose row sums to zero. Then all the matrices obtained by
deleting one row have the same determinant up to a sign.  -/
Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin n) R),
  ∑ j, M j = 0 →
    ∀ (j₁ j₂ : Fin (n + 1)),
      (M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.symm_dual_id : ∀ {α : Type u_2} [inst : SupSet α], sSupHom.dual.symm (sInfHom.id αᵒᵈ) = sSupHom.id α
-- Mathlib.Order.OrderDual
OrderDual.ofDual_comp_toDual : ∀ {α : Type u_1}, ⇑OrderDual.ofDual ∘ ⇑OrderDual.toDual = id
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.closedCell_subset_skeletonLT`. -/
Topology.CWComplex.closedCell_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.not_isUnit_X_sub_C : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] (r : R), ¬IsUnit (Polynomial.X - Polynomial.C r)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.ofCompId_left_as : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (t :
    CategoryTheory.Bicategory.LeftExtension f
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))),
  t.ofCompId.left.as = PUnit.unit
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_p_lt_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ‖↑p‖ < 1
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_eq_toL1_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : α → β) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ),
  MeasureTheory.Integrable.toL1 f hf = MeasureTheory.Integrable.toL1 g hg ↔ f =ᵐ[μ] g