mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Util.Qq
/-- Join a list of elements of type `α` into a container `β`.

Usually `β` is `q(Multiset α)` or `q(Finset α)` or `q(Set α)`.

As an example
```lean
mkSetLiteralQ q(Finset ℝ) (List.range 4 |>.map fun n : ℕ ↦ q($n•π))
```
produces the expression `{0 • π, 1 • π, 2 • π, 3 • π} : Finset ℝ`.
 -/
Qq.mkSetLiteralQ : {u v : Lean.Level} →
  {α : Q(Type u)} →
    (β : Q(Type v)) →
      List Q(«$α») →
        autoParam Q(EmptyCollection «$β») Qq.mkSetLiteralQ._auto_1 →
          autoParam Q(Singleton «$α» «$β») Qq.mkSetLiteralQ._auto_3 →
            autoParam Q(Insert «$α» «$β») Qq.mkSetLiteralQ._auto_5 → Q(«$β»)
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer_eq_iInf : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.centralizer s = ⨅ g ∈ s, Subgroup.centralizer {g}
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀ =
    CategoryTheory.Limits.limit.lift (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor✝ f n₀)
      { pt := K,
        π :=
          { app := fun q => ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj q).obj.ι,
            naturality := ⋯ } }
-- Mathlib.Algebra.GradedMulAction
/-- A graded version of `Mul.toSMul`  -/
GradedMonoid.GMul.toGSMul : {ιA : Type u_1} → (A : ιA → Type u_4) → [inst : Add ιA] → [GradedMonoid.GMul A] → GradedMonoid.GSMul A A
-- Mathlib.Algebra.Module.Presentation.Differentials
/-- The `S`-module `Ω[S⁄R]` contains an obvious solution to the system of linear
equations `pres.differentialsRelations.Solution` when `pres` is a presentation
of `S` as an `R`-algebra.  -/
Algebra.Presentation.differentialsSolution : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] → (pres : Algebra.Presentation R S ι σ) → pres.differentialsRelations.Solution Ω[S⁄R]
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (hl₁ : S₁.LeftHomologyData) (hl₂ : S₂.LeftHomologyData) (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : hl₁.IsPreservedBy F] [inst_6 : hl₂.IsPreservedBy F],
  F.map (CategoryTheory.ShortComplex.leftHomologyMap' φ hl₁ hl₂) =
    CategoryTheory.ShortComplex.leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
-- Init.Data.List.OfFn
List.head_ofFn : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α} (h : List.ofFn f ≠ []), (List.ofFn f).head h = f ⟨0, ⋯⟩
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.symm_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (e : α ≃+*o β), e.symm.symm = e
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.add_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x y : A}, x ∈ S → y ∈ S → x + y ∈ S
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_image : ∀ {δ : Type u_1} {δ' : Type u_2} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)]
  {μ : (i : δ) → MeasureTheory.Measure (X i)} [inst_1 : DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : DecidableEq δ'] {e : δ' → δ},
  Function.Injective e →
    ∀ (s : Finset δ') {f : ((i : δ') → X (e i)) → ENNReal},
      Measurable f →
        ∀ (x : (i : δ) → X i),
          (∫⋯∫⁻_Finset.image e s, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x =
            (∫⋯∫⁻_s, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackLimitCone_cone : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.Types.pullbackLimitCone f g).cone = CategoryTheory.Limits.Types.pullbackCone f g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}, CategoryTheory.IsPullback inr.op inl.op g.op f.op ↔ CategoryTheory.IsPushout f g inl inr
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.ofFactorizationData_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.diag A)),
  (HomotopicalAlgebra.PathObject.ofFactorizationData h).ι = h.i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.Limits.pullback.snd f g)) =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f' f) g
-- Mathlib.Logic.Function.Defs
/-- A point `x` is a fixed point of `f : α → α` if `f x = x`.  -/
Function.IsFixedPt : {α : Type u₁} → (α → α) → α → Prop
-- Mathlib.Data.Int.Cast.Lemmas
Commute.self_intCast_mul_intCast_mul : ∀ {α : Type u_3} [inst : Ring α] (a : α) (m n : ℤ), Commute (↑m * a) (↑n * a)
-- Mathlib.Topology.ContinuousMap.Algebra
continuousAddSubgroup.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β],
  continuousAddSubgroup α β = { toAddSubmonoid := continuousAddSubmonoid α β, neg_mem' := ⋯ }
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.completeTheory.isMaximal : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M] [Nonempty M], (L.completeTheory M).IsMaximal
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
mem_doublyStochastic_iff_sum : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = 1) ∧ ∀ (j : n), ∑ i, M i j = 1
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.norm_eq_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (i : ι), ‖v i‖ = 1
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).f i =
    CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g f g (𝒰.f i)
      (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (a : ↑s →₀ S) (a_1 : M),
  (↑((AddMonoidAlgebra.supportedEquivFinsupp s).symm a)).coeff a_1 = if h : a_1 ∈ s then a ⟨a_1, h⟩ else 0
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.nat_rawCast_0 : ∀ {R : Type u_1} [sR : CommSemiring R], Nat.rawCast 0 = 0
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfSMulDisjoint_baseSet : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstSMul G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1),
  (hf.trivializationOfSMulDisjoint hfG U open_U disjoint).baseSet = f '' U
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc) h) =
    CategoryTheory.CategoryStruct.comp (I.snd i) (CategoryTheory.CategoryStruct.comp (d.inj (J.snd i)) h)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.funLeft_id : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : Type u_10}
  (g : n → M), (LinearMap.funLeft R M id) g = g
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n), s.exsphere ∅ = s.insphere
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M], Submonoid.instInhabited = { default := ⊥ }
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.ext : ∀ {x y : ZFSet.{u}}, (∀ (z : ZFSet.{u}), z ∈ x ↔ z ∈ y) → x = y
-- Mathlib.Data.List.AList
AList.union_empty : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s : AList β}, s ∪ ∅ = s
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabImport : Lean.Elab.Command.CommandElab
-- Init.Data.Option.Lemmas
Option.SomeLtNone.wellFounded_lt : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → WellFounded (Option.SomeLtNone.lt r)
-- Aesop.Search.SearchM
Aesop.SearchM.instNonemptyContext : Nonempty Aesop.SearchM.Context
-- Mathlib.Order.Defs.Unbundled
/-- A lower set relative to a predicate `P` is a set such that all elements satisfy `P`
and any element less than one of its members and satisfying `P` is also a member.  -/
IsRelLowerSet : {α : Type u_1} → [LE α] → Set α → (α → Prop) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.map_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} {f'' : X'' ⟶ Z''} {g'' : Y'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y')
  (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'') [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' g'] [inst_3 : CategoryTheory.Limits.HasPullback f'' g'']
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
  (e₃ : CategoryTheory.CategoryStruct.comp f' j₃ = CategoryTheory.CategoryStruct.comp j₁ f'')
  (e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₂ g'') {Z_1 : C}
  (h : CategoryTheory.Limits.pullback f'' g'' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₁ j₁)
        (CategoryTheory.CategoryStruct.comp i₂ j₂) (CategoryTheory.CategoryStruct.comp i₃ j₃) ⋯ ⋯)
      h
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rci.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rci α}, r.iter.toList = r.toList
-- Mathlib.Order.Atoms
/-- A complemented modular coatomic lattice is strongly coatomic.
Not an instance to prevent loops.  -/
ComplementedLattice.isStronglyCoatomic : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] [ComplementedLattice α]
  [IsCoatomic α], IsStronglyCoatomic α
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.GoTo.right : ExistsAndEq.GoTo
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.instAppend : {α : Type u_1} → [inst : BEq α] → Append (Aesop.UnorderedArraySet α)
-- Init.Data.Array.Bootstrap
Array.appendList_eq_append : ∀ {α : Type u_1} {xs : Array α} {l : List α}, xs.appendList l = xs ++ l
-- Mathlib.Logic.Function.FromTypes
Function.FromTypes.const_succ_apply : ∀ {n : ℕ} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) (x : p 0),
  Function.FromTypes.const p t x = Function.FromTypes.const (Matrix.vecTail p) t
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_intCast : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : IntCast β] (n : ℤ),
  ⇑↑n = ↑n
-- Mathlib.Topology.VectorBundle.Basic
trivialization_linear : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] [VectorBundle R F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e], Bundle.Trivialization.IsLinear R e
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.direction_prod_le : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (s : AffineSubspace k P) (t : AffineSubspace k Q),
  (s.prod t).direction ≤ s.direction.prod t.direction
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k).getKey a h' = m.getKey a ⋯
-- Mathlib.CategoryTheory.Action.Continuous
ContinuousMonoidHom.toContinuousMonoidHom.congr_simp : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : MonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Data.Finite.Defs
not_finite_iff_infinite : ∀ {α : Sort u_1}, ¬Finite α ↔ Infinite α
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
Matrix.ProjectiveSpecialLinearGroup.rank_two_simple : ∀ {F : Type u_2} [inst : Field F], 4 ≤ Nat.card F → IsSimpleGroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F)
-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Lean.Elab.TerminationMeasure.delab.go.match_1.eq_1 : ∀ (motive : ℕ → Lean.TSyntaxArray `ident → Sort u_1) (vars : Lean.TSyntaxArray `ident)
  (h_1 : (vars : Lean.TSyntaxArray `ident) → motive 0 vars)
  (h_2 : (i : ℕ) → (vars : Lean.TSyntaxArray `ident) → motive i.succ vars),
  (match 0, vars with
    | 0, vars => h_1 vars
    | i.succ, vars => h_2 i vars) =
    h_1 vars
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Equivalent types give rise to multiplicatively equivalent free groups.

The converse can be found in `Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean`, as
`Equiv.ofFreeGroupEquiv`.  -/
FreeGroup.freeGroupCongr : {α : Type u_1} → {β : Type u_2} → α ≃ β → FreeGroup α ≃* FreeGroup β
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageZeroHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : DecidableEq β] [inst_2 : Zero β]
  [inst_3 : FunLike F α β] [inst_4 : ZeroHomClass F α β] (f : F),
  Finset.imageZeroHom f = { toFun := Finset.image ⇑f, map_zero' := ⋯ }
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.inv₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : GroupWithZero β] [ContinuousInv₀ β] [TopologicalSpace.MetrizableSpace β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable f⁻¹ μ
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The equivalence between `LightDiagram` and a small category.  -/
LightDiagram.equivSmall : LightDiagram ≌ LightDiagram'
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.succ?_eq_minValueSealed : ∀ {x : Int8}, Std.PRange.succ? x = if x + 1 = Int8.minValueSealed✝ then none else some (x + 1)
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- If two functions differ only on a discrete set, then their proximity functions
agree, except perhaps at radius 0.
 -/
ValueDistribution.proximity_congr_codiscrete : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f g : ℂ → E} {a : WithTop E} {r : ℝ},
  f =ᶠ[Filter.codiscrete ℂ] g → r ≠ 0 → ValueDistribution.proximity f a r = ValueDistribution.proximity g a r
-- Init.Data.Nat.Bitwise.Basic
Nat.xor_eq : ∀ {m n : ℕ}, m.xor n = m ^^^ n
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- The Dirac measure, "evaluation at `x`".  -/
AbstractMeasure.dirac : {X : Type u_1} →
  (R : Type u_3) →
    [inst : TopologicalSpace X] →
      [inst_1 : CommRing R] → [inst_2 : TopologicalSpace R] → [inst_3 : IsTopologicalRing R] → X → AbstractMeasure X R R
-- Mathlib.Order.RelClasses
Std.Asymm.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Asymm r], Std.Asymm (Function.swap r)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `IsLocalization S T`, then `M[S⁻¹]` has a `T`-action.
This should eventually be replaced with `IsLocalizedModule f N` and `SMul T N`.  -/
LocalizedModule.smulOfIsLocalization : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} →
      {M : Type v} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (T : Type u_1) →
              [inst_3 : CommSemiring T] → [inst_4 : Algebra R T] → [IsLocalization S T] → SMul T (LocalizedModule S M)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot_eq_smul_coroot_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [Finite ι]
  [IsAddTorsionFree M] [IsAddTorsionFree N] {i j : ι} {t : R}, P.coroot i = t • P.coroot j ↔ P.root j = t • P.root i
-- Mathlib.RingTheory.Trace.Defs
/-- Let `T / S / R` be a tower of finite extensions of fields. Then
$\text{Trace}_{T/R} = \text{Trace}_{S/R} \circ \text{Trace}_{T/S}$.  -/
Algebra.trace_comp_trace : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] [Module.Free R S]
  [Module.Finite R S] [Module.Free S T] [Module.Finite S T],
  Algebra.trace R S ∘ₗ ↑R (Algebra.trace S T) = Algebra.trace R T
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.colorClasses_finite : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) [Finite α], C.colorClasses.Finite
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcOptions.toJson : Lean.Lsp.RpcOptions → Lean.Json
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instCompleteLattice : {ι : Type u_1} → CompleteLattice (AbstractSimplicialComplex ι)
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.Limits.ColimitPresentation.bind.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)] {X : C}
  (P : CategoryTheory.Limits.ColimitPresentation J X)
  (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j))
  [inst_3 : ∀ (j : J), CategoryTheory.IsFiltered (I j)]
  [inst_4 : ∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)], P.bind Q = P.bind Q
-- Mathlib.Algebra.Polynomial.Bivariate
/-- Given valuations `x` and `y` of the variables in an `R`-algebra `A`, `aevalAeval x y` is
the unique `R`-algebra homomorphism from `R[X][Y]` to `A` sending `X` to `x` and `Y` to `y`.  -/
Polynomial.aevalAeval : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → A → A → Polynomial (Polynomial R) →ₐ[R] A
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {ι : Type u_2} [Small.{w, u_2} ι] {X : ι → C}
  (f : (i : ι) → X i ⟶ S) [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C]
  {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.shrinkYoneda.{w, v, u}.obj (X i)}
  (hc : CategoryTheory.Limits.IsColimit c) {U : C} (g : U ⟶ S),
  CategoryTheory.Presheaf.imageSieve
      (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm g) =
    CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.ofArrows X f)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.mk.injEq : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (toFun : M → N)
  (map_formula' :
    autoParam (∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x)
      FirstOrder.Language.ElementaryEmbedding.map_formula'._autoParam)
  (toFun_1 : M → N)
  (map_formula'_1 :
    autoParam (∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun_1 ∘ x) ↔ φ.Realize x)
      FirstOrder.Language.ElementaryEmbedding.map_formula'._autoParam),
  ({ toFun := toFun, map_formula' := map_formula' } = { toFun := toFun_1, map_formula' := map_formula'_1 }) =
    (toFun = toFun_1)
-- Init.Data.Array.Erase
Array.getElem?_eraseIdx_of_ge : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {j : ℕ}, i ≤ j → (xs.eraseIdx i h)[j]? = xs[j + 1]?
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_twoMore_iff_toBitVec : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.twoMore ↔
    BitVec.extractLsb' 4 4 b.toBitVec = 14#4
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- The ring homomorphism of monoid algebras induced by a homomorphism of the base rings.  -/
MonoidAlgebra.mapRingHom : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Monoid M] → (R →+* S) → MonoidAlgebra R M →+* MonoidAlgebra S M