mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.SolveByElim
/-- `mkAssumptionSet` builds a collection of lemmas for use in
the backtracking search in `solve_by_elim`.

* By default, it includes all local hypotheses, along with `rfl`, `trivial`, `congrFun`
  and `congrArg`.
* The flag `noDefaults` removes these.
* The flag `star` includes all local hypotheses, but not `rfl`, `trivial`, `congrFun`,
  or `congrArg`. (It doesn't make sense to use `star` without `noDefaults`.)
* The argument `add` is the list of terms inside the square brackets that did not have `-`
  and can be used to add expressions or local hypotheses
* The argument `remove` is the list of terms inside the square brackets that had a `-`,
  and can be used to remove local hypotheses.
  (It doesn't make sense to remove expressions which are not local hypotheses,
  to remove local hypotheses unless `!noDefaults || star`,
  and it does not make sense to use `star` unless you remove at least one local hypothesis.)

`mkAssumptionSet` returns not a `List expr`, but a `List (TermElabM Expr) × TermElabM (List Expr)`.
There are two separate problems that need to be solved.

### Stuck metavariables

Lemmas with implicit arguments would be filled in with metavariables if we created the
`Expr` objects immediately, so instead we return thunks that generate the expressions
on demand. This is the first component, with type `List (TermElabM Expr)`.

As an example, we have `def rfl : ∀ {α : Sort u} {a : α}, a = a`, which on elaboration will become
`@rfl ?m_1 ?m_2`.

Because `solve_by_elim` works by repeated application of lemmas against subgoals,
the first time such a lemma is successfully applied,
those metavariables will be unified, and thereafter have fixed values.
This would make it impossible to apply the lemma
a second time with different values of the metavariables.

See https://github.com/leanprover-community/mathlib/issues/2269

### Relevant local hypotheses

`solve_by_elim*` works with multiple goals,
and we need to use separate sets of local hypotheses for each goal.
The second component of the returned value provides these local hypotheses.
(Essentially using `getLocalHyps`, along with some filtering to remove hypotheses
that have been explicitly removed via `only` or `[-h]`.)

 -/
Lean.Meta.SolveByElim.mkAssumptionSet : Bool →
  Bool →
    List Lean.Term →
      List Lean.Term →
        Array Lean.Ident →
          Lean.MetaM
            (List (Lean.Elab.TermElabM Lean.Expr) ×
              (Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Elab.TermElabM (List Lean.Expr)))
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instDeterministicHomRightUnitor : ∀ {X : SFinKer}, CategoryTheory.Deterministic (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicBound.default : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toArray_roc : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m<...=n).toArray.size), (m<...=n).toArray[i] = m + 1 + ↑i
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.mem_closure : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {x : M},
  x ∈ AddSubsemigroup.closure s ↔ ∀ (S : AddSubsemigroup M), s ⊆ ↑S → x ∈ S
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonApp : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.map_pow : ∀ {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : Semiring β] (f : α →+* β) (a : α) (n : ℕ),
  f (a ^ n) = f a ^ n
-- Batteries.Tactic.Trans
/-- Environment extension storing transitivity lemmas  -/
Batteries.Tactic.transExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)
-- Init.Data.Option.Basic
/-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
`none ~ none`.  -/
Option.Rel : {α : Type u_1} → {β : Type u_2} → (α → β → Prop) → Option α → Option β → Prop
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
equivalence.  -/
CStarMatrix.reindexₗ : {m : Type u_1} →
  {n : Type u_2} →
    (R : Type u_3) →
      (A : Type u_5) →
        {l : Type u_7} →
          {o : Type u_8} →
            [inst : Semiring R] →
              [inst_1 : AddCommMonoid A] →
                [inst_2 : Module R A] → m ≃ l → n ≃ o → CStarMatrix m n A ≃ₗ[R] CStarMatrix l o A
-- Mathlib.Data.Finset.Preimage
Finset.card_preimage : ∀ {α : Type u} {β : Type v} (s : Finset β) (f : α → β) (hf : Set.InjOn f (f ⁻¹' ↑s))
  [inst : DecidablePred fun x => x ∈ Set.range f], (s.preimage f hf).card = {x ∈ s | x ∈ Set.range f}.card
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instInhabitedExtTheorems : Inhabited Lean.Meta.Ext.ExtTheorems
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.diagonal_SpecMap : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  CategoryTheory.Limits.pullback.diagonal (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      (AlgebraicGeometry.pullbackSpecIso R S S).inv
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.measure_preimage : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  μ s ≠ 0 →
    μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → ∀ {A : Set E}, MeasurableSet A → ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Bird's equation (3), assuming equation (1) at `p` as the induction hypothesis.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.paper_eq3 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} (i j : Fin n),
  BirdDet.Eq1✝ A p →
    (BirdDet.Spec.stepEntry A)^[p + 1] A i j =
      (-1) ^ (p + 1) *
        (∑ α ∈ BirdDet.S✝ (p + 1) i, BirdDet.pminor✝ A α * A i j -
          ∑ k > i, ∑ α ∈ BirdDet.S✝ p i, BirdDet.bminor✝ A i k α * A k j)
-- Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
_private.Mathlib.Algebra.Module.StablyFree.FreeOfInvertible.0.exteriorPower.cofactorToLeft.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {n : ℕ} (bN : Module.Basis (Fin n) R N),
  exteriorPower.cofactorToLeft✝ bN =
    exteriorPower.alternatingMapLinearEquiv (AlternatingMap.alternatizeUncurryFin (exteriorPower.cofactorLinear✝ bN))
-- Batteries.Data.List.Pairwise
List.pwFilter_subset : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] (l : List α), List.pwFilter R l ⊆ l
-- Mathlib.Data.Finset.Sups
Finset.disjSups_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s₁ s₂ t₁ t₂ : Finset α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁.disjSups t₁ ⊆ s₂.disjSups t₂
-- ProofWidgets.Data.Html
Lean.Parser.Category.proofWidgetsJsxAttrVal : Lean.Parser.Category
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.v₁₂.τ₃ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₃ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find
`i ∈ t` such that `‖∑ j ∈ t, f j‖ ≤ ‖f i‖`.  -/
IsUltrametricDist.exists_norm_finsetSum_le_of_nonempty : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {t : Finset ι},
  t.Nonempty → ∀ (f : ι → M), ∃ i ∈ t, ‖∑ j ∈ t, f j‖ ≤ ‖f i‖
-- Init.Data.Option.Basic
Option.max_none_left : ∀ {α : Type u_1} [inst : Max α] {o : Option α}, none ⊔ o = o
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.of : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C),
  ∀ S ∈ J.coverings X, J.Saturate X (CategoryTheory.Sieve.generate S)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t : Cone F.op` is a limit cone, then `t.unop : Cocone F` is a colimit cocone.
 -/
CategoryTheory.Limits.IsLimit.unop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F.op} →
            CategoryTheory.Limits.IsLimit t → CategoryTheory.Limits.IsColimit t.unop
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.SavedState.mk.sizeOf_spec : ∀ (term : Lean.Elab.Term.SavedState) (tactic : Lean.Elab.Tactic.State),
  sizeOf { term := term, tactic := tactic } = 1 + sizeOf term + sizeOf tactic
-- Init.Data.SInt.Lemmas
ISize.ofInt_eq_ofNat : ∀ {n : ℕ}, ISize.ofInt ↑n = ISize.ofNat n
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1, h with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      h_3 => h_2 size k v l size_2 k_2 v_2 l_1 r h r_2 h_3) =
    h_2 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 h
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.not_coprime_iff_dvd : ∀ {m n : ℕ}, ¬m.Coprime n ↔ ∃ p, Nat.Prime p ∧ p ∣ m ∧ p ∣ n
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.map_hexagon_forward : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app
                ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))).hom
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app
                ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).hom
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
          (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app
                  ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.maxKey?.get ⋯ = km → t.getKey km hc = km
-- Init.Data.String.Lemmas.Splits
String.splits_slice : ∀ {s : String} {p₀ p₁ : s.Pos} (h : p₀ ≤ p₁) (p : (s.slice p₀ p₁ h).Pos),
  p.Splits (s.slice p₀ (String.Pos.ofSlice p) ⋯).copy (s.slice (String.Pos.ofSlice p) p₁ ⋯).copy
-- Mathlib.Analysis.RCLike.Extend
Module.Dual.extendRCLikeₗ_symm_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (f : Module.Dual 𝕜 F), Module.Dual.extendRCLikeₗ.symm f = RCLike.reLm ∘ₗ ↑ℝ f
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balRight.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α)
  (c : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l),
  (match RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) with
    | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
    | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
    | l => h_3 l) =
    h_2 a x b y c
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_vadd_inter : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  ((x +ᵥ A) ∩ B).card = A.addConvolution (-B) (-x)
-- Mathlib.Data.Set.Inclusion
Set.inclusion_inj : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t) {x y : ↑s}, Set.inclusion h x = Set.inclusion h y ↔ x = y
-- Mathlib.Order.InitialSeg
InitialSeg.antisymm_toFun : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : InitialSeg r s)
  (g : InitialSeg s r), ⇑(f.antisymm g) = ⇑f
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.map_pi_eq_stdGaussian : ∀ {ι : Type u_1} [inst : Fintype ι],
  MeasureTheory.Measure.map (WithLp.toLp 2) (MeasureTheory.Measure.pi fun x => ProbabilityTheory.gaussianReal 0 1) =
    ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.post_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
  [inst_3 : CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)] {E : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} E]
  (H : CategoryTheory.Functor D E) [h : CategoryTheory.Limits.HasColimit ((F.comp G).comp H)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post (F.comp G) H)
      (H.map (CategoryTheory.Limits.colimit.post F G)) =
    CategoryTheory.Limits.colimit.post F (G.comp H)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.WeakRankFunction.mk.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (rank rank_1 : h.ι → α)
  (e_rank : rank = rank_1) (lt : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y),
  { rank := rank, lt := lt } = { rank := rank_1, lt := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Basic
RootPairing.ext_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] [Finite ι] [CharZero R] [IsDomain R]
  [Module.IsTorsionFree R M] {P₁ P₂ : RootPairing ι R M N},
  P₁ = P₂ ↔ P₁.toLinearMap = P₂.toLinearMap ∧ P₁.root = P₂.root ∧ Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot
-- Mathlib.Data.Sym.Basic
Sym.eq_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {s : Sym α n} {a : α}, s = Sym.replicate n a ↔ ∀ b ∈ s, b = a
-- Mathlib.RingTheory.Flat.Equalizer
/-- (Implementation): Inverse for `LinearMap.tensorKerEquiv`.  -/
LinearMap.tensorKerInv : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f : N →ₗ[R] P) →
                                  [Module.Flat R M] →
                                    ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker →ₗ[S]
                                      TensorProduct R M ↥f.ker
-- Mathlib.Analysis.InnerProductSpace.Subspace
/-- A family `f` of mutually-orthogonal elements of `E` is summable, if and only if
`(fun i ↦ ‖f i‖ ^ 2)` is summable.  -/
OrthogonalFamily.summable_iff_norm_sq_summable : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ [CompleteSpace E] (f : (i : ι) → G i), (Summable fun i => (V i) (f i)) ↔ Summable fun i => ‖f i‖ ^ 2
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
/-- The composition of the normalizing isomorphisms `η_f : p ≫ f ≅ pf` and `η_g : pf ≫ g ≅ pfg`.  -/
Mathlib.Tactic.Bicategory.normalizeIsoComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      {p : a ⟶ b} →
        {f : b ⟶ c} →
          {g : c ⟶ d} →
            {pf : a ⟶ c} →
              {pfg : a ⟶ d} →
                (CategoryTheory.CategoryStruct.comp p f ≅ pf) →
                  (CategoryTheory.CategoryStruct.comp pf g ≅ pfg) →
                    (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp f g) ≅ pfg)
-- Lean.Syntax
Lean.SyntaxNode : Type
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, k ∈ t → (t.insertMany l).get? k = t.get? k
-- Mathlib.Data.List.Sort
RelEmbedding.pairwise_swap_listMap : ∀ {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α},
  List.Pairwise (Function.swap rb) (List.map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `liminf (xᵢ - c) = (liminf xᵢ) - c`.  -/
liminf_sub_const : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [F.NeBot] [inst_4 : AddCommSemigroup R] [inst_5 : Sub R] [ContinuousSub R]
  [OrderedSub R] (f : ι → R) (c : R),
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f → Filter.liminf (fun i => f i - c) F = Filter.liminf f F - c
-- Mathlib.SetTheory.ZFC.PSet
PSet.setoid : Setoid PSet.{u_1}
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized₀.congr_simp : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p p_1 : Submonoid R) (e_p : p = p_1)
  (f f_1 : M →ₗ[R] N) (e_f : f = f_1) [inst_5 : IsLocalizedModule p f] (M' M'_1 : Submodule R M),
  M' = M'_1 → Submodule.localized₀ p f M' = Submodule.localized₀ p_1 f_1 M'_1
-- Lean.Data.Json.FromToJson.Basic
Lean.NameMap.fromJson? : {α : Type} → [Lean.FromJson α] → Lean.Json → Except String (Lean.NameMap α)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.provideds : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State → Array Bool
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.coeff_expand_of_not_dvd : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) {m : σ →₀ ℕ} {i : σ},
  ¬p ∣ m i → (MvPowerSeries.coeff m) ((MvPowerSeries.expand p hp) φ) = 0
-- Lean.SubExpr
/-- A subexpression of the goal type.  -/
Lean.SubExpr.GoalLocation.target : Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
-- Mathlib.Topology.Homotopy.Lifting
PathConnectedSpace.somePath.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : PathConnectedSpace X] (x y : X),
  PathConnectedSpace.somePath x y = PathConnectedSpace.somePath x y
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.sectionsEquivHom_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type u₂)) (X : Type u₂)
  [inst_1 : Unique X] (s : ↑F.sections) (j : C), ((F.sectionsEquivHom X) s).app j = TypeCat.ofHom fun x => ↑s j
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ), f.resultant g m n = (f.sylvester g m n).det