ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<GOAL>∀ (x : S), x ∈ Set.range ⇑f
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<GOAL>x ∈ Set.range ⇑f
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<GOAL>∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<VAR>r : ↑s<VAR>a : Localization.Away ↑r<VAR>e' : (Localization.awayMap f ↑r) a = (algebraMap S (Localization.Away (f ↑r))) x<GOAL>∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<VAR>r : ↑s<VAR>b : R<VAR>n : ℕ<VAR>e' : (Localization.awayMap f ↑r) (IsLocalization.mk' (Localization.Away ↑r) b ⟨(fun x => ↑r ^ x) n, ⋯⟩) = (algebraMap S (Localization.Away (f ↑r))) x<GOAL>∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<VAR>r : ↑s<VAR>b : R<VAR>n : ℕ<VAR>e' : IsLocalization.mk' (Localization.Away (f ↑r)) (f b) ⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩ = (algebraMap S (Localization.Away (f ↑r))) x<GOAL>∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<VAR>r : ↑s<VAR>b : R<VAR>n : ℕ<VAR>e' : (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) = (algebraMap S (Localization.Away (f ↑r))) (f b)<GOAL>∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<VAR>r : ↑s<VAR>b : R<VAR>n : ℕ<VAR>e' : (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) = (algebraMap S (Localization.Away (f ↑r))) (f b)<VAR>n' : ℕ<VAR>e'' : ↑⟨(fun x => f ↑r ^ x) n', ⋯⟩ * (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) = ↑⟨(fun x => f ↑r ^ x) n', ⋯⟩ * f b<GOAL>∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<VAR>r : ↑s<VAR>b : R<VAR>n : ℕ<VAR>e' : (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) = (algebraMap S (Localization.Away (f ↑r))) (f b)<VAR>n' : ℕ<VAR>e'' : f ↑r ^ n' * (x * f (↑r ^ n)) = f ↑r ^ n' * f b<GOAL>∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<VAR>this : Algebra R S := f.toAlgebra<VAR>x : S<VAR>r : ↑s<VAR>b : R<VAR>n : ℕ<VAR>e' : (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) = (algebraMap S (Localization.Away (f ↑r))) (f b)<VAR>n' : ℕ<VAR>e'' : f (↑r ^ (n' + n)) * x = f (↑r ^ n' * b)<GOAL>∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n m : ℕ<VAR>h : Fin n = Fin m<GOAL>_root_.cast h = cast ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>h : Fin n = Fin n<GOAL>_root_.cast h = cast ⋯
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hco : (orderOf x).Coprime (orderOf y)<GOAL>orderOf (x * y) = orderOf x * orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hco : (orderOf x).Coprime (orderOf y)<GOAL>minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 = orderOf x * orderOf y
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>cos x * cos (2 * x) - sin x * sin (2 * x) = 4 * cos x ^ 3 - 3 * cos x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) = 4 * cos x ^ 3 - 3 * cos x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2<GOAL>cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) = 4 * cos x ^ 3 - 3 * cos x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2<GOAL>cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) = 2 * cos x * cos x * cos x + 2 * cos x * (1 - sin x ^ 2) - 3 * cos x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>wittOne p 0 = 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>(map (Int.castRingHom ℚ)) (wittOne p 0) = (map (Int.castRingHom ℚ)) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Tendsto m f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ 0<GOAL>Tendsto (fun x => m x / b) f (𝓝 (a / b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Tendsto m f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ 0<GOAL>a ≠ 0 ∨ b⁻¹ ≠ ⊤
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d<GOAL>a ∣ b * c → a ∣ c
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m n : ℕ<VAR>φ : R⟦X⟧<GOAL>(trunc n φ).coeff m = if m < n then (coeff R m) φ else 0
<VAR>q q' : Λ'<GOAL>q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
<VAR>q' : Λ'<VAR>p✝ : Γ' → Bool<VAR>k₁✝ k₂✝ : K'<VAR>q : Λ'<VAR>q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q<GOAL>q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)
<VAR>q' : Λ'<VAR>p✝ : Γ' → Bool<VAR>k✝ : K'<VAR>q : Λ'<VAR>q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q<GOAL>q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)
<VAR>q' q : Λ'<VAR>q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q<GOAL>q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)
<VAR>q' : Λ'<VAR>k✝ : K'<VAR>s✝ : Option Γ' → Option Γ'<VAR>q : Λ'<VAR>q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q<GOAL>q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k✝ s✝ q) (trStmts₁ q)
<VAR>q' : Λ'<VAR>q : Option Γ' → Λ'<VAR>q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)<GOAL>(q' ∈ Finset.univ.biUnion fun s => trStmts₁ (q s)) → trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s))
<VAR>q' q : Λ'<VAR>q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q<GOAL>(q' = unrev q → insert (Λ'.move (fun x => false) rev main q) (trStmts₁ q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧ (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
<VAR>q' q₁ q₂ : Λ'<VAR>q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁<VAR>q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂<GOAL>(q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧ (q' = unrev q₂ → insert (Λ'.move (fun x => false) rev main q₂) (trStmts₁ q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧ (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>inst✝ : LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬Pairwise (Disjoint on f)<GOAL>∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>inst✝ : LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬univ.Pairwise (Disjoint on f)<GOAL>∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>inst✝ : LinearOrder ι<VAR>f : ι → Set α<VAR>h✝ : ¬univ.Pairwise (Disjoint on f)<VAR>i : ι<VAR>_hi : i ∈ univ<VAR>j : ι<VAR>_hj : j ∈ univ<VAR>h : i < j ∧ ∃ x, x ∈ f i ∩ f j<GOAL>∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace α'<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝ : TopologicalSpace β<VAR>h'f : HasCompactMulSupport f<VAR>hf : Continuous f<VAR>k : Set β<VAR>hk : IsClosed k<VAR>h'k : 1 ∉ k<GOAL>IsCompact (f ⁻¹' k)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace α'<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x✝ : α<VAR>inst✝ : TopologicalSpace β<VAR>h'f : HasCompactMulSupport f<VAR>hf : Continuous f<VAR>k : Set β<VAR>hk : IsClosed k<VAR>h'k : 1 ∉ k<VAR>x : α<VAR>hx : x ∈ f ⁻¹' k<GOAL>x ∈ mulTSupport f
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace α'<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x✝ : α<VAR>inst✝ : TopologicalSpace β<VAR>h'f : HasCompactMulSupport f<VAR>hf : Continuous f<VAR>k : Set β<VAR>hk : IsClosed k<VAR>h'k : 1 ∉ k<VAR>x : α<VAR>hx : x ∈ f ⁻¹' k<GOAL>x ∈ mulSupport f
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : CharZero k<VAR>h : s.card ≠ 0<GOAL>∑ i ∈ s, centroidWeights k s i = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : CharZero k<VAR>h : s.card ≠ 0<GOAL>↑s.card * (↑s.card)⁻¹ = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : CharZero k<VAR>h : s.card ≠ 0<GOAL>↑s.card ≠ 0
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝⁷ : (i : ι) → Module R (φ i)<VAR>S : Type ?u.32694<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>f g : (i : ι) → φ i →ₗ[R] M<GOAL>(fun f => ∑ i : ι, f i ∘ₗ proj i) (f + g) = (fun f => ∑ i : ι, f i ∘ₗ proj i) f + (fun f => ∑ i : ι, f i ∘ₗ proj i) g
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝⁷ : (i : ι) → Module R (φ i)<VAR>S : Type ?u.32694<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>c : S<VAR>f : (i : ι) → φ i →ₗ[R] M<GOAL>{ toFun := fun f => ∑ i : ι, f i ∘ₗ proj i, map_add' := ⋯ }.toFun (c • f) = (RingHom.id S) c • { toFun := fun f => ∑ i : ι, f i ∘ₗ proj i, map_add' := ⋯ }.toFun f
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝⁷ : (i : ι) → Module R (φ i)<VAR>S : Type ?u.32694<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>f : (i : ι) → φ i →ₗ[R] M<VAR>i : ι<VAR>x : φ i<GOAL>((fun f i => f ∘ₗ single i) ({ toFun := fun f => ∑ i : ι, f i ∘ₗ proj i, map_add' := ⋯, map_smul' := ⋯ }.toFun f) i) x = (f i) x
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝⁷ : (i : ι) → Module R (φ i)<VAR>S : Type ?u.32694<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>f : ((i : ι) → φ i) →ₗ[R] M<VAR>x : (i : ι) → φ i<GOAL>({ toFun := fun f => ∑ i : ι, f i ∘ₗ proj i, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun f i => f ∘ₗ single i) f)) x = f x
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝⁷ : (i : ι) → Module R (φ i)<VAR>S : Type ?u.32694<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>f : ((i : ι) → φ i) →ₗ[R] M<VAR>x : (i : ι) → φ i<GOAL>f (∑ j : ι, Pi.single j (x j)) = f x
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<GOAL>Irrational (x - ↑q)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>cyclotomic n R ∣ X ^ n - 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>cyclotomic n ℤ ∣ X ^ n - 1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>cyclotomic 0 ℤ ∣ X ^ 0 - 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>hn : n > 0<GOAL>cyclotomic n ℤ ∣ X ^ n - 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>hn : n > 0<GOAL>cyclotomic n ℤ ∣ ∏ i ∈ n.divisors, cyclotomic i ℤ
<VAR>K : Option Γ' → Finset Λ'<VAR>S : Finset Λ'<GOAL>Supports (Finset.univ.biUnion K) S ↔ ∀ (a : Option Γ'), Supports (K a) S
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>h : ∀ ε > 0, b - ε ≤ a<GOAL>b ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>h : a < b<GOAL>∃ ε > 0, a < b - ε
<VAR>r : ℕ<VAR>s t : ℤ<VAR>r' : ℕ<VAR>s' t' : ℤ<VAR>h : 0 < r<GOAL>r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
<VAR>s t : ℤ<VAR>r' : ℕ<VAR>s' t' : ℤ<VAR>r : ℕ<VAR>h : 0 < r.succ<GOAL>r.succ.xgcdAux s t r' s' t' = (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>l : List α<VAR>H : Pairwise R l<GOAL>Pairwise (fun l₁ l₂ => Lex R l₁.reverse l₂.reverse) l.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>l : List α<VAR>H : Pairwise R l<VAR>this : Pairwise (Lex (swap fun b a => R a b)) l.reverse.sublists'<GOAL>Pairwise (fun l₁ l₂ => Lex R l₁.reverse l₂.reverse) l.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>x ∈ closedBall x ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>0 ≤ ε
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hf : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hf : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (f x) = edist x (f x) * ↑K ^ 0
<VAR>l r : List Char<GOAL>{ s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }.Valid
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>inst✝ : FiniteDimensional K V₂<GOAL>Injective ⇑B.flip ↔ Surjective ⇑B
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>inst✝ : FiniteDimensional K V₂<GOAL>Injective ⇑B.flip ↔ Injective ⇑B.dualMap
<VAR>n d : ℤ<GOAL>(n /. d).num = d.sign * n / ↑(n.gcd d)
<VAR>n d : ℤ<VAR>this : ∀ (m : ℕ), (↑m + 1).natAbs = m + 1<GOAL>(n /. d).num = d.sign * n / ↑(n.gcd d)
<VAR>x y : ℝ<VAR>f g : CauSeq ℚ abs<GOAL>Real.lt { cauchy := ⟦f⟧ } { cauchy := ⟦g⟧ } ↔ f < g
<VAR>x y : ℝ<VAR>f g : CauSeq ℚ abs<GOAL>(match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x x_1 => x < x_1) Real.definition.proof_1✝) ↔ f < g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<GOAL>(λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s✝ : α → α → Prop<VAR>s : Set β<VAR>f : β → α<GOAL>DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>X₁ X₂ X₃ : ModuleCat R<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>hfg : LinearMap.range f = LinearMap.ker g<GOAL>(moduleCatMkOfKerLERange f g ⋯).Exact
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝ : AddGroup n<VAR>v : n → α<GOAL>(circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>x : M ∗ N<GOAL>(fst x, snd x) = toProd x