mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
ContinuousOn.arcsin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {s : Set X},
  ContinuousOn f s → ContinuousOn (fun x => Real.arcsin (f x)) s
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.inlX.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder] (i j : ι)
  (hij : c.Rel j i), HomologicalComplex.cylinder.inlX K i j hij = HomologicalComplex.cylinder.inlX K i j hij
-- Mathlib.Algebra.Divisibility.Units
isUnit_of_dvd_one : ∀ {α : Type u_1} [inst : CommMonoid α] {a : α}, a ∣ 1 → IsUnit a
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_pure : ∀ {α : Type u_1} (x : α), (pure x).HasBasis (fun x => True) fun x_1 => {x}
-- Mathlib.Data.WSeq.Basic
/-- Prepend an element to a weak sequence  -/
Stream'.WSeq.cons : {α : Type u} → α → Stream'.WSeq α → Stream'.WSeq α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_discr : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.twoTorsionPolynomial.discr = 16 * W.Δ
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioi_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ioi a)), Subtype.val '' Set.Iic b = Set.Ioc a ↑b
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapId_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  ((CategoryTheory.StrictlyUnitaryPseudofunctor.id B).mapId a).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (r : R),
  Polynomial.taylor r = { toFun := fun f => f.comp (Polynomial.X + Polynomial.C r), map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instDFunLike : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] → DFunLike (ContMDiffSection I F n V) M V
-- Mathlib.RingTheory.MatrixAlgebra
/-- `Matrix.kronecker` as an algebra equivalence, when the two arguments are tensored.  -/
Matrix.kroneckerAlgEquiv : (m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_5) →
      [inst : CommSemiring R] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq n] →
            [inst_3 : Fintype m] →
              [inst_4 : DecidableEq m] → TensorProduct R (Matrix m m R) (Matrix n n R) ≃ₐ[R] Matrix (m × n) (m × n) R
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.pdiv_apply : ∀ {R : Type u_1} [inst : GroupWithZero R] (f g : ArithmeticFunction R) (n : ℕ), (f.pdiv g) n = f n / g n
-- Mathlib.CategoryTheory.Core
/-- The natural isomorphism
```
                  F.core
            Core C ⥤ Core D
 inclusion C  ‖          ‖  inclusion D
              V          V
              C    ⥤    D
                    F
```
thought of as pseudonaturality of `inclusion`,
when viewing `Core` as a pseudofunctor.
 -/
CategoryTheory.Functor.coreCompInclusionIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          F.core.comp (CategoryTheory.Core.inclusion D) ≅ (CategoryTheory.Core.inclusion C).comp F
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.isAddMonHom_counitIsoAux : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.AddMon C),
  CategoryTheory.IsAddMonHom (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom
-- Aesop.Script.TacticState
Aesop.Script.TacticState.mk.sizeOf_spec : ∀ (visibleGoals : Array Aesop.GoalWithMVars) (invisibleGoals : Std.HashSet Lean.MVarId),
  sizeOf { visibleGoals := visibleGoals, invisibleGoals := invisibleGoals } =
    1 + sizeOf visibleGoals + sizeOf invisibleGoals
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_unsat_coeff_cert : Int.Internal.Linear.Poly → ℤ → Bool
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.toQuadraticMap_polarBilin : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N), Q.polarBilin.toQuadraticMap = 2 • Q
-- Mathlib.Order.Preorder.Chain
Flag.mk.inj : ∀ {α : Type u_4} {inst : LE α} {carrier : Set α} {Chain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier}
  {max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 => x1 ≤ x2) s → carrier ⊆ s → carrier = s} {carrier_1 : Set α}
  {Chain'_1 : IsChain (fun x1 x2 => x1 ≤ x2) carrier_1}
  {max_chain'_1 : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 => x1 ≤ x2) s → carrier_1 ⊆ s → carrier_1 = s},
  { carrier := carrier, Chain' := Chain', max_chain' := max_chain' } =
      { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 } →
    carrier = carrier_1
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.prop_red_T_pow : ∀ {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Prop},
  (∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.S • B)) →
    (∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.T • B)) →
      ∀ (B : FixedDetMatrix (Fin 2) ℤ m) (n : ℤ), C (ModularGroup.T ^ n • B) ↔ C B
-- Init.Data.Sum.Lemmas
Sum.elim_comp_inr : ∀ {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ Sum.inr = g
-- Mathlib.Order.Cover
WithBot.bot_covBy_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ⊥ ⋖ ↑a ↔ IsMin a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}, t.min he ∈ t
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan.eq_1 : ∀ (x : ℝ), Real.tan x = (Complex.tan ↑x).re
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- **Alias** of `AffineIndependent.notMem_affineSpan_sdiff`.

---

If a family is affinely independent, a point in the family is not
in the affine span of the other points, if the underlying ring is
nontrivial.  -/
AffineIndependent.notMem_affineSpan_diff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p → ∀ (i : ι) (s : Set ι), p i ∉ affineSpan k (p '' (s \ {i}))
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coroot_eq_iff : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K]
  (α β : LieModule.Weight K (↥H) L), LieAlgebra.IsKilling.coroot α = LieAlgebra.IsKilling.coroot β ↔ α = β
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getStructId?.goQ? : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_subst : ∀ {τ : Type u_1} {S : Type u_3} [inst : CommRing S] (p : ℕ) (hp : p ≠ 0) {f : MvPowerSeries τ S},
  PowerSeries.HasSubst f →
    ∀ (φ : PowerSeries S),
      (MvPowerSeries.expand p hp) (PowerSeries.subst f φ) = PowerSeries.subst ((MvPowerSeries.expand p hp) f) φ
-- Mathlib.Order.Hom.Basic
OrderIso.refl_trans : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), (OrderIso.refl α).trans e = e
-- Mathlib.Data.Quot
/-- Choose an element of the equivalence class using the axiom of choice.
Sound but noncomputable.  -/
Quotient.out : {α : Sort u_1} → {s : Setoid α} → Quotient s → α
-- Mathlib.Tactic.Ring.Common
/-- Negates a monomial `va` to get another monomial.

* `-c = (-c)` (for `c` coefficient)
* `-(a₁ * a₂) = a₁ * -a₂`
 -/
Mathlib.Tactic.Ring.Common.evalNegProd : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          {a : Q(«$α»)} →
            (rα : Q(CommRing «$α»)) →
              Mathlib.Tactic.Ring.Common.ExProd bt sα a →
                Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) q(-«$a»))
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_add_iff_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    0 ≤ᵐ[μ] f →
      0 ≤ᵐ[μ] g → (MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ)
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.nontrivial : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M],
  Nontrivial M
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasis.congr_simp : ∀ {n n_1 : ℕ} (e_n : n = n_1) {K : Type u} [inst : Field K] {ζ ζ_1 : K} (e_ζ : ζ = ζ_1) [inst_1 : NeZero n]
  [inst_2 : CharZero K] [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n),
  hζ.integralPowerBasis = ⋯.integralPowerBasis
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart_symm_apply : ∀ (x y : ℝ) [h : Fact (x < y)] (z : EuclideanHalfSpace 1), ↑(IccLeftChart x y).symm z = ⟨min ((↑z).ofLp 0 + x) y, ⋯⟩
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.getElem?_toList_eq : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  r.toList[i]? =
    Option.filter (fun x => decide (x < r.upper)) (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least)
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [inst_5 : ∀ (F : CategoryTheory.Functor C₁ D), L.HasLeftKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor C₂ D), R.HasLeftKanExtension F] (F : CategoryTheory.Functor C₂ D),
  CategoryTheory.IsIso (w.lanBaseChange.app F) ↔
    (CategoryTheory.StructuredArrow.right
          ((CategoryTheory.Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare
            w)).IsLeftKanExtension
      (CategoryTheory.StructuredArrow.hom
        ((CategoryTheory.Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.map_zero : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  (f : A →ₑ+[φ] B), f 0 = 0
-- Aesop.Frontend.Basic
Aesop.Frontend.elabBoolLit : {m : Type → Type} →
  [Monad m] → [Lean.MonadRef m] → [MonadExceptOf Lean.Exception m] → Lean.TSyntax `Aesop.bool_lit → m Bool
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.tr.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2to1.Λ' K Γ Λ σ → Sort u_5) (q : Λ)
  (h_1 : (q : Λ) → motive (Turing.TM2to1.Λ'.normal q))
  (h_2 : (k : K) → (s : Turing.TM2to1.StAct K Γ σ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.go k s q))
  (h_3 : (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.ret q)),
  (match Turing.TM2to1.Λ'.normal q with
    | Turing.TM2to1.Λ'.normal q => h_1 q
    | Turing.TM2to1.Λ'.go k s q => h_2 k s q
    | Turing.TM2to1.Λ'.ret q => h_3 q) =
    h_1 q
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'_symm_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C}
  (f : Y ⟶ X) {n a : ℤ}
  (x : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Z) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X))
  (a' : ℤ) (h : n + a = a'),
  (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm
      (CategoryTheory.CategoryStruct.comp x ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f.op)) =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm x)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_id : ∀ {X : AlgebraicGeometry.Scheme} {V V' : X.Opens} (i : V ≤ V'),
  AlgebraicGeometry.Scheme.Hom.resLE (CategoryTheory.CategoryStruct.id X) V' V i = X.homOfLE i
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.monoidAlgebraFree_obj_carrier : ∀ (R : Type u) [inst : Ring R] (X : Type u), ↑((ModuleCat.monoidAlgebraFree R).obj X) = MonoidAlgebra R X
-- Mathlib.GroupTheory.GroupAction.IterateAct
/-- The value of `n : IterateAddAct f`.  -/
IterateAddAct.val : {α : Type u_1} → {f : α → α} → IterateAddAct f → ℕ
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply : ∀ {M : Type u_4} [inst : Monoid M] (x : ↥(IsUnit.submonoid M)),
  ↑(Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x)⁻¹ = ↑(Classical.choose ⋯)⁻¹
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_finsetSum : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {α : Type u_3} (s : Finset α)
  (f : α → M → G), fwdDiff h (∑ k ∈ s, f k) = ∑ k ∈ s, fwdDiff h (f k)
-- Mathlib.Tactic.Find
/-- `#find t` finds definitions and theorems whose result type matches the term `t`, and prints them as
info lines. Use holes in `t` to indicate arbitrary subexpressions, for example `#find _ ∧ _` will
match any conjunction.

`#find` is also available as a tactic, and there is also the `find` tactic which looks for lemmas
which are `apply`able against the current goal.

Examples:
```lean
#find _ + _ = _ + _
#find ?n + _ = _ + ?n
#find (_ : Nat) + _ = _ + _
#find Nat → Nat
```
 -/
Mathlib.Tactic.Find.«command#find_» : Lean.ParserDescr
-- Mathlib.Data.Complex.Basic
Complex.I_mul_im : ∀ (z : ℂ), (Complex.I * z).im = z.re
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G),
  (CategoryTheory.Functor.Monoidal.coreMonoidalTransport i).εIso.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
      (i.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.to_double_hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} {hi₀₁ : c.Rel i₀ i₁} {K : HomologicalComplex C c} {φ φ' : K ⟶ HomologicalComplex.double f hi₀₁},
  φ = φ' ↔ φ.f i₀ = φ'.f i₀ ∧ φ.f i₁ = φ'.f i₁
-- Mathlib.Topology.Constructions
/-- A finite product of discrete spaces is discrete.  -/
Pi.discreteTopology : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [Finite ι]
  [∀ (i : ι), DiscreteTopology (A i)], DiscreteTopology ((i : ι) → A i)
-- Mathlib.Logic.Equiv.Fin.Basic
finAddFlip_apply_natAdd : ∀ {n : ℕ} (k : Fin n) (m : ℕ), finAddFlip (Fin.natAdd m k) = Fin.castAdd m k
-- Init.Data.Int.Order
Int.add_le_add_iff_right : ∀ {a b : ℤ} (c : ℤ), a + c ≤ b + c ↔ a ≤ b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
/-- Note this also holds for `z = 0`, but we do not need this case for `sin_pi_mul_eq`.  -/
EulerSine.integral_cos_mul_cos_pow_even : ∀ {z : ℂ} (n : ℕ),
  z ≠ 0 →
    (1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n + 2) =
      (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n)
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.measurableSet_Icc : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) [Countable ι], MeasurableSet (BoxIntegral.Box.Icc I)
-- Mathlib.AlgebraicGeometry.Birational.Composition
/-- Composition respects equivalence of partial maps on the right.  -/
AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_right : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] {g₁ g₂ : Y.PartialMap Z}, g₁.equiv g₂ → (f.comp g₁).equiv (f.comp g₂)
-- Init.Data.Nat.ToString
Nat.toDigits_append_toDigits : ∀ {b n d : ℕ}, 1 < b → 0 < n → d < b → b.toDigits n ++ b.toDigits d = b.toDigits (b * n + d)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalNameStx : Lean.Term → Lean.Elab.TermElabM (Lean.Name × Lean.Expr)
-- Init.Data.String.Iterate
String.Slice.PosIterator.mk.inj : ∀ {s : String.Slice} {currPos currPos_1 : s.Pos},
  { currPos := currPos } = { currPos := currPos_1 } → currPos = currPos_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (m.alter k f).get? k' = if h : (k == k') = true then cast ⋯ (f (m.get? k)) else m.get? k'
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.piUnique_symm_apply : ∀ {α : Type u_9} [inst : Unique α] (R : Type u_10) [inst_1 : Semiring R] (f : α → Type u_11)
  [inst_2 : (x : α) → AddCommMonoid (f x)] [inst_3 : (x : α) → Module R (f x)]
  [inst_4 : (x : α) → TopologicalSpace (f x)], ⇑(ContinuousLinearEquiv.piUnique R f).symm = uniqueElim
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.max!.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : Unit → motive none) (h_2 : (x : α) → motive (some x)),
  (match some x with
    | none => h_1 ()
    | some x => h_2 x) =
    h_2 x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.length_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.toList.length = t.size
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The underlying lean expression of an `AtomIso` term.  -/
Mathlib.Tactic.BicategoryLike.AtomIso.e : Mathlib.Tactic.BicategoryLike.AtomIso → Lean.Expr
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.trans_assoc : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₂ ≃ᴬ[k] P₃) (e₃ : P₃ ≃ᴬ[k] P₄),
  (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.coeff_hermite_succ_succ : ∀ (n k : ℕ),
  (Polynomial.hermite (n + 1)).coeff (k + 1) =
    (Polynomial.hermite n).coeff k - (↑k + 2) * (Polynomial.hermite n).coeff (k + 2)
-- Mathlib.Order.Hom.Lattice
InfHom.instBot : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → [Bot β] → Bot (InfHom α β)
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_iff' : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α},
  Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s
-- ImportGraph.Tools.ImportDiff
/-- `#import_diff foo bar ...` computes the new transitive imports that are added to a given file when
modules `foo, bar, ...` are added to the set of imports of the file. More precisely, it computes the
import diff between when `foo, bar, ...` are added to the imports and when `foo, bar, ...` are removed
from the imports.

Note: the command also works when some of the modules passed as arguments are already present in the file's
imports.  -/
«command#import_diff_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.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 : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D'),
  (CategoryTheory.StructuredArrow.prodEquivalence S S' T T').functor =
    CategoryTheory.StructuredArrow.prodFunctor S S' T T'
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Prefix of a Dyck word as a Dyck word, given that the count of `U`s and `D`s in it are equal.  -/
DyckWord.take : (p : DyckWord) → (i : ℕ) → List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p) → DyckWord
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.le_skipWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String} {pos : s.Pos}, pos ≤ pos.skipWhile pat
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureInformation : Lean.ToJson Lean.Lsp.SignatureInformation
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_self : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.singularPart μ = 0
-- Std.Data.DTreeMap.Lemmas
_private.Std.Data.DTreeMap.Lemmas.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a