ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h : ∑' (n : ℕ), (sFiniteSeq 0 n) s = 0<GOAL>(sFiniteSeq 0 n) s = 0 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h : ∀ (i : ℕ), (sFiniteSeq 0 i) s = 0<GOAL>(sFiniteSeq 0 n) s = 0 s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>map id ⟨s, al⟩ = ⟨s, al⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>↑(map id ⟨s, al⟩) = ↑⟨s, al⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>Stream'.map (Option.map id) s = s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x : R<GOAL>IsSelfAdjoint (star x * x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<GOAL>generateFrom (memPartition t n) ≤ generateFrom (range t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<GOAL>generateFrom (memPartition t n) ≤ generateFrom (⋃ n, memPartition t n)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>g✝ : G<VAR>a✝ b : α<VAR>g : G<VAR>a : α<GOAL>g⁻¹ • g • a = a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℤ<VAR>n : ℕ<VAR>this : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k<GOAL>‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(map I f)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<GOAL>Function.Injective ⇑(map I f)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<GOAL>∀ (m : AdicCompletion I M), (map I f) m = 0 → m = 0
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCompletion I M<GOAL>(map I f) x = 0 → x = 0
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCompletion I M<VAR>a : AdicCauchySequence I M<GOAL>(map I f) ((mk I M) a) = 0 → (mk I M) a = 0
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCompletion I M<VAR>a : AdicCauchySequence I M<VAR>hx : (map I f) ((mk I M) a) = 0<GOAL>(mk I M) a = 0
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCompletion I M<VAR>a : AdicCauchySequence I M<VAR>hx : (map I f) ((mk I M) a) = 0<VAR>n : ℕ<VAR>x✝ : n ≥ 42<GOAL>↑a (n + k) ∈ I ^ n • ⊤
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCompletion I M<VAR>a : AdicCauchySequence I M<VAR>hx : (map I f) ((mk I M) a) = 0<VAR>n : ℕ<VAR>x✝ : n ≥ 42<GOAL>↑a (n + k) ∈ Submodule.comap f (I ^ n • range f)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCompletion I M<VAR>a : AdicCauchySequence I M<VAR>hx : (map I f) ((mk I M) a) = 0<VAR>n : ℕ<VAR>x✝ : n ≥ 42<GOAL>f (↑a (n + k)) ∈ I ^ n • (I ^ k • ⊤ ⊓ range f)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>k : ℕ<VAR>hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCompletion I M<VAR>a : AdicCauchySequence I M<VAR>hx : (map I f) ((mk I M) a) = 0<VAR>n : ℕ<VAR>x✝ : n ≥ 42<GOAL>f (↑a (n + k)) ∈ I ^ (n + k) • ⊤ ⊓ range f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ : ι →₀ α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>f g : ι →₀ α<VAR>i : ι<VAR>a b : α<VAR>j : ι<GOAL>(single i (a - b)) j = (single i a - single i b) j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ : ι →₀ α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>f g : ι →₀ α<VAR>i : ι<VAR>a b : α<GOAL>(single i (a - b)) i = (single i a - single i b) i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ : ι →₀ α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>f g : ι →₀ α<VAR>i : ι<VAR>a b : α<VAR>j : ι<VAR>h : i ≠ j<GOAL>(single i (a - b)) j = (single i a - single i b) j
<VAR>p : ℝ≥0∞<VAR>𝕜✝ : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>𝕜 : Type u_5<VAR>inst✝ : SeminormedCommRing 𝕜<VAR>b : Basis ι 𝕜 (PiLp p fun x => 𝕜)<VAR>A : Matrix ι ι 𝕜<GOAL>b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i
<VAR>p : ℝ≥0∞<VAR>𝕜✝ : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>𝕜 : Type u_5<VAR>inst✝ : SeminormedCommRing 𝕜<VAR>b : Basis ι 𝕜 (PiLp p fun x => 𝕜)<VAR>A : Matrix ι ι 𝕜<VAR>this : (b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun x => 𝕜) i))).toMatrix ⇑(Pi.basisFun 𝕜 ι) * A = of fun i j => ((b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun x => 𝕜) i))).repr (Aᵀ j)) i<GOAL>b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i
<VAR>p : ℝ≥0∞<VAR>𝕜✝ : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>𝕜 : Type u_5<VAR>inst✝ : SeminormedCommRing 𝕜<VAR>b : Basis ι 𝕜 (PiLp p fun x => 𝕜)<VAR>A : Matrix ι ι 𝕜<VAR>this : (b.toMatrix fun x => (basisFun p 𝕜 ι) x) * A = of fun i j => (b.repr ((WithLp.equiv p (ι → 𝕜)).symm (Aᵀ j))) i<GOAL>b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i
<VAR>f g : ℕ → ℂ<VAR>s a b : ℂ<VAR>hf : LSeriesHasSum f s a<VAR>hg : LSeriesHasSum g s b<GOAL>LSeriesHasSum (f ⍟ g) s (a * b)
<VAR>f g : ℕ → ℂ<VAR>s a b : ℂ<VAR>hf : LSeriesHasSum f s a<VAR>hg : LSeriesHasSum g s b<GOAL>HasSum (fun n => ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2) (a * b)
<VAR>f g : ℕ → ℂ<VAR>s a b : ℂ<VAR>hf : LSeriesHasSum f s a<VAR>hg : LSeriesHasSum g s b<VAR>hsum : Summable fun x => term f s x.1 * term g s x.2<GOAL>HasSum (fun n => ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2) (a * b)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>ofFn f = pmap (fun i hi => f ⟨i, hi⟩) (range n) ⋯
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>ofFn f = map (fun x => f ⟨↑x, ⋯⟩) (range n).attach
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LocalRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : LocalRing S<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>a : R<VAR>ha : IsUnit ((residue R) a)<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LocalRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : LocalRing S<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>a : R<VAR>ha : IsUnit ((residue R) a)<VAR>h : ¬IsUnit a<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LocalRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : LocalRing S<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>a : R<VAR>ha : IsUnit 0<VAR>h : ¬IsUnit a<GOAL>False
<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>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a a' : α<VAR>h : b ∈ f.fix a<VAR>h' : b ∈ f.fix a'<VAR>fa : Sum.inr a' ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>(fixInduction h fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯) = hind a a' h' fa (fixInduction h' fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯)
<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>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a a' : α<VAR>h : b ∈ f.fix a<VAR>h' : b ∈ f.fix a'<VAR>fa : Sum.inr a' ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>Sum.casesOn (motive := fun x => (f a).get ⋯ = x → C a) ((f a).get ⋯) (fun b' e => let_fun e := ⋯; hbase a ⋯) (fun a'' e => let_fun e := ⋯; hind a a'' ⋯ e ((fun a' h' => fixInduction ⋯ fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯) a'' e)) ⋯ = hind a a' h' fa (fixInduction h' fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯)
<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>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a a' : α<VAR>h : b ∈ f.fix a<VAR>h' : b ∈ f.fix a'<VAR>fa : Sum.inr a' ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>(fun x e => Sum.casesOn (motive := fun y => (f a).get ⋯ = y → C a) x (fun b' e => let_fun e := ⋯; hbase a ⋯) (fun a'' e => let_fun e := ⋯; hind a a'' ⋯ e ((fun a' h' => fixInduction ⋯ fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯) a'' e)) ⋯ = hind a a' h' fa (fixInduction h' fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯)) (Sum.inr a') ⋯
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<GOAL>Inducing ⇑(productOfMemOpens X)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<GOAL>inst✝ = ⨅ i, induced (fun x => x ∈ i) inferInstance
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>h : IsPreconnected s<GOAL>IsPreconnected univ
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝⁵ : SetLike σ A<VAR>inst✝⁴ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝³ : GradedRing 𝒜<VAR>a : A<VAR>n i : ι<VAR>inst✝² : Sub ι<VAR>inst✝¹ : OrderedSub ι<VAR>inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : i ≤ n<VAR>b : ↥(𝒜 i)<GOAL>↑(((decompose 𝒜) (a * ↑b)) n) = ↑(((decompose 𝒜) a) (n - i)) * ↑b
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q
<VAR>E : Type<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>z : ℂ<VAR>x : E<VAR>s : Set E<VAR>fa : AnalyticAt ℂ f x<VAR>ga : AnalyticAt ℂ g x<VAR>m : f x ∈ slitPlane<GOAL>AnalyticAt ℂ (fun z => f z ^ g z) x
<VAR>E : Type<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>z : ℂ<VAR>x : E<VAR>s : Set E<VAR>fa : AnalyticAt ℂ f x<VAR>ga : AnalyticAt ℂ g x<VAR>m : f x ∈ slitPlane<VAR>e : (fun z => f z ^ g z) =ᶠ[𝓝 x] fun z => cexp (log (f z) * g z)<GOAL>AnalyticAt ℂ (fun z => f z ^ g z) x
<VAR>E : Type<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>z : ℂ<VAR>x : E<VAR>s : Set E<VAR>fa : AnalyticAt ℂ f x<VAR>ga : AnalyticAt ℂ g x<VAR>m : f x ∈ slitPlane<VAR>e : (fun z => f z ^ g z) =ᶠ[𝓝 x] fun z => cexp (log (f z) * g z)<GOAL>AnalyticAt ℂ (fun z => cexp (log (f z) * g z)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f : β → γ<VAR>e : α ≃ᵐ β<VAR>hfe : Measurable (f ∘ ⇑e)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f : β → γ<VAR>e : α ≃ᵐ β<VAR>hfe : Measurable (f ∘ ⇑e)<VAR>this : Measurable (f ∘ ⇑(e.symm.trans e).toEquiv)<GOAL>Measurable f
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y✝ y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>y : 𝕜<VAR>x✝ : G<GOAL>(y • f ⋆[L, μ] g) x✝ = (y • (f ⋆[L, μ] g)) x✝
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>B W : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝ : EffectiveEpiFamily X π<VAR>m₁ m₂ : B ⟶ W<VAR>h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂<GOAL>m₁ = m₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>B W : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝ : EffectiveEpiFamily X π<VAR>m₁ m₂ : B ⟶ W<VAR>h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂<VAR>this : m₂ = desc X π (fun a => π a ≫ m₂) ⋯<GOAL>m₁ = m₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>B W : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝ : EffectiveEpiFamily X π<VAR>m₁ m₂ : B ⟶ W<VAR>h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂<VAR>this : m₂ = desc X π (fun a => π a ≫ m₂) ⋯<GOAL>m₁ = desc X π (fun a => π a ≫ m₂) ⋯
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : ∃ M, Infinite ↑M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<GOAL>∃ N, #↑N = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ t✝ s t : Set α<VAR>inst✝¹ : Fintype ↑s<VAR>inst✝ : Fintype ↑t<VAR>h : s.toFinset = t.toFinset<GOAL>s = t
<VAR>R : Type u<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x y : R<GOAL>Commute (star x) y ↔ Commute x (star y)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q✝ q r : ℚ<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q + r) = ↑q + ↑r
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q✝ q r : ℚ<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q.num * ↑r.den + ↑q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q✝ q r : ℚ<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q.den * r.den) ≠ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>m : α → β<VAR>f : Filter α<VAR>g : Set (Set β)<VAR>b : β<GOAL>Tendsto m f (𝓝 b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
<VAR>α : Type u<VAR>β : Type u_1<VAR>m : α → β<VAR>f : Filter α<VAR>g : Set (Set β)<VAR>b : β<GOAL>(∀ i ∈ g, b ∈ i → ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ last n<VAR>h' : optParam (i.rev ≠ 0) ⋯<GOAL>(i.castPred h).rev = i.rev.pred h'
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R✝<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R✝ M<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R<VAR>h : I.FG<VAR>f : R →+* S<GOAL>(Ideal.map f I).FG
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>α : Type u_2<VAR>inst✝ : MulAction M α<VAR>m : Mˣ<GOAL>Function.Bijective fun a => ↑m • a
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>α : Type u_2<VAR>inst✝ : MulAction M α<VAR>m : Mˣ<GOAL>∃ g, (Function.LeftInverse g fun a => ↑m • a) ∧ Function.RightInverse g fun a => ↑m • a
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>α : Type u_2<VAR>inst✝ : MulAction M α<VAR>m : Mˣ<GOAL>(Function.LeftInverse (fun a => m⁻¹ • a) fun a => ↑m • a) ∧ Function.RightInverse (fun a => m⁻¹ • a) fun a => ↑m • a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s✝ : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>s : Set ((i : ι) → α i)<GOAL>sᶜ ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), (eval i '' s)ᶜ ∈ f i
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasStrictFDerivAt (fun u => exp 𝕂 (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (exp 𝕂 (t • x))) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸<VAR>h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)<GOAL>HasStrictFDerivAt (fun u => exp 𝕂 (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (exp 𝕂 (t • x))) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸<VAR>h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)<GOAL>(ContinuousLinearMap.smulRight 1 x).smulRight (exp 𝕂 (t • x)) = exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸<VAR>h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)<VAR>t' : 𝕊<GOAL>Commute (t' • x) (exp 𝕂 (t • x))
<VAR>n : ℕ<GOAL>∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
<GOAL>∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.89869<VAR>inst✝ : MulAction R X<VAR>r : R<VAR>s : ↥S<GOAL>r /ₒ s * 1 = r /ₒ s
<VAR>a✝ b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>a n : ℕ<VAR>hp : 1 < a.succ<VAR>hk : 1 < n.succ<VAR>h : a.succ ^ n.succ ∣ a.succ<GOAL>a.succ * a.succ ^ n ∣ a.succ * 1
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁷ : PartialOrder Γ✝<VAR>inst✝⁶ : PartialOrder Γ'<VAR>inst✝⁵ : VAdd Γ✝ Γ'<VAR>inst✝⁴ : IsOrderedCancelVAdd Γ✝ Γ'<VAR>inst✝³ : AddCommMonoid V<VAR>Γ : Type u_5<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : Zero R<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ R V<VAR>hx : ¬x = 0<VAR>hy : ¬(of R).symm y = 0<GOAL>((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff