mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_left_injective_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) [Invertible A], Function.Injective fun x => x * A
-- Mathlib.RingTheory.Polynomial.RationalRoot
/-- Rational root theorem part 2:
if `r : f.codomain` is a root of a polynomial over the ufd `A`,
then the denominator of `r` divides the leading coefficient  -/
den_dvd_of_is_root : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {p : Polynomial A} {r : K},
  (Polynomial.aeval r) p = 0 → ↑(IsFractionRing.den A r) ∣ p.leadingCoeff
-- Mathlib.Order.Monotone.Monovary
Antivary.symm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Antivary f g → Antivary g f
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If `M` is a commutative group that contains a primitive `n`th root of unity
and `a : ZMod n` is nonzero, then there exists a group homomorphism `φ` from the
additive group `ZMod n` to the multiplicative group `Mˣ` such that `φ a ≠ 1`.  -/
ZMod.exists_monoidHom_apply_ne_one : ∀ {M : Type u_7} [inst : CommMonoid M] {n : ℕ} [NeZero n],
  (∃ ζ, IsPrimitiveRoot ζ n) → ∀ {a : ZMod n}, a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.δ_simplex : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ),
  hl.δ.simplex =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.SimplicialObject.δ
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := m + 1 })
            (SSet.stdSimplex.obj { len := n }))
          l.castSucc))
      (x.cast hd).simplex
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.init.eq_1 : ∀ {α : Type u_1} {n : ℕ} (x : Fin (n + 1) ↪ α), Fin.Embedding.init x = { toFun := Fin.init ⇑x, inj' := ⋯ }
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.NatTrans.ofOpSequence_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor ℕᵒᵖ C}
  (app : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n))
  (naturality :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯).op) (app n) =
        CategoryTheory.CategoryStruct.comp (app (n + 1)) (G.map (CategoryTheory.homOfLE ⋯).op))
  (n : ℕᵒᵖ), (CategoryTheory.NatTrans.ofOpSequence app naturality).app n = app (Opposite.unop n)
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.repr_range : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), (↑b.repr).range = Finsupp.supported R R Set.univ
-- Mathlib.Topology.Compactness.Compact
IsCompact.prod : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  IsCompact s → IsCompact t → IsCompact (s ×ˢ t)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
/-- A literal natural number or a base + offset expression.  -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} [inst_1 : SizeOf C]
  [inst_2 : SizeOf ι] (iso : (i j : ι) → I.left (i, j) ≅ I.left (j, i))
  (iso_hom_fst : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.fst (j, i)) = I.snd (i, j))
  (iso_hom_snd : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.snd (j, i)) = I.fst (i, j))
  (fst_eq_snd : ∀ (i : ι), I.fst (i, i) = I.snd (i, i)),
  sizeOf { iso := iso, iso_hom_fst := iso_hom_fst, iso_hom_snd := iso_hom_snd, fst_eq_snd := fst_eq_snd } = 1
-- Mathlib.Data.ENat.Basic
ENat.le_natCast_iff : ∀ {n : ℕ∞} {k : ℕ}, n ≤ ↑k ↔ ∃ n₀, n = ↑n₀ ∧ n₀ ≤ k
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.End_toSemigroup_toMul_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (φ₁ φ₂ : A →ₗc[R] A), φ₁ * φ₂ = φ₁.comp φ₂
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_if : ∀ {m n : ℤ}, (m...=n).toArray = if m ≤ n then #[m] ++ ((m + 1)...=n).toArray else #[]
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Adj.toWalk.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk = h.toWalk
-- Init.PropLemmas
forall_eq' : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∀ (a : α), a' = a → p a) ↔ p a'
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D'),
  (CategoryTheory.CostructuredArrow.prodEquivalence S S' T T').functor =
    CategoryTheory.CostructuredArrow.prodFunctor S S' T T'
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_neg_toReal_eq : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal), (-f.toReal).nnrealPart = 0
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
/-- `circleMap` is `2π`-periodic.  -/
periodic_circleMap : ∀ (c : ℂ) (R : ℝ), Function.Periodic (circleMap c R) (2 * Real.pi)
-- Mathlib.Topology.ContinuousMap.Compact
BoundedContinuousFunction.norm_toContinuousMap_eq : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : BoundedContinuousFunction α E), ‖f.toContinuousMap‖ = ‖f‖
-- Mathlib.Probability.Martingale.Basic
/-- A family of integrable functions `f : ι → Ω → E` is a submartingale with respect to a
filtration `ℱ` if `f` is strongly adapted with respect to `ℱ` and for all `i ≤ j`,
`f i ≤ᵐ[μ] μ[f j | ℱ.le i]`.  -/
MeasureTheory.Submartingale : {Ω : Type u_1} →
  {E : Type u_2} →
    {ι : Type u_3} →
      [inst : Preorder ι] →
        {m0 : MeasurableSpace Ω} →
          [inst_1 : NormedAddCommGroup E] →
            [NormedSpace ℝ E] → [LE E] → (ι → Ω → E) → MeasureTheory.Filtration ι m0 → MeasureTheory.Measure Ω → Prop
-- Mathlib.Topology.Order
WithTopology.nontrivialTopology_iff : ∀ {α : Type u} {t : TopologicalSpace α}, NontrivialTopology (WithTopology α t) ↔ t ≠ ⊤
-- Mathlib.Topology.Order.Monotone
/-- An antitone function continuous at the infimum of a nonempty set sends this infimum to
the supremum of the image of this set.  -/
AntitoneOn.map_csInf_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousWithinAt f A (sInf A) →
    AntitoneOn f A →
      A.Nonempty →
        autoParam (BddBelow A) AntitoneOn.map_csInf_of_continuousWithinAt._auto_1 → f (sInf A) = sSup (f '' A)
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_eq_iInter_inter : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  {v : Set τ}, v ∈ f → omegaLimit f ϕ s = ⋂ u, closure (Set.image2 ϕ (↑u ∩ v) s)
-- Init.Data.Vector.Find
Vector.find?_replicate_of_neg : ∀ {α : Type} {p : α → Bool} {n : ℕ} {a : α}, ¬p a = true → Vector.find? p (Vector.replicate n a) = none
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankLeOne.mk : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        {v : Valuation R Γ₀} →
          (hom' : (MonoidWithZeroHom.ofClass v).ValueGroup₀ →*₀ NNReal) → StrictMono ⇑hom' → v.RankLeOne
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}, 0 ≤ a → ↑⌊a⌋₊ ≤ a
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.set.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → α → Sort u_2) (a : α) (as : List α) (n : ℕ) (b : α)
  (h_1 : (head : α) → (as : List α) → (b : α) → motive (head :: as) 0 b)
  (h_2 : (a : α) → (as : List α) → (n : ℕ) → (b : α) → motive (a :: as) n.succ b)
  (h_3 : (x : ℕ) → (x_1 : α) → motive [] x x_1),
  (match a :: as, n.succ, b with
    | head :: as, 0, b => h_1 head as b
    | a :: as, n.succ, b => h_2 a as n b
    | [], x, x_1 => h_3 x x_1) =
    h_2 a as n b
-- Mathlib.CategoryTheory.Limits.Final
/-- The hypotheses also imply that `F` is final, see `final_of_comp_full_faithful`.  -/
CategoryTheory.Functor.final_of_comp_full_faithful' : ∀ {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 D)
  (G : CategoryTheory.Functor D E) [G.Full] [G.Faithful] [(F.comp G).Final], G.Final
-- Mathlib.Data.Fin.SuccPred
Fin.one_succAbove_one : ∀ {n : ℕ}, Fin.succAbove 1 1 = 2
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Left duals are isomorphic.  -/
CategoryTheory.leftDualIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X₁ X₂ Y : C} → CategoryTheory.ExactPairing X₁ Y → CategoryTheory.ExactPairing X₂ Y → (X₁ ≅ X₂)
-- Mathlib.Data.List.SplitBy
List.isChain_getLast_head_splitBy : ∀ {α : Type u_1} (r : α → α → Bool) (l : List α),
  List.IsChain (fun a b => ∃ (ha : a ≠ []) (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (List.splitBy r l)
-- Mathlib.Order.Filter.Basic
Filter.eventually_principal : ∀ {α : Type u} {a : Set α} {p : α → Prop}, (∀ᶠ (x : α) in Filter.principal a, p x) ↔ ∀ x ∈ a, p x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit =
    { functor := CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C,
      inverse := CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C,
      unitIso := CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso C,
      counitIso := CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso C, functor_unitIso_comp := ⋯ }
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the topologies of uniform convergence and pointwise convergence induce
the same topology on `ι`.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.

This is a consequence of `Equicontinuous.comap_uniformFun_eq`, stated in terms of `IsInducing`
for convenience.  -/
Equicontinuous.inducing_uniformFun_iff_pi : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] [CompactSpace X],
  Equicontinuous F → (Topology.IsInducing (⇑UniformFun.ofFun ∘ F) ↔ Topology.IsInducing F)
-- Mathlib.Topology.Separation.Basic
/-- Limits are unique up to separability.

A weaker version of `tendsto_nhds_unique` for `R1Space`.  -/
tendsto_nhds_unique_inseparable : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [R1Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot],
  Filter.Tendsto f l (nhds a) → Filter.Tendsto f l (nhds b) → Inseparable a b
-- Mathlib.Algebra.Group.Irreducible.Defs
of_irreducible_mul : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Irreducible (a * b) → IsUnit a ∨ IsUnit b
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp F.toRightDerivedZero
      (CategoryTheory.CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom h) =
    h
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.padicNormE.is_norm : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ_[p]), ↑(padicNormE q) = ‖q‖
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
AddMonoidAlgebra.mem_vaddAntidiagonal_of_addGroup : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G P]
  [inst_2 : Semiring R] [inst_3 : Zero V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) (gh : G × P),
  gh ∈ Finset.VAddAntidiagonal p ⋯ ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = -gh.1 +ᵥ p
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.const_mul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Mul γ] [MeasurableMul γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => c * f x) (fun x => c * g x) μ ν
-- Mathlib.Logic.Equiv.Defs
Equiv.sigmaEquivProd_symm_apply : ∀ (α : Type u_1) (β : Type u_2) (a : α × β), (Equiv.sigmaEquivProd α β).symm a = ⟨a.1, a.2⟩
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringRightPreservesLimits : ∀ {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 : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v_2, u_2} D]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v_2, v_3, u_2, u_3} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', max u_1 v_2, max u_1 v_3, max (max (max u_1 u_2) v_1) v_2,
      max (max (max u_1 u_3) v_1) v_3}
    ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
-- Mathlib.RingTheory.Valuation.Basic
/-- A valuation on an `A`-algebra `B` is trivial on constants if the nonzero elements of the
base ring `A` are mapped to `1`.

This is true, for example, when `A` is a finite field.
See `Valuation.FiniteField.instIsTrivialOn`.  -/
Valuation.IsTrivialOn : {Γ₀ : Type u_4} →
  [inst : LinearOrderedCommMonoidWithZero Γ₀] →
    {B : Type u_7} →
      (A : Type u_8) → [inst_1 : CommSemiring A] → [inst_2 : Ring B] → [Algebra A B] → Valuation B Γ₀ → Prop
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.addSubgroupOfClosure_apply : ∀ {M : Type u_7} {R : Type u_8} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : IsAddTorsionFree R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M)
  (h : A = AddSubgroup.closure (Set.range ⇑b)) (i : ι), ↑((Module.Basis.addSubgroupOfClosure A b h) i) = b i
-- Mathlib.NumberTheory.LSeries.ZetaZeros
/-- The complement of the zero set of `riemannZeta` is codiscrete.  -/
_private.Mathlib.NumberTheory.LSeries.ZetaZeros.0.compl_riemannZetaZeros_mem_codiscrete : riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ
-- Mathlib.Dynamics.Flow
Flow.instInhabited : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] → [inst_1 : TopologicalSpace α] → [inst_2 : AddZero τ] → Inhabited (Flow τ α)
-- Mathlib.Combinatorics.Derangements.Finite
card_derangements_fin_add_two : ∀ (n : ℕ),
  Fintype.card ↑(derangements (Fin (n + 2))) =
    (n + 1) * Fintype.card ↑(derangements (Fin n)) + (n + 1) * Fintype.card ↑(derangements (Fin (n + 1)))
-- Mathlib.Algebra.BigOperators.Group.List.Basic
Commute.list_prod_right : ∀ {M : Type u_4} [inst : Monoid M] (l : List M) (y : M), (∀ x ∈ l, Commute y x) → Commute y l.prod
-- Mathlib.Data.FunLike.Group
FunLike.coe_coeMulHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [inst_3 : IsMulApply F α β], ⇑(FunLike.coeMulHom F α β) = DFunLike.coe
-- Init.Data.Nat.ToString
Nat.three_eq_digitChar : ∀ {n : ℕ}, '3' = n.digitChar ↔ n = 3
-- Mathlib.Topology.Perfect
IsOpen.perfect_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PerfectSpace α] {U : Set α}, IsOpen U → Perfect (closure U)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableWithinAt.congr_mono : ∀ {𝕜 : 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] {f f₁ : E → F} {x : E} {s t : Set E},
  DifferentiableWithinAt 𝕜 f s x → Set.EqOn f₁ f t → f₁ x = f x → t ⊆ s → DifferentiableWithinAt 𝕜 f₁ t x
-- Mathlib.Computability.Language
Language.mul_self_kstar_comm : ∀ {α : Type u_1} (l : Language α), KStar.kstar l * l = l * KStar.kstar l
-- Mathlib.Data.Set.Card
/-- A tactic useful for transferring proofs for `encard` to their corresponding `card` statements  -/
Set.tacticTo_encard_tac : Lean.ParserDescr
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.inf : {α : Type u_1} → [inst : HeytingAlgebra α] → Min (Heyting.Regular α)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.toList_flatMapAfterM.match_1.eq_2 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3) (it₂ : Std.IterM m γ)
  (h_1 : Unit → motive none) (h_2 : (it₂ : Std.IterM m γ) → motive (some it₂)),
  (match some it₂ with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_2 it₂
-- Mathlib.Algebra.Group.Defs
/-- Note that most of the lemmas about powers of two refer to it as `sq`.  -/
pow_two : ∀ {M : Type u_2} [inst : Monoid M] (a : M), a ^ 2 = a * a
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- The length one sequence `(o)` is a fundamental sequence for `o + 1`.  -/
Ordinal.IsFundamentalSeq.add_one : ∀ (o : Ordinal.{u_1}), Ordinal.IsFundamentalSeq fun x => ⟨o, ⋯⟩
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- **Alias** of `Finset.card_smul_finset_le`. -/
Finset.smul_finset_card_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α}, (a • s).card ≤ s.card
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.Context.xs : Lean.Meta.Grind.Collector.Context✝ → Array Lean.Expr
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowMap_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (i : J) (hi : i ≤ j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap F i i ⋯ hi =
    CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.id (F.obj ⟨i, hi⟩))
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.isUnsat : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Bool
-- Mathlib.Topology.Constructions
Topology.IsInducing.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i},
  (∀ (i : ι), Topology.IsInducing (f i)) → Topology.IsInducing (Pi.map f)
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.mk.inj : ∀ {rw : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma}
  {grw : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma}
  {app : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma}
  {appAt : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma}
  {rw_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma}
  {grw_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma}
  {app_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma}
  {appAt_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma},
  { rw := rw, grw := grw, app := app, appAt := appAt } = { rw := rw_1, grw := grw_1, app := app_1, appAt := appAt_1 } →
    rw = rw_1 ∧ grw = grw_1 ∧ app = app_1 ∧ appAt = appAt_1
-- Mathlib.Algebra.Order.Ring.Cone
/-- Interpret a cone in a ring as a cone in the underlying additive group.  -/
RingCone.toAddGroupCone : {R : Type u_1} → [inst : Ring R] → RingCone R → AddGroupCone R
-- Init.Data.String.Decode
ByteArray.utf8EncodeChar_utf8DecodeChar : ∀ {b : ByteArray} {i : ℕ} {h : (b.utf8DecodeChar? i).isSome = true},
  (String.utf8EncodeChar (b.utf8DecodeChar i h)).toByteArray = b.extract i (i + (b.utf8DecodeChar i h).utf8Size)
-- Mathlib.Algebra.Group.Prod
AddHom.comp_coprod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : AddCommSemigroup P]
  {Q : Type u_6} [inst_3 : AddCommSemigroup Q] (h : P →ₙ+ Q) (f : M →ₙ+ P) (g : N →ₙ+ P),
  h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
-- Mathlib.Data.Set.Basic
Set.eq_or_ssubset_of_subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s = t ∨ s ⊂ t
-- Mathlib.Topology.Homeomorph.TransferInstance
/-- Transfer a `TopologicalSpace` across an `Equiv`  -/
Equiv.topologicalSpace : {α : Type u_2} → {β : Type u_3} → [TopologicalSpace β] → α ≃ β → TopologicalSpace α
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app : ∀ (R : CommRingCatᵒᵖ),
  AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app R =
    (CommRingCat.ofHom
        (algebraMap (↑R.1)
          ((AlgebraicGeometry.structureSheafInType ↑(Opposite.unop R) ↑(Opposite.unop R)).obj.obj (Opposite.op ⊤)))).op
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y),
  P.isoModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_map : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → γ} (it : Std.IterM m β),
  (Std.IterM.map f it).toArray = (fun x => Array.map f x) <$> it.toArray
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_eq_self : ∀ {R : Type u_3} {c₃ : R} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {c₁ c₂ : R}
  {a : QuaternionAlgebra R c₁ c₂ c₃}, star a = a ↔ a = ↑a.re
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.unique_zsmul_zmod : ∀ {α : Type u_1} {a : α} [inst : AddGroup α] [inst_1 : Fintype α],
  (∀ (x : α), x ∈ AddSubgroup.zmultiples a) → ∀ (x : α), ∃! n, x = n.val • a
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualCoannihilator_dualAnnihilator_dualCoannihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (U : Submodule R (Module.Dual R M)), U.dualCoannihilator.dualAnnihilator.dualCoannihilator = U.dualCoannihilator
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.set_smul_eq_of_le : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (s : Set S) (N p : Submodule R M),
  (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → p ≤ s • N → s • N = p