ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<VAR>exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<VAR>exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)<VAR>en_mem_range : en ∈ range (rTensor N (ker G).subtype)<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<VAR>exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)<VAR>kn : ↥(ker G) ⊗[R] N<VAR>hkn : (rTensor N (ker G).subtype) kn = en<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<VAR>exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)<VAR>ma : Finset (↥(ker G) × N)<VAR>hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<VAR>exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)<VAR>ma : Finset (↥(ker G) × N)<VAR>hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en<GOAL>∃ a y, (∀ (i : ι), n i = ∑ j : { x // x ∈ ma }, a i j • y j) ∧ ∀ (j : { x // x ∈ ma }), ∑ i : ι, a i j • m i = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<VAR>exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)<VAR>ma : Finset (↥(ker G) × N)<VAR>hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en<GOAL>∃ y, (∀ (i : ι), n i = ∑ j : { x // x ∈ ma }, (match j with | ⟨(kj, snd), property⟩ => ↑kj i) • y j) ∧ ∀ (j : { x // x ∈ ma }), ∑ i : ι, (match j with | ⟨(kj, snd), property⟩ => ↑kj i) • m i = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing 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>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<VAR>exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G<VAR>exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)<VAR>ma : Finset (↥(ker G) × N)<VAR>hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en<GOAL>(∀ (i : ι), n i = ∑ j : { x // x ∈ ma }, (match j with | ⟨(kj, snd), property⟩ => ↑kj i) • match j with | ⟨(fst, yj), property⟩ => yj) ∧ ∀ (j : { x // x ∈ ma }), ∑ i : ι, (match j with | ⟨(kj, snd), property⟩ => ↑kj i) • m i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝² : Fintype β<VAR>inst✝¹ : (b : β) → PseudoMetricSpace (π b)<VAR>inst✝ : Nonempty β<VAR>a b : α<GOAL>(dist (fun x => a) fun x => b) = dist a b
<VAR>m n✝ n : ℕ<GOAL>-↑n = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t✝ t₁ t₂ u : Set α<VAR>p : Prop<VAR>inst✝ : Decidable p<VAR>t : ¬p → Set α<VAR>x : α<GOAL>(x ∈ if h : p then ∅ else t h) ↔ ∃ (h : ¬p), x ∈ t h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t✝ t₁ t₂ u : Set α<VAR>p : Prop<VAR>inst✝ : Decidable p<VAR>t : ¬p → Set α<VAR>x : α<GOAL>(¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ (h : ¬p), x ∈ t h
<VAR>ι : Type u<VAR>s : Finset ι<VAR>a b : ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>a * b ≤ a ^ p / p.toNNReal + b ^ q / q.toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝³ : One M<VAR>inst✝² : One N<VAR>inst✝¹ : One P<VAR>inst✝ : DecidableEq α<VAR>f : α → M<VAR>x a : α<GOAL>a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>k : ℕ<VAR>hkmn : m * (k + 1) ≤ n<GOAL>IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>k : ℕ<VAR>hkmn : m * (k + 1) ≤ n<VAR>hkmn' : m * k ≤ n<GOAL>IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>k : ℕ<VAR>hkmn : m * (k + 1) ≤ n<VAR>hkmn' : m * k ≤ n<VAR>x : Fin (n + 1)<GOAL>x ∈ Iio ↑(k + 1) ↔ x ∈ Iic ↑k
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>k : ℕ<VAR>hkmn : m * (k + 1) ≤ n<VAR>hkmn' : m * k ≤ n<VAR>x : ℕ<GOAL>x ∈ Iio (k + 1) ↔ x ∈ Iic k
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommMonoid M<VAR>ψ : AddChar R M<VAR>x✝ : R<GOAL>(ψ.mulShift 0) x✝ = 1 x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>x : H<VAR>x✝ : x ∈ s<GOAL>0 ≤ ⟪x, 0⟫_ℝ
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.37256, u_1} C<VAR>P : Karoubi C<GOAL>P.p = P.p ≫ P.p ≫ { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p
<VAR>m : ℤ<GOAL>‖↑m‖ = ‖m‖
<VAR>m : ℤ<GOAL>‖↑↑m‖ = ‖↑m‖
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>((1 ≤ x.1 ∧ x.1 < n + 1) ∧ 1 ≤ x.2 ∧ x.2 < n + 1) ∧ x.1 * x.2 = n ↔ x.1 * x.2 = n ∧ ¬n = 0
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x.1 * x.2 = n ∧ (1 ≤ x.1 ∧ x.1 < n + 1) ∧ 1 ≤ x.2 ∧ x.2 < n + 1 ↔ x.1 * x.2 = n ∧ ¬n = 0
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x.1 * x.2 = n → ((1 ≤ x.1 ∧ x.1 < n + 1) ∧ 1 ≤ x.2 ∧ x.2 < n + 1 ↔ ¬n = 0)
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.20862, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c<VAR>i j : ι<VAR>hij : ¬c.symm.Rel i j<GOAL>(X.d j i).unop = 0
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.20862, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c<VAR>x✝⁴ x✝³ x✝² : ι<VAR>x✝¹ : c.symm.Rel x✝⁴ x✝³<VAR>x✝ : c.symm.Rel x✝³ x✝²<GOAL>(fun i j => (X.d j i).unop) x✝⁴ x✝³ ≫ (fun i j => (X.d j i).unop) x✝³ x✝² = 0
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<GOAL>∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<VAR>this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n<GOAL>False
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<VAR>this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n<VAR>𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)<GOAL>False
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<VAR>this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n<VAR>𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)<VAR>hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))<GOAL>False
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<VAR>this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n<VAR>𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)<VAR>hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))<GOAL>n < n
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<VAR>this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n<VAR>𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)<VAR>hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))<GOAL>n = 𝒜.card
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<VAR>this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n<VAR>𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)<VAR>hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))<GOAL>∀ a ∈ 𝒜 \\ 𝒜, (fun s => ∏ p ∈ s, p) a ∈ Ioo 0 n
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<VAR>hn : n ≠ 0<VAR>hf : StrictMonoOn f (Set.Iio n)<VAR>this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n<VAR>𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)<VAR>hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))<GOAL>Set.InjOn (fun s => ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α → β<VAR>hf : Surjective f<VAR>x : 𝕎 β<VAR>n : ℕ<GOAL>(mapFun f (mk p fun n => Classical.choose ⋯)).coeff n = x.coeff n
<VAR>α : Type u_1<VAR>n : Nat<VAR>f : Fin n → α<GOAL>ofFn f = ofFnTR f
<VAR>α : Type u_1<VAR>n : Nat<VAR>f : Fin n → α<GOAL>ofFn f = ofFnTR.go f n ⋯ []
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g✝ : α → F β<VAR>h : β → G γ<VAR>f✝ : β → γ<VAR>x✝ : t β<VAR>f : β → F γ<VAR>g : α → β<VAR>x : t α<GOAL>traverse f (g <$> x) = traverse (f ∘ g) x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g✝ : α → F β<VAR>h : β → G γ<VAR>f✝ : β → γ<VAR>x✝ : t β<VAR>f : β → F γ<VAR>g : α → β<VAR>x : t α<GOAL>traverse f (traverse (pure ∘ g) x) = traverse (f ∘ g) x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g✝ : α → F β<VAR>h : β → G γ<VAR>f✝ : β → γ<VAR>x✝ : t β<VAR>f : β → F γ<VAR>g : α → β<VAR>x : t α<GOAL>traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g✝ : α → F β<VAR>h : β → G γ<VAR>f✝ : β → γ<VAR>x✝ : t β<VAR>f : β → F γ<VAR>g : α → β<VAR>x : t α<GOAL>Comp.instApplicativeComp = inst✝³
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A✝ : Rep k G✝<VAR>G : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : MulAction G A<VAR>f : G × G → A<VAR>hf : IsTwoCocycle f<VAR>g : G<VAR>this : f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)<GOAL>g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A✝ : Rep k G✝<VAR>G : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : MulAction G A<VAR>f : G × G → A<VAR>hf : IsTwoCocycle f<VAR>g : G<VAR>this : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)<GOAL>g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
<VAR>α β : Type u<VAR>n : ℕ<GOAL>succ ↑n ≤ ℵ₀
<VAR>α β : Type u<VAR>n : ℕ<GOAL>Nonempty (Fin n.succ ↪ ℕ)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle y ((o.rotation (o.oangle x y)) x) = 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>-o.oangle ((o.rotation (o.oangle x y)) x) y = 0
<VAR>n : ℕ<VAR>x✝ : 0 < n + 4<GOAL>(n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom
<VAR>n : ℕ<VAR>x✝ : 0 < n + 4<GOAL>(n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : _root_.Embedding g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<VAR>this✝³ : MeasurableSpace β := borel β<VAR>this✝² : BorelSpace β<VAR>this✝¹ : MeasurableSpace γ := borel γ<VAR>this✝ : BorelSpace γ<GOAL>AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : _root_.Embedding g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<VAR>this✝³ : MeasurableSpace β := borel β<VAR>this✝² : BorelSpace β<VAR>this✝¹ : MeasurableSpace γ := borel γ<VAR>this✝ : BorelSpace γ<VAR>H : AEStronglyMeasurable (fun x => g (f x)) μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : _root_.Embedding g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<VAR>this✝³ : MeasurableSpace β := borel β<VAR>this✝² : BorelSpace β<VAR>this✝¹ : MeasurableSpace γ := borel γ<VAR>this✝ : BorelSpace γ<VAR>H : AEStronglyMeasurable (fun x => g (f x)) μ<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.convs m = g.convs n
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : ↑r < ‖f‖<GOAL>∃ x, ↑r * ‖x‖ < ‖f x‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y ≠ 0 → x ≠ 0 ∧ y ≠ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>¬(x ≠ 0 ∧ y ≠ 0) → ¬(o.kahler x) y ≠ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>x = 0 ∨ y = 0 → ↑⟪x, y⟫_ℝ + ↑((o.areaForm x) y) * Complex.I = 0
<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>ha : IsOfFinOrder a<GOAL>(↑(powers a)).Finite
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<VAR>h : a < b<GOAL>Ico a b = cons a (Ioo a b) ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<GOAL>n = n + 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : AddSemigroup α<VAR>h1 : Periodic f c₁<VAR>h2 : Periodic f c₂<GOAL>Periodic f (c₁ + c₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : R0Space X<VAR>x y : X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Inducing f<VAR>a b : Y<GOAL>a ⤳ b → b ⤳ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>x✝ : X ^ n ∣ f<VAR>d : ℕ<VAR>hd : d < n<VAR>g : R[X]<VAR>hgf : f = X ^ n * g<GOAL>f.coeff d = 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>a b : R<VAR>h : a + b = 1<GOAL>a • x + b • y = b • y - b • x + (a • x + b • x)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>a b : R<VAR>h : a + b = 1<GOAL>b • y - b • x + (a • x + b • x) = b • (y - x) + x
<VAR>q : ℤ[X]<VAR>hp : IsUnitTrinomial 0<GOAL>False
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁹ : Category.{u_7, u_1} C<VAR>inst✝⁸ : Category.{u_6, u_2} D<VAR>inst✝⁷ : Category.{?u.24322, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : HasShift C A<VAR>inst✝³ : HasShift D A<VAR>inst✝² : HasShift E A<VAR>inst✝¹ : HasShift C B<VAR>inst✝ : HasShift D B<VAR>a b : A<VAR>e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a<VAR>e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b<VAR>X : C<GOAL>(isoAdd e₁ e₂).inv.app X = (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map (e₁.inv.app X) ≫ e₂.inv.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>s : Set β<GOAL>l (sSup (u '' s)) = sSup s
<VAR>q₁ q₂ : Λ'<VAR>s : Option Γ'<VAR>c d : List Γ'<VAR>v : List ℕ<VAR>n : ℕ<GOAL>Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList ((n + 1) :: v)) [] c d } (Nat.rec { l := some q₁, var := none, stk := elim (trList ((n + 1) :: v).tail) [] c d } (fun n_1 x => { l := some q₂, var := none, stk := elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d }) ((n + 1) :: v).headI)