mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable functions into a vector bundle.
Version at a point  -/
mdifferentiableAt_totalSpace : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  (f : M → Bundle.TotalSpace F E) {x₀ : M},
  MDiffAt f x₀ ↔ (MDiffAt fun x => (f x).proj) x₀ ∧ (MDiffAt fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
-- Mathlib.Algebra.Group.Prod
Prod.instAddCancelMonoid : {M : Type u_3} → {N : Type u_4} → [AddCancelMonoid M] → [AddCancelMonoid N] → AddCancelMonoid (M × N)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coeFnLinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {N : Type u_6}
  [inst_4 : TopologicalSpace N] [inst_5 : ChartedSpace H N] {n : WithTop ℕ∞} {V : Type u_10}
  [inst_6 : NormedAddCommGroup V] [inst_7 : NormedSpace 𝕜 V] (a : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
  (a_1 : N), ContMDiffMap.coeFnLinearMap a a_1 = a a_1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sectionsMk_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (s : (X : Cᵒᵖ) → ↑(M.obj X))
  (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), (CategoryTheory.ConcreteCategory.hom (M.map f)) (s X) = s Y) (X : Cᵒᵖ),
  ↑(PresheafOfModules.sectionsMk s hs) X = s X
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.coherentTopology.eq_induced : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [inst_2 : F.PreservesFiniteEffectiveEpiFamilies] [inst_3 : F.ReflectsFiniteEffectiveEpiFamilies] [inst_4 : F.Full]
  [inst_5 : F.Faithful] [inst_6 : F.EffectivelyEnough] [inst_7 : CategoryTheory.Precoherent D],
  CategoryTheory.coherentTopology C = F.inducedTopology (CategoryTheory.coherentTopology D)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] {m : M}
  (f : CategoryTheory.ShiftedHom X Y m),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (CategoryTheory.Localization.SmallShiftedHom.mk W f) = f.map L
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.RightUnitorBimod.hom_inv_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S),
  CategoryTheory.CategoryStruct.comp (Bimod.RightUnitorBimod.hom P) (Bimod.RightUnitorBimod.inv P) =
    CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X P (Bimod.regular S))
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.mersenne_int_pos : ∀ {p : ℕ}, p ≠ 0 → 0 < 2 ^ p - 1
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.nonneg.eq_1 : ∀ (H : Type u_1) [inst : AddCommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedAddMonoid H],
  AddGroupCone.nonneg H = { toAddSubmonoid := AddSubmonoid.nonneg H, eq_zero_of_mem_of_neg_mem' := ⋯ }
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.rfl : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}, m.Equiv m
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instIsReduced : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [h : AlgebraicGeometry.IsReduced S],
  AlgebraicGeometry.IsReduced (AlgebraicGeometry.AffineSpace n S)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.containsThenInsertIfNew a b).2
-- Init.Control.Option
/-- Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
 -/
OptionT.run : {m : Type u → Type v} → {α : Type u} → OptionT m α → m (Option α)
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `algebraicClosure F E`
under the map `i` is equal to `algebraicClosure F K`.  -/
algebraicClosure.map_eq_of_algEquiv : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (i : E ≃ₐ[F] K),
  IntermediateField.map (↑i) (algebraicClosure F E) = algebraicClosure F K
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.cau_seq_zero_ne_one : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], ¬0 ≈ 1
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_algebraMap_tmul : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GSemiring 𝒜] [inst_9 : DirectSum.GAlgebra R 𝒜] (r : R) (b : DirectSum ι fun i => ℬ i),
  (TensorProduct.gradedComm R 𝒜 ℬ) ((algebraMap R (DirectSum ι fun i => 𝒜 i)) r ⊗ₜ[R] b) =
    b ⊗ₜ[R] (algebraMap R (DirectSum ι fun i => 𝒜 i)) r
-- Mathlib.RingTheory.Artinian.Module
/-- Any injective endomorphism of an Artinian module is surjective.  -/
IsArtinian.surjective_of_injective_endomorphism : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (f : M →ₗ[R] M), Function.Injective ⇑f → Function.Surjective ⇑f
-- Lean.Elab.PreDefinition.Structural.Basic
/-- Lets say we have `n` mutually recursive functions whose recursive arguments are from a group
of `m` mutually inductive data types. This mapping does not have to be one-to-one: for one type
there can be zero, one or more functions. We use the logic in the `FunPacker` modules to combine
the bodies (and motives) of multiple such functions.

Therefore we have to take the `n` functions, group them by their recursive argument's type,
and for each such type, keep track of the order of the functions.

We represent these positions as an `Array (Array Nat)`. We have that

* `positions.size = indInfo.numTypeFormers`
* `positions.flatten` is a permutation of `[0:n]`, so each of the `n` functions has exactly one
  position, and each position refers to one of the `n` functions.
* if `k ∈ positions[i]` then the recursive argument of function `k` is has type `indInfo.all[i]`
  (or corresponding nested inductive type)

 -/
Lean.Elab.Structural.Positions : Type
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.nsmul_modEq_nsmul : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} [IsAddTorsionFree M] {n : ℕ},
  n ≠ 0 → (n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p])
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.hom_id : ∀ {J : Type w} (X : CategoryTheory.Limits.WidePullbackShape J),
  CategoryTheory.Limits.WidePullbackShape.Hom.id X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Data.Set.Card
Set.encard_eq_add_one_iff : ∀ {α : Type u_1} {s : Set α} {k : ℕ∞}, s.encard = k + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
/-- Data for user-defined theorems marked with the `congr` attribute.

This type should be confused with `CongrTheorem` which represents different kinds of automatically
generated congruence theorems. The `simp` tactic also uses some of them.
 -/
Lean.Meta.SimpCongrTheorem : Type
-- Init.Data.BitVec.Basic
/-- Unsigned modulo for bitvectors. Usually accessed via the `%` operator.

SMT-LIB name: `bvurem`.
 -/
BitVec.umod : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonTextDocumentClientCapabilities : Lean.FromJson Lean.Lsp.TextDocumentClientCapabilities
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeriesTerm.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l),
  p.changeOriginSeriesTerm k l s hs = (ContinuousMultilinearMap.curryFinFinset 𝕜 E F hs ⋯) (p (k + l))
-- Mathlib.Analysis.Convex.Segment
/-- If `z = lineMap x y c` is a point on the line passing through `x` and `y`, then the open
segment `openSegment 𝕜 x y` is included in the union of the open segments `openSegment 𝕜 x z`,
`openSegment 𝕜 z y`, and the point `z`. Informally, `(x, y) ⊆ {z} ∪ (x, z) ∪ (z, y)`.  -/
openSegment_subset_union : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (x y : E) {z : E},
  z ∈ Set.range ⇑(AffineMap.lineMap x y) → openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.mk_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T} {A B : T}
  (f : A ⟶ B) (hf : P f), (CategoryTheory.MorphismProperty.Arrow.mk f hf).left = A
-- Std.Data.ExtDHashMap.Lemmas
/-- Variant of `get?_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtDHashMap.Const.get?_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.map f m) k =
    Option.pmap (fun v h' => f (m.getKey k h') v) (Std.ExtDHashMap.Const.get? m k) ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {U : TopologicalSpace.Opens X} (hU : Nonempty ↥U) {y : Y},
  y ∈ (e.subtypeRestr hU).target → (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y = ↑e.symm y
-- Mathlib.Data.Nat.Bitwise
Nat.lt_of_testBit : ∀ {n m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
-- Init.Data.Nat.Basic
Nat.sub_ne_zero_of_lt : ∀ {a b : ℕ}, a < b → b - a ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.uniqueUpToIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y}
  (hb : b.IsBilimit),
  (CategoryTheory.Limits.biprod.uniqueUpToIso X Y hb).hom = CategoryTheory.Limits.biprod.lift b.fst b.snd
-- Mathlib.Order.Interval.Set.Basic
Set.self_mem_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∈ Set.Ici a
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coeMonoidHom_injective : ∀ {ι : Type u_2} {R : Type u_3} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : CommRing R],
  Function.Injective ⇑Matrix.SpecialLinearGroup.coeMonoidHom
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.IsConj.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G) (s s' : S.Splitting), S.IsConj s s' = ∃ n, ⇑s = fun g => S.inl n * s' g * (S.inl n)⁻¹
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.denote.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x_1 : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Power.denote ctx { x := x_1, k := 1 } = Lean.Grind.CommRing.Var.denote ctx x_1
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.dense_span : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E), (Submodule.span 𝕜 (Set.range ⇑b)).topologicalClosure = ⊤
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- The ring homomorphism taking a multivariate power series `f(X)` to `f(aX)`.  -/
MvPowerSeries.rescale : {σ : Type u_1} → {R : Type u_9} → [inst : CommSemiring R] → (σ → R) → MvPowerSeries σ R →+* MvPowerSeries σ R
-- Mathlib.Order.Hom.Lattice
LatticeHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {f g : LatticeHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Order.Rel.GaloisConnection
/-- `leftDual` maps any set `J` of elements of type `α` to the set `{b : β | ∀ a ∈ J, a ~[R] b}` of
elements `b` of type `β` such that `a ~[R] b` for every element `a` of `J`.  -/
SetRel.leftDual : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set α → Set β
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.declLt : Lean.IR.Decl → Lean.IR.Decl → Bool
-- Mathlib.Data.Fintype.Powerset
Finset.univ_filter_card_eq : ∀ (α : Type u_1) [inst : Fintype α] (k : ℕ), {s | s.card = k} = Finset.powersetCard k Finset.univ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedSignature : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.Signature a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.detail? : Lean.Lsp.CallHierarchyItem → Option String
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getEntryLT k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      if hkky : compare k ky = Ordering.gt then Std.DTreeMap.Internal.Impl.getEntryLTD k r ⟨ky, y⟩
      else Std.DTreeMap.Internal.Impl.getEntryLT k l ⋯ ⋯
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.carrier_eq_coe : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Closeds α), s.carrier = ↑s
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_map_dualMap_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (W : Submodule R M) (f : N →ₗ[R] M),
  Submodule.map f.dualMap W.dualAnnihilator ≤ (Submodule.comap f W).dualAnnihilator
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.mul_one : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (x : OreLocalization S R),
  x * 1 = x
-- Lean.Parser.Extra
Lean.Parser.sepBy1Indent.formatter : Lean.PrettyPrinter.Formatter → String → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Sym.Lemmas
Lean.Sym.ite_cond_congr : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop) {inst' : Decidable c'},
  c = c' → (if c then a else b) = if c' then a else b
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.sub` -/
Differentiable.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 f → Differentiable 𝕜 g → Differentiable 𝕜 fun i => f i - g i
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentSymbol : Lean.ToJson Lean.Lsp.DocumentSymbol
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.compFlipUncurryIso_inv_app : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor B D)
  (G : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (X : C × B),
  (F.compFlipUncurryIso G).inv.app X = CategoryTheory.CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_map_vecMul : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} [inst : CommSemiring R] {S : Type u_9} [inst_1 : Semiring S]
  [inst_2 : Algebra R S] [inst_3 : Fintype ι] (b : Module.Basis ι R S) (v : ι' → S),
  Matrix.vecMul (⇑b) ((b.toMatrix v).map ⇑(algebraMap R S)) = v
-- Mathlib.Data.Finite.Defs
Finite.exists_equiv_fin : ∀ (α : Sort u_3) [h : Finite α], ∃ n, Nonempty (α ≃ Fin n)
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Dirac delta measures at two points are equal if every measurable set contains either both or
neither of the points.  -/
MeasureTheory.dirac_eq_dirac_iff_forall_mem_iff_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {x y : α},
  MeasureTheory.Measure.dirac x = MeasureTheory.Measure.dirac y ↔ ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
-- Mathlib.GroupTheory.Complement
AddSubgroup.RightTransversal.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.RightTransversal = { T // AddSubgroup.IsComplement (↑H) T }
-- Init.Data.Rat.Lemmas
Rat.neg_mul : ∀ (a b : ℚ), -a * b = -(a * b)
-- Lean.Elab.Tactic.Basic
/-- Returns the list of goals. Goals may or may not already be assigned.  -/
Lean.Elab.Tactic.getGoals : Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_empty : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {v : ι → F} (r : ι → F),
  (Lagrange.interpolate ∅ v) r = 0
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.symm_iff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.symm.IsImage t s ↔ e.IsImage s t
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_self : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n),
  (DirichletCharacter.changeLevel ⋯) χ = χ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {j : Fin (n + 3)} {i : Fin (n + 2)},
  j = i.castSucc →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (X.δ i) h)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loopyOn_isLoop_iff : ∀ {α : Type u_1} {e : α} {E : Set α}, (Matroid.loopyOn E).IsLoop e ↔ e ∈ E
-- Lean.Message
/-- If `true`, report range as given; see `msgToInteractiveDiagnostic`.  -/
Lean.BaseMessage.keepFullRange : {α : Type u} → Lean.BaseMessage α → Bool
-- Mathlib.Analysis.Fourier.Notation
FourierInvModule.fourierInv_add : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] (self : FourierInvModule R E F) (f g : E),
  FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g
-- Mathlib.Data.Finset.Max
/-- A version of `Finset.max'_image` with LHS and RHS reversed.
Also, this version assumes that `s` is nonempty, not its image.  -/
Monotone.map_finset_max' : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Monotone f → ∀ {s : Finset α} (h : s.Nonempty), f (s.max' h) = (Finset.image f s).max' ⋯
-- Mathlib.Tactic.CongrExclamation
/-- The maximum number of arguments to consider when doing congruence of function applications.
For example, with `f a b c = g w x y z`, setting `maxArgs := some 2` means it will only consider
either `f a b = g w x y` and `c = z` or `f a = g w x`, `b = y`, and `c = z`. Setting
`maxArgs := none` (the default) means no limit.

When the functions are dependent, `maxArgs` can prevent congruence from working at all.
In `Fintype.card α = Fintype.card β`, one needs to have `maxArgs` at `2` or higher since
there is a `Fintype` instance argument that depends on the first.

When there aren't such dependency issues, setting `maxArgs := some 1` causes `congr!` to
do congruence on a single argument at a time. This can be used in conjunction with the
iteration limit to control exactly how many arguments are to be processed by congruence.  -/
Congr!.Config.maxArgs : Congr!.Config → Option ℕ
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNatAux.eq_2 : ∀ (b q i : ℕ),
  LucasLehmer.norm_num_ext.sModNatAux b q i.succ = (LucasLehmer.norm_num_ext.sModNatAux b q i ^ 2 + (q - 2)) % q
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap.congr_simp : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] {X Y : C₁} (f f_1 : L₁.obj X ⟶ L₁.obj Y),
  f = f_1 → Φ.homMap L₁ L₂ f = Φ.homMap L₁ L₂ f_1
-- Mathlib.CategoryTheory.Shift.Localization
/-- In the context of localization of categories, if a functor
is induced by a functor which commutes with the shift, then
this functor commutes with the shift.  -/
CategoryTheory.Functor.commShiftOfLocalization : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (L : CategoryTheory.Functor C D) →
              (W : CategoryTheory.MorphismProperty C) →
                [L.IsLocalization W] →
                  (A : Type w) →
                    [inst_4 : AddMonoid A] →
                      [inst_5 : CategoryTheory.HasShift C A] →
                        (F : CategoryTheory.Functor C E) →
                          (F' : CategoryTheory.Functor D E) →
                            [CategoryTheory.Localization.Lifting L W F F'] →
                              [inst_7 : CategoryTheory.HasShift D A] →
                                [inst_8 : CategoryTheory.HasShift E A] →
                                  [L.CommShift A] → [F.CommShift A] → F'.CommShift A
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nndist_eq_iSup : ∀ {ι : Type u_2} [inst : Fintype ι] {β : ι → Type u_5} [inst_1 : (i : ι) → PseudoMetricSpace (β i)] (x y : PiLp ⊤ β),
  nndist x y = ⨆ i, nndist (x.ofLp i) (y.ofLp i)