mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Prod
Prod.isCentralVAdd : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd M β] [inst_2 : VAdd Mᵃᵒᵖ α]
  [inst_3 : VAdd Mᵃᵒᵖ β] [IsCentralVAdd M α] [IsCentralVAdd M β], IsCentralVAdd M (α × β)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
BitVec.reduceBitVecToFin : Lean.Meta.Simp.DSimproc
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bindList_cons' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β))
  (s : ForInStep β) (a : α) (l : List α),
  ForInStep.bindList f (a :: l) s = do
    let x ← s.bind (f a)
    ForInStep.bindList f l x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff!_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.diff! m₂) = true ↔
          Std.DTreeMap.Internal.Impl.contains k m₁ = true ∧ ¬Std.DTreeMap.Internal.Impl.contains k m₂ = true
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_iff`.

---

Definition of `IsLittleO` in terms of filters.  -/
Asymptotics.IsLittleO.of_bound : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → f =o[l] g
-- Init.Data.Option.Lemmas
Option.min_eq_or : ∀ {α : Type u_1} [LE α] [inst : Min α], (∀ (x y : α), x ⊓ y = x ∨ x ⊓ y = y) → ∀ {a b : Option α}, a ⊓ b = a ∨ a ⊓ b = b
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.mkMetric.congr_simp : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  (m m_1 : ENNReal → ENNReal), m = m_1 → MeasureTheory.Measure.mkMetric m = MeasureTheory.Measure.mkMetric m_1
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_of_support_subset : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {f : Π₀ (i : ι), β i}
  {g : (i : ι) → β i → γ} {s : Finset ι}, f.support ⊆ s → (∀ i ∈ s, g i 0 = 0) → f.sum g = ∑ i ∈ s, g i (f i)
-- Mathlib.Data.Finsupp.Basic
Finsupp.notMem_graph_snd_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) (f : α →₀ M), (a, 0) ∉ f.graph
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.exp_log : ∀ {x : ℂ}, x ≠ 0 → Complex.exp (Complex.log x) = x
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Config.mk.inj : ∀ {maxSteps maxSteps_1 : ℕ}, { maxSteps := maxSteps } = { maxSteps := maxSteps_1 } → maxSteps = maxSteps_1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.forget_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Under X},
  (CategoryTheory.Under.forget X).obj U = U.right
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRecFromOne_eq : ∀ {motive : ℕ → Sort u} {zero : motive 0} {one : motive 1}
  {bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (Nat.bit b n)} (b : Bool) (n : ℕ) (h : n ≠ 0),
  Nat.binaryRecFromOne zero one bit (Nat.bit b n) = bit b n h (Nat.binaryRecFromOne zero one bit n)
-- Mathlib.Order.Circular
sbtw_cyclic_left : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c a
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.hom_inv_apply : ∀ {M N : MonCat} (e : M ≅ N) (s : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Init.System.ST
ST.Out.mk.injEq : ∀ {σ α : Type} (val : α) (state : Void σ) (val_1 : α) (state_1 : Void σ),
  ({ val := val, state := state } = { val := val_1, state := state_1 }) = (val = val_1 ∧ state = state_1)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instNeg : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → Neg (LieDerivation R L M)
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), ↑e.toPartialEquiv = ⇑e
-- Lean.Meta.Basic
Lean.Meta.Diagnostics.mk.injEq : ∀ (unfoldCounter unfoldAxiomCounter heuristicCounter instanceCounter : Lean.PHashMap Lean.Name ℕ)
  (synthPendingFailures : Lean.PHashMap Lean.Expr Lean.MessageData)
  (unfoldCounter_1 unfoldAxiomCounter_1 heuristicCounter_1 instanceCounter_1 : Lean.PHashMap Lean.Name ℕ)
  (synthPendingFailures_1 : Lean.PHashMap Lean.Expr Lean.MessageData),
  ({ unfoldCounter := unfoldCounter, unfoldAxiomCounter := unfoldAxiomCounter, heuristicCounter := heuristicCounter,
        instanceCounter := instanceCounter, synthPendingFailures := synthPendingFailures } =
      { unfoldCounter := unfoldCounter_1, unfoldAxiomCounter := unfoldAxiomCounter_1,
        heuristicCounter := heuristicCounter_1, instanceCounter := instanceCounter_1,
        synthPendingFailures := synthPendingFailures_1 }) =
    (unfoldCounter = unfoldCounter_1 ∧
      unfoldAxiomCounter = unfoldAxiomCounter_1 ∧
        heuristicCounter = heuristicCounter_1 ∧
          instanceCounter = instanceCounter_1 ∧ synthPendingFailures = synthPendingFailures_1)
-- Batteries.Data.Array.Scan
Array.scanlM_pure : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → β}
  {as : Array α}, Array.scanlM (fun x1 x2 => pure (f x1 x2)) init as = pure (Array.scanl f init as)
-- Mathlib.Order.SupIndep
/-- **Alias** of the reverse direction of `Finset.supIndep_iff_pairwiseDisjoint`. -/
Set.PairwiseDisjoint.supIndep : ∀ {α : Type u_1} {ι : Type u_3} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  (↑s).PairwiseDisjoint f → s.SupIndep f
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_unop : ∀ {G : Type u_2} [inst : Group G] (S : Subgroup Gᵐᵒᵖ), S.unop.op = S
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex is finite iff the total number of its cells is finite.  -/
Topology.RelCWComplex.finite_iff_finite_cells : ∀ {X : Type u_2} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D],
  Topology.RelCWComplex.Finite C ↔ Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
-- Init.Data.Format.Basic
Std.Format.append.injEq : ∀ (a a_1 a_2 a_3 : Std.Format), (a.append a_1 = a_2.append a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_one : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  TensorProduct.AlgebraTensorModule.map 1 1 = 1
-- Mathlib.CategoryTheory.EpiMono
/-- Every split epi whose section is epi is an iso.  -/
CategoryTheory.IsIso.of_epi_section' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (hf : CategoryTheory.SplitEpi f)
  [CategoryTheory.Epi hf.section_], CategoryTheory.IsIso f
-- Init.System.IOError
IO.Error.otherError.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.otherError osCode details = IO.Error.otherError osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Order.Hom.Basic
/-- A strictly monotone function with a right inverse is an order isomorphism.  -/
StrictMono.orderIsoOfRightInverse : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrder α] →
      [inst_1 : Preorder β] → (f : α → β) → StrictMono f → (g : β → α) → Function.RightInverse g f → α ≃o β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasStrictDerivAt_arccos : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → HasStrictDerivAt Real.arccos (-(1 / √(1 - x ^ 2))) x
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- The ring equivalence defined by a pair of ring homomorphisms satisfying `RingHomInvPair`.  -/
RingHomInvPair.toRingEquiv : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] → (σ : R₁ →+* R₂) → (σ' : R₂ →+* R₁) → [RingHomInvPair σ σ'] → R₁ ≃+* R₂
-- Lean.Compiler.InitAttr
_private.Lean.Compiler.InitAttr.0.Lean.runInitAttrs : Lean.Environment → Lean.Options → IO Unit
-- Init.Data.List.Attach
List.map_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β}, List.map f (wfParam xs) = List.map f xs.attach.unattach
-- Mathlib.Data.Finset.Image
/-- If the image of a finset is nontrivial, the finset is nontrivial.
For the converse direction under an injectivity hypothesis see `Finset.Nontrivial.image_of_injOn`,
and for the combined iff see `Finset.image_nontrivial_iff_of_injOn`.  -/
Finset.nontrivial_of_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
  (Finset.image f s).Nontrivial → s.Nontrivial
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toList_ne_nil : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toList ≠ []
-- Mathlib.Algebra.Ring.Opposite
/-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines
a ring homomorphism from `Rᵐᵒᵖ`.  -/
RingHom.fromOpposite : {R : Type u_2} →
  {S : Type u_3} →
    [inst : Semiring R] → [inst_1 : Semiring S] → (f : R →+* S) → (∀ (x y : R), Commute (f x) (f y)) → Rᵐᵒᵖ →+* S
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.sub_const : ∀ {𝕜 : 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 : E → F}
  {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → ∀ (c : F), DifferentiableWithinAt 𝕜 (fun y => f y - c) s x
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ComposableArrows.Precomp.map.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (isLt : 0 < n + 1 + 1) (isLt_1 : 1 < n + 1 + 1) (x_3 : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩),
  CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨1, isLt_1⟩ x_3 = f
-- Mathlib.Algebra.Group.Prod
addAddHom_apply : ∀ {α : Type u_6} [inst : AddCommSemigroup α] (a : α × α), addAddHom a = a.1 + a.2
-- Lean.EnvExtension
/-- Get the current state of the given `SimplePersistentEnvExtension`.  -/
Lean.SimplePersistentEnvExtension.getState : {α σ : Type} →
  [Inhabited σ] →
    (ext : Lean.SimplePersistentEnvExtension α σ) →
      Lean.Environment →
        optParam Lean.EnvExtension.AsyncMode ext.toEnvExtension.asyncMode → optParam Lean.Name Lean.Name.anonymous → σ
-- Mathlib.Order.Cover
WithTop.coe_covBy_top : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ↑a ⋖ ⊤ ↔ IsMax a
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Given an exact pairing on `Y Y'`,
we get a bijection on hom-sets `(Y' ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z)`
by "pulling the string on the left" up or down.

This gives the adjunction `tensorLeftAdjunction Y Y' : tensorLeft Y' ⊣ tensorLeft Y`.

This adjunction is often referred to as "Frobenius reciprocity" in the
fusion categories / planar algebras / subfactors literature.
 -/
CategoryTheory.tensorLeftHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Y' Z : C) →
        [CategoryTheory.ExactPairing Y Y'] →
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y' X ⟶ Z) ≃
            (X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricMeasure_pos : ∀ {p : ↑unitInterval}, p ≠ 0 → p ≠ 1 → ∀ (n : ℕ), 0 < (1 - ↑p) ^ n * ↑p
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.not_mem_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → k ∉ t₁ \ t₂
-- Mathlib.LinearAlgebra.Dimension.Finite
exists_finset_linearIndependent_of_le_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  ↑n ≤ Module.rank R M → ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  a ≤ b → ¬IsMin a → insert a (Set.Ioc a b) = Set.Ioc (Order.pred a) b
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map which maps zero to zero,
`j : M →+ M'` is a monoid map which sends non-zero elements to non-zero elements, such that the
scalar multiplications on `M` and `M'` are compatible, then `j` sends linearly independent families
of vectors to linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map'`.  -/
LinearIndependent.map_of_surjective_injective : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {R' : Type u_6} {M' : Type u_7} [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R' M'],
  LinearIndependent R v →
    ∀ (i : R → R') (j : M →+ M'),
      Function.Surjective i →
        (∀ (m : M), j m = 0 → m = 0) → (∀ (r : R) (m : M), j (r • m) = i r • j m) → LinearIndependent R' (⇑j ∘ v)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteProducts.reflects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsFiniteProducts F] (n : ℕ),
  CategoryTheory.Limits.ReflectsLimitsOfShape (CategoryTheory.Discrete (Fin n)) F
-- Mathlib.GroupTheory.Congruence.Star
addConGen_star : ∀ {A : Type u_1} [inst : AddMonoid A] [inst_1 : StarAddMonoid A] {r : A → A → Prop},
  (∀ (a b : A), r a b → r (star a) (star b)) → ∀ ⦃a b : A⦄, (addConGen r) a b → (addConGen r) (star a) (star b)
-- Lean.ExtraModUses
/-- Whether dependency must be imported as `public`.  -/
Lean.ExtraModUse.isExported : Lean.ExtraModUse → Bool
-- Mathlib.Tactic.ComputeDegree
/-- `monicity` tries to solve a goal of the form `Monic f`.
It converts the goal into a goal of the form `natDegree f ≤ n` and one of the form `f.coeff n = 1`
and calls `compute_degree` on those two goals.

The variant `monicity!` starts like `monicity`, but calls `compute_degree!` on the two side-goals.
 -/
Mathlib.Tactic.ComputeDegree.tacticMonicity! : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_srem : ∀ (a b : BitVec 64), Int64.ofBitVec (a.srem b) = Int64.ofBitVec a % Int64.ofBitVec b
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly₂.instInhabitedHAdd : {p : ℕ} → [inst : Fact (Nat.Prime p)] → Inhabited (WittVector.IsPoly₂ p fun x x_1 x1 x2 => x1 + x2)
-- Mathlib.Topology.Order.Lattice
Continuous.finset_sup_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L},
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => s.sup fun x => f x a
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sum_X_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (i : E.I₀), (E.sum F).X (Sum.inl i) = E.X i
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertList_of_contains_left_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getEntry? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getEntry? k toInsert
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Hom.base : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y : AlgebraicGeometry.PresheafedSpace C} → X.Hom Y → (↑X ⟶ ↑Y)
-- Mathlib.RingTheory.MvPolynomial
MvPolynomial.finrank_eq_one : ∀ {σ : Type u} {K : Type v} [inst : CommRing K] [IsEmpty σ], Module.finrank K (MvPolynomial σ K) = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f f_1 : K.X p ⟶ X),
  f = f_1 →
    ∀ {n : ℤ} (x : p + n = q) (T : CochainComplex.HomComplex.Triplet n),
      CochainComplex.HomComplex.Cochain.toSingleMk f x T = CochainComplex.HomComplex.Cochain.toSingleMk f_1 x T
-- Mathlib.Tactic.CancelDenoms.Core
/-- An expression with denominators cancelled.  -/
Mathlib.Tactic.CancelDenoms.CancelResult.cancelled : {u : Lean.Level} →
  {α : Q(Type u)} → {mα : Q(Mul «$α»)} → {e v : Q(«$α»)} → Mathlib.Tactic.CancelDenoms.CancelResult mα e v → Q(«$α»)
-- Mathlib.Logic.Equiv.Defs
/-- An equivalence `f : α₁ ≃ α₂` generates an equivalence between `Σ a, β (f a)` and `Σ a, β a`.  -/
Equiv.sigmaCongrLeft : {α₁ : Type u_1} → {α₂ : Type u_2} → {β : α₂ → Type u_3} → (e : α₁ ≃ α₂) → (a : α₁) × β (e a) ≃ (a : α₂) × β a
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_singleton_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, Set.Icc a b = {c} ↔ a = c ∧ b = c
-- Mathlib.Data.Multiset.FinsetOps
Multiset.cons_ndunion : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α) (a : α),
  (a ::ₘ s).ndunion t = Multiset.ndinsert a (s.ndunion t)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineIsometry.toAffineIsometryEquiv_apply : ∀ {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : NormedAddCommGroup V₁] [inst_2 : SeminormedAddCommGroup V₂] [inst_3 : NormedSpace 𝕜 V₁]
  [inst_4 : NormedSpace 𝕜 V₂] [inst_5 : MetricSpace P₁] [inst_6 : PseudoMetricSpace P₂] [inst_7 : NormedAddTorsor V₁ P₁]
  [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : FiniteDimensional 𝕜 V₁] [inst_10 : FiniteDimensional 𝕜 V₂]
  [inst_11 : Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : Module.finrank 𝕜 V₁ = Module.finrank 𝕜 V₂) (x : P₁),
  (li.toAffineIsometryEquiv h) x = li x
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar : ∀ {ι : Type u_1} [Finite ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ},
  LinearMap.det f ≠ 0 →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [μ.IsAddHaarMeasure],
      MeasureTheory.Measure.map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
-- Mathlib.Algebra.Star.Basic
star_zpow₀ : ∀ {R : Type u} [inst : GroupWithZero R] [inst_1 : StarMul R] (x : R) (z : ℤ), star (x ^ z) = star x ^ z
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittAdd_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.wittAdd p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, if an `AddCommMonoid` map
`g : M →+ P` induces a map `f.lift hg : N →+ P` then for all `z : N`, we have
`g y + f.lift hg z = g x`, where `x : M, y ∈ S` are such that `z + f y = f x`.  -/
AddSubmonoid.LocalizationMap.lift_add_left : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N),
  g ↑(f.sec z).2 + (f.lift hg) z = g (f.sec z).1
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- To UV-compress a set family, we compress each of its elements, except that we don't want to
reduce the cardinality, so we keep all elements whose compression is already present.  -/
UV.compression : {α : Type u_1} →
  [inst : GeneralizedBooleanAlgebra α] →
    [DecidableRel Disjoint] → [DecidableLE α] → [DecidableEq α] → α → α → Finset α → Finset α
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal} {g : α → E},
  AEMeasurable f μ →
    MeasureTheory.Integrable (f • g) μ → μ.withDensityᵥ (f • g) = (μ.withDensity fun x => ↑(f x)).withDensityᵥ g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, Std.DTreeMap.Const.get? (t₁ ∩ t₂) k = if k ∈ t₂ then Std.DTreeMap.Const.get? t₁ k else none
-- Mathlib.Data.ZMod.Units
ZMod.unitsMap.congr_simp : ∀ {n m : ℕ} (hm : n ∣ m), ZMod.unitsMap hm = ZMod.unitsMap hm
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.AtomIso.mk : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.AtomIso
-- Init.Data.List.Nat.Modify
List.modify_cons : ∀ {α : Type u_1} {f : α → α} {a : α} {l : List α} {i : ℕ},
  (a :: l).modify i f = if i = 0 then f a :: l else a :: l.modify (i - 1) f
-- Mathlib.RingTheory.Idempotents
/-- A complete orthogonal family of idempotents in a commutative semiring
give rise to a direct product decomposition.  -/
CompleteOrthogonalIdempotents.ringEquivOfComm : {R : Type u_1} →
  {I : Type u_2} →
    [inst : Fintype I] →
      {e : I → R} → [inst_1 : CommSemiring R] → (he : CompleteOrthogonalIdempotents e) → R ≃+* ((i : I) → ⋯.Corner)
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.mul_right : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] [IsLinearTopology S S] (c : σ → S)
  {x : σ → S}, MvPowerSeries.HasEval x → MvPowerSeries.HasEval (x * c)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} [F.Final] (i : F ≅ F'), F'.Final
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_div_two : Real.cos (Real.pi / 2) = 0
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoalParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.PlainGoalParams
-- Mathlib.Computability.Partrec
Computable₂.partrec₂ : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, Computable₂ f → Partrec₂ fun a => ↑(f a)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.norm_vadd_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)), ‖c +ᵥ f‖ = ‖f‖
-- Mathlib.Algebra.Group.ForwardDiff
/-- **Alias** of `fwdDiff_iter_finsetSum`. -/
fwdDiff_iter_finset_sum : ∀ {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) (n : ℕ), (fwdDiff h)^[n] (∑ k ∈ s, f k) = ∑ k ∈ s, (fwdDiff h)^[n] (f k)
-- Init.Data.String.Basic
String.utf8ByteSize_slice : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂}, (s.slice p₁ p₂ h).utf8ByteSize = p₂.offset.byteIdx - p₁.offset.byteIdx