ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra K L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Finite K L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Free R M<VAR>x y : L<VAR>r : R<VAR>b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L<GOAL>Polynomial.map ((evalRingHom r).comp ↑(MvPolynomial.aeval fun i => C ((b.repr y) i) * X + C ((b.repr x) i))) ((↑φ).polyCharpoly b) = charpoly (φ (r • y + x))
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra K L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Finite K L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Free R M<VAR>x y : L<VAR>r : R<VAR>b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L<VAR>aux : (fun i => (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))<GOAL>Polynomial.map ((evalRingHom r).comp ↑(MvPolynomial.aeval fun i => C ((b.repr y) i) * X + C ((b.repr x) i))) ((↑φ).polyCharpoly b) = charpoly (φ (r • y + x))
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : IsDomain R<VAR>h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : IsDomain R<VAR>h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>∀ (p : ℕ), p ≠ 0 → CharP R p → P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : IsDomain R<VAR>h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<VAR>p : ℕ<VAR>p_pos : p ≠ 0<VAR>p_char : CharP R p<GOAL>P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : IsDomain R<VAR>h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<VAR>p : ℕ<VAR>p_pos : p ≠ 0<VAR>p_char : CharP R p<VAR>p_prime : Nat.Prime p<GOAL>P
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + k
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>t : Finset α<VAR>x✝ : t ∈ 𝒜<VAR>hst : t ⊆ t✝<GOAL>(t✝ \ t).card = k ↔ t✝.card = t.card + k
<VAR>G : Type u<VAR>inst✝² : Groupoid G<VAR>inst✝¹ : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>a b : Generators G<VAR>e : a ⟶ b<VAR>H : e ∈ wideSubquiverSymmetrify T a b<GOAL>loopOfHom T (of e) = 𝟙 (IsFreeGroupoid.SpanningTree.root' T)
<VAR>G : Type u<VAR>inst✝² : Groupoid G<VAR>inst✝¹ : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>a b : Generators G<VAR>e : a ⟶ b<VAR>H : e ∈ wideSubquiverSymmetrify T a b<GOAL>treeHom T (let_fun this := a; this) ≫ of e = treeHom T b
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>R₄ : Type u_4<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>E₄ : Type u_8<VAR>F : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝³³ : Semiring R<VAR>inst✝³² : Semiring R₂<VAR>inst✝³¹ : Semiring R₃<VAR>inst✝³⁰ : Semiring R₄<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₁₄ : R →+* R₄<VAR>σ₄₁ : R₄ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₄₂ : R₄ →+* R₂<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₄₃ : R₄ →+* R₃<VAR>inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁<VAR>inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃<VAR>inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂<VAR>inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃<VAR>inst✝²³ : RingHomInvPair σ₁₄ σ₄₁<VAR>inst✝²² : RingHomInvPair σ₄₁ σ₁₄<VAR>inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂<VAR>inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄<VAR>inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃<VAR>inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄<VAR>inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁<VAR>inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂<VAR>inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁<VAR>inst✝⁹ : SeminormedAddCommGroup E<VAR>inst✝⁸ : SeminormedAddCommGroup E₂<VAR>inst✝⁷ : SeminormedAddCommGroup E₃<VAR>inst✝⁶ : SeminormedAddCommGroup E₄<VAR>inst✝⁵ : Module R E<VAR>inst✝⁴ : Module R₂ E₂<VAR>inst✝³ : Module R₃ E₃<VAR>inst✝² : Module R₄ E₄<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : Module R F<VAR>e✝ e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>range ⇑e = univ
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>R₄ : Type u_4<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>E₄ : Type u_8<VAR>F : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝³³ : Semiring R<VAR>inst✝³² : Semiring R₂<VAR>inst✝³¹ : Semiring R₃<VAR>inst✝³⁰ : Semiring R₄<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₁₄ : R →+* R₄<VAR>σ₄₁ : R₄ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₄₂ : R₄ →+* R₂<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₄₃ : R₄ →+* R₃<VAR>inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁<VAR>inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃<VAR>inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂<VAR>inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃<VAR>inst✝²³ : RingHomInvPair σ₁₄ σ₄₁<VAR>inst✝²² : RingHomInvPair σ₄₁ σ₁₄<VAR>inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂<VAR>inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄<VAR>inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃<VAR>inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄<VAR>inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁<VAR>inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂<VAR>inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁<VAR>inst✝⁹ : SeminormedAddCommGroup E<VAR>inst✝⁸ : SeminormedAddCommGroup E₂<VAR>inst✝⁷ : SeminormedAddCommGroup E₃<VAR>inst✝⁶ : SeminormedAddCommGroup E₄<VAR>inst✝⁵ : Module R E<VAR>inst✝⁴ : Module R₂ E₂<VAR>inst✝³ : Module R₃ E₃<VAR>inst✝² : Module R₄ E₄<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : Module R F<VAR>e✝ e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>range ⇑e.toIsometryEquiv = univ
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsOpen s<GOAL>IsOpen (Sigma.mk i '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsOpen s<GOAL>∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsOpen s<VAR>j : ι<GOAL>IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>j : ι<VAR>s : Set (σ j)<VAR>hs : IsOpen s<GOAL>IsOpen (Sigma.mk j ⁻¹' (Sigma.mk j '' s))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsOpen s<VAR>j : ι<VAR>hne : j ≠ i<GOAL>IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.6198, u_1} C<VAR>inst✝ : Category.{?u.6202, u_2} D<VAR>F : C ⥤ Cat<VAR>X Y Z : Grothendieck F<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>(F.map (f.base ≫ g.base)).obj X.fiber = (F.map g.base).obj ((F.map f.base).obj X.fiber)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x : M<VAR>b : Basis ι R M<VAR>i : ι<VAR>f : ι →₀ R<GOAL>(b.coord i) (b.repr.symm f) = f i
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N : Type w<VAR>inst✝ : L.Structure N<VAR>hn : K.Nonempty<VAR>h : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)<VAR>hc : (Quotient.mk' '' K).Countable<VAR>fg : ∀ M ∈ K, Structure.FG L ↑M<VAR>hp : Hereditary K<VAR>jep : JointEmbedding K<GOAL>∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N : Type w<VAR>inst✝ : L.Structure N<VAR>hn : K.Nonempty<VAR>h : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)<VAR>hc : (Quotient.mk' '' K).Countable<VAR>fg : ∀ M ∈ K, Structure.FG L ↑M<VAR>hp : Hereditary K<VAR>jep : JointEmbedding K<VAR>F : ℕ → Quotient equivSetoid<VAR>hF : Quotient.mk' '' K = range F<GOAL>∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N : Type w<VAR>inst✝ : L.Structure N<VAR>hn : K.Nonempty<VAR>h : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)<VAR>hc : (Quotient.mk' '' K).Countable<VAR>fg : ∀ M ∈ K, Structure.FG L ↑M<VAR>hp : Hereditary K<VAR>jep : JointEmbedding K<VAR>F : ℕ → Quotient equivSetoid<VAR>hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, Quotient.mk' x = ⟦a⟧) ↔ ∃ y, F y = ⟦a⟧<GOAL>∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N : Type w<VAR>inst✝ : L.Structure N<VAR>hn : K.Nonempty<VAR>h : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)<VAR>hc : (Quotient.mk' '' K).Countable<VAR>fg : ∀ M ∈ K, Structure.FG L ↑M<VAR>hp : Hereditary K<VAR>jep : JointEmbedding K<VAR>F : ℕ → Quotient equivSetoid<VAR>hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a<GOAL>∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N : Type w<VAR>inst✝ : L.Structure N<VAR>hn : K.Nonempty<VAR>h : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)<VAR>hc : (Quotient.mk' '' K).Countable<VAR>fg : ∀ M ∈ K, Structure.FG L ↑M<VAR>hp : Hereditary K<VAR>jep : JointEmbedding K<VAR>F : ℕ → Quotient equivSetoid<VAR>hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a<VAR>hF' : ∀ (n : ℕ), (F n).out ∈ K<GOAL>∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N : Type w<VAR>inst✝ : L.Structure N<VAR>hn : K.Nonempty<VAR>h : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)<VAR>hc : (Quotient.mk' '' K).Countable<VAR>fg : ∀ M ∈ K, Structure.FG L ↑M<VAR>hp : Hereditary K<VAR>jep : JointEmbedding K<VAR>F : ℕ → Quotient equivSetoid<VAR>hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a<VAR>hF' : ∀ (n : ℕ), (F n).out ∈ K<VAR>P : ↑K → ℕ → Bundled L.Structure<VAR>hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K<VAR>hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)<VAR>hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)<GOAL>∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>f : R → R<VAR>a : A<VAR>ha : ¬(p a ∧ ContinuousOn f (spectrum R a))<GOAL>cfc f a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<VAR>h : MeasurableSet (insert a s)<VAR>ha : a ∈ s<GOAL>MeasurableSet s
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>m.IsCaratheodory (⋃ i, s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>∀ (t : Set α), m (t ∩ ⋃ i, s i) + m (t \ ⋃ i, s i) ≤ m t
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)<GOAL>m (t ∩ ⋃ i, s i) + m (t \ ⋃ i, s i) ≤ m t
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)<GOAL>(⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)) + m (t \ ⋃ i, s i) ≤ m t
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)<GOAL>⨆ b, m (t ∩ ⋃ i, ⋃ (_ : i < b), s i) + m (t \ ⋃ i, s i) ≤ m t
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)<VAR>n : ℕ<GOAL>m (t \ ⋃ i, s i) ≤ m (t \ ⋃ i, ⋃ (_ : i < n), s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)<VAR>n : ℕ<GOAL>⋃ i, ⋃ (_ : i < n), s i ⊆ ⋃ i, s i
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : RestrictGermPredicate P A x ↑f<VAR>h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z<VAR>hx : x ∈ A<GOAL>∀ᶠ (y : X) in 𝓝 x, P y ↑g
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : RestrictGermPredicate P A x ↑f<VAR>h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z<VAR>hx : x ∈ A<GOAL>∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : RestrictGermPredicate P A x ↑f<VAR>h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z<VAR>hx : x ∈ A<VAR>y : X<VAR>hy : P y ↑f<VAR>h'y : ∀ᶠ (x : X) in 𝓝 y, g x = f x<GOAL>P y ↑g
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝<VAR>inst✝¹ : Algebra F L<VAR>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<GOAL>normalClosure F (↥K) L = ⨆ f, map (↑f) K
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝<VAR>inst✝¹ : Algebra F L<VAR>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>f : L →ₐ[F] L<GOAL>map f K ≤ ⨆ f, map (↑f) K
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝<VAR>inst✝¹ : Algebra F L<VAR>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>f : L ≃ₐ[F] L<GOAL>map (↑f) K ≤ ⨆ f, map f K
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>b ::ₘ Ico a b = Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<VAR>i : ι'<VAR>hi : p i<VAR>h'i : s i = ∅<GOAL>liminf f v = sSup univ
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>x y : α → Σˣ f<VAR>xy : x ≈ y<GOAL>∃ i, ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))), unify f x i hx = unify f y i hy
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>x y : α → Σˣ f<VAR>xy : x ≈ y<VAR>i : ι<VAR>hi : i ∈ upperBounds (range (Sum.elim (fun a => (x a).fst) fun a => (y a).fst))<GOAL>∃ i, ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))), unify f x i hx = unify f y i hy
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>x y : α → Σˣ f<VAR>xy : x ≈ y<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (x a).fst) ∩ upperBounds (range fun a => (y a).fst)<GOAL>∃ i, ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))), unify f x i hx = unify f y i hy
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>x y : α → Σˣ f<VAR>xy : x ≈ y<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Sigma.fst ∘ x) a) ∩ upperBounds (range fun a => (Sigma.fst ∘ y) a)<GOAL>∃ i, ∃ (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))), unify f x i hx = unify f y i hy
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ s₁ s₂ t₁ t₂ u : Set E<VAR>x y : E<VAR>s : ι → Set E<VAR>t : Set E<GOAL>convexJoin 𝕜 (⋃ i, s i) t = ⋃ i, convexJoin 𝕜 (s i) t
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ s₁ s₂ t₁ t₂ u : Set E<VAR>x y : E<VAR>s : ι → Set E<VAR>t : Set E<GOAL>⋃ x, ⋃ i, ⋃ (_ : x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y = ⋃ i, ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f g : X → ℝ<VAR>s t : Set X<VAR>hf : IntegrableOn f s μ<VAR>hg : IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>h : ∀ x ∈ s, f x ≤ g x<GOAL>f ≤ᶠ[ae (μ.restrict s)] g
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>xs : List α<VAR>n m : Fin xs.length<VAR>h : xs.get n = xs.get m<VAR>hne : n ≠ m<GOAL>¬xs.Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>xs : List α<VAR>n m : Fin xs.length<VAR>h : xs.get n = xs.get m<VAR>hne : n ≠ m<GOAL>¬Injective xs.get
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ →+* ℂ<VAR>h : Continuous ⇑f<GOAL>f = ofReal
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure (Measure α)<GOAL>μ.join = μ.bind id
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a✝ a' : α<VAR>b✝ b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>hs : s ⊆ s'<VAR>ht : t ⊆ t'<VAR>a : α<VAR>ha : a ∈ s<VAR>b : β<VAR>hb : b ∈ t<GOAL>f a b ∈ image2 f s' t'
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : IsTrivial L M<VAR>x y : L<GOAL>((traceForm R L M) x) y = (0 x) y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : IsTrivial L M<VAR>x y : L<GOAL>φ x ∘ₗ φ y = 0
<VAR>f : Type u₀ → Type u₁<VAR>inst✝ : EquivFunctor f<VAR>α β : Type u₀<VAR>e : α ≃ β<VAR>γ : Type u₀<VAR>ab : α ≃ β<VAR>bc : β ≃ γ<VAR>x : f α<GOAL>((mapEquiv f ab).trans (mapEquiv f bc)) x = (mapEquiv f (ab.trans bc)) x