ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<VAR>hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<VAR>hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p<VAR>hE₂ : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∧ B ↑p =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C ↑p<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<VAR>hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p<VAR>hE₂ : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∧ B ↑p =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C ↑p<VAR>hA : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∨ A ↑p =ᶠ[ae μ] univ<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<VAR>hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p<VAR>hE₂ : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∧ B ↑p =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C ↑p<VAR>hA : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∨ A ↑p =ᶠ[ae μ] univ<VAR>hB : ∀ (p : Nat.Primes), B ↑p =ᶠ[ae μ] ∅ ∨ B ↑p =ᶠ[ae μ] univ<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<VAR>hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p<VAR>hE₂ : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∧ B ↑p =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C ↑p<VAR>hA : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∨ A ↑p =ᶠ[ae μ] univ<VAR>hB : ∀ (p : Nat.Primes), B ↑p =ᶠ[ae μ] ∅ ∨ B ↑p =ᶠ[ae μ] univ<GOAL>(∀ᵐ (x : 𝕊), x ∉ E) ∨ E ∈ ae volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<VAR>hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p<VAR>hE₂ : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∧ B ↑p =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C ↑p<VAR>hA : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∨ A ↑p =ᶠ[ae μ] univ<VAR>hB : ∀ (p : Nat.Primes), B ↑p =ᶠ[ae μ] ∅ ∨ B ↑p =ᶠ[ae μ] univ<GOAL>E =ᶠ[ae volume] ∅ ∨ E =ᶠ[ae volume] univ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<VAR>hA₀ : ∀ (p : ℕ), MeasurableSet (A p)<VAR>hB₀ : ∀ (p : ℕ), MeasurableSet (B p)<VAR>hE₀ : NullMeasurableSet E μ<VAR>hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p<VAR>hE₂ : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∧ B ↑p =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C ↑p<VAR>hA : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∨ A ↑p =ᶠ[ae μ] univ<VAR>hB : ∀ (p : Nat.Primes), B ↑p =ᶠ[ae μ] ∅ ∨ B ↑p =ᶠ[ae μ] univ<VAR>hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p<GOAL>E =ᶠ[ae volume] ∅ ∨ E =ᶠ[ae volume] univ
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>Nat.find ⋯ = Group.nilpotencyClass G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>Nat.find ⋯ = Nat.find ⋯
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → lowerCentralSeries G n = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>∀ (n : ℕ), lowerCentralSeries G n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
<VAR>X : Type u_1<VAR>x✝ : X<GOAL>(toFreeAbelianGroup.comp toFinsupp) (of x✝) = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<GOAL>swap i j • σ = σ → (summand a b σ) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>swap i j • Quotient.mk'' σ = Quotient.mk'' σ → (summand a b (Quotient.mk'' σ)) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>swap i j • Quotient.mk'' σ = Quotient.mk'' σ → (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<VAR>σ : Perm (ιa ⊕ ιb)<VAR>hσ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ<GOAL>(Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∀ (val val_1 : ιa), v (σ (Sum.inl val)) = v (σ (Sum.inl val_1)) → σ (Sum.inl val) ≠ σ (Sum.inl val_1) → swap (σ (Sum.inl val)) (σ (Sum.inl val_1)) • Quotient.mk'' σ = Quotient.mk'' σ → (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∀ (val : ιa) (val_1 : ιb), v (σ (Sum.inl val)) = v (σ (Sum.inr val_1)) → σ (Sum.inl val) ≠ σ (Sum.inr val_1) → swap (σ (Sum.inl val)) (σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ → (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∀ (val : ιb) (val_1 : ιa), v (σ (Sum.inr val)) = v (σ (Sum.inl val_1)) → σ (Sum.inr val) ≠ σ (Sum.inl val_1) → swap (σ (Sum.inr val)) (σ (Sum.inl val_1)) • Quotient.mk'' σ = Quotient.mk'' σ → (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ✝ : Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>σ : Perm (ιa ⊕ ιb)<GOAL>∀ (val val_1 : ιb), v (σ (Sum.inr val)) = v (σ (Sum.inr val_1)) → σ (Sum.inr val) ≠ σ (Sum.inr val_1) → swap (σ (Sum.inr val)) (σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ → (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>α : Type u_1<VAR>inst✝ : (constantsOn α).Structure M<VAR>a : α<VAR>x : Fin 0 → M<GOAL>funMap (Sum.inr a) x = ↑(L.con a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>α : Type u_1<VAR>inst✝ : (constantsOn α).Structure M<VAR>a : α<VAR>x : Fin 0 → M<GOAL>funMap (Sum.inr a) default = ↑(L.con a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>l.sublists ~ l.sublists'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>map (map l.get) (finRange l.length).sublists ~ map (map l.get) (finRange l.length).sublists'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>(finRange l.length).sublists ~ (finRange l.length).sublists'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>∀ (a : List (Fin l.length)), a ∈ (finRange l.length).sublists ↔ a ∈ (finRange l.length).sublists'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>(finRange l.length).sublists.Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>(finRange l.length).sublists'.Nodup
<VAR>n : ℕ<GOAL>∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a n.primeFactorsList
<VAR>α : Type u_1<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidablePred SupIrred<VAR>a : α<GOAL>↑(birkhoffFinset a) = birkhoffSet a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ d✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>g✝ : b✝ ⟶ c✝<VAR>h✝ : c✝ ⟶ d✝<GOAL>(map₂ (Bicategory.associator f✝ g✝ h✝).hom).app = ((mapComp (f✝ ≫ g✝) h✝).hom ≫ Bicategory.whiskerRight (mapComp f✝ g✝).hom (map h✝) ≫ (Bicategory.associator (map f✝) (map g✝) (map h✝)).hom ≫ Bicategory.whiskerLeft (map f✝) (mapComp g✝ h✝).inv ≫ (mapComp f✝ (g✝ ≫ h✝)).inv).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ d✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>g✝ : b✝ ⟶ c✝<VAR>h✝ : c✝ ⟶ d✝<VAR>X : WithTerminal ↑a✝<GOAL>(map₂ (Bicategory.associator f✝ g✝ h✝).hom).app X = ((mapComp (f✝ ≫ g✝) h✝).hom ≫ Bicategory.whiskerRight (mapComp f✝ g✝).hom (map h✝) ≫ (Bicategory.associator (map f✝) (map g✝) (map h✝)).hom ≫ Bicategory.whiskerLeft (map f✝) (mapComp g✝ h✝).inv ≫ (mapComp f✝ (g✝ ≫ h✝)).inv).app X
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f g₁ g₂ : R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<GOAL>const R g₁ g₂ U hu₂ * const R f g₁ U hu₁ = const R f g₂ U hu₂
<VAR>K : Type u_1<VAR>inst✝¹ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>l₁ : Λ<VAR>v : σ<VAR>T : (k : K) → List (Γ k)<VAR>c' : Cfg₂<VAR>h₁ : c' ∈ step M { l := some l₁, var := v, stk := T }<VAR>h₂ : { l := some l₁, var := v, stk := T }.l ∈ Finset.insertNone S<GOAL>c'.l ∈ Finset.insertNone S
<VAR>K : Type u_1<VAR>inst✝¹ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>l₁ : Λ<VAR>v : σ<VAR>T : (k : K) → List (Γ k)<VAR>c' : Cfg₂<VAR>h₁ : c' ∈ step M { l := some l₁, var := v, stk := T }<VAR>h₂ : SupportsStmt S (M l₁)<GOAL>c'.l ∈ Finset.insertNone S
<VAR>K : Type u_1<VAR>inst✝¹ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>l₁ : Λ<VAR>v : σ<VAR>T : (k : K) → List (Γ k)<VAR>c' : Cfg₂<VAR>h₂ : SupportsStmt S (M l₁)<VAR>h₁ : stepAux (M l₁) v T = c'<GOAL>c'.l ∈ Finset.insertNone S
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : Rᵐᵒᵖ<VAR>n : ℕ<GOAL>(opRingEquiv R).symm (C r * X ^ n) = op (C (unop r) * X ^ n)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X = 𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>((α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom = ((α_ X Y Z).inv ≫ 𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)) ≫ (α_ Z Y X).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>((α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom = (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>((α_ X Y Z).inv ≫ 𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)) ≫ (α_ Z Y X).hom = X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>x : B<VAR>y : Ω[A⁄R]<GOAL>(mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (map R R A B) y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>x : B<VAR>y : Ω[A⁄R]<GOAL>x • (mapBaseChange R A B) (1 ⊗ₜ[A] y) = x • (map R R A B) y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>x : B<VAR>y : Ω[A⁄R]<GOAL>(mapBaseChange R A B) (1 ⊗ₜ[A] y) = (map R R A B) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<GOAL>(a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂<VAR>c : α × β<VAR>h₁ : (a₁, b) < c<VAR>h₂ : c < (a₂, b)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂<VAR>c : α × β<VAR>h₁ : (a₁, b) < c<VAR>h₂ : c < (a₂, b)<VAR>this : c.2 = b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂<VAR>c : α × β<VAR>h₁ : a₁ < c.1<VAR>h₂ : c.1 < a₂<VAR>this : c.2 = b<GOAL>False
<VAR>n m : ℕ<VAR>hm : NeZero m<VAR>h : n ∣ m<GOAL>Function.Surjective ⇑(unitsMap h)
<VAR>n m : ℕ<VAR>hm : NeZero m<VAR>h : n ∣ m<GOAL>∀ (x : ℕ), x.Coprime n → ∃ k, (x + k * n).Coprime m