ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>A : C<VAR>i₁₂ : I₁₂<VAR>f g : (K.total c₁₂).X i₁₂ ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g<GOAL>∀ (i : I₁ × I₂) (hij : c₁.π c₂ c₁₂ i = i₁₂), K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ f = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ g
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>φ ψ : MvPowerSeries σ k<VAR>h : (constantCoeff σ k) ψ ≠ 0<GOAL>φ = ψ⁻¹ ↔ φ * ψ = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<VAR>this : s =ᶠ[𝓝[≠] x] t<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<VAR>this✝ : s =ᶠ[𝓝[≠] x] t<VAR>this : 𝓝[s \ {x}] x = 𝓝[t \ {x}] x<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>x : M<VAR>i j : ι<VAR>hij : i ≠ j<VAR>a : α j<VAR>hx : x ∈ A i<GOAL>((h.collectedBasis v).repr x) ⟨j, a⟩ = 0
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>x : M<VAR>i j : ι<VAR>hij : i ≠ j<VAR>a : α j<VAR>hx : x ∈ A i<GOAL>((sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange (fun i => ⇑(v i).repr) ⋯ (↑(LinearEquiv.ofBijective (coeLinearMap A) h).symm x))) ⟨j, a⟩ = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>hn : n ≤ finrank R M<VAR>h : ¬finrank R M = 0<GOAL>∃ s, s.card = n ∧ LinearIndependent R Subtype.val
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<GOAL>x ∈ ⊥.jacobson
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<GOAL>∀ (y : R), IsUnit (-x * y + 1)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<GOAL>IsUnit (-x * y + 1)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<GOAL>IsUnit (1 + -x * y)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<GOAL>IsUnit (1 + -x * y)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<GOAL>IsUnit (1 + -x * y)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]<GOAL>IsUnit (1 + -x * y)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]<GOAL>∃ b, (1 + -x * y) * b = 1
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]<GOAL>(1 + -x * y) * L = 1
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]<GOAL>(1 + -(x * y)) * L - 1 = 0
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]<GOAL>∀ (n : ℕ), (1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>n : ℕ<VAR>hL : f n ≡ L [SMOD I ^ n • ⊤]<GOAL>(1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>n : ℕ<VAR>hL : f n - L ∈ I ^ n<GOAL>(1 + -(x * y)) * L - 1 - 0 ∈ I ^ n
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>n : ℕ<VAR>hL : f n - L ∈ I ^ n<GOAL>(1 + -(x * y)) * L - 1 ∈ I ^ n
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsAdicComplete I R<VAR>x : R<VAR>hx : x ∈ I<VAR>y : R<VAR>f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i<VAR>hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]<VAR>L : R<VAR>n : ℕ<VAR>hL : f n - L ∈ I ^ n<GOAL>(1 - x * y) * f n - 1 ∈ I ^ n
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>inst✝⁹ : Category.{u_13, u_1} C₁<VAR>inst✝⁸ : Category.{u_15, u_2} C₂<VAR>inst✝⁷ : Category.{u_14, u_5} C₃<VAR>inst✝⁶ : Category.{u_11, u_6} C₄<VAR>inst✝⁵ : Category.{u_17, u_3} C₁₂<VAR>inst✝⁴ : Category.{u_12, u_4} C₂₃<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j = ((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : V1<VAR>c : k<GOAL>(lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : V1<VAR>c : k<GOAL>c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁
<VAR>R : Type u_1<VAR>inst✝⁴⁵ : Semiring R<VAR>S : Type u_2<VAR>inst✝⁴⁴ : Semiring S<VAR>R₂ : Type u_3<VAR>inst✝⁴³ : Semiring R₂<VAR>S₂ : Type u_4<VAR>inst✝⁴² : Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>M₂ : Type u_8<VAR>N₂ : Type u_9<VAR>P₂ : Type u_10<VAR>Nₗ : Type u_11<VAR>Pₗ : Type u_12<VAR>M' : Type u_13<VAR>N' : Type u_14<VAR>P' : Type u_15<VAR>inst✝⁴¹ : AddCommMonoid M<VAR>inst✝⁴⁰ : AddCommMonoid N<VAR>inst✝³⁹ : AddCommMonoid P<VAR>inst✝³⁸ : AddCommMonoid M₂<VAR>inst✝³⁷ : AddCommMonoid N₂<VAR>inst✝³⁶ : AddCommMonoid P₂<VAR>inst✝³⁵ : AddCommMonoid Nₗ<VAR>inst✝³⁴ : AddCommMonoid Pₗ<VAR>inst✝³³ : AddCommGroup M'<VAR>inst✝³² : AddCommGroup N'<VAR>inst✝³¹ : AddCommGroup P'<VAR>inst✝³⁰ : Module R M<VAR>inst✝²⁹ : Module S N<VAR>inst✝²⁸ : Module R₂ P<VAR>inst✝²⁷ : Module S₂ P<VAR>inst✝²⁶ : Module R M₂<VAR>inst✝²⁵ : Module S N₂<VAR>inst✝²⁴ : Module R P₂<VAR>inst✝²³ : Module S₂ P₂<VAR>inst✝²² : Module R Pₗ<VAR>inst✝²¹ : Module S Pₗ<VAR>inst✝²⁰ : Module R M'<VAR>inst✝¹⁹ : Module S N'<VAR>inst✝¹⁸ : Module R₂ P'<VAR>inst✝¹⁷ : Module S₂ P'<VAR>inst✝¹⁶ : SMulCommClass S₂ R₂ P<VAR>inst✝¹⁵ : SMulCommClass S R Pₗ<VAR>inst✝¹⁴ : SMulCommClass S₂ R₂ P'<VAR>inst✝¹³ : SMulCommClass S₂ R P₂<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>R' : Type u_16<VAR>S' : Type u_17<VAR>inst✝¹² : Semiring R'<VAR>inst✝¹¹ : Semiring S'<VAR>inst✝¹⁰ : Module R' M<VAR>inst✝⁹ : Module S' N<VAR>inst✝⁸ : Module R' Pₗ<VAR>inst✝⁷ : Module S' Pₗ<VAR>inst✝⁶ : SMulCommClass S' R' Pₗ<VAR>inst✝⁵ : SMul S' S<VAR>inst✝⁴ : IsScalarTower S' S N<VAR>inst✝³ : IsScalarTower S' S Pₗ<VAR>inst✝² : SMul R' R<VAR>inst✝¹ : IsScalarTower R' R M<VAR>inst✝ : IsScalarTower R' R Pₗ<VAR>B : M →ₗ[R] N →ₗ[S] Pₗ<VAR>r' : R'<VAR>m : M<VAR>x✝ : N<GOAL>(B (r' • m)) x✝ = r' • (B m) x✝
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x y : L<GOAL>⁅χ x, χ y⁆ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>f fa g : α → α<VAR>x y : α<VAR>fb : β → β<VAR>m n k : ℕ<VAR>e : Perm α<VAR>h : Function.Commute f g<GOAL>Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x✝ : α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x<GOAL>(f.toCycle hf).Nontrivial
<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 : α → DirectLimit G f<GOAL>∃ i y, x = fun a => ⟦Structure.Sigma.mk f i (y a)⟧
<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 : α → DirectLimit G f<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Quotient.out (x a)).fst)<GOAL>∃ i y, x = fun a => ⟦Structure.Sigma.mk f i (y a)⟧
<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 : α → DirectLimit G f<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Quotient.out (x a)).fst)<VAR>a : α<GOAL>x a = ⟦Structure.Sigma.mk f i (unify f (Quotient.out ∘ x) i hi a)⟧
<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 : α → DirectLimit G f<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Quotient.out (x a)).fst)<VAR>a : α<GOAL>Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f ((Quotient.out ∘ x) a).fst i ⋯) ((Quotient.out ∘ x) a).snd)
<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 : α → DirectLimit G f<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Quotient.out (x a)).fst)<VAR>a : α<VAR>r : ((Quotient.out ∘ x) a).fst ≤ i<GOAL>Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)
<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 : α → DirectLimit G f<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Quotient.out (x a)).fst)<VAR>a : α<VAR>r : ((Quotient.out ∘ x) a).fst ≤ i<VAR>this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i<GOAL>Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)
<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 : α → DirectLimit G f<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Quotient.out (x a)).fst)<VAR>a : α<VAR>r : ((Quotient.out ∘ x) a).fst ≤ i<VAR>this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i<GOAL>(f (Quotient.out (x a)).fst i ⋯) (Quotient.out (x a)).snd = (f (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst i this) (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).snd
<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 : α → DirectLimit G f<VAR>i : ι<VAR>hi : i ∈ upperBounds (range fun a => (Quotient.out (x a)).fst)<VAR>a : α<VAR>r : ((Quotient.out ∘ x) a).fst ≤ i<VAR>this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i<GOAL>(Quotient.out (x a)).fst ∈ range fun a => (Quotient.out (x a)).fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F✝ : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝ : IsDomain R<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>e : ZMod ↑n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers<VAR>F : Fintype ↥(Subgroup.zpowers ζ)<GOAL>Fintype.card ↥(rootsOfUnity n R) = ↑n
<VAR>k : ℕ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => x ^ k) =o[atTop] fun x => rexp (b * x)
<VAR>ι : Type u_1<VAR>Γ : ι → Type u_2<VAR>inst✝ : (i : ι) → Inhabited (Γ i)<VAR>i : ι<VAR>L : ListBlank ((i : ι) → Γ i)<VAR>n : ℕ<GOAL>(ListBlank.map (proj i) L).nth n = L.nth n i
<VAR>ι : Type u_1<VAR>Γ : ι → Type u_2<VAR>inst✝ : (i : ι) → Inhabited (Γ i)<VAR>i : ι<VAR>L : ListBlank ((i : ι) → Γ i)<VAR>n : ℕ<GOAL>(proj i).f (L.nth n) = L.nth n i
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed K<VAR>f : k →+* K<VAR>p : k[X]<VAR>hp : p.degree ≠ 0<VAR>hsep : p.Separable<GOAL>(map f p).degree ≠ 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed K<VAR>f : k →+* K<VAR>p : k[X]<VAR>hp : p.degree ≠ 0<VAR>hsep : p.Separable<VAR>x : K<VAR>hx : (map f p).IsRoot x<GOAL>eval₂ f x p = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>h : a :: b :: l ≠ []<GOAL>(a :: b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>h : a :: b :: l ≠ []<GOAL>a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>h : a :: b :: l ≠ []<GOAL>(b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>hw : w.IsReal<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(normAtPlace w) x = ‖x.1 ⟨w, hw⟩‖
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : UniqueFactorizationMonoid N<VAR>inst✝² : UniqueFactorizationMonoid M<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>m p : Associates M<VAR>n : Associates N<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>hn : ¬n = 0<VAR>hm : ¬m = 0<GOAL>multiplicity p m ≤ multiplicity (↑(d ⟨p, ⋯⟩)) n
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : UniqueFactorizationMonoid N<VAR>inst✝² : UniqueFactorizationMonoid M<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>m p : Associates M<VAR>n : Associates N<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>hn : ¬n = 0<VAR>hm : ¬m = 0<GOAL>↑(d ⟨p, ⋯⟩) ^ (multiplicity p m).get ⋯ ∣ n
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>h : u ≠ v<VAR>p : G.Walk u v<GOAL>v ∈ p.support.tail
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>h : u ≠ v<VAR>w✝² : V<VAR>w✝¹ : G.Adj u w✝²<VAR>w✝ : G.Walk w✝² v<GOAL>v ∈ (cons w✝¹ w✝).support.tail
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<GOAL>(fun x => x / a) '' [[b, c]] = [[b / a, c / a]]
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>|a| ≤ b ↔ -b ≤ a ∧ a ≤ b
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>w z : P<VAR>t₁ : R<VAR>ht₁ : t₁ ∈ Set.Icc 0 1<VAR>t₂ : R<VAR>ht₂ : t₂ ∈ Set.Icc 0 1<GOAL>Wbtw R w ((lineMap w ((lineMap w z) t₁)) t₂) z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>w z : P<VAR>t₁ : R<VAR>ht₁ : t₁ ∈ Set.Icc 0 1<VAR>t₂ : R<VAR>ht₂ : t₂ ∈ Set.Icc 0 1<GOAL>(lineMap w z) (t₂ * t₁) = (lineMap w ((lineMap w z) t₁)) t₂
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hp1 : p.degree = 1<GOAL>Prime p