mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.tsupport_subset : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} {m : ℕ},
  ↑m ≤ n → HasFTaylorSeriesUpTo n f p → (tsupport fun x => p x m) ⊆ tsupport f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sinh_antiperiodic : Function.Antiperiodic Complex.sinh (↑Real.pi * Complex.I)
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropySupBotHom.eq_1 : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X),
  Dynamics.coverEntropySupBotHom T = { toFun := Dynamics.coverEntropy T, map_sup' := ⋯, map_bot' := ⋯ }
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- A finite number of random variables are independent if and only if their joint characteristic
function is equal to the product of the characteristic functions. This is the version for Banach
spaces, see `iIndepFun_iff_charFun_pi` for the Hilbert space version.  -/
ProbabilityTheory.iIndepFun_iff_charFunDual_pi : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [inst : Fintype ι]
  [MeasureTheory.IsProbabilityMeasure P] {E : ι → Type u_3} {mE : (i : ι) → MeasurableSpace (E i)}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)]
  [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [inst_6 : (i : ι) → NormedSpace ℝ (E i)]
  [inst_7 : DecidableEq ι],
  (∀ (i : ι), AEMeasurable (X i) P) →
    (ProbabilityTheory.iIndepFun X P ↔
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω x => X x ω) P) L =
          ∏ i, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P) (L ∘SL ContinuousLinearMap.single ℝ E i))
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_domRestrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (K : Submodule R M) (f : M →ₛₗ[τ₁₂] M₂), (f.domRestrict K).range = Submodule.map f K
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRightAux_cons : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i j : C}
  {η : g ⟶ h} {ηs : i ⟶ j}
  {ηs' : CategoryTheory.MonoidalCategoryStruct.tensorObj i f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj j f}
  {η₁ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj g (CategoryTheory.MonoidalCategoryStruct.tensorObj i f) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj h (CategoryTheory.MonoidalCategoryStruct.tensorObj j f)}
  {η₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj g (CategoryTheory.MonoidalCategoryStruct.tensorObj i f) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj h j) f}
  {η₃ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj g i) f ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj h j) f},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight ηs f = ηs' →
    CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl g).hom
            (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl h).hom))
          ηs' =
        η₁ →
      CategoryTheory.CategoryStruct.comp η₁ (CategoryTheory.MonoidalCategoryStruct.associator h j f).inv = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator g i f).hom η₂ = η₃ →
          CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom η ηs) f =
            η₃
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn : ∀ (p : ℝ),
  AkraBazziRecurrence.GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) x‖
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.coe_mulRight : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (r : R), ⇑(AddMonoidHom.mulRight r) = fun x => x * r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₂.contains k = false → (m₁.diff m₂).getD k fallback = m₁.getD k fallback
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs xs_1 : List ((a : α) × β a)) (e_xs : xs = xs_1)
  (h : xs.isEmpty = false), Std.Internal.List.maxKey xs h = Std.Internal.List.maxKey xs_1 ⋯
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.guitartExact_id : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] (F : CategoryTheory.Functor C₁ C₂),
  (CategoryTheory.TwoSquare.mk (CategoryTheory.Functor.id C₁) F F (CategoryTheory.Functor.id C₂)
      (CategoryTheory.CategoryStruct.id F)).GuitartExact
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Composition on the left by a (lipschitz-continuous) homomorphism of topological `R`-algebras,
as an `AlgHom`. Similar to `AlgHom.compLeftContinuous`.  -/
BoundedContinuousFunction.AlgHom.compLeftContinuousBounded : {α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      (𝕜 : Type u_1) →
        [inst : NormedField 𝕜] →
          [inst_1 : TopologicalSpace α] →
            [inst_2 : NormedRing γ] →
              [inst_3 : NormedAlgebra 𝕜 γ] →
                [inst_4 : NormedRing β] →
                  [inst_5 : NormedAlgebra 𝕜 β] →
                    (g : β →ₐ[𝕜] γ) →
                      {C : NNReal} →
                        LipschitzWith C ⇑g → BoundedContinuousFunction α β →ₐ[𝕜] BoundedContinuousFunction α γ
-- Mathlib.Analysis.RCLike.Basic
IsRCLikeNormedField.out : ∀ {𝕜 : Type u_3} {hk : NormedField 𝕜} [self : IsRCLikeNormedField 𝕜], ∃ h, hk = h.toNormedField
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?_intermediateZip.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n' : ℕ) → motive n'.succ),
  (match 0 with
    | 0 => h_1 ()
    | n'.succ => h_2 n') =
    h_1 ()
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, t.getKeyD a fallback = (t.getKey? a).getD fallback
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add' : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x y : R), v (x + y) ≤ v x ∨ v (x + y) ≤ v y
-- Lean.Environment
/-- The kind of the constant, known immediately.  -/
Lean.AsyncConstantInfo.kind : Lean.AsyncConstantInfo → Lean.ConstantKind
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_of_succ_ne : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  (∀ (b : α), Order.succ b ≠ a) → Order.IsSuccPrelimit a
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homologyData₀_left_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  (X.homologyData₀ R).left.π = SSet.π₀.fromChainComplexXZero X R
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsNotG2.toIsIrreducible : ∀ {ι : 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} [self : P.IsNotG2],
  P.IsIrreducible
-- Batteries.Tactic.OpenPrivate
/-- Add info to the info tree corresponding to a module name.  -/
Lean.Elab.addModuleInfo : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.Ident → m Unit
-- Mathlib.Order.Category.BddDistLat
bddDistLat_dual_comp_forget_to_distLat : BddDistLat.dual.comp (CategoryTheory.forget₂ BddDistLat DistLat) =
  (CategoryTheory.forget₂ BddDistLat DistLat).comp DistLat.dual
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
IsIntegralClosure.range_le_span_dualBasis : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  {L : Type u_3} [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C]
  [inst_12 : IsScalarTower A C L] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L] {ι : Type u_5}
  [inst_15 : Finite ι] [inst_16 : DecidableEq ι] (b : Module.Basis ι K L),
  (∀ (i : ι), IsIntegral A (b i)) →
    ∀ [IsIntegrallyClosed A],
      (↑A (Algebra.linearMap C L)).range ≤ Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis ⋯ b))
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.ofInt'.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Std.Time.Format.Modifier
/-- `V`: Time zone ID.
- `V` (1 letter): outputs `"unk"` (unknown zone placeholder per Unicode CLDR).
- `VV` (2 letters): outputs the IANA zone ID (e.g., `"America/Los_Angeles"`), or `"Z"` for UTC.
 -/
Std.Time.Modifier.V : Std.Time.ZoneId → Std.Time.Modifier
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatIso_associator : ∀ {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E),
  CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Bicategory.associator F G H) =
    F.toFunctor.associator G.toFunctor H.toFunctor
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.finrank_maxGenEigenspace_zero_eq : ∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M),
  Module.finrank K ↥(φ.maxGenEigenspace 0) = (LinearMap.charpoly φ).natTrailingDegree
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_function_term : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {n : ℕ} (v : Fin n → M) (f : L.Functions n),
  FirstOrder.Language.Term.realize v f.term = FirstOrder.Language.Structure.funMap f v
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.splitter : (motive : Lean.Expr → Sort u_1) →
  (e : Lean.Expr) →
    ((name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us)) →
      ((f x : Lean.Expr) → motive (f.app x)) →
        ((binderName : Lean.Name) →
            (ty body : Lean.Expr) →
              (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo)) →
          (Unit → motive (Lean.Expr.sort Lean.Level.zero)) →
            ((a : Lean.Level) → motive (Lean.Expr.sort a.succ)) →
              ((u : Lean.Level) →
                  (u = Lean.Level.zero → False) →
                    (∀ (a : Lean.Level), u = a.succ → False) → motive (Lean.Expr.sort u)) →
                ((x : Lean.Expr) →
                    (∀ (name : Lean.Name) (us : List Lean.Level), x = Lean.Expr.const name us → False) →
                      (∀ (f x_2 : Lean.Expr), x = f.app x_2 → False) →
                        (∀ (binderName : Lean.Name) (ty body : Lean.Expr) (binderInfo : Lean.BinderInfo),
                            x = Lean.Expr.forallE binderName ty body binderInfo → False) →
                          (x = Lean.Expr.sort Lean.Level.zero → False) →
                            (∀ (a : Lean.Level), x = Lean.Expr.sort a.succ → False) →
                              (∀ (u : Lean.Level), x = Lean.Expr.sort u → False) → motive x) →
                  motive e
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_comp_proj : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B),
  DiscreteQuotient.ofLE h ∘ A.proj = B.proj
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.ListBlank.append.match_1.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (motive : List Γ → Turing.ListBlank Γ → Sort u_2) (L : Turing.ListBlank Γ)
  (h_1 : (L : Turing.ListBlank Γ) → motive [] L)
  (h_2 : (a : Γ) → (l : List Γ) → (L : Turing.ListBlank Γ) → motive (a :: l) L),
  (match [], L with
    | [], L => h_1 L
    | a :: l, L => h_2 a l L) =
    h_1 L
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- `H.equiv₀` is natural  -/
CategoryTheory.Sheaf.H.equiv₀_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T) {F G : CategoryTheory.Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : F.H 0),
  (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op T))) ((CategoryTheory.Sheaf.H.equiv₀ F hT) x) =
    (CategoryTheory.Sheaf.H.equiv₀ G hT) ((CategoryTheory.Sheaf.H.map f 0) x)
-- Mathlib.Algebra.Group.Even
even_unop_iff : ∀ {α : Type u_2} [inst : Add α] {a : αᵃᵒᵖ}, Even (AddOpposite.unop a) ↔ Even a
-- Aesop.Util.Basic
Aesop.elabPattern : Lean.Syntax → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Group.Units.Opposite
/-- The units of the opposites are equivalent to the opposites of the units.  -/
Units.opEquiv : {M : Type u_2} → [inst : Monoid M] → Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
/-- **Alias** of `PrimeSpectrum.finite_setOfPred_isMin`. -/
PrimeSpectrum.finite_setOf_isMin : ∀ (R : Type u) [inst : CommSemiring R] [IsNoetherianRing R], {x | IsMin x}.Finite
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instInhabitedContext : Inhabited Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context
-- Lean.Elab.DocString
/-- The arguments it should receive, as a string.  -/
Lean.Doc.CodeSuggestion.args : Lean.Doc.CodeSuggestion → Option String
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine'.match_1.congr_eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (k₁ k₂ : ℤ),
  p₁ = Int.Internal.Linear.Poly.num k₁ →
    p₂ = Int.Internal.Linear.Poly.num k₂ →
      (match p₁, p₂ with
        | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => h_1 k₁ k₂
        | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p => h_2 k₁ a x p
        | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ => h_3 a x p k₂
        | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_1 k₁ k₂
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.desc_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc g h)
      (CategoryTheory.CategoryStruct.comp f h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g f)
        (CategoryTheory.CategoryStruct.comp h f))
      h_1
-- Mathlib.Algebra.Torsor.Defs
AddTorsor.toVSub : {G : outParam (Type u_1)} → {P : Type u_2} → {inst : AddGroup G} → [self : AddTorsor G P] → VSub G P
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.mk.inj : ∀ {ref : Lean.Syntax} {structural : Bool} {vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]} {body : Lean.Term}
  {synthetic : Bool} {ref_1 : Lean.Syntax} {structural_1 : Bool}
  {vars_1 : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]} {body_1 : Lean.Term} {synthetic_1 : Bool},
  { ref := ref, structural := structural, vars := vars, body := body, synthetic := synthetic } =
      { ref := ref_1, structural := structural_1, vars := vars_1, body := body_1, synthetic := synthetic_1 } →
    ref = ref_1 ∧ structural = structural_1 ∧ vars = vars_1 ∧ body = body_1 ∧ synthetic = synthetic_1
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.nat_gcd_helper_2' : ∀ (x y a b : ℕ), x * a = y * b + 1 → x.gcd y = 1
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.toRightFun_mul_inv_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hT : Subgroup.IsComplement (↑H) T) (g : G),
  ↑(hT.toRightFun g) * g⁻¹ ∈ H
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.postcomposeEquivalence`.

---

If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of
cones.
 -/
CategoryTheory.Limits.Cones.postcomposeEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} → (F ≅ G) → (CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Ioo_of_le : ∀ {a b : ℝ}, a ≤ b → MeasureTheory.volume.real (Set.Ioo a b) = b - a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- commutation with `f'`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.commf' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
  CategoryTheory.CategoryStruct.comp h₁.f' self.φK = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f'
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_sdiff_Ioo_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Icc a b \ Set.Ioo a b = {a, b}
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.unopFunctorCompFst_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op),
  (CategoryTheory.Comma.unopFunctorCompFst L R).inv.app X = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.RingTheory.AlgebraTower
/-- If `R` and `A` have a bijective `algebraMap R A` and act identically on `M`,
then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.  -/
Module.Basis.algebraMapCoeffs : {R : Type u_1} →
  (A : Type u_3) →
    {ι : Type u_5} →
      {M : Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Algebra R A] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] →
                    [IsScalarTower R A M] →
                      Module.Basis ι R M → Function.Bijective ⇑(algebraMap R A) → Module.Basis ι A M
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.top_prod : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup N),
  ⊤.prod H = AddSubgroup.comap (AddMonoidHom.snd G N) H
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_inj : ∀ {r s : ℝ}, Circle.exp r = Circle.exp s ↔ r ≡ s [PMOD 2 * Real.pi]
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.liftCover.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {ι : Type u_5} (S : ι → Set α)
  (φ : (i : ι) → C(↑(S i), β))
  (hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩)
  (hS : ∀ (x : α), ∃ i, S i ∈ nhds x),
  ContinuousMap.liftCover S φ hφ hS = { toFun := Set.liftCover S (fun i => ⇑(φ i)) hφ ⋯, continuous_toFun := ⋯ }
-- Mathlib.Computability.ContextFreeGrammar
/-- There is a replacement later in the string.  -/
ContextFreeRule.Rewrites.cons : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} (x : Symbol T N) {s₁ s₂ : List (Symbol T N)},
  r.Rewrites s₁ s₂ → r.Rewrites (x :: s₁) (x :: s₂)
-- Mathlib.Order.WellQuasiOrder
wellQuasiOrdered_le : ∀ {α : Type u_1} [inst : LE α] [h : WellQuasiOrderedLE α], WellQuasiOrdered fun x1 x2 => x1 ≤ x2
-- Init.Data.Nat.Basic
Nat.add_left_comm : ∀ (n m k : ℕ), n + (m + k) = m + (n + k)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
prod_le_borel_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α]
  [mβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β], Prod.instMeasurableSpace ≤ borel (α × β)
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.prodMk'_prod_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (μ : AbstractMeasure X R R)
  (ν : AbstractMeasure Y R R) [inst_5 : LocallyCompactSpace X] [inst_6 : LocallyCompactSpace Y] (f : C(X, R))
  (g : C(Y, R)), ((AbstractMeasure.prodMk' μ) ν) (f.comp ContinuousMap.fst * g.comp ContinuousMap.snd) = μ f * ν g
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFractionRel.unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  {z₁ z₂ : W.LeftFraction X Y},
  CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂ →
    CategoryTheory.MorphismProperty.RightFractionRel z₁.unop z₂.unop
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_of_sheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) {A : Type u'}
  [inst_2 : CategoryTheory.Category.{v, u'} A] (F : CategoryTheory.Sheaf J A), S.SheafCondition F.obj
-- Mathlib.Probability.Process.Filtration
/-- A measure is σ-finite with respect to filtration if it is σ-finite with respect
to all the sub-σ-algebra of the filtration.  -/
MeasureTheory.SigmaFiniteFiltration : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} → [inst : Preorder ι] → MeasureTheory.Measure Ω → MeasureTheory.Filtration ι m → Prop
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.lift_unique : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (g : TensorAlgebra R M →ₐ[R] A),
  g.toLinearMap ∘ₗ TensorAlgebra.ι R = f ↔ g = (TensorAlgebra.lift R) f
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.algebraMap_injective_of_span_eq_top : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Set R),
  Ideal.span s = ⊤ → Function.Injective ⇑(algebraMap R ((a : ↑s) → Localization.Away ↑a))